Achieving Information Flow Security Through Precise Control of Effects

William Lawrence Harrison (University of Missouri, Columbia)
Monday April 18, 10am
3124 Siebel

Abstract:

Confidentiality and integrity concerns within the setting of shared-state concurrency are really about controlling interference and interaction between threads. It is a natural and compelling idea, therefore, to apply the mathematics of effects---monads---to this problem as monads provide precise control of such effects. In fact, layering monads---i.e., modularly constructing monads with monad transformers---yields fine-grained control of effects and their interactions. This research demonstrates how the fine-grained tailoring of effects possible with monad transformers promotes integrity and information security concerns. As a proof of concept, we show that a classic design in computer security (the separation kernel of Rushby) can be realized and verified in a straightforward manner within any pure, higher-order, typed functional language.