Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
The development and proof of a formal specification for a multilevel secure system
Glasgow J., Macewen G. ACM Transactions on Computer Systems5 (2):151-184,1987.Type:Article
Date Reviewed: Oct 1 1987

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.

Reviewer:  Morrie Gasser Review #: CR123595
Bookmark and Share
Security and Protection (C.2.0 ... )
Information Flow Controls (D.4.6 ... )
Lucid (D.3.2 ... )
Snet (C.2.4 ... )
Would you recommend this review?
Other reviews under "Security and Protection": Date
Introduction to data security and controls (2nd ed.)
Edward R. I., QED Information Sciences, Inc., Wellesley, MA, 1991. Type: Book (9780894353864)
Aug 1 1992
Security for computer networks: an introduction to data security in teleprocessing and electronic funds transfer
Davies D., Price W., John Wiley & Sons, Inc., New York, NY, 1984. Type: Book (9780471900634)
Oct 1 1985
Factors affecting distributed system security
Nessett D. IEEE Transactions on Software Engineering SE-13(2): 233-248, 1987. Type: Article
Jun 1 1988

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2023 ThinkLoud®
Terms of Use
| Privacy Policy