Verification of Secure Systems
John Rushby
Technical Report 166, Computing Laboratory, Newcastle University, UK;
August 1981
Abstract
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.
Files
Newcastle University recently recovered this paper. Beware that it is a
scan and 50MB in size: scanned PDF
BibTeX Entry
@techreport{Rushby81b,
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