Workshop on
Foundations of Computer Security - FCS'03
Ottawa, Canada, 26-27 June 2003
Domain Separation by Construction
William Harrison, Mark Tullsen, and James Hook (OGI - USA)
Abstract
This paper advocates a novel approach to language-based security: by
structuring software with monads (a form of abstract data type for effects),
we are able to maintain separation of effects by construction. The thesis
of this work is that well-understood properties of monads and monad
transformers aid in the construction and verification of secure software.
We introduce a formulation of non-interference based on monads rather than
the typical trace-based formulation. Using this formulation, we prove a
non-interference style property for a simple instance of our system model.
Because monads may be easily and safely represented within any pure,
higher-order, typed functional language, the resulting system models may be
directly realized within such a language.