On 1/27/20, Klein, Gerwin (Data61, Kensington NSW)
Thinking through confidentiality, integrity, availability, and capDL theorems this also sounds fine, if you present both untyped caps, you are not gaining more authority by merging them. capDL can probably not express the operation (it doesn’t have the information wether two untypeds are adjacent) but doesn’t really need to, since you wouldn’t run it in system initialisation.
capDL limitations won't be an issue for UX/RT since it won't use capDL at all (the only user code in common with CAmkES will be libsel4, with the other low-level code being Rust-based and derived from feL4 and Robigalia). Kernel capabilities will just be treated as a supervisor implementation detail and not exposed to applications at all (only the root server and the low-level system library will deal with kernel objects directly). File descriptors and mapping descriptors (identifying a specific mapping of a file) will be the only true capabilities that normal user programs see (they will be wrappers for groups of kernel capabilities). There will also be process file permissions that will be capability-like in that they can be transferred securely between processes, but unlike true capabilities will not serve as identifiers. These will be the main security mechanism, since they will be more compatible with Unix software than a pure capability model. I wouldn't think that they'd be an issue for CAmkES either since it probably wouldn't ever need to merge any untyped objects. Not sure about Genode, but AFAIK it uses its own XML-based capability definition language everywhere rather than using capDL, and it treats untyped objects as an implementation detail much like UX/RT.
In total probably 6-8 weeks of verification work. You likely would want to tweak the operation such that user space does the revocation in a separate syscall to avoid reasoning about preemption in the new operation.
Yes, requiring the user process to revoke the capability first would
probably actually make more sense.
On 1/27/20, Klein, Gerwin (Data61, Kensington NSW)
Still not quite sure I understand correctly what seL4_Untyped_Replace would do. The description above sounds like the following:
- c_u: a cap to an untyped - c_o: a cap to an object retyped from that untyped, i.e. c_u is the direct parent of c_o - you want a retype operation that is equivalent to: - revoke c_o - delete c_o. There is now a hole in somewhere in the space covered by c_u. - retype a new object of equal or smaller size into the space made available by that hole
Yes, that's exactly what I meant.
In terms of kernel design, this one is harder to justify to the minimality principle, because you could achieve the same effect with the additional untyped cap that I think you were mentioning before, i.e. between c_u and c_o, have a cap c_u2 of the size that is needed for c_o, and revoke/retype that one (which also neatly covers what could go wrong if the authorising cap disappears, e.g. because some overlord server revoked everything — the kernel would catch that at invocation time of the in-between untyped).
UX/RT won't have to deal with issues relating to revocation of the parent untyped, since only the root server will deal with untyped objects and it will only ever use one copy of each untyped capability, although that could be a problem for other OSes with a more recursive architecture.
Given the size of most objects, one untyped cap per object sounds like not too bad of an overhead, but of course this also means managing the relationship between these untypeds and the object caps.
It's still more overhead than the Linux kernel's buddy allocator, which uses bitmaps to track free blocks, rather than having to use some kind of associative array. I know that some use of associative arrays is probably unavoidable (at least with the allocator design I'm using), but it would be nice to have as few capabilities as possible so as much as possible can be tracked with bitmaps.