While intransitive noninterference is a natural property for any secure OS kernel to enforce, proving that the implementation of any particular general-purpose kernel enforces this property is yet to be achieved. In this paper we take a significant step towards this vision by presenting a machine-checked formulation of intransitive noninterference for OS kernels, and its associated sound and complete unwinding conditions, as well as a scalable proof calculus over nondeterministic state monads for discharging these unwinding conditions across a kernel's implementation. Our ongoing experience applying this noninterference framework and proof calculus to the seL4 microkernel validates their utility and real-world applicability. © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Murray, T., Matichuk, D., Brassil, M., Gammie, P., & Klein, G. (2012). Noninterference for operating system kernels. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 126–142). https://doi.org/10.1007/978-3-642-35308-6_12
Mendeley helps you to discover research relevant for your work.