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
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 mpj@pdx.edu 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.
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:devel-bounces@sel4.systems] On Behalf Of Gerwin Klein Sent: Wednesday, 21 October 2015 9:28 AM To: Mark Jones mpj@pdx.edu Cc: devel@sel4.systems 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:
- there was space pressure in the implementation, i.e. for some capabilities
we ran out of bits to store level/depth information.
- 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 mpj@pdx.edu 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. _______________________________________________ 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.
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 Kevin.Elphinstone@nicta.com.au 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:devel-bounces@sel4.systems] On Behalf Of Gerwin Klein Sent: Wednesday, 21 October 2015 9:28 AM To: Mark Jones mpj@pdx.edu Cc: devel@sel4.systems 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:
- there was space pressure in the implementation, i.e. for some capabilities
we ran out of bits to store level/depth information.
- 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 mpj@pdx.edu 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. _______________________________________________ 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.
On 21 Oct 2015, at 14:02 , Kevin Elphinstone Kevin.Elphinstone@nicta.com.au wrote:
BTW, Dhammika's use case was paravirtualised Linux, which is now better handled by CPU hardware extensions on ARM and x86.
… but points to a general use case: One of the attractions of clean object capability models is that any operation can be transparently virtualised. If an original cap can be derived, but a derived one cannot, then this breaks transparency at some point.
There’s the old saying that in CS there are only three valid constants: zero, one and infinity. We have a two in there, which clearly smells badly.
Gernot
________________________________
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.
… but points to a general use case: One of the attractions of clean object capability models is that any operation can be transparently virtualised. If an original cap can be derived, but a derived one cannot, then this breaks transparency at some point.
I can't see the relationship between derivation and virtualisation of object invocation? A level of indirection can be obtained by substitution of a real object reference, and a "virtual" object reference.
It's length of chains of delegation that we have compromised on, more specifically control of the scope of revocation of delegation.
There’s the old saying that in CS there are only three valid constants: zero, one and infinity. We have a two in there, which clearly smells badly.
I thought that is what I implied. We have two valid constants and no invalid ones :-) The addition of infinity is what one wants in the ideal. Though I'd argue that if you can design your user-level system to only need zero and one, one can avoid taking the space hit for infinity in the kernel.
The move to 64-bit may actually free up enough space in caps to implement an infinity, which would be pretty compelling if it came for "free".
- Kevin
________________________________
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.
-
Gernot Heiser -
Gerwin Klein -
Kevin Elphinstone -
Mark Jones