Unix (In)Security

[smk at axiom.UUCP]

KVM was an attempt at a secure kernel implementation of VM.  It got
farther than most secure OS projects.

You can't formally prove any complex system.  There is too much handwaving
in showing the formal specs/model really meet your requirements and the
design meets the specs.  With that much handwaving, you can have the perfect
spec and a design that implements something completely different.  Nothing
short of formal ties between the stages will satisfy me (not to mention the
proofs of correctness for the compiler/assembler/translator, the machine
instruction set itself -- as anyone working on a braindamaged micro can attest
to).
-- 
	--steve kramer
	{allegra,genrad,ihnp4,utzoo,philabs,uw-beaver}!linus!axiom!smk	(UUCP)
	linus!axiom!smk at mitre-bedford					(MIL)