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.

Stewart Webb is a Software Engineer and Computer Science Masters graduate with an interest in Operating Systems and Programming Languages. In 2019 he was fortunate to study on exchange at the ETH Zurich Systems Group, taking their Advanced Operating Systems subject that involved building an OS atop the microkernel base of their Barrelfish research operating system project. In 2022 he finished his masters thesis at the University of Melbourne, which was a research project taken from Trustworthy Systems at the University of New South Wales, looking at their seL4 microkernel's capability subsystem for resource management (which was copied and adapted into Barrelfish), and the 'object-capability' family of programming languages, looking for better language-level ways to work with operating system capabilities for system building. He currently works as a Sysadmin and Software Engineer at Unique Micro Design in Clayton, Victoria, working on ticketing and access control systems, payment handling software, an IoT device management platform, and RFID inventory management projects.