A model for verification of data security in operating systems
- 1 September 1978
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 21 (9), 737-749
- https://doi.org/10.1145/359588.359597
Abstract
Program verification applied to kernel architectures forms a promising method for providing uncircumventably secure, shared computer systems. A precise definition of data security is developed here in terms of a general model for operating systems. This model is suitable as a basis for verifying many of those properties of an operating system which are necessary to assure reliable enforcement of security. The application of this approach to the UCLA secure operating system is also discussed.This publication has 12 references indexed in Scilit:
- Security Kernel validation in practiceCommunications of the ACM, 1976
- Minicomputer systems: Organization and programming (PDP-11): Richard H. Eckhouse, Jr.Computer Languages, 1975
- An interactive program verification systemPublished by Association for Computing Machinery (ACM) ,1975
- A verifiable protection systemPublished by Association for Computing Machinery (ACM) ,1975
- An axiomatic definition of the programming language PASCALActa Informatica, 1973
- An Assessment of Techniques for Proving Program CorrectnessACM Computing Surveys, 1972
- The Vienna Definition LanguageACM Computing Surveys, 1972
- Proof of correctness of data representationsActa Informatica, 1972
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- The correctness of programsJournal of Computer and System Sciences, 1969