Skip to main content
SpringerLink
Log in

Proof of separability A verification technique for a class of security kernels

  • Conference paper
  • First Online:
International Symposium on Programming (Programming 1982)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 137))

Included in the following conference series:

Abstract

A formal model of ‘secure isolation’ between the users of a shared computer system is presented. It is then developed into a security verification technique called ‘Proof of Separability’ whose basis is to prove that the behaviour perceived by each user of the shared system is indistinguishable from that which could be provided by an unshared machine dedicated to his private use.

Proof of Separability is suitable for the verification of security kernels which enforce the policy of isolation; it explicitly addresses issues relating to the interpretation of instructions and the flow of control (including interrupts) which have been ignored by previous treatments.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Ames, S.R. Jr., "Security Kernels: Are they the Answer to the Computer Security Problem?", Presented at the 1979 WESCON Professional Program, San Francisco, CA. (September 1979).

    Google Scholar 

  2. Anderson, J.P., "Computer Security Technology Planning Study", ESD-TR-73-51 (October 1972). (Two volumes).

    Google Scholar 

  3. Attanasio, C.R., P.W. Markstein, and R.J. Phillips, "Penetrating an Operating System: a Study of VM/370 Integrity", IBM Systems Journal Vol. 15(1), pp.102–116 (1976).

    Google Scholar 

  4. Barnes, D., "Computer Security in the RSRE PPSN", Networks 80, pp.605–620, Online Conferences (1980).

    Google Scholar 

  5. Berson, T.A. and G.L. Barksdale Jr., "KSOS — Development Methodology for a Secure Operating System", AFIPS Conference Proceedings Vol. 48, pp.365–371 (1979).

    Google Scholar 

  6. Cristian, F., "Robust Data Types", Technical Report 170, Computing Laboratory, University of Newcastle upon Tyne, England (1981). (To appear in Acta Informatica).

    Google Scholar 

  7. Feiertag, R.J., K.N. Levitt, and L. Robinson, "Proving Multilevel Security of a System Design", Proceedings of the Sixth ACM Symposium on Operating System Principles, pp.57–65 (1977).

    Google Scholar 

  8. Feiertag, R.J., "A Technique for Proving Specifications are Multilevel Secure", CSL-109, SRI International, Menlo Park, CA. (January 1980).

    Google Scholar 

  9. "KSOS Verification Plan", WDL-TR7809, Ford Aerospace and Communications Corporation, Palo Alto, CA. (March 1978).

    Google Scholar 

  10. Goguen, J.A. and J. Meseuger, "Security Policies and Security Models", Internal Report, SRI International, Menlo Park, CA. (December 1981).

    Google Scholar 

  11. Gold, B.D. et al., "A Security Retrofit of VM/370", AFIPS Conference Proceedings Vol. 48, pp.335–344 (1979).

    Google Scholar 

  12. Hathaway, A., "LSI Guard System Specification (type A)", Draft, Mitre Corporation, Bedford, MA. (July 1980).

    Google Scholar 

  13. Hebbard, B. et al., "A Penetration Analysis of the Michigan Terminal System", ACM Operating Systems Review Vol. 14(1), pp.7–20 (January 1980).

    Google Scholar 

  14. Lampson, B.W., "A Note on the Confinement Problem", CACM Vol. 16(10), pp.613–615 (October 1973).

    Google Scholar 

  15. Linde, R.R., "Operating System Penetration", AFIPS Conference Proceedings Vol. 44, pp.361–368 (1975).

    Google Scholar 

  16. Millen, J.K., "Security Kernel Validation in Practice", CACM Vol. 19(5), pp.243–250 (May 1976).

    Google Scholar 

  17. Nibaldi, G.H., "Proposed Technical Evaluation Criteria for Trusted Computer Systems", M79-225, Mitre Corporation, Bedford, MA. (1979).

    Google Scholar 

  18. Popek, G.J. and D.A. Farber, "A Model for Verification of Data Security in Operating Systems", CACM Vol. 21(9), pp.737–749 (September 1978).

    Google Scholar 

  19. Rushby, J.M., "The Design and Verification of Secure Systems", Proceedings of the 8th ACM Symposium on Operating System Principles, Asilomar, CA., pp.12–21 (December 1981).

    Google Scholar 

  20. Rushby, J.M., "Verification of Secure Systems", Technical Report No. 166, Computing Laboratory, University of Newcastle upon Tyne (September 1981).

    Google Scholar 

  21. Wilkinson, A.L. et al., "A Penetration Study of a Burroughs Large System", ACM Operating Systems Review Vol. 15(1), pp.14–25 (January 1981).

    Google Scholar 

  22. Woodward, J.P.L., "Applications for Multilevel Secure Operating Systems", AFIPS Conference Proceedings Vol. 48, pp.319–328 (1979).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Newcastle upon Tyne, NE1 7RU, Newcastle upon Tyne, England

    J. M. Rushby

Authors
  1. J. M. Rushby
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mariangiola Dezani-Ciancaglini Ugo Montanari

Rights and permissions

Reprints and permissions

Copyright information

© 1982 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rushby, J.M. (1982). Proof of separability A verification technique for a class of security kernels. In: Dezani-Ciancaglini, M., Montanari, U. (eds) International Symposium on Programming. Programming 1982. Lecture Notes in Computer Science, vol 137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11494-7_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-11494-7_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-11494-9

  • Online ISBN: 978-3-540-39184-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation