Design and Verification of Secure Systems

John Rushby

8th ACM Symposium on Operating System Principles (SOSP), Pacific Grove, California. December, 1981. Appears in ACM Operating Systems Review, Volume 15, Number 5, pp 12-21.

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

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

BibTeX Entry

@inproceedings{Rushby81:SOSP,
	AUTHOR = {John Rushby},
	TITLE = {The Design and Verification of Secure Systems},
	BOOKTITLE = {Eighth ACM Symposium on Operating System Principles ({SOSP})},
	ADDRESS = {Asilomar, CA},
	MONTH = dec,
	YEAR = 1981,
	PAGES = {12--21},
	NOTE = {(ACM {\em Operating Systems Review\/}, Vol.\ 15, No.\ 5)}
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page