Home → Magazine Archive → September 1978 (Vol. 21, No. 9) → A model for verification of data security in operating... → Abstract

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

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


No entries found