This is a retrospective of computer security research and the process of building a secure operating system for the US government 1983-1990. The paper presents the case study of Kernelized Secure Operating System (KSOS), an A1 security-kernel operating system. KSOS was written to protect SCI/compartmented data (sometimes referred to as “above TOP SECRET”), and entered production. KSOS-11 ran on PDP-11, and KSOS-32 ran on DEC VaX. KSOS-11 ran in less than 64K bytes and was a fully functional OS including a security kernel, UNIX compatibility layer and first generation TCP/IP stack.
The design for KSOS was the first operating system design that was mathematically “proven correct” using formal specifications and computer based theorem provers.
The presentation also discusses the computing technology of the day - 16 bit computers, line editors, primitive (by current standards) compilers, theorem provers and how that affected development methods and what could be accomplished.
This presentation is a technical retrospective of computer security research during 1983- 1990 placed in its social and technical context. This presentation is being written especially for DEF CON’s 20th anniversary and has never been published before. The last paper published specifically on KSOS was at the 7th NBS Computer Security Conference in 1984.