article

Free access

Specification and verification of the UCLA Unix security kernel

Authors:

Bruce J. Walker,

Richard A. Kemmerer,

Gerald J. PopekAuthors Info & Claims

Communications of the ACM, Volume 23, Issue 2

Pages 118 - 131

https://doi.org/10.1145/358818.358825

Published: 01 February 1980 Publication History

PDF eReader

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.

Google Scholar

[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.

Google Scholar

[3]

Gerhart, S.L. private communication.

Google Scholar

[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.

Digital Library

Google Scholar

[5]

Hoare, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10 (October 1969), 576-583.

Digital Library

Google Scholar

[6]

Hoare, C.A.R. Procedures and parameters: an axiomatic approach. Lecture Notes in Mathematics 188, E. Engler, Ed., Springer-Verlag, 1971, 102-116.

Google Scholar

[7]

Hoare, C.A.R. Proof of correctness of data representations. Acta lnformatica 1 (1972), 271-282.

Google Scholar

[8]

Hoare, C.A.R., and Wirth, N. An axiomatic definition of the programming language PASCAL. Acta Informatica 2 (1973), 335-355.

Digital Library

Google Scholar

[9]

Jensen, K. and Wirth, N. PASCAL user manual and report. Lecture Notes in Computer Science 18, Springer-Verlag, 1974.

Digital Library

Google Scholar

[10]

Kalish, D. and Montague, R. Logic techniques of formal reasoning. Harcourt, Brace, and World, Inc., New York, N.Y., 1964.

Google Scholar

[11]

Kemmerer, R.A. Verification of the UCLA security kernel: Abstract model, mapping, theorem generation and proof. Ph.D. Th., UCLA, Los Angeles, Calif., 1979.

Digital Library

Google Scholar

[12]

Lampson, B.W. Protection. Proc. 5th Annual Princeton Conf. on Information Science and Systems, Princeton, March 1971, 437-443.

Google Scholar

[13]

Lampson, B.W. A note on the confinement problem. Comm. ACM 16, 10 (October 1973), 613-615.

Digital Library

Google Scholar

[14]

Lampson, B.W., et al. Report on the programming language EUCLID. SIGPLAN Notices, 12, 2, February 1977.

Digital Library

Google Scholar

[15]

Liskov, B., and Zilles, S. Programming with abstract data types. Proc. ACM Conf. on Very High Level Languages, SIG- PLAN Notices, 9, April 1974, 50-59.

Digital Library

Google Scholar

[16]

Liskov, B., and Zilles, S. Specification techniques for data abstractions. IEEE Trans. Software Eng. 1, 1 March 1975, 7-19.

Digital Library

Google Scholar

[17]

Luckham, D., and Suzuki, N. Automatic program verification V: Verification-oriented proof rules for arrays, records and Pointers. Stanford Artificial Intelligence Laboratory Memo AIM- 278, March 1976.

Digital Library

Google Scholar

[18]

Musser, D. AFFIRM user's guide. USC/Information Sciences Institute, Marina del Rey, Calif. (forthcoming)

Google Scholar

[19]

Parnas, D.L. A technique for software module specification with examples. Comm. ACM 15, 5 (May 1972), 330-336.

Digital Library

Google Scholar

[20]

Popek, G.J. Protection Structures. Computer 7, 6 (June 1974), 22-33.

Google Scholar

[21]

Popek, G.J., Kampe, M., Kline, C.S., and Walton, E.J. The UCLA data secure operating system. UCLA Technical Report, July 1977.

Google Scholar

[22]

Popek, G.J. and Farber, D. A Model for verification of data security in operating systems. Comm. ACM 21, 9 (September 1978), 737-749.

Digital Library

Google Scholar

[23]

Popek, G.J., Kampe, M., Kline, C.S., and Walton, E.J. UCLA data secure Unix. Proc. 1979 NCC, AFIPS Press, 355-364.

Google Scholar

[24]

Ritchie, D.M., and Thompson, K. The Unix time-sharing system. Bell System Technical Journal 57, 6 (July-August 1978), 1905-1930.

Crossref

Google Scholar

[25]

Robinson, L., et al. On attaining reliable software for a secure operating systems. Proc. 1975 Int. Conf. on Reliable Software, April 1975, 267-284.

Digital Library

Google Scholar

[26]

Robinson, L., and Levitt, K.N. Proof techniques for hierarchically structured programs. Comm. ACM 20, 4 (April 1977), 271- 283.

Digital Library

Google Scholar

[27]

Shaw, M., Wulf, W.A., and London, R.L. Abstraction and verification in alphard: Defining and specifying iteration and generators. Comm. ACM 20, 8 (August 1977), 553-563.

Digital Library

Google Scholar

[28]

Walker, B.J. Verification of the UCLA security kernel: data defined specifications. Master's Th., UCLA, Los Angeles, Calif., October 1977.

Google Scholar

[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).

Google Scholar

[30]

Walton, E.J. The UCLA PASCAL translation system. UCLA Computer Science Dept. Technical Report, January 1976.

Google Scholar

[31]

Wells, R.E. Specification and implementation of a verifiable communication system. Master's Th., U. of Texas at Austin, December 1976.

Google Scholar

[32]

Wirth, N. The programming language PASCAL. Acta Informatica 1 (1971), 33-63.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[34]

Yonke, M.D. The XIVUS environment: XIVUS working paper no. 1. USC/lnformation Sciences Institute, Marina del Rey, Calif., April 1976.

Google Scholar

Cited By

View all

Wang ZLan YHe XLv J(2024)A Formal Verification Approach for Linux Kernel DesigningTechnologies10.3390/technologies1208013212:8(132)Online publication date: 12-Aug-2024
https://doi.org/10.3390/technologies12080132
Qian ZSun GXing XDhiman G(2024)Refinement modeling and verification of secure operating systems for communication in digital twinsDigital Communications and Networks10.1016/j.dcan.2022.07.01210:2(304-314)Online publication date: Apr-2024
https://doi.org/10.1016/j.dcan.2022.07.012
Qian ZXia RSun GXing XXia K(2023)A measurable refinement method of design and verification for micro-kernel operating systems in communication networkDigital Communications and Networks10.1016/j.dcan.2022.03.0249:5(1070-1079)Online publication date: Oct-2023
https://doi.org/10.1016/j.dcan.2022.03.024
Show More Cited By

Specification and verification of the UCLA Unix security kernel
1. Software and its engineering
  1. Software creation and management

Recommendations

Specification and verification of the UCLA Unix security kernel (Extended Abstract)
SOSP '79: Proceedings of the seventh ACM symposium on Operating systems principles

Data Secure Unix, a kernel structured operating system, was constructed as part of an ongoing effort at UCLA to develop procedures by which operating systems can be produced and shown secure. Program verification methods were extensively applied as a ...
Security Kernel validation in practice

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 ...
A model for verification of data security in operating systems

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 23, Issue 2

Feb. 1980

69 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/358818

Editor:
Robert L. Ashenhurst
Univ. of Chicago, Chicago, IL

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 February 1980

Published in CACM Volume 23, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

89
Total Citations
View Citations
1,135
Total Downloads

Downloads (Last 12 months)126
Downloads (Last 6 weeks)26

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Wang ZLan YHe XLv J(2024)A Formal Verification Approach for Linux Kernel DesigningTechnologies10.3390/technologies1208013212:8(132)Online publication date: 12-Aug-2024
https://doi.org/10.3390/technologies12080132
Qian ZSun GXing XDhiman G(2024)Refinement modeling and verification of secure operating systems for communication in digital twinsDigital Communications and Networks10.1016/j.dcan.2022.07.01210:2(304-314)Online publication date: Apr-2024
https://doi.org/10.1016/j.dcan.2022.07.012
Qian ZXia RSun GXing XXia K(2023)A measurable refinement method of design and verification for micro-kernel operating systems in communication networkDigital Communications and Networks10.1016/j.dcan.2022.03.0249:5(1070-1079)Online publication date: Oct-2023
https://doi.org/10.1016/j.dcan.2022.03.024
Nicole OLemerre MBardin SRival X(2021)No Crash, No Exploit: Automated Verification of Embedded Kernels2021 IEEE 27th Real-Time and Embedded Technology and Applications Symposium (RTAS)10.1109/RTAS52030.2021.00011(27-39)Online publication date: May-2021
https://doi.org/10.1109/RTAS52030.2021.00011
Qian ZJin YSun GXing XXia K(2021)Formal design and verification of system task in intelligent transportation systems based on micro-kernel architectureJournal of Ambient Intelligence and Humanized Computing10.1007/s12652-021-03454-9Online publication date: 29-Aug-2021
https://doi.org/10.1007/s12652-021-03454-9
Qian ZLiu YJin YXing XZhang MGong SLiu WYang WTan JZhang L(2018)Research on Formal Design and Verification of Operating SystemsEmbedded Systems Technology10.1007/978-981-13-1026-3_6(81-88)Online publication date: 10-Jul-2018
https://doi.org/10.1007/978-981-13-1026-3_6
Nelson LSigurbjarnarson HZhang KJohnson DBornholt JTorlak EWang X(2017)HyperkernelProceedings of the 26th Symposium on Operating Systems Principles10.1145/3132747.3132748(252-269)Online publication date: 14-Oct-2017
https://dl.acm.org/doi/10.1145/3132747.3132748
Sewell TKam FHeiser G(2017)High-assurance timing analysis for a high-assurance real-time operating systemReal-Time Systems10.1007/s11241-017-9286-353:5(812-853)Online publication date: 1-Sep-2017
https://dl.acm.org/doi/10.1007/s11241-017-9286-3
Ren LChang RYin QWang W(2017)Using the B Method to Formalize Access Control Mechanism with TrustZone Hardware Isolation (Short Paper)Information Security Practice and Experience10.1007/978-3-319-72359-4_47(759-769)Online publication date: 8-Dec-2017
https://doi.org/10.1007/978-3-319-72359-4_47
Liang HZhang DJia XPei XLi G(2016)Verifying RTuinOS using VCC: From approach to practice2016 17th IEEE/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD)10.1109/SNPD.2016.7515927(373-378)Online publication date: May-2016
https://doi.org/10.1109/SNPD.2016.7515927
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

References

Cited By

Recommendations