More Web Proxy on the site http://driver.im/

article

Free access

A model for verification of data security in operating systems

Authors:

Gerald J. Popek,

David A. FarberAuthors Info & Claims

Communications of the ACM, Volume 21, Issue 9

Pages 737 - 749

https://doi.org/10.1145/359588.359597

Published: 01 September 1978 Publication History

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]

Chirica, L.M. Contributions to compiler correctness. Ph.D. Diss., Comptr. Sci. Dept., U. of California, Los Angeles, Sept. 1976.

Digital Library

[7]

Eckhouse, R. Minicomputer Systems: Organization and Programming (PDP-I1). Prentice-Hall, Englewood Cliffs, N.J., 1975.

Digital Library

[8]

Elspas, B. et al. An assessment of techniques for proving program correctness. A CM Computing Surveys 4, 2 (June 1972), 97-147.

Digital Library

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

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

Digital Library

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

London, R. An interactive program verification system. Proc. Int. Conf. Reliable Software, Los Angeles, Calif., May 1975, pp. 482-492.

Digital Library

[20]

Manna, Z. The correctness of programs. J. Comptr. Syst. Sci. 3, (1969), 119-127.

Digital Library

[21]

Millen, J.K. Security kernel validation in practice. Comm. ACM 10 5 (May 1976), 243-250.

Digital Library

[22]

Milner, R. An algebraic definition of simulation between programs. Memo AIM-142, Stanford AI Proj., Stanford U., Stanford, Calif., Feb. 1971.

Digital Library

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

Popek, G., and Kline, C. A verifiable protection system. Proc. Int. Conf. Reliable Software, Los Angeles, Calif., May 1975, pp. 294-304.

Digital Library

[26]

Popek, G., and Kline, C. Issues in kernel design. Proc. AFIPS 1978 NCC, AFIPS Press, Montvale, N.J., pp. 1079-1086.

Digital Library

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

Wegner, P. The Vienna definition language. A CM Computing Surveys 4, 1 (March 1972), pp. 5-63.

Digital Library

[30]

Wirth, N. The programming language Pascal. Acta Informatica 1 (1971), 35-63.

Digital Library

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

Cited By

Wang XWang H(2023)Cloud Computing Security Evaluation Based on Multidimensional Immune Algorithm (MIA)2023 3rd Asia-Pacific Conference on Communications Technology and Computer Science (ACCTCS)10.1109/ACCTCS58815.2023.00086(246-250)Online publication date: Feb-2023
https://doi.org/10.1109/ACCTCS58815.2023.00086
Popescu ALammich PHou P(2021)CoCon: A Conference Management System with Formally Verified Document ConfidentialityJournal of Automated Reasoning10.1007/s10817-020-09566-965:2(321-356)Online publication date: 1-Feb-2021
https://dl.acm.org/doi/10.1007/s10817-020-09566-9
Pomonis MPetsios TKeromytis APolychronakis MKemerlis V(2019)Kernel Protection Against Just-In-Time Code ReuseACM Transactions on Privacy and Security10.1145/327759222:1(1-28)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1145/3277592
Show More Cited By

Index Terms

A model for verification of data security in operating systems
1. Security and privacy
  1. Systems security
    1. Operating systems security
2. Social and professional topics
  1. Computing / technology policy
    1. Computer crime

Recommendations

A survey on security issues in IoT operating systems
Abstract
The security issues of the core (operating systems) of the Internet of Things (IoT) are becoming increasingly urgent and prominent, this article conducts a systematic research and summary of the security of the current mainstream IoT operating ...
Specification and verification of the UCLA Unix security kernel
Practical Security Systems with Smartcards
HOTOS '99: Proceedings of the The Seventh Workshop on Hot Topics in Operating Systems

Secure hardware is a useful tool for enhancing computer system security. Traditionally, researchers have attempted to build secure operating systems by creating secure hardware and developing on top of it. Our approach is to integrate commodity secure ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM

Communications of the ACM Volume 21, Issue 9

Sept. 1978

82 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/359588

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

Issue’s Table of Contents

Copyright © 1978 ACM.

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 September 1978

Published in CACM Volume 21, Issue 9

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

52
Total Citations
View Citations
1,511
Total Downloads

Downloads (Last 12 months)134
Downloads (Last 6 weeks)22

Reflects downloads up to 09 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang XWang H(2023)Cloud Computing Security Evaluation Based on Multidimensional Immune Algorithm (MIA)2023 3rd Asia-Pacific Conference on Communications Technology and Computer Science (ACCTCS)10.1109/ACCTCS58815.2023.00086(246-250)Online publication date: Feb-2023
https://doi.org/10.1109/ACCTCS58815.2023.00086
Popescu ALammich PHou P(2021)CoCon: A Conference Management System with Formally Verified Document ConfidentialityJournal of Automated Reasoning10.1007/s10817-020-09566-965:2(321-356)Online publication date: 1-Feb-2021
https://dl.acm.org/doi/10.1007/s10817-020-09566-9
Pomonis MPetsios TKeromytis APolychronakis MKemerlis V(2019)Kernel Protection Against Just-In-Time Code ReuseACM Transactions on Privacy and Security10.1145/327759222:1(1-28)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1145/3277592
Pomonis MPetsios TKeromytis APolychronakis MKemerlis V(2017)kR^XProceedings of the Twelfth European Conference on Computer Systems10.1145/3064176.3064216(420-436)Online publication date: 23-Apr-2017
https://dl.acm.org/doi/10.1145/3064176.3064216
Kanav SLammich PPopescu A(2014)A Conference Management System with Verified Document ConfidentialityProceedings of the 16th International Conference on Computer Aided Verification - Volume 855910.1007/978-3-319-08867-9_11(167-183)Online publication date: 18-Jul-2014
https://dl.acm.org/doi/10.1007/978-3-319-08867-9_11
Cao HZhang HYan FHuang B(2011)Formal analysis research for information flow of software2011 2nd International Conference on Control, Instrumentation and Automation (ICCIA)10.1109/ICCIAutom.2011.6183958(246-249)Online publication date: Dec-2011
https://doi.org/10.1109/ICCIAutom.2011.6183958
Kang EJackson DKohls C(2010)Patterns for building dependable systems with trusted basesProceedings of the 17th Conference on Pattern Languages of Programs10.1145/2493288.2493307(1-14)Online publication date: 16-Oct-2010
https://dl.acm.org/doi/10.1145/2493288.2493307
Kang EJackson D(2010)Dependability Arguments with Trusted BasesProceedings of the 2010 18th IEEE International Requirements Engineering Conference10.1109/RE.2010.38(262-271)Online publication date: 27-Sep-2010
https://dl.acm.org/doi/10.1109/RE.2010.38
Klein G(2009)Operating system verification—An overviewSadhana10.1007/s12046-009-0002-434:1(27-69)Online publication date: 16-Jul-2009
https://doi.org/10.1007/s12046-009-0002-4
Jaeger T(2008)Operating System SecuritySynthesis Lectures on Information Security, Privacy, and Trust10.2200/S00126ED1V01Y200808SPT0011:1(1-218)Online publication date: Jan-2008
https://doi.org/10.2200/S00126ED1V01Y200808SPT001
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents