Several mathematical models have been developed which describe various kinds of composition for secure systems. These models can be complex and unsatisfactory in the sense that it is difficult for a system designer to determine exactly how to connect components together to achieve a particular (security) property. We provide a simple mathematical model which we use to describe security policies and components. The model provides a means for describing the combination of both components and policies and for showing whether combinations of components will satisfy specified policies. If the system designer can describe a system in the terms we present, then the designer can use these terms to analyze some of the security properties of the system.>

The authors present a formal, mathematical model for a trusted file server (TFS) for a multilevel secure distributed computer system. The goal is to produce formal verification from the top-level specification down through code for the entire system of which a TFS is one component. By viewing the TFS as a black box, it is possible to specify its security as a relation that must hold invariantly between an output stream of responses and an input stream of requests. Using the proposed approach, the authors have provided a small (perhaps minimal) set of compromise security constraints on the TFS. They have produced an implementation of the TFS in Gypsy and verified that the implementation satisfies this model. It is also shown that the specified relation is stronger than noninterference, and that a noninterference model cannot cover the security-relevant functionality of deleting or changing the size of a file.>

Research in developing formalisms for secure distributed systems reveals that a graph-theoretic model captures the fundamental notion of trust, while permitting a rigorous and elegant decomposition into lower levels of implementation. With such a model, security labels need be applied to directed edges only, not to events, ports, processes, messages, or whatever. Moreover, the usual concept of "secure state" does not lend itself to defining security in a distributed system, whereas our Model guarantees secure transitions in precisely this context.