[seL4] Re: More about Objects

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