On 11 Sep 2018, at 00:46, Amit Goyal wrote:

Hi All,

As far as I understand, in seL4, the notion of a subject is similar to a thread (process). Each process has a different cspace and thus has different capabilities. Correct me, if I am wrong.

User and even process are not notions that exist in seL4, they are higher-level abstractions you need to build on top of the primitive ones. As far as the kernel is concerned, a subject is a thread that presents a capability. In terms of security policies, the smallest identifiable unit would be thread+address space+Cspace, this corresponds to a simple notion of a process (although the Unix notion of a process is more high level, including process groups and hierarchies). A “user” is an even more high-level notion, which incorporates related processes with similar privileges, including access rights to persistent data (files) and some authentication mechanism that connects a human user to a set of privileges. These are all high-level notions that can all be built on top. If you want to see how to map such high-level abstractions onto microkernel primitives I recommend looking at the Gnode OS, they’ve built a complete Unix-like OS on top of L4 microkernels, a less complete version runs on seL4.

Currently, we can make different components say server and client which run on the same seL4 kernel. They can interact with each other by creating endpoint and adding capability for that endpoint, in others cspace.

Now, I want to extend it and run client and server on different host machines which run seL4. The threads (client and server) thus generated will be different users as per the standard linux convention.

a) How does the communication happen in such a scenario in seL4? The problem which I see is how the capabilities for endpoint on one machine will be minted into other machine's process cspace. b) I also want to understand the notion of a user in seL4.

If your aim is to have a location-independent notion of privileges then you’ll have some data structure that maps those privileges onto local entities. . Eg opening a file would result in some authorisation check (which could consist in mapping a user ID to rights via an ACL, or be affected by the “user” providing the right key to decrypt the file). The data (or meta data) would then be allocated in seL4 objects to which the user’s process is given caps. If the user does the same thing on different nodes, the caps would be different; in fact, seL4 caps have no meaning outside the kernel that created them. Gernot