Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!rutgers!apple!well!nagle
From: nagle@well.UUCP (John Nagle)
Newsgroups: comp.unix.wizards
Subject: Re: Getting rid of the root account
Message-ID: <12653@well.UUCP>
Date: 11 Jul 89 18:47:21 GMT
References: <127@orchid.warwick.ac.uk> <16659@rpp386.Dallas.TX.US> <16662@rpp386.Dallas.TX.US> <4554@ficc.uu.net>
Reply-To: nagle@well.UUCP (John Nagle)
Lines: 40

In article <4554@ficc.uu.net> peter@ficc.uu.net (Peter da Silva) writes:
>Security and convenience are diametrically opposed goals.
>
>In any real system that's open enough to get any actual work done, there
>will be holes. No matter how many people work though the code in an attempt
>to verify it... an operating system is far more complicated than any
>mathematical proof, for example, and look at the work necessary to validate
>one of those.

     Sadly, this remains true.  As one of the few people ever to build a
working verification system, (see my paper in POPL '83), I have to agree
with this.  Only machine verifications are worth anything; hand proofs of
even tiny programs tend to contain errors, usually in the direction that
makes bad proofs succeed.  Still, in 1983, we were up to programs of a few
hundred lines, proven to obey all their assertions and invariants and not
to violate any subrange, array bound, or machine overflow constraint.
Don Good's work at the University of Texas continues, and they are steadily
advancing what can be proven correct.

     Unfortunately, a secure operating system doesn't look anything like
UNIX internally.  You want a much smaller system.  The vocabulary of things
that a user application can ask of the operating system is much too large.
Every system call has potential holes, and the semantics of many system
calls, especially those which alter the execution environment, are very
hard to model formally.  "Mount", as pointed out above, is especially messy.
    
     A good argument can be made that trust and user programmability 
should never meet in the same CPU.  The notion of a secure file server 
is in many ways more promising than the notion of a secure operating system.

>So all you get for your effort is a warm fuzzy feeling that your system
>is secure. If you really want security, lock the terminal and computer up
>in a faraday cage, and don't let anything in or out except well filtered
>line current.

     That's how high-level systems are still secured today.  Solid steel, 
line power filters, airlocks with RF-tight gaskets, and several levels
of physical security to keep anybody from getting close.

					John Nagle