Description:
TECHNOLOGY AREA(S): Info Systems
OBJECTIVE: Develop a formally verifiable operating system microkernel that can enforce information flow control policies over user space processes.
DESCRIPTION: Certifying software for use, such as through DO-178C, is expensive and time consuming. One way to tackle this problem is to rely on microkernels, which are simpler to understand, analyze, and certify. They also provide separation guarantees for unprivileged user space programs, so the unprivileged programs can be analyzed separately and independently. Recent advances in microkernel design has not only led to high performance designs such as the L4 microkernel, but also designs that are amenable for formal verification. seL4 is the world’s first formally verified microkernel – it has been proven to be free from common bugs and vulnerabilities [1, 2]. It achieved this by adapting the design goals of the original L4 microkernel [3] to achieve efficient performance, and introducing a capability system for security. In seL4, the verification/certification artifacts are provided as explicitly described assumptions and mathematical proofs that cover all possible executions and states rather than simply the states covered through testing. As another example, CertiKOS adopts a compositional approach for building certified concurrent OS kernels. The researchers have successfully developed a practical concurrent OS kernel and verified its functional correctness using the formal proof management tool Coq (https://coq.inria.fr/). These examples demonstrate that formally verified microkernels are feasible and provide a strong foundation for security solutions in embedded systems and other military and commercial devices. One key issue is how to leverage the verified microkernel to construct a general purpose platform for developing secure computer systems that comprehensively extend security guarantees down to user space programs without sacrificing kernel performance. For example, the seL4 microkernel uses a capability system to control access to kernel objects. However, these artifacts and access controls do not extend to user-space objects, processes, and applications. Unverified user-space programs will also create their own objects with their own security requirements. A common security requirement is to prevent unauthorized leakage and/or modification of resources via information flow control, both within programs and across systems. Without careful development practice and complete security mediation, it is possible for such user-space programs to leak sensitive data or improperly enforce access control, which undermines the security properties of the holistic system. While systems that enforce information flow control were developed using verified kernels in the past [4, 5], they often had to trust vast amounts of unverified software. This leads to excessive implicit trust (i.e., a large trusted computing base) and weakens the security guarantees. Information flow control methods were also applied to compilers to validate information flow control in programs [6], but such methods were found to be difficult to apply to legacy programs and only apply to type-safe programming languages not typically employed in embedded systems software. This topic seeks innovative technologies that provide efficient information control flow solutions to increase the foundational basis of trust for a microkernel-based system. A highly competitive solution should include techniques to reduce the trusted computing base (e.g., number of lines of code that must be assumed trustworthy and correct) and enable validation of information flow control for system software. The anticipated capabilities should consider the end-to-end workflow, at both the kernel and user levels, and how such new capabilities can be integrated with current microkernels as well as transitioned into the microkernel ecosystem for wider usage in the community.
PHASE I: Investigate the design space for information flow based security for microkernels. Define metrics for measuring trusted computing base reductions as well as formal verification difficulty. Develop an information flow based security model that can be used to describe how critical information flows between user space programs as well as through the microkernel. Develop initial formal arguments and/or validation case on how the new information flow model can be integrated into existing or upcoming formally verified microkernels without violating their verified integrity. Prepare for Phase II implementation.
PHASE II: Fully develop the technology and demonstrate the security gains and performance degradation using the metrics defined during Phase I. Demonstrate the capability using an exemplar user space application such as secure messaging where the secret key material must be tightly controlled. Provide formal arguments on how information flow control for the secret key material (as an example) remains protected.
PHASE III: Create the verification artifacts and demonstrate the information flow control capabilities against representative malicious processes in a relevant environment with realistic concept of operations.
REFERENCES:
1. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S.Winwood. sel4: Formal verification of an os kernel. In Proceedings of ACM Symposium on Operating Syste; 2. R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim, V. Sjöberg, and D. Costanzo. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels In Proc. 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), GA, pages 65; 3. K. Elphinstone and G. Heiser. From L3 to seL4: What have we learnt in 20 years of L4 microkernels? In Proceedings of the 24th ACM Symposium on Operating Systems Principles, pages 133–150, 2013.; 4. S. A. Ames, M. Gasser, and R. R. Schell. Security Kernel Design and Implementation: An Introduction. IEEE Computer, 16(7):14–22, 1983.KEYWORDS: Information Flow Control, Microkernels, Operating Systems, Formal Verification
