Source Code for KSOS, a DoD-Backed Secure Unix Ancestor, Now Publicly Available
The source code for KSOS, a secure Unix-like operating system developed in the late 1970s and 1980s with US Department of Defense backing, has been released by The Unix Heritage Society.
The source code for KSOS, a secure Unix-like operating system developed in the late 1970s and 1980s with US Department of Defense backing, is now publicly available for the first time. Preserved and released by volunteers at The Unix Heritage Society (TUHS), KSOS represents an early and significant effort in building provably secure operating systems.
Originally known as Secure UNIX and later as the Kernelized Secure Operating System (KSOS), the project was sponsored by the US Department of Defense (DoD) with the goal of providing a secure OS for larger minicomputers. Despite its age, KSOS incorporated modern security principles. Notably, it was implemented in Modula, a type-safe programming language created by Niklaus Wirth, predating the widespread adoption of languages like Rust for secure systems development. This choice, along with a design focused on formal verification, aimed to ensure a high level of trust and security.
The development of KSOS began in 1978 at Ford Aerospace, with key figures like Peter Neumann and Tom Perrine involved. Perrine, who later described KSOS's relevance in a 2002 USENIX journal article, highlighted that even decades ago, the project was successfully implementing concepts that other systems were still struggling to develop. The system was designed to be formally verifiable, a rigorous process to mathematically prove its correctness and security properties, a feature rarely achieved even in modern operating systems.
KSOS was not merely an academic exercise; it saw production use. Tom Perrine detailed in a recent TUHS email that KSOS was utilized in the Trusted Downgrade System, part of a multi-level-secure intelligence fusion system developed by Logicon for various US agencies, including ACCAT-GUARD and USAFE-GUARD. A VAX port, known as KSOS-32, was also developed, with its Modula code adapted to Modula-2.
The public release was facilitated by Tom Perrine, who discovered an old tarball of the source code. With assistance from John O Goyo and Thalia Archibald, the code was successfully added to the TUHS archive, making it accessible to researchers and historians. The TUHS has a track record of preserving vital historical computing artifacts, including past recoveries of early UNIX tapes.
While the source code is now available, a new challenge has emerged: finding the original compiler used to build KSOS. It's noted that KSOS was not self-hosting, meaning it was compiled on a separate UNIX system, a detail that might aid in its reconstruction or analysis.
KSOS's legacy is recognized in contemporary discussions about secure computing. It was mentioned in a recent FOSDEM talk on Confidential Computing, where it was cited as one of the first security-focused kernels that emphasized formal verification and rejected "security through obscurity" by making its source code publicly available.
The availability of KSOS's source code offers a valuable glimpse into the early history of secure operating system design, demonstrating that advanced concepts in type safety and formal verification were being explored and implemented decades before they became mainstream in modern cybersecurity practices.