Design and verification of secure systems
- 1 December 1981
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGOPS Operating Systems Review
- Vol. 15 (5), 12-21
- https://doi.org/10.1145/1067627.806586
Abstract
This paper reviews some of the difficulties that arise in the verification of kernelized secure systems and suggests new techniques for their resolution. It is proposed that secure systems should be conceived as distributed systems in which security is achieved partly through the physical separation of its individual components and partly through the mediation of trusted functions performed within some of those components. The purpose of a security kernel is simply to allow such a 'distributed' system to actually run within a single processor; policy enforcement is not the concern of a security kernel. This approach decouples verification of components which perform trusted functions from verification of the security kernel. This latter task may be accomplished by a new verification technique called 'proof of separability' which explicitly addresses the security relevant aspects of interrupt handling and other issues ignored by present methods.Keywords
This publication has 15 references indexed in Scilit:
- Specification and verification of the UCLA Unix security kernelCommunications of the ACM, 1980
- A model for verification of data security in operating systemsCommunications of the ACM, 1978
- Issues in kernel designPublished by Springer Science and Business Media LLC ,1978
- Certification of programs for secure information flowCommunications of the ACM, 1977
- Proving multilevel security of a system designPublished by Association for Computing Machinery (ACM) ,1977
- Security Kernel validation in practiceCommunications of the ACM, 1976
- A comment on the confinement problemPublished by Association for Computing Machinery (ACM) ,1975
- A verifiable protection systemPublished by Association for Computing Machinery (ACM) ,1975
- A note on the confinement problemCommunications of the ACM, 1973
- Proof of correctness of data representationsActa Informatica, 1972