Appears in ACM Operating Systems Review, Volume 15, Number 5.
From Reprint of a paper presented at the 8th ACM Symposium on Operating System Principles.
Pacific Grove, California.
December, 1981.
Pages 12–21.

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

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.

@inproceedings{sosp81,
    AUTHOR = {John Rushby},
    TITLE = {Design and Verification of Secure Systems},
    BOOKTITLE = {Reprint of a paper presented at the 8th {ACM} Symposium on Operating System Principles},
    YEAR = {1981},
    VOLUME = {15},
    NUMBER = {5},
    PAGES = {12-21},
    ADDRESS = {Pacific Grove, California},
    MONTH = {dec},
    URL = {http://www.csl.sri.com/papers/sosp81/},
    JOURNAL = {{ACM} Operating Systems Review}
}

• sosp81.dvi.gz
• sosp81.pdf
• sosp81.ps