Unix (In)Security

[jbn at wdl1.UUCP]

      One of the attempts to implement a secure kernel for UNIX was the
Kernalized Secure Operating System developed at Ford Aerospace from 1978
to 1980.  This was to be a very tight system; the entire system was designed
and specified in a formal specification language (SPECIAL) and attempts
were made to prove that the system interface did not contain any design
errors that could be exploited; the proof attempt was subcontracted to
SRI International and used a program which took in the interface
specification, applied the Bell-LaPadua security model, and generated
theorems to be proved with the Boyer-Moore theorem prover.  This was
interesting but not too useful in practice.
      The security model was DoD-oriented; the system had classification
levels for files, and stringent rules about access.  For example, programs
were not only forbidden to read data at a higher security level than the
one they were running at; they could not write a file at a lower security
level.  This prevents Trojan Horse programs from giving data away.
      The kernel itself did not emulate UNIX; there was a UNIX emulator
that ran on top of the kernel that did this.  The kernel supported only
block-oriented files and had a flat directory structure, for simplicity;
the UNIX file system semantics were simulated in the emulator.
      The entire kernel was coded in Modula I.  There were no pointers,
everything was done with subscripted tables.  It ran on a PDP 11/70,
worked reasonably well, but was much slower than PWB/Unix on the
same hardware.  The real problem was that the kernel wouldn't fit in
64K until we took out all the speed optimizations to make it fit;
schemes to support a larger kernel by using the memory management hardware
were considered and rejected as possibly leading to security bugs.  This
problem combined with a serious performance problem caused by the
emulator approach led to a very slow system; overall UNIX performance
was about 25% of PWB/UNIX.
      It is still used at Logicon as a base for a special-purpose
application, but the UNIX emulator is not used; only the kernel remains.
      In retrospect, had the system been implemented on a machine without
the PDP-11s address space restriction, it probably would have been much
more successful, although it inherently would have run at about half the
speed of a UNIX on the same hardware.  But for many DoD applications this
would have been quite acceptable.
      There were a number of useful results.  One is that it was demonstrated
that it is possible to write an operating system in a very restrictive 
language without overriding the type system.  (Modula I did not have ANY
way to get around strong typing.)  There were about 900 lines of assembler
in the system, almost all of which were present strictly to handle memory
management and domain crossing.  All the device drivers and the file system
were 100% Modula I.  This was at times painful, but debugging was very easy.
Once everything compiled, it tended to run.  And when it didn't, finding the
problem was usually trivial.  But getting everything to compile (in one giant
compile for the kernel) could take days; the compilations themselves took
20 minutes each.
      Another was that the specification/verification approach needed a lot
of work to be usable.  Don Good's group at the University of Texas has
advanced the state of the art much further than SRI ever did in this
area (despite much hype from SRI at the time).  It is now possible to
build small, secure, real-time programs, using the Gypsy language and
its verification system developed at U. Texas.
      I myself designed and implemented the file system and all I/O for
KSOS.  It was an interesting two years.  Many of the people on the project
went off to found Sytek, Inc, which went on to develop the local area net
for the IBM PC.  
      Some of the people who worked on the project were

		Mike Pliner
		Jay McCauley
		Rance DeLong
		Dan Ladermann
		Mark Gang
		Thomas Berson
		Luke Dion
		Norm Abromowitz
		Ken Biba
		Pat Carruthers
		
		
					John Nagle
					Ford Aerospace and Communcations Corp.