This clear, well-written research paper presents an approach to the formal mathematical specification of a multilevel secure system that is particularly suited to networks. It provides an alternative to the more common specification techniques applied to secure operating systems. The approach uses the dataflow specification language, Lucid, and an experimental, multilevel Secure Network (SNet) that is currently being implemented. A unique characteristic of SNet is that it permits pure unidirectional communication; it thereby avoids the complexity of two-way protocols used in other approaches while permitting secure data transfer from a low to a high security level. The Lucid specification of SNet contains an upper-layer, abstract model proven to adhere to a set of security constraints and a lower, concrete layer proven to obey its own constraints that are in turn proven to imply the model’s constraints. A primary purpose of the paper is to present the complete specification of both layers and the proofs, focusing more on the model and mathematical foundations of the technique than on the design kf SNet.
While some of the specific decisions made in the definition of the security properties of SNet would not apply to other multilevel networks (for example, the label on a message transmitted by a trusted host shoul` probably be limited by a minimum as well as a maximum level), the approach and mathematical treatment are sound. With suitable tools to process and prove the Lucid specifications (the topic of tools is not covered in the paper), this approach appears at least as practical as any other technique for the formal specification of a secure network. It is stated, but not discussed in detail, that the Lucid language can also serve as a functional programming language or can be converted to Concurrent Euclid. If true, this example is one of the few that come close to the elusive goal of verifying the implementation of a practical system.