The Provably Secure Operating System (PSOS) project began in 1973 and continued until 1983. The 1980 PSOS final report includes the system architecture and many of the basic hardware and operating system layers, plus some illustrative applications (all formal specified in the SPECIAL language of HDM, the Hierarchical Development Methodology). The Feiertag/Neumann paper summarizing the architecture as of 1979 is available in a retyped, more or less correct, hand-edited pdf form. A 2003 paper, PSOS Revisited by me and Rich Feiertag, was presented at ACSAC 2003 in Las Vegas in December 2003, as part of the Classic Papers track (which was initiated at ACSAC 2002 for the Karger-Schell paper on the Multics multilevel secure evaluation). Please read it if you are interested in capability architectures. The PSOS project continued from 1980 to 1983, supporting the Goguen-Meseguer papers and the Extended HDM effort that led to SRI’s PVS system.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?