Specification and verification of the UCLA Unix security kernel

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Specification and verification of the UCLA Unix security kernel

Full text

Pdf (1.19 MB)

Source

Communications of the ACM archive
Volume 23 , Issue 2 (February 1980) table of contents

Pages: 118 - 131

Year of Publication: 1980

ISSN:0001-0782

Authors

Bruce J. Walker	Univ. of California at Los Angeles, Los Angeles
Richard A. Kemmerer	Univ. of California at Los Angeles, Los Angeles
Gerald J. Popek	Univ. of California at Los Angeles, Los Angeles

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 15, Downloads (12 Months): 65, Citation Count: 24

Additional Information:

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/358818.358825 What is a DOI?

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	Eggert, P.R., Hall, M., and Kemmerer, R.A. KAL KAN: An assertion language - - for the verification of korrect ALPO notation. Comptr. Sci. Dept. Memo 156, UCLA, Los Angeles, Calif., March 1976.
	2	Gerhart, S.L., and Wile, D.F. Preliminary report of the delta experiment: Specification and verification of a multiple-user file updating module. Proc. Specification of Reliable Software Conf., April 1979, 198-211.
	3	Gerhart, S.L. private communication.
	4	Good, D.I., London, R.L., and Bledsoe, W.W. An interactive program verification system. IEEE Trans. Software Eng. l, 1 March 1975, 59-67.
	5	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]
	6	Hoare, C.A.R. Procedures and parameters: an axiomatic approach. Lecture Notes in Mathematics 188, E. Engler, Ed., Springer-Verlag, 1971, 102-116.
	7	Hoare, C.A.R. Proof of correctness of data representations. Acta lnformatica 1 (1972), 271-282.
	8	Hoare, C.A.R., and Wirth, N. An axiomatic definition of the programming language PASCAL. Acta Informatica 2 (1973), 335-355.
	9	Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
	10	Kalish, D. and Montague, R. Logic techniques of formal reasoning. Harcourt, Brace, and World, Inc., New York, N.Y., 1964.
	11	Richard Allen Kemmerer, Formal verification of the ucla security kernel: abstract model, mapping functions, theorem generation, and proofs., 1979
	12	Lampson, B.W. Protection. Proc. 5th Annual Princeton Conf. on Information Science and Systems, Princeton, March 1971, 437-443.
	13	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]
	14	B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
	15	Barbara Liskov , Stephen Zilles, Programming with abstract data types, Proceedings of the ACM SIGPLAN symposium on Very high level languages, p.50-59, March 28-29, 1974, Santa Monica, California, United States
	16	Liskov, B., and Zilles, S. Specification techniques for data abstractions. IEEE Trans. Software Eng. 1, 1 March 1975, 7-19.
	17	David C. Luckham , Norihisa Suzuki, Automatic program verification V: verification-oriented proof rules for arrays, records and pointers, Stanford University, Stanford, CA, 1976
	18	Musser, D. AFFIRM user's guide. USC/Information Sciences Institute, Marina del Rey, Calif. (forthcoming)
	19	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]
	20	Popek, G.J. Protection Structures. Computer 7, 6 (June 1974), 22-33.
	21	Popek, G.J., Kampe, M., Kline, C.S., and Walton, E.J. The UCLA data secure operating system. UCLA Technical Report, July 1977.
	22	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 [doi>10.1145/359588.359597]
	23	Popek, G.J., Kampe, M., Kline, C.S., and Walton, E.J. UCLA data secure Unix. Proc. 1979 NCC, AFIPS Press, 355-364.
	24	Ritchie, D.M., and Thompson, K. The Unix time-sharing system. Bell System Technical Journal 57, 6 (July-August 1978), 1905-1930.
	25	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
	26	Lawrence Robinson , Karl N. Levitt, Proof techniques for hierarchically structured programs, Communications of the ACM, v.20 n.4, p.271-283, April 1977 [doi>10.1145/359461.359483]
	27	Mary Shaw , William A. Wulf , Ralph L. London, Abstraction and verification in Alphard: defining and specifying iteration and generators, Communications of the ACM, v.20 n.8, p.553-564, Aug. 1977 [doi>10.1145/359763.359782]
	28	Walker, B.J. Verification of the UCLA security kernel: data defined specifications. Master's Th., UCLA, Los Angeles, Calif., October 1977.
	29	Walker, B.J., Popek, G.J., and Kemmerer, R.A. Formalization of the top-level specification/verification of the UCLA security kernel. UCLA Computer Science Dept. Technical Report (forthcoming).
	30	Walton, E.J. The UCLA PASCAL translation system. UCLA Computer Science Dept. Technical Report, January 1976.
	31	Wells, R.E. Specification and implementation of a verifiable communication system. Master's Th., U. of Texas at Austin, December 1976.
	32	Wirth, N. The programming language PASCAL. Acta Informatica 1 (1971), 33-63.
	33	Wulf, W.A., London, R.L., and Shaw, M. An introduction to the construction and verification of ALPHARD programs. IEEE Trans. Software Eng. 2, 4 December 1976, 253-265.
	34	Yonke, M.D. The XIVUS environment: XIVUS working paper no. 1. USC/lnformation Sciences Institute, Marina del Rey, Calif., April 1976.

