A model for verification of data security in operating systems

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.

REFERENCES

• 1: Abraham, S. "Access authorization and control mechanisms for operating systems. Masters Th., Comptr. Sci. Dept., U. of California, Los Angeles, 1976.
• 2: Bell, D., and Lapadula, L. Secure computer system: Unified exposition and multics interpretation. Tech. Rep. 2997, Mitre, Bedford, Mass., July 1975.
• 3: Birman, A. "On Proving Correctness of Micrograms. IBM J. Res. and Develop. 18, 3 (May 1974), 250-266.
• 4: Bisbey, R., Popek, G., and Carlstedt, J. Inconsistency of a single data value over time. USC/ISI Res. Rep., U. of Southern California, Los Angeles, Feb. 1975.
• 5: Carlstedt, J., Bisbey, R., and Popek, G. Pattern directed protection evaluation. USC/ISI Res. Rep. 75-31, U. of Southern California, Los Angeles, Jan. 1975.
• 6: Laurian Mircea Chirica, Contributions to compiler correctness., 1976
• 7: Richard H. Eckhouse, Jr. , L. Robert Morrison, Minicomputer Systems: Organization, Programming and Applications (PDP-11), Prentice Hall Professional Technical Reference, 1979
• 8: Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972 [doi>10.1145/356599.356602]
• 9: Fiorani, P. The UCLA virtual machine monitor. Master's Th., Comptr. Sci. Dept., U. of California, Los Angeles, 1975.
• 10: Floyd, R. Assigning meanings to programs. Proceedings of Symposia in Applied Mathematics, VoL 19, Amer. Math. Soc., Providence, R.l., pp. 19-31.
• 11: Good, D. Private communication, O. of Texas, 1975.
• 12: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 13: Hoare, C.A.R. Proof of correctness of data representations. Acta lnformatica 1 (1972), 271-281.
• 14: Hoare, C.A.R. An axiomatic definition of the programming language PASCAL. Acta lnformatica 2 (1973), 335-355.
• 15: Kampe, M., Kline, C., Popek, G., and Walton, E. The UCLA data secure operating system. Tecb. Rep., U. of California, Los Angeles, July 1977.
• 16: Kemmerer, R. Verification of large programs: Mapping issues. Ph.D. Th., Comptr. Sci. Dept., U. of California, Los Angeles, 1978 (forthcoming).
• 17: Kline, C., and Popek, G. Encryption in computer network security. Tech. Rep., U. of California, Los Angeles, April 1977. Submitted for publication.
• 18: Lampson, B.W. Protection. Proc. Fifth Annual Princeton Conf. Inform. Sci. and Syst., Princeton U., Princeton, N.J., March 1971, pp. 437-443; also Operating Syst. Rev. (ACM) 8, 1 (Jan. 1974), 18-24.
• 19: Donald I. Good , Ralph L. London , W. W. Bledsoe, An interactive program verification system, Proceedings of the international conference on Reliable software, p.482-492, April 21-23, 1975, Los Angeles, California
• 20: Manna, Z. The correctness of programs. J. Comptr. Syst. Sci. 3, (1969), 119-127.
• 21: Jonathan K. Millen, Security Kernel validation in practice, Communications of the ACM, v.19 n.5, p.243-250, May 1976 [doi>10.1145/360051.360059]
• 22: Robin Milner, An algebraic definition of simulation between programs, Stanford University, Stanford, CA, 1971
• 23: Neumann, P., et al. On the design of a probably secure operating system. Proc. Workshop on Protection in Operating Systems. IRIA. Rocquencourt, France, (Aug. 1974), pp. 161-175.
• 24: Popek, G., and Kline, C. Verifiable secure operating systems software. Proc. AFIPS 1974 NCC, AFIPS Press, Montvale, N.J., pp. 135-142.
• 25: Gerald J. Popek , Charles S. Kline, A verifiable protection system, Proceedings of the international conference on Reliable software, p.294-304, April 21-23, 1975, Los Angeles, California
• 26: Gerald J. Popek , Charles S. Kline, Issues in Kernel Design, Operating Systems, An Advanced Course, p.209-227, January 1978
• 27: Walker, B. Verification of the UCLA security kernel: datadefined specifications. Master's Th., Comptr. Sci. Dept., University of California, Los Angeles, Oct. 1977.
• 28: Walton, E. The UCLA kernel. Master's Th., Comptr. Sci. Dept., U. of California, Los Angeles, 1975.
• 29: Peter Wegner, The Vienna Definition Language, ACM Computing Surveys (CSUR), v.4 n.1, p.5-63, March 1972 [doi>10.1145/356596.356598]
• 30: Wirth, N. The programming language Pascal. Acta Informatica 1 (1971), 35-63.
• 31: Wirth, N., and Jensen, K. The programming language Pascal (revised report). In Pascal User Manual and Report, Springer-Verlag, 1974, pp 133-170.
• 32: {DEC 73} PDP-I 1/45 Processor Handbook. Digital Equipment Corp., Maynard, Mass., 1973.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS

Additional Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS

General Terms:
Design, Performance, Security, Theory, Verification

Keywords:
operating systems, program verification, protection, security