Source: The Register
Article note: Neat! It's amazing how many "Still chasing the same dream 50 years later" things there are in computing, and how little attention people pay to the previous attempts.
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 things KSOS did successfully a couple of decades earlier. That's even more true today. To learn more about how KSOS worked, there's a 1978 Executive Summary [PDF] – which, despite its title, runs to 15 pages. Clearly, executives back then had longer attention spans. Perrine gave a talk about KSOS at DEF CON 20 in 2012, which you can watch on YouTube. KSOS isn't forgotten. For instance, it came up in a talk at last year's FOSDEM: Confidential Computing's Recent Past, Emerging Present, and Long-Lasting Future. Page 8 of the slide deck [PDF] says KSOS was "among the first security-focused kernels, emphasizing formal verification" and "source code was publicly available, rejecting 'security through obscurity.'" KSOS was not confined to academic research. It was used in production. Last October, Perrine explained more in another TUHS email: "KSOS – for PDP-11, originally developed by Ford Aerospace, and then extended at Logicon. It did have a supervisor-mode UNIX-system-call-compatible system. Later, there was also a userland library that implemented something that mostly matched the UNIX system calls. It had no kernel code in common with UNIX. It was written in Modula. "KSOS was used in the Trusted Downgrade System of the multi-level-secure 'all-source' intel fusion system that Logicon built for a few agencies. ACCAT-GUARD and USAFE-GUARD, for example. "KSOS-32 – a VAX 'port' of KSOS (which was then retconned as 'KSOS-11'). The Modula code from -11 was run though Emacs macros to produce Modula-2, and then parts were rewritten as needed. "I worked on both systems at Logicon." It's Perrine we have to thank for KSOS reappearing in public view after 38 years – he found an old tarball of the source code, and with the help of John O Goyo and Thalia Archibald, it made its way to the TUHS code archive. Now there’s a new quest: find the original compiler used to build it. One thing that may help slightly is that KSOS was not self-hosting: it was compiled under UNIX. We have mentioned TUHS's important work before: for instance, when a tape of UNIX V4 was found in University of Utah boffin Robert Ricci's department — and successfully recovered. Bootnote Mr Goyo also found time to email The Reg FOSS desk about the recovery, for which we thank him. ®
