A model for verification of data security in operating systems
By Gerald J. Popek, David A. Farber
Communications of the ACM,
Vol. 21 No. 9, Pages 737-749
10.1145/359588.359597
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.
The full text of this article is premium content
0 Comments
No entries found
Log in to Read the Full Article
Purchase the Article
Log in
Create a Web Account
If you are an ACM member, Communications subscriber, Digital Library subscriber, or use your institution's subscription, please set up a web account to access premium content and site
features. If you are a SIG member or member of the general public, you may set up a web account to comment on free articles and sign up for email alerts.