The development and proof of a formal specification for a multilevel secure system
- 1 March 1987
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computer Systems
- Vol. 5 (2) , 151-184
- https://doi.org/10.1145/13677.22724
Abstract
This paper describes current work on the design and specification of a multilevel secure distributed system called SNet. It discusses security models in general, the various problems of information flows in SNet, and the abstract and concrete security model components for SNet. It also introduces Lucid as a language for specifying distributed systems. The model components are expressed in Lucid; these Lucid partial specifications are shown to be correct with respect to the formal model, and the two model components are shown to be consistent. The complete functional specification of SNet in Lucid, its implementation in Concurrent Euclid, and the verification of the implementation with respect to the Lucid specification are not discussed.Keywords
This publication has 8 references indexed in Scilit:
- Adequate proof principles for invariance and liveness properties of concurrent programsScience of Computer Programming, 1984
- Formal Specification and Verification of Distributed SystemsIEEE Transactions on Software Engineering, 1983
- A Distributed Secure SystemComputer, 1983
- Formal Models for Computer SecurityACM Computing Surveys, 1981
- Proving multilevel security of a system designACM SIGOPS Operating Systems Review, 1977
- Lucid—A Formal System for Writing and Proving ProgramsSIAM Journal on Computing, 1976
- A lattice model of secure information flowCommunications of the ACM, 1976
- The next 700 programming languagesCommunications of the ACM, 1966