Re: [seL4] Are there any plans to re-add seL4_Untyped_RetypeAtOffset?

On 28 Jan 2020, at 14:56, Andrew Warkentin wrote:

On 1/27/20, Klein, Gerwin (Data61, Kensington NSW) wrote:

...

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.

Yes, I think capDL will not be a problem. The non-expressiveness would take the form of non-determinism, i.e. when you call the merge operation, the capDL state would non-deterministically fail or perform the operation, you just can’t predict which one it does. This means you only have to deal with it if you use capDL and if you use that operation in capDL, for which I can’t see a real use case. System description and system initialisation would still work as before.

...

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.

Got it.

...

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.

This one is slightly different to the expressiveness for capDL. For expressiveness the context/use case matters, but the atomicity here is a case of security/correctness, which would have to work in all contexts. I.e. it would probably be fine in UX/RT by design, but if the feature could be abused elsewhere to break the security of the kernel, we could not include it. This specific one is not really such a big issue, though, it could be enforced easily in the kernel, it just caught my attention because the security reasoning is a bit more subtle there than usual.

...

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.

In this I should really defer to the kernel design experts, since I'm more the verification side. Compared to the searchable CDT it would certainly be a much simpler operation, and maybe the trade-off for performance (memory overhead, speed, and complexity) is worth it. It would basically be the properly implemented replacement of the Recycle operation the API used to have in the very beginning, but that we had to drop because it had too many surprising corner cases to be actually useful (it allowed you to reset an object to a neutral state -- the idea was that it would be as if it had been deleted and retyped, but that wasn’t really the case in the end). Cheers, Gerwin