Verification of Secure Systems

John Rushby

Technical Report 166, Computing Laboratory, Newcastle University, UK; August 1981


This report surveys techniques for verifying security kernels. It begins with a tutorial description of two established methods for performing this task: these are `access control verification' and `verification by information flow analysis.' Both of these techniques are shown to be inadequate, on their own, to the task of verifying the security of a toy kernel which enforces a policy of isolation. A new method of verification by `proof of separability' is proposed which deals with this problem quite simply and naturally: the basic idea is to prove that, to each of its users, the behaviour of the shared system is indistinguishable from that of an idealised (and manifestly secure) system which supports that user alone.

The application of this idea is then extended to more complex security policies and systems and is shown to lead to a clearer understanding of the role of a security kernel and of its relationship to `trusted processes' and other security critical software within the system.

It is argued that the advantages of the verification and structuring techniques introduced here are such that they should substantially replace those usedin current practice.


 *NEW* Newcastle University recently recovered this paper. Beware that it is a scan and 50MB in size: scanned PDF

BibTeX Entry

	AUTHOR = {John Rushby},
	INSTITUTION = {Computing Laboratory, University of Newcastle
		upon Tyne},
	TITLE = {Verification of Secure Systems},
	YEAR = 1981,
	MONTH = aug,
	ADDRESS = {Newcastle upon Tyne, UK},
	NUMBER = 166

Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page