Date Added: May 2011
In this paper, the controlling information flow and maintaining integrity via monadic encapsulation of effects. This paper is constructive, relying on properties of monads and monad transformers to build, verify, and extend secure software systems. The authors illustrate this approach by construction of abstract operating systems called separation kernels. Starting from a mathematical model of shared-state concurrency based on monads of resumptions and state, they outline the development by stepwise refinements of separation kernels supporting Unix-like system calls, inter domain communication, and a formally verified security policy.