In 2022 I finally completed my Master of Computer Science at The University of Melbourne.
The tail half or so of it consisted of a research project I poached from UNSW's Trustworthy Systems OS research group, wanting to try my hand at some operating systems related research. Toby Murray was my (very capabaple) supervisor, who worked on some of the original seL4 papers.
The PDF here is as I submitted it for assessment. Unimelb, in all their #1-university-in-Australia wisdom, for some reason don't publish their Computer Science masters theses - not even internally. Which is a bit of a shame if you ask me. So in spite of this I have been led to self-publish it here for sharing instead.
In January 2023 I presented a talk on the project at a summer school on Systems and Software Security at the University of Adelaide.
Download:
The seL4 microkernel provides one of the highest levels of security assurances possible for an operating system via its machine-checked proofs of properties such as integrity, authority confinement, and information-flow non-interference. The key mechanism underlying these proofs and assurances is its capability system for resource management, which is used to describe all memory and communication channels between user-level components of an seL4 system.
Object Capability programming languages make similar use of a capability security model for expressing authority propagation throughout code. In these languages, object references are viewed as the capabilities, such that having a reference to an object represents the rights to use and control that object, with the assumption that object references cannot be invented or forged (for example by dereferencing arbitrary memory addresses). Security mechanisms and policies can become expressed through object-oriented programming patterns such as object proxies, and execution contexts usually specify ways to be launched with initial capabilities, or channels to obtain subsequent capabilities via once the program starts.
Whilst many tools have been developed for building systems with seL4 such as capDL and CAmKES, they rely on static distribution of capabilities upfront at project build time, and in general do not provide for dynamic capability transfer once the system has started. In practice, for runtime/dynamic access control, many systems revert to standard POSIX layers where ambient authority for resource access returns, throwing out the fine-grained access control possibilities that come for free with a capability model. In theory, an object capability language would provide a better means for building dynamic capability systems, especially if such a language can have seL4 capabilities for kernel objects mapped into it.
Many Object Capability languages exist (E, Oz-E, Jessie/SES, SHILL, Pony, Dala) but their purposes/research goals are varied and their implementations can rest on many layers of software. This research surveys various object capability languages from the research community and evaluates their appropriateness for mapping to seL4. The Pony language is examined as a frontrunner for an implementation due to its C-like performance and relatively minimal set of language implementation dependencies. However many trade-offs are still involved due to the minimal mechanisms provided by seL4 (compared to more prevalent monolithic kernels), which are explored with an aim to more formally detail and compare the properties and limitations of both seL4 and object capability language capability models and mechanisms.
Below is a diagram I developed as part of trying to track and trace the lineage of Capabilities as an Operating Systems concept throughout the history of OS research. It is by no means complete but at least provides some understanding of the people and institutions who have contributed various bodies of work exploring or utilizing capabilities within operating systems, with a specific focus on where the capability model within the seL4 microkernel actually came from (i.e. which papers/theses specifically)