Secure Unix ancestor KSOS did type safety before Rust made it cool

For the first time, the source code of KSOS, backed by the US Department of Defense in the late 1970s and 1980s, is available to the public in the archives of The Unix Heritage Society (TUHS). TUHS volunteers preserve the historical source code and documentation of the original UNIX – or as much of it as is left. A few days ago, in an email to its mailing list, TUHS founder Warren Toomey announced the addition of KSOS to the collection.

"KSOS was the US Department of Defense (DoD) Kernelized Secure Operating System (KSOS, formerly called Secure UNIX). KSOS is intended to provide a provably secure operating system for larger minicomputers," he wrote. Despite its age, KSOS sounds surprisingly modern.

It was a Unix-compatible OS, implemented in a type-safe programming language, Modula, rather than C. Modula was the late great Niklaus Wirth's successor to Pascal and, in turn, the forerunner to Modula-2 – which we described when it was added to the GNU Compiler Collection in 2022. KSOS was designed to be formally verifiable, so that it could be trusted for use in highly secure systems.

It ran on commodity hardware, and its development was sponsored by the US DOD. Very few OS kernels have been formally verified, and one of the best-known modern examples is the seL4 microkernel, as used in the Ironclad OS we covered last year, and also in the new QSOE RISC-V RTOS. KSOS isn't some cutting-edge experimental new Rust effort, like the Asterinas project we described last year or the even newer Maestro project.

What became KSOS started in 1978 at Ford Aerospace (yes, that Ford). On the team were Peter Neumann, who later ran the RISKS Digest – The Register was quoting him in 2004 – and Tom Perrine, who described it and its modern relevance in a 2002 article for the USENIX journal ;login:. It's titled "The Kernelized Secure Operating system (KSOS)" [PDF], and at only three and a bit pages long, it's well worth a read.

Even then, 24 years ago, projects were struggling to reinvent t