User-level fault handling does require capabilities and is afaik semantically equivalent to synchronous IPC using seL4_Call/Reply_Recv. The only difference is that instead of the faulting thread populating the IPC buffer and invoking seL4_Call, the kernel constructs the fault message and sends it to the faulting thread's designated fault handler endpoint (if such an endpoint capability has been provided) on its behalf. - Alwin

Hello T, "Object methods" are just system calls in the technical sense, they are fully executed in kernel mode. You can find the (generated) syscall numbers in your build directory: build/libsel4/include/sel4/syscall.h It's generated from libsel4/include/api/syscall.xml by a script. The start will look something like: typedef enum { seL4_SysCall = -1, seL4_SysReplyRecv = -2, seL4_SysSend = -3, seL4_SysNBSend = -4, seL4_SysRecv = -5, seL4_SysReply = -6, seL4_SysYield = -7, seL4_SysNBRecv = -8, (The rest is either debug-only or platform dependent.) The "object methods" are a seL4_SysCall on a cap of a specific type. ("Call" in the seL4 sense of doing a send + wait for reply, not to be confused with "syscall".) The call will be decoded depending on the cap's type, and that object's handling code will check the invocation number to see what you want to do. To avoid doing the wrong thing when passing a cap of the wrong type, all invocations have a unique number: build/libsel4/include/sel4/invocation.h This two-tiered numbering system makes it easier to quickly handle IPC seL4_SysCalls. Capabilities in seL4 are a bit like file descriptors in other OSes: A generic interface to do things with specific "objects", via a few standardised system calls (read, write versus recv and send). In the end it's all semantics. If you are confused how the kernel knows whether you are calling a method on the endpoint object or sending a message to another task: That's solved by endpoints not having any methods to call. Same trick is used for notifications. I hope that clears things up. Greetings, Indan On 2024-09-09 13:19, tunacici7@gmail.com wrote:

Think I'm starting to understand this. My current understanding of a syscall is operations like read(), write() or mkdir() are implemented in the kernel. So they are executed at a higher execution level (e.g., Ring 0 in x64, EL1 in ARM64) and each have their own syscall numbers. Most user applications don't directly invoke them, but rather use a libc wrapper with the same syscall name.

In seL4, this idea is a bit different. The kernel itself handles send+receive and yield (and also their variations) syscalls inside the kernel at a higher execution level. Object methods are implemented using those syscalls inside libsel4. Which executes at a lower execution level (e.g., Ring 4, EL0).

Here I am, again, a little bit confused. Sorry. When I looked at the source and did some debugging I see that, as an example, UntypedRetype is implemented in libsel4 (sel4_client.h) Like you, and others, said it is implemented using send+receive system calls. So, everything is good so far. But, what about their syscall numbers you have mentioned that have been vectored for efficiency? I was not able to find them in the source (both after and before system call stub generation). I looked inside syscall.h after syscall_header_gen.py.

I'm sure I'm missing something or my understanding of what a syscall needs more work.

Thanks for the previous answers. It motivated me to debug an application (a tutorial) and see how parts of libsel4 is actually implemented. -T

Hey Indan,

After reading your (and others) words, it finally clicked for me! Like you (and others) have said in seL4 all interaction are done by invoke objects via capabilities.

It sounds obvious at first (many resources talk about this), but understanding is another story:)

In case there are others like me that are still having a problem understanding system calls and object methods in seL4, I have collected my thoughts below.

System call is, in a more "traditional" sense, in other OSes is like this: - execute 'syscall' with a specific system call number from the user space - there are many syscall numbers defined in those OSes (e.g., read, write, mkdir)

In seL4, however, it's a bit different: - still execute 'syscall' from the user space - but this time only Send, Recv, Yield (and other variations) have

Thanks T. Having this in a documentation would be nice to improve seL4 learning curve. I really appreciated reading all the explanations, but this T summary is very helpful, like the few really important things an experienced skydiver say to beginners to increase their self confidence. On Tuesday, September 10, 2024, wrote: their syscall numbers defined

- those are the only "system calls" that we can directly compare to

other "traditional" OSes

- now, in handling of the system calls (e.g., Send()) there is a

decoder (see 'decodeInvocation(...)')

- those decoders determine which specific capability to invoke (see

'libsel4/include/interfaces/sel4.xml' for all invocations)

- each of the invocations have their own numbers (similar to system

call numbers)

- so (like Indan have said) we have a two-tiered system (first is

architecture/CPU 'syscall' and second is seL4 'invocations')

- because of this we have a separation in API reference between

System Calls and Object Methods

- and since object methods (like UntypedRetype) are handled inside

the seL4 they are executed at higher privilege level

Again, thanks everyone for the help & replies.

-T _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

On 11 Sep 2024, at 07:02, Hugo V.C. wrote:

...

Thanks T. Having this in a documentation would be nice to improve seL4 learning curve. I really appreciated reading all the explanations, but

Thanks for the links Gernot. "I don’t think tutorials on microkernels and capabilities belong into the seL4 kernel documentation" Sure. I have no idea how you guys can deal with this... I'm on the commercial side, just thinking about how people can "easily" become seL4 developer... On Wednesday, September 11, 2024, Gernot Heiser via Devel wrote: this

...

T summary is very helpful, like the few really important things an experienced skydiver say to beginners to increase their self confidence.

I don’t think tutorials on microkernels and capabilities belong into the seL4 kernel documentation. However, the white paper could be more explicit about this, I’ll think about that. (I guess the white paper is due for an upgrade anyway, given that the Microkit is now the preferred way for building seL4-based systems.)

Incidentally, I yesterday delivered my first Advanced OS lecture for the year, and I had strengthened the explanation of cap invocation, see - p16ff of https://cgi.cse.unsw.edu.au/~cs9242/24/lectures/01a-intro.pdf - p4 of https://cgi.cse.unsw.edu.au/~cs9242/24/lectures/01b-sel4.pdf

Gernot

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

On 12 Sep 2024, at 06:41, Hugo V.C. wrote:

...

"I don’t think tutorials on microkernels and capabilities belong into

Well, people usually like to understand how things work, moreover on a system like seL4. And, whether you like or not, there will be forks, hacks, modifications... the more info you provide, the more involved the community will be. Frameworks are a must to speed up real life adoption, but ideally, all the low level info must be clear and the easier the better. I used to pentest an RTOS derivative of VxWorks on top of some Marvel Armada cpus, at the beginning with public very abstract info, but the fun came when I got (legit) access to confidential low level cpu specs of the different models... then I undestood why some fault injection attacks were being successful. Developers can do their job with just Mikrokit, but many of them, will have curiosity to understand why they need to do things the way they are forced. By being able to fully understand how things really work at low level, they get more involved, they can also contribute with improvements, and, hopefully, they will be happier than just blindly trust. It's about letting the door open to developers and engineers to learn at deeper level, as easy as possible. Maybe a door some people will never open, but for those who dare to open, would be nice to be sure they get engaged. On Wednesday, September 11, 2024, Gernot Heiser via Devel wrote: the seL4 kernel documentation"

...

Sure. I have no idea how you guys can deal with this... I'm on the

commercial side, just thinking about how people can "easily" become seL4 developer…

How is this affected by low-level technical details that are hidden behind libraries, especially if you use higher-level frameworks such as the Microkit?

Gernot

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

Hello Hugo,

The thing is, to fully understand how things work on a low level you can read the seL4 source, it's not that much, it's open and available to everyone. And it's really the best way to find out specific details. So the door is wide open already.

People are welcome to ask questions to increase their understanding of how seL4 works, that's how this thread started.

Perhaps it's nice to have a medium level description of how seL4 works on a technical level, but it will always describe someone's personal mental model, and will always be a simplification, hence slightly incorrect for some corner cases.

However, the seL4 manual is not the place for such info, it's strength is exactly its terseness. Its goal is to give an overview of seL4, if there is too much detail that overview becomes lost and the manual becomes huge and not easily readable any more. The information should be limited to what the user needs to know when using sel4. Giving too much details too early only leads to confusion, people need to build a mental model of how seL4 works first and then they can adjust it when learning more.

We can add more information to the website, feel free to open a pull request or open an issue to request specific documentation. I agree that there is so much more to say about seL4, but manpower is limited.

Greetings,

Indan

On 2024-09-11 23:15, Hugo V.C. wrote:

...

Well, people usually like to understand how things work, moreover on a system like seL4. And, whether you like or not, there will be forks,

hacks,

...

modifications... the more info you provide, the more involved the community will be.

Frameworks are a must to speed up real life adoption, but ideally, all

...

low level info must be clear and the easier the better.

I used to pentest an RTOS derivative of VxWorks on top of some Marvel Armada cpus, at the beginning with public very abstract info, but the fun came when I got (legit) access to confidential low level cpu specs of the different models... then I undestood why some fault injection attacks were being successful.

Developers can do their job with just Mikrokit, but many of them, will have curiosity to understand why they need to do things the way they are forced. By being able to fully understand how things really work at low level,

...

get more involved, they can also contribute with improvements, and, hopefully, they will be happier than just blindly trust.

It's about letting the door open to developers and engineers to learn at deeper level, as easy as possible.

Maybe a door some people will never open, but for those who dare to open, would be nice to be sure they get engaged.

On Wednesday, September 11, 2024, Gernot Heiser via Devel wrote:

...

On 12 Sep 2024, at 06:41, Hugo V.C. wrote:

...

"I don’t think tutorials on microkernels and capabilities belong into

the seL4 kernel documentation"

...

...

Sure. I have no idea how you guys can deal with this... I'm on the

commercial side, just thinking about how people can "easily" become seL4 developer…

...

How is this affected by low-level technical details that are hidden

behind libraries, especially if you use higher-level frameworks such as

Hi Indan, yes source code is available, but people is not reading source code of a "standard" system, so just reading it, even if the most accurate way to know what's going on (this is how anyone will do it for Linux Kernel, in example) in the specific case of seL4, can be a bit frustrating, as most things we know about OS here do not apply. To be more clear, for anyone comming from Linux Kernel, seL4 is an alien... :-) And yes, door is open to read the code, that's why is open source. Sure. But I talk about another kind of door, the one of understanding how things work, maybe, with that medium level description you mention, really I don't know. Please don't misunderstand me 🙏, I'm not telling seL4 is opaque, it's Open Source, that's wonderful! I'm just telling that maybe having access to source code and the technical manual, is not enougth to the average seL4 newbie engineer. You guys do an amazing job. Manpower is probably the "problem". I know. I really know. Ok, step by step. On Thursday, September 12, 2024, Indan Zupancic wrote: the they the

...

Microkit?

...

Gernot

On 11 Sep 2024, at 00:18, Indan Zupancic wrote:

I'd like to improve the manual to make the above clearer, but not sure how to approach it. Call everything an object, even if it doesn't require state? Does that make things clearer or more confusing? The manual sidesteps the issue by not really mentioning it at all currently. Or call everything a resource and only resources that require storage objects? Or call the stateless ones kernel services and make an explicit list of them? But in a sense it's an implementation detail whether something needs state and whether that fits in the cap or not, so why call it differently?

There is always a difference between an object and the cap to the object, no matter if the object is a memory-backed object or a pseudo object. The only time there is no observable difference (where it’s just an implementation detail) is if there exists exactly one cap to the object. The difference is similar to the difference between memory and a point to that memory. When you copy a pointer, it still points to the same memory, and changes in that memory are observable via both (then aliased) pointers. Same for caps and objects. While the manual currently is attempting to shortcut this difference and mostly just talks about objects, I think it is important to make the difference explicit even though it does sound cumbersome to spell it out each time. It is also the case that almost all caps in seL4 carry additional information (for instance access rights). Two copies of a cap to the same object can have different access rights, no matter if that object is memory-backed or not. So, from my side the important distinction to make is between cap and object. Some objects need memory resources, some don’t. We could call those pseudo objects, but I think that distinction is less important. And we should decide whether we are invoking caps or objects. That part doesn’t really matter, so I’m sure there will be strong opinions about it ;-). I think it makes sense to say that we are invoking object methods because people are familiar with that concept from OO, and to do that you need to present a cap to the object, which may provide additional state (access rights, mapping info, etc). This is the same for all kinds of objects. Cheers, Gerwin

On 23 Sep 2024, at 12:05, Indan Zupancic wrote: On 2024-09-23 09:53, Gerwin Klein wrote: While the manual currently is attempting to shortcut this difference and mostly just talks about objects, I think it is important to make the difference explicit even though it does sound cumbersome to spell it out each time. The big shortcut is not mentioning pseudo objects at all currently. Right, I agree that this needs to change. It is also the case that almost all caps in seL4 carry additional information (for instance access rights). Two copies of a cap to the same object can have different access rights, no matter if that object is memory-backed or not. That is totally different, access rights are properties of the cap, not the object they point to. That is clear to everyone and doesn't cause confusion. It's a concept people are familiar with. I’ll concede that people are familiar with it and therefore not confused, but it is cap state :-) The other cap state is also not for properties of the object the cap points to. That’s probably where the main confusion is, because it sounds like object state. Maybe one analogy is that it is state of a "view" of the object. What does make things weird is if object state is stored in caps, because that causes for the user unexpected limitation to what you can do with the caps. Hm, I think it comes down to a question of design perspective in the end. In terms of behaviour, there is no object state stored in caps in seL4, it’s always been cap state. You fundamentally can’t really store object state in caps, because caps and objects are observationally different — to change actual object state stored in caps you’d have to find all caps for that object and change it there as well. But you can choose to stretch the concept of capability and represent an additional concept with a cap, usually something that is similar to authority and where you might have multiple different views to the same object. E.g. the mapping info for a page is where the concept of "cap" is stretched a little. The mapping info is a property of the mapping, not of the frame object the cap points to. I.e. the mapping is represented by the cap, not the frame object. You could choose to not represent the mapping with a cap, and instead use a new kind of object or some other mechanism (that’s where it’s a question of design perspective), but the cap state is not trying to represent object state of the frame object. It’s something in addition to the object that can be different in each cap to the object. Because frames can be mapped in multiple locations and address spaces, and all these mappings point to the same frame and represent authority to read/write etc, modelling that situation as state in the cap was a reasonable fit, but it does stretch the concept a bit, because it’s now more than just pointer + authority. The restrictions on copying are mostly not because of the cap state (some are), but because of the limited depth of the capability derivation tree (CDT). If we added another pointer to all caps (which would double cap size), the CDT could be a proper tree and we could remove a lot of these strange restrictions. Currently the cap state sometimes doubles as indication on which level in the CDT a cap is, and that’s where a lot of the copying restrictions come in. So, from my side the important distinction to make is between cap and object. Some objects need memory resources, some don’t. We could call those pseudo objects, but I think that distinction is less important. In that case I'll add all the missing objects to the Kernel Objects chapter. 👍 Cheers, Gerwin

On 23 Sep 2024, at 14:55, Indan Zupancic wrote:

On 2024-09-23 12:58, Gerwin Klein wrote:

...

The other cap state is also not for properties of the object the cap points to. That’s probably where the main confusion is, because it sounds like object state. Maybe one analogy is that it is state of a "view" of the object.

...

What does make things weird is if object state is stored in caps, because that causes for the user unexpected limitation to what you can do with the caps. Hm, I think it comes down to a question of design perspective in the end. In terms of behaviour, there is no object state stored in caps in seL4, it’s always been cap state.

I don't think that's true:

- Untyped: capFreeIndex

This one is true, that’s why there can be only exactly one active copy of the Untyped when it is not empty. (Apart from the whole discussion whether the concept of untyped object makes sense — for me, there are no untyped objects, only untyped caps and allocatable memory, but with the uniqueness constraint it doesn’t really matter, they are the same behaviourally).

- IRQHandler: capIRQ

This just says what object the cap refers to, it’s not object state, it’s the pointer to the virtual object. Same also for SMC caps, IOPorts, SGI caps etc.

- SchedControl: core

Same as above, it’s for which object (=core) the cap is, not object state. One difference is that this state information is immutable after the cap has been created, whereas things like rights, mapping info etc can change. There are also the badges on endpoints caps, which are also not object state and could be seen as a more fine grained target pointer.

E.g. Aarch64: - Frames, PT, VSpace: capFMappedAddress - ASIDPool: capASIDBase and capASIDPool

Those are the mapping info state that I tried to explain, they would not make sense inside the target object — they’d need to be an addition kind of object that doesn’t exist. ASIDPool caps etc just extend that same mapping info concept from frames higher up.

All that is part of the object state, or even the object itself if there is nothing else.

I would still argue that only the UT caps have real object state.

...

You fundamentally can’t really store object state in caps, because caps and objects are observationally different — to change actual object state stored in caps you’d have to find all caps for that object and change it there as well.

Exactly, and that's why caps with object state in them can't be copied or have other restrictions, if that state is not read-only.

Yup.

...

E.g. the mapping info for a page is where the concept of "cap" is stretched a little. The mapping info is a property of the mapping, not of the frame object the cap points to. I.e. the mapping is represented by the cap, not the frame object. You could choose to not represent the mapping with a cap, and instead use a new kind of object or some other mechanism (that’s where it’s a question of design perspective), but the cap state is not trying to represent object state of the frame object. It’s something in addition to the object that can be different in each cap to the object. Because frames can be mapped in multiple locations and address spaces, and all these mappings point to the same frame and represent authority to read/write etc, modelling that situation as state in the cap was a reasonable fit, but it does stretch the concept a bit, because it’s now more than just pointer + authority.

That is why a page cap is a page cap and not a frame cap: Because the object in question is not just the frame, it is a frame + mapping.

It’s possible that you can view it that way (I haven’t thought through all paths), but it is much more direct to view the cap itself as representing the mapping, because that is what it actually does and mappings behave a lot like caps. I’m not claiming it’s brilliant and easy to understand either way, it’s just what (mostly) solved the double parent problem you mention below. For my own understanding, I don’t really like forcing everything into the simple cap/object paradigm when reality is more complex. Even in the case where you can prove that they are the same (Untypeds), I’ve found it easier to understand the behaviour when I mentally extend the cap concept and not try to have a layer of (mental) indirection via objects that aren’t really there. It can help explain things the first time because it matches existing concepts, but I find it dangerous for edge cases. .

Page caps have the problem that they have two parents: Both the untyped they were allocated from and the VSpace the mapping is in, and seL4 can only clean up one automatically.

Agreed, that’s the source of the mapping info design wrinkle. The it is now seL4 can clean up automatically the one chain that matters for the kernel and can prevent the user from violating security on the other chain by more runtime checking (if used correctly, at least). We tried a different design with shadow page tables many years ago that could do both automatically IIRC, but it was much more complex and needed more memory. Would still be worth revisiting this whole thing again at some point, but it’d be a fairly big redesign.

I think the page caps as they are cause a lot of unnecessary caps to be in the system. To me it would make more sense if you could have untyped for either kernel use or user space use, and if they're marked for user space use you can do virtual mappings on them without creating new caps. In a way being able to mark UT as device memory would do it, then it only needs to have one bit to mark if any kernel objects were allocated.

You’d still need to clean up mappings when the memory those mappings point into goes away. Not doing that could violate integrity eventually, because even if everything is user memory, you still need to account for which sub system the memory is for.

Anyway, cap restrictions depend on implementation details which are opaque to the user.

We can agree on that :-) Cheers, Gerwin