In Reading a Microkit System Description, I followed the configuration that connects programs and resources. This second note looks at the seL4 capability model behind those access decisions.
When I read a software diagram, I want to know what each component can actually access. A box named “service” describes a role. The permissions available to its code determine which operations it can request.
Capability-based systems make that second question concrete. They give us a way to discuss access in terms of particular objects and permitted operations.
Begin with an Object and an Operation
In seL4, a capability is a kernel-managed reference carrying authority over an object or resource. User code invokes kernel operations through capabilities; an ordinary number chosen by the program does not create that authority. The seL4 capabilities tutorial introduces this model and the capability spaces that hold those references.
For a first pass, I ask three questions together:
- Which object is involved?
- Which operation is being requested?
- Which component holds the capability needed for that operation?
Keeping the questions together avoids an overly broad statement such as “this component has access.” Access becomes a relationship I can explain.
The Handle and the Authority Are Different Ideas
Code needs a way to refer to a capability. seL4 uses capability spaces, with slots that contain capabilities. The tutorial develops the terminology of CSpaces, CNodes, and CSlots in more detail.
The distinction matters when reading code. A variable that identifies a slot is part of how the program locates its authority. Copying the numeric value into another program is not, by itself, a transfer of the capability.
I find it helpful to annotate an invocation with both pieces of information: the reference used by the code and the object that reference is expected to identify.
Use a Familiar Application Analogy
Imagine an image-conversion utility. It needs an input image and somewhere to place the converted result. A design can provide those particular handles instead of requiring the utility to discover everything it might need through a broad application interface.
This is an application-design analogy, not a claim that the seL4 kernel supplies a filesystem. It illustrates the question I want to ask: can the caller provide the specific authority needed for the task?
The same question is useful when reviewing a service interface. A request to perform one operation should lead to a clear explanation of which resource the service will use on the caller's behalf.
Communication Has Authority Too
Messaging is another useful example. The seL4 IPC tutorial explains how programs invoke capabilities to endpoints when communicating.
That makes a communication path something to examine explicitly. I want to understand who can use the interface, which request is being made, and how the receiving code interprets it. Checking that a connection exists and checking that the request has a sensible meaning are separate review tasks.
A Small Reading Exercise
Choose a short public seL4 tutorial example. Pick one kernel invocation and trace its capability argument back to the place where that authority was made available.
Write down the object and operation in ordinary language. That exercise builds a useful habit: explaining permissions as concrete relationships instead of treating them as background configuration.