NICTA
UNSW
Australian National University
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.
@inproceedings{Murray_MBGK_12, isbn = {978-3-642-35307-9}, publisher = {Springer}, booktitle = {International Conference on Certified Programs and Proofs}, month = dec, paperurl = {https://trustworthy.systems/publications/nicta_full_text/6004.pdf}, year = {2012}, editor = {{Chris Hawblitzel and Dale Miller}}, keywords = {information flow, refinement, scheduling, state monads}, title = {Noninterference for Operating System Kernels}, pages = {126--142}, author = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Klein, Gerwin}, address = {Kyoto, Japan} }