Security Kernel validation in practice

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Security Kernel validation in practice

Full text

Pdf (676 KB)

Source

Communications of the ACM archive
Volume 19 , Issue 5 (May 1976) table of contents

Pages: 243 - 250

Year of Publication: 1976

ISSN:0001-0782

Author

Jonathan K. Millen

The MITRE Corp., Bedford, MA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 29, Citation Count: 27

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/360051.360059 What is a DOI?

ABSTRACT

A security kernel is a software and hardware mechanism that enforces access controls within a computer system. The correctness of a security kernel on a PDP-11/45 is being proved. This paper describes the technique used to carry out the first step of the proof: validating a formal specification of the program with respect to axioms for a secure system.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Schiller, W.L. The design and specification of a security kernel for the PDP-11/45. ESD-TR-75-69, The MITRE Corporation, Bedford, Mass., March 1975.
	2	Bell, D.E., and Burke, E.L. A software validation technique for certification: the methodology. ESD-TR-75-54, Volume I, The MITRE Corporation, Bedford, Mass., Nov. 1974.
	3	Bell, D.E., and LaPadula, L.J. Secure computer systems; Mathematical Foundations. ESD-TR-73-278, Vol. I-III, The MITRE Corporation, Bedford, Mass.
	4	D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
	5	William Robert Price, Implications of a virtual memory mechanism for implementing protection in a family of operating systems, 1973
	6	Lawrence Robinson , Karl N. Levitt , Peter G. Neumann , Ashok R. Saxena, On attaining reliable software for a secure operating system, Proceedings of the international conference on Reliable software, p.267-284, April 21-23, 1975, Los Angeles, California
	7	Butler W. Lampson, A note on the confinement problem, Communications of the ACM, v.16 n.10, p.613-615, Oct. 1973 [doi>10.1145/362375.362389]
	8	Anderson, J.P. Computer security technology planning study. ESD-TR-73-51, USAF Electronic Systems Division, Bedford, Mass., Oct. 1972.
	9	Schell, R., Downey, P., and Popek, G., Preliminary notes the design of a secure military computer system. MCI-73-1, USAF Electronic Systems Div., Jan. 1972.
	10	Design for Multics security enhancements. ESD-TR-74-176, Honeywell Information Systems, Inc., Dec. 1973.

CITED BY 27

	Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980
	Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Untrusted hosts and confidentiality: secure program partitioning, ACM SIGOPS Operating Systems Review, v.35 n.5, Dec. 2001
	Dorothy E. Denning , Peter J. Denning, Data Security, ACM Computing Surveys (CSUR), v.11 n.3, p.227-249, Sept. 1979
	R. J. Feiertag , K. N. Levitt , L. Robinson, Proving multilevel security of a system design, ACM SIGOPS Operating Systems Review, v.11 n.5, p.57-65, November 1977
	Peter G. Neumann , Richard J. Feiertag , Karl N. Levitt , Lawrence Robinson, Software development and proofs of multi-level security, Proceedings of the 2nd international conference on Software engineering, p.421-428, October 13-15, 1976, San Francisco, California, United States
	G. H. Chisholm , A. S. Wojcik, An Application of Formal Analysis to Software in a Fault-Tolerant Environment, IEEE Transactions on Computers, v.48 n.10, p.1053-1064, October 1999
	Robert P. Trueblood , H. Rex Hartson , Johannes J. Martin, MULTISAFE—a modular multiprocessing approach to secure database management, ACM Transactions on Database Systems (TODS), v.8 n.3, p.382-409, Sept. 1983
	J. M. Rushby, Design and verification of secure systems, ACM SIGOPS Operating Systems Review, v.15 n.5, p.12-21, December 1981
	Richard A. Kemmerer, Shared resource matrix methodology: an approach to identifying storage and timing channels, ACM Transactions on Computer Systems (TOCS), v.1 n.3, p.256-277, August 1983
	Maureen Harris Cheheyl , Morrie Gasser , George A. Huff , Jonathan K. Millen, Verifying Security, ACM Computing Surveys (CSUR), v.13 n.3, p.279-339, Sept. 1981
	Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Secure program partitioning, ACM Transactions on Computer Systems (TOCS), v.20 n.3, p.283-328, August 2002
	Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977
	Lloyd Fosdick , Donald I. Good, SIGSOFT tutorial on program verification (Tutorial Session), Proceedings of the annual conference, p.521-522, October 20-22, 1976, Houston, Texas, United States
	Ellis Choen, Information transmission in computational systems, ACM SIGOPS Operating Systems Review, v.11 n.5, p.133-139, November 1977
	Gerald J. Popek , David A. Farber, A model for verification of data security in operating systems, Communications of the ACM, v.21 n.9, p.737-749, Sept. 1978
	Richard A. Kemmerer, Cybersecurity, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	R. Stockton Gaines , Norman Z. Shapiro, Some security principles and their application to computer security, ACM SIGOPS Operating Systems Review, v.12 n.3, p.19-28, July 1978
	Andrew C. Myers , Barbara Liskov, Protecting privacy using the decentralized label model, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.410-442, Oct. 2000
	Carl E. Landwehr, Formal Models for Computer Security, ACM Computing Surveys (CSUR), v.13 n.3, p.247-278, Sept. 1981
	Chii-Ren Tsai , Virgil D. Gligor , C. S. Shandersekaran, On the Identification of Covert Storage Channels in Secure Systems, IEEE Transactions on Software Engineering, v.16 n.6, p.569-580, June 1990
	Richard P. Reitman , Gregory R. Andrews, Certifying information flow properties of programs: an axiomatic approach, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.283-290, January 29-31, 1979, San Antonio, Texas
	Donald Mackenzie , Garrel Pottinger, Mathematics, Technology, and Trust: Formal Verification, Computer Security, and the U.S. Military, IEEE Annals of the History of Computing, v.19 n.3, p.41-59, July 1997
	C. Mohan, Survey of recent operating systems research, designs and implementations, ACM SIGOPS Operating Systems Review, v.12 n.1, p.53-89, January 1978
	Richard A. Kemmerer , Phillip A. Porras, Covert Flow Trees: A Visual Approach to Analyzing Covert Storage Channels, IEEE Transactions on Software Engineering, v.17 n.11, p.1166-1185, November 1991
	Deborah Downs , Gerald J. Popek, Data base management systems security and INGRES, Proceedings of the fifth international conference on Very Large Data Bases, p.280-290, October 03-05, 1979, Rio de Janeiro, Brazil
	Charles R. Young, A security policy for a profile-oriented operating system, Proceedings of the May 4-7, 1981, national computer conference, May 04-07, 1981, Chicago, Illinois
	Stephen T. Walker, The advent of trusted computer operating systems, Proceedings of the May 19-22, 1980, national computer conference, May 19-22, 1980, Anaheim, California

INDEX TERMS

Keywords:
correctness, formal specification, protection, security kernel, validation, verification

Collaborative Colleagues:

Jonathan K. Millen: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player