|
This project is investigating the potential for language-based security techniques in the construction of low-level systems software. The specific focus is on the development of an open, capability-enhanced microkernel whose design is based on seL4, a "security enhanced" version of the L4 microkernel that was developed, by a team in Australia, as the first fully verified, general purpose operating system.
The work on seL4 is rightly celebrated as a landmark for formal verification, and provides a strong foundation for building trustworthy systems. The costs of its development and maintenance, however, are quite high. We have observed that many of the security properties established in the seL4 verification (including the absence of code injection attacks, buffer overflows, and null pointer dereferences) could have been guaranteed automatically by writing it in a language that incorporates language-based security mechanisms such as an enhanced type system. Motivated by such insights, the specific goals of this project are to evaluate: whether it is actually feasible to write software of this kind in a language with meaningful, language-based security guarantees; what practical impact this might have, particularly in reducing verification costs; and whether it is possible to meet the performance goals that are typically required in such applications.
The primary impact of this project will be in increasing the applicability of verification and language-based security techniques for the construction of secure computer systems. It will also generate and distribute key artefacts including the microkernel implementation, with associated teaching materials, for use in education, research, and industry.
|
TWC: Small: Using a Capability-Enhanced Microkernel as a Testbed for Language-based Security (CEMLaBS)