The seL4_IRQControl cap gives authority to obtain irq handler capabilities. seL4 allows you to move this cap around but doesn’t let you copy it. Can anyone shed light onto why? This seems like a deviation from the standard, policy freedom of seL4.
I don’t fully remember, but what my brain reconstructs are the following constraints:
- If you allow copying of a cap, in the current implementation of the CDT (cap derivation tree) you need to decide whether the copies are siblings or descendants of the cap you copied from, which determines which caps are captured by cap revocation. The CDT at the moment only has one level that it can remember on its own, the rest of that info has to come from the cap content.
- That means, you either have to decide on a sibling/descendant policy globally (e.g. UntypedCaps are all descendants, not siblings, unless you can tell by the area they govern), or you have to invent cap content that lets you decide for a larger (finite) number of levels.
- There would be space in the IRQControlCap to do that, but you’d have to pick a number of levels.
- This is one side (implementation + model complexity + needs a policy decision in any case). The other side was: what are the use cases for copying? The usual use case for copying is delegating authority to a subsystem, but IRQControl has global effect, so delegation doesn’t really make that much sense. The component it goes to needs to have a global view of the system (typically the initialiser) – if there are two such components, they’d have to coordinate. Conceivable that one might want to build a system like that, but unlikely.
- A more interesting use case might be to want to delegate IRQControl authority over a subset of IRQs. In terms of integrity that would make sense, in terms of confidentiality, that would probably create global channels. In either case, it would not be easy to implement (similar to IOPorts on X64), you’d again get into cap content determining CDT levels. Possible, but we didn’t see a strong need for it at the time. (This might change)
So, in total, without a good use case for when we would need to copy that cap, we made the most restrictive and easiest-to-implement policy the default.
This is not that hard to change if a strong use case/need comes along. One level of copying would be easy, as would be a global policy of always sibling/always descendant. Multiple finite levels would also be possible, but fiddly and harder to implement. If there is a use case that really needs that, we should probably think about a CDT implementation that can remember multiple levels on its own without referring to cap content.
My understanding of the CDT is that the first instance of any capability to a particular object is an ‘original capability’ that can be used to revoke and derived capabilities. This means that caps passed to the root task are ‘original capabilities’.
When an untyped object is retyped, that newly created object is an ‘original capability’ that may be revoked using the original untyped and itself may be used to revoke objects derived from it.
When an unbadged capability is minted with a non-zero badge, the minted capability is an ‘original capacility’ to the badged version of that capability. The unbadged capability may be used to revoke the badged capability and the badged capability may be used to revoke capabilities derived from it.
All other badges (i.e. those produced as a result of a copy) are not ‘original capabilities’.
I don’t recall whether mutating a capability turns it into an original capability, but I suspect that it does not.
In this sense, the implication for the CDT should essentially already be defined for copies of the capability.
From my reading of the kernel, it doesn’t directly model ‘node parents’, ‘children’, or ‘siblings’ so directly, but an ‘original capability’ is the direct parent of capabilities derived directly from it and so will always produce children. All capabilities derived from non-‘original capabilities’ will be siblings of the source capability.
That is mostly correct, yes. In the current implementation, all cap table entries have a bit for encoding wether it is an original cap in the sense you described or not. That is the only (storage) commonality between all cap types. The rest of the derivation relation is determined by position in the doubly-linked CDT list, cap type, and cap content. The concept behind the encoding is a derivation tree that describes which (other) caps should disappear if a cap is revoked.
For instance, all typed descendants of an untyped cap will be to the right of the untyped cap in the list, and their object pointer will be contained in the memory region of the untyped cap (that’s what sameRegionAs determines). That is, we are using the list, cap types, cap content of the untyped cap (memory region), and cap content of the descendant cap (object pointer) to determine wether a cap is one level down or in the same level of the tree. For revocation, everything that is in the same subtree one ore more level down would be removed. For endpoint caps, additional content is used (badges), to implement multiple levels between endpoint caps to give the user more flexibility in delegation and revocation.
Such a tree could be encoded much more directly if we spent two pointers more per cap, but that would double the overhead of capability storage, and so we didn’t do that initially. We have revisited that decision a few times, and AFAIR even decided we should change it, but it’s been on the backburner for a quite a while.