Thanks for your comments and explanations: exactly the kinds of insights that I was hoping for. It is particularly interesting to see how a range of considerations helped to shape the design.
I did wonder if the multiple levels approach in Dhammika's PhD might have opened up some possibility for a covert channel (assuming there was some way to observe a failure when deriving a capability at maximum depth). But I don't have a specific exploit in mind ... and it doesn't seem we need to worry about this anyway with the current approach :-) Thanks again, and best wishes, Mark On Oct 20, 2015, at 8:02 PM, Kevin Elphinstone <[email protected]> wrote: > Gerwin is correct. > > There is an elegance in a model that supports zero or one level of depth, or > maybe zero, one, and effectively "unlimited". We felt at the time that zero, > one, and some seemingly arbitrarily small constant (defined by really tight > implementation restrictions) would not be as nice, and result in unexpected > "boundary" situations arising. If we had no use case at the time, then we > could avoid the (very) small constant altogether. > > We always expected to revisit at some point if, as Gerwin says, "a pressing > reason (or enticing funding ;-)) to do it", arose. Regarding Dhammika's PhD, > at some point the kernel had to stop being a moving target for verification > so we drew a line at a sane point in the sand. Dhammika's PhD had no such > restrictions on continued evolution, hence the discrepancy between the PhD > and current 'mainline'. > > BTW, Dhammika's use case was paravirtualised Linux, which is now better > handled by CPU hardware extensions on ARM and x86. > > - Kevin > > >> -----Original Message----- >> From: Devel [mailto:[email protected]] On Behalf Of Gerwin Klein >> Sent: Wednesday, 21 October 2015 9:28 AM >> To: Mark Jones <[email protected]> >> Cc: [email protected] >> Subject: 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 <[email protected]> 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 >>> [email protected] >>> 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. >> _______________________________________________ >> Devel mailing list >> [email protected] >> 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. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
