Kernel Objects
Kernel makes use of the following primitive types:
- Capability Nodes: CapNodes
- Thread Control Blocks
- Low-level interrupt support: IRQControl, IRQHandlers
- Protection domain: VSpace
- Raw memory: Untyped
Containers for capabilities with a way to quickly search them.
A capability is an unforgeable token that references a specific kernel object (such as a thread control block) and carries access rights that control what methods may be invoked. Conceptually, a capability resides in an application’s capability space; an address in this space refers to a slot which may or may not contain a capability. An application may refer to a capability - to request a kernel service, for example - using the address of the slot holding that capability. This means, the Vesper capability model is an instance of a segregated (or partitioned) capability system, where capabilities are managed by the kernel.
Capability spaces are implemented as a directed graph of kernel-managed capability nodes (CapNodes). A CapNode is a table of slots, where each slot may contain further CapNode capabilities. An address of a capability in a capability space is the concatenation of the indices of slots within CapNodes forming the path to the destination slot.
Capabilities can be copied and moved within capability spaces, and also sent via IPC. This allows creation of applications with specific access rights, the delegation of authority to another application, and passing to an application authority to a newly created (or selected) kernel service. Furthermore, capabilities can be minted to create a derived capability with a subset of the rights of the original capability (never with more rights). A newly minted capability can be used for partial delegation of authority.
Capabilities can also be revoked to withdraw authority. Revocation recursively removes any capabilities that have been derived from the original capability being revoked. The propagation of capabilities through the system is controlled by a take-grant-based model [EKE08,Boy09].
[EKE08] Dhammika Elkaduwe, Gerwin Klein, and Kevin Elphinstone. Verified protection model of the seL4 microkernel. In Jim Woodcock and Natarajan Shankar, editors, Proceedings of Verified Software: Theories, Tools and Experiments 2008, volume 5295 of Lecture Notes in Computer Science, pages 99–114, Toronto, Canada, October 2008. Springer-Verlag.
[Boy09] Andrew Boyton. A verified shared capability model. In Gerwin Klein, Ralf Huuck, and Bastian Schlich, editors, Proceedings of the 4th Workshop on Systems Software Verification, volume 254 of Electronic Notes in Computer Science, pages 25–44, Aachen, Germany, October 2009. Elsevier.
While Vesper does not dictate any policies about thread control, it provides mechanisms for manipulating thread state if you are given a corresponding capability.
System support for interrupts includes enabling/disabling appropriate interrupt lines and access to capabilities that will be called when interrupts arrive.
Includes manipulation of default memory access rights and capabilities for accessing this memory from the outside.
Raw memory includes capabilities for access to untyped memory blobs and capabilities to retype this memory into different kernel or user memory objects.
