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

  • J. M. Rushby
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 137)


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.


Total Function Covert Channel Verification Technique Storage Channel Separation Kernel 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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. [2]
    Anderson, J.P., "Computer Security Technology Planning Study", ESD-TR-73-51 (October 1972). (Two volumes).Google Scholar
  3. [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. [4]
    Barnes, D., "Computer Security in the RSRE PPSN", Networks 80, pp.605–620, Online Conferences (1980).Google Scholar
  5. [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. [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. [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. [8]
    Feiertag, R.J., "A Technique for Proving Specifications are Multilevel Secure", CSL-109, SRI International, Menlo Park, CA. (January 1980).Google Scholar
  9. [9]
    "KSOS Verification Plan", WDL-TR7809, Ford Aerospace and Communications Corporation, Palo Alto, CA. (March 1978).Google Scholar
  10. [10]
    Goguen, J.A. and J. Meseuger, "Security Policies and Security Models", Internal Report, SRI International, Menlo Park, CA. (December 1981).Google Scholar
  11. [11]
    Gold, B.D. et al., "A Security Retrofit of VM/370", AFIPS Conference Proceedings Vol. 48, pp.335–344 (1979).Google Scholar
  12. [12]
    Hathaway, A., "LSI Guard System Specification (type A)", Draft, Mitre Corporation, Bedford, MA. (July 1980).Google Scholar
  13. [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. [14]
    Lampson, B.W., "A Note on the Confinement Problem", CACM Vol. 16(10), pp.613–615 (October 1973).Google Scholar
  15. [15]
    Linde, R.R., "Operating System Penetration", AFIPS Conference Proceedings Vol. 44, pp.361–368 (1975).Google Scholar
  16. [16]
    Millen, J.K., "Security Kernel Validation in Practice", CACM Vol. 19(5), pp.243–250 (May 1976).Google Scholar
  17. [17]
    Nibaldi, G.H., "Proposed Technical Evaluation Criteria for Trusted Computer Systems", M79-225, Mitre Corporation, Bedford, MA. (1979).Google Scholar
  18. [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. [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. [20]
    Rushby, J.M., "Verification of Secure Systems", Technical Report No. 166, Computing Laboratory, University of Newcastle upon Tyne (September 1981).Google Scholar
  21. [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. [22]
    Woodward, J.P.L., "Applications for Multilevel Secure Operating Systems", AFIPS Conference Proceedings Vol. 48, pp.319–328 (1979).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1982

Authors and Affiliations

  • J. M. Rushby
    • 1
  1. 1.Computing LaboratoryUniversity of Newcastle upon TyneNewcastle upon TyneEngland

Personalised recommendations