Formal specification of information flow security policies and their enforcement in security critical systems

We propose the view that formal specification of a security critical system can be realized by placing suitable restrictions on the otherwise unrestricted functional behavior of its entities. We propose a framework based on traces for developing the specification of such a system. We come up with the characterization of a specification that maximizes functionality of the system with respect to the security policy that it is required to satisfy. The utility of the concepts developed in this paper are illustrated by considering the implementation of MLS policy expressed as restrictions on the information flow relations using the access control mechanisms provided by the take-grant model