CITED BY 24

	Duane Olawsky , Todd Fine , Edward Schneider , Ray Spencer, Developing and using a “policy neutral” access control policy, Proceedings of the 1996 workshop on New security paradigms, p.60-67, September 17-20, 1996, Lake Arrowhead, California, United States
	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
	J. M. Rushby, Design and verification of secure systems, ACM SIGOPS Operating Systems Review, v.15 n.5, p.12-21, December 1981
	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
	Matt Bishop, Analyzing the security of an existing computer system, Proceedings of 1986 ACM Fall joint computer conference, p.1115-1119, November 1986, Dallas, Texas, United States
	Jonathan M. Silverman, Reflections on the verification of the security of an operating system kernel, ACM SIGOPS Operating Systems Review, v.17 n.5, p.143-154, October 1983
	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
	Gregory R. Andrews, Parallel programs: proofs, principles, and practice, Communications of the ACM, v.24 n.3, p.140-145, March 1981
	Richard A. Kemmerer, Cybersecurity, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	Carl E. Landwehr, Formal Models for Computer Security, ACM Computing Surveys (CSUR), v.13 n.3, p.247-278, Sept. 1981
	W. R. Bevier, Kit: A Study in Operating System Verification, IEEE Transactions on Software Engineering, v.15 n.11, p.1382-1396, November 1989
	Wen-Pai Lu , Malur K. Sundareshan, A Model for Multilevel Security in Computer Networks, IEEE Transactions on Software Engineering, v.16 n.6, p.647-659, June 1990
	Gerwin Klein , Ralf Huuck, High assurance system software, Proceedings of the 10th Australian workshop on Safety critical systems and software, p.59-67, August 25, 2005, Sydney, Australia
	Rafal Kolanski , Gerwin Klein, Formalising the L4 microkernel API, Proceedings of the 12th Computing: The Australasian Theroy Symposium, p.53-68, January 16-19, 2006, Hobart, Australia
	Kevin Elphinstone , Gerwin Klein , Philip Derrin , Timothy Roscoe , Gernot Heiser, Towards a practical, verified kernel, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
	Harvey Tuch , Gerwin Klein , Michael Norrish, Types, bytes, and separation logic, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Harvey Tuch , Gerwin Klein , Gernot Heiser, OS verification: now!, Proceedings of the 10th conference on Hot Topics in Operating Systems, p.2-2, June 12-15, 2005, Santa Fe, NM
	Spencer E. Minear, Providing policy control over object operations in a mach based system, Proceedings of the 5th conference on USENIX UNIX Security Symposium, p.13-13, June 05-07, 1995, Salt Lake City, Utah
	Philip Derrin , Kevin Elphinstone , Gerwin Klein , David Cock , Manuel M. T. Chakravarty, Running the manual: an approach to high-assurance microkernel development, Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, September 17-17, 2006, Portland, Oregon, USA
	Rafal Kolanski, A Logic for Virtual Memory, Electronic Notes in Theoretical Computer Science (ENTCS), 217, p.61-77, July, 2008
	Tom In der Rieden , Alexandra Tsyban, CVM -- A Verified Framework for Microkernel Programmers, Electronic Notes in Theoretical Computer Science (ENTCS), 217, p.151-168, July, 2008
	Gernot Heiser , Kevin Elphinstone , Ihor Kuz , Gerwin Klein , Stefan M. Petters, Towards trustworthy computing systems: taking microkernels to the next level, ACM SIGOPS Operating Systems Review, v.41 n.4, July 2007
	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
	Hendrik Tews , Marcus Völp , Tjark Weber, Formal Memory Models for the Verification of Low-Level Operating-System Code, Journal of Automated Reasoning, v.42 n.2-4, p.189-227, April 2009

INDEX TERMS

Keywords:
ALPHARD, Unix, formal specifications, operating systems, programming methodology, protection, security, security kernel, verification

Collaborative Colleagues:

Bruce J. Walker: colleagues

Richard A. Kemmerer: colleagues

Gerald J. Popek: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player