Proof of Separability---A Verification Technique for a Class of Security Kernels

John Rushby

Proceedings of the 5th International Symposium on Programming, Springer Verlag LNCS Vol. 137, pp. 352--367, Turin, Italy, 1982

Abstract

A formal model of "secure isolation" between the users of a shared computer system is presented. It is then developed into a security verification technique called "Proof of Separability" whose basis is to prove that the behaviour perceived by each user of the shared system is indistinguishable from that which could be provided by an unshared machine dedicated to his private use.

Proof of Separability is suitable for the verification of security kernels which enforce the policy of isolation; it explicitly addresses issues relating to the interpretation of instructions and the flow of control (including interrupts) which have been ignored by previous treatments.

Note: this version was scanned in from a printed copy and the files are large.

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

BibTeX Entry

@inproceedings{Rushby82,
	AUTHOR = {John Rushby},
	TITLE = {{Proof of Separability---A} Verification Technique for
		a Class of Security Kernels},
	MONTH = apr,
	YEAR = 1982,
	BOOKTITLE = {Proc.\ 5th International Symposium on Programming},
	ADDRESS = {Turin, Italy},
	PAGES = {352--367},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 137,
	EDITORS = {M. Dezani-Cianaglini and U. Montanari}
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page