Formalizing Information Flow in a Haskell Hypervisor

Separation kernels are the holy grail of secure sys- tems, remaining elusive despite years of research into their design, implementation, and analysis. Though separation kernel research has achieved many successes, the disconnect between information flow theory and system implementation is a significant barrier to further progress. In this paper, we show how a particular branch of information flow theory, noninterference, can be utilized to formulate correctness and security properties of a microkernel- style hypervisor. Thus, we not only provide a first step towards a formally verified separation kernel, but also reduce the gap between information flow theory and operating systems practice.