Re: [seL4] Support for multiple levels of derived capabilities?

Hi Mark, yes, Dhammika’s prototype implementation was more regular than the current seL4 CDT. Kevin might have better memory, but as far as I remember, there were two factors: 1) there was space pressure in the implementation, i.e. for some capabilities we ran out of bits to store level/depth information. 2) we hadn’t come up yet with any user-level design that actually needed deep levels for typed capabilities. Note that you *do* get deep levels in current seL4 with untyped caps and that there is the badge mechanism for endpoint caps (not the same as derivation levels but gives you something similar). These were the two types where we could see designs that make use of deeper levels of “revoke”. We basically decided to treat these two special to enable such designs and keep the rest to a one-level structure that was simple to implement. We picked at least one level to enable the case where a server manages caps on behalf of clients. That said, we’re not particularly happy with this design. It works for anything we wanted to do so far, but it lacks elegance and regularity. Dhammika’s idea of regular deep levels certainly remains appealing, and we have had a few ideas in the meantime of what to do about it. One such different design is the “searchable” CDT in the experimental branch, which doesn’t have these seemingly arbitrary restrictions (it’s called “searchable" for other reasons). It’d be nice to pull that one into master, but verification impact/effort for completely changing such a fundamental mechanism would be fairly high, so we’re waiting for a pressing reason (or enticing funding ;-)) to do it. Cheers, Gerwin

On 21.10.2015, at 06:50, Mark Jones wrote:

I have a question about the way that derived capabilities are handled in seL4. I'm posting here in the hope that somebody might be able to share some insights about this part of the design.

As I understand it, early versions of seL4's Mint operation allowed multiple derived levels of capabilities. (I'm thinking, in particular, of the description of Capability Derivation Trees, or CDTs, on Pages 36-38 of Dhammika Elkaduwe's thesis.) This, for example, would make it possible to construct a system with multiple threads, A, B, and C, each holding a capability to the same object where the capability in C is a CDT child of the capability in B, which in turn is a CDT child of the capability in A. In this scenario, B would have authority to revoke the capability in C, including any further CDT children that C had created, but it wouldn't typically have authority over other children of the original capability in A.

So far as I can tell, this is not possible in the current version of seL4. Specifically, the reference manual (API version 1.3, Page 11) indicates that "Ordinary original capabilities can have one level of derived capabilities" and that "Further copies of these derived capabilities will create siblings". In the scenario above, this suggests that the capabilities in B and C would be siblings and that there would be no easy way for B to track any additional sibling copies that C might have created.

Can someone provide background about why this change was made? I've seen that Dhammika had a working implementation of the original design, and although it was still technically limited to 128 levels, this was not found to be an issue in practice. But perhaps there were security concerns or problems with verification? Or maybe people who worked with the original system found that it wasn't useful in practice, or that it was hard to use effectively? Or maybe I've just misunderstood some aspect of the above?

Thanks and best wishes, Mark

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.