Daily Archives: 2026-07-06

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

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. ®

Posted in News | Leave a comment

Zombie ‘who owns Unix?’ lawsuit comes alive again

Source: The Register

Article note: What year is it? They had most of their claims dismissed, lost on standing, lost on merits, lost their parallel case with Novell, have been sold twice, but are apparently still trying to troll. 23 years later. The (notional) roots are Project Monterey, which was a 90s/early 2000s unified UNIX project that was doomed from the start, flopped, and was caught up in the Itanium failbus.

The ancient dispute over ownership of UNIX, and perhaps Linux too, has returned to court. Again. As The Register has explained many, many, times since this matter first went to court in 2003, the roots of the case are the 1998 alliance between IBM and a company called the Santa Cruz Operation which sold a version of UNIX for x86 CPUs. Those two companies, plus Intel and Sequent, created “Project Monterey” – an effort to create a unified version of UNIX that could run on multiple processors. By 2001, Project Monterey was close to delivering a unified UNIX, an achievement made possible by blending code from IBM and SCO. By then, a little project called “Linux” already ran on multiple processors. Big Blue decided Linux was the future and bailed from Project Monterey – then allegedly contributed some Monterey code to the open-source project and to its own AIX and Z operating systems. SCO felt it owned some of that code, so sued IBM. SCO and its successors struggled to survive, but interested parties kept the lawsuit alive because the chance to emerge as owner of parts of the Linux codebase, and IBM’s code, had the potential to turn into a colossal payday. The case and its successors ended in 2021, with a settlement that saw litigants agree to end the matter without IBM admitting fault. But by then, SCO had sold its software to a biz called Xinuos that decided to fight on. The Xinuos case has burbled along quietly since, and on June 22nd reached the milestone of a hearing. The matter has become a little more modern, if only because this hearing was held online and the presiding judge appeared to unwittingly be on mute at one point. But the arguments otherwise seemed to revisit Project Monterey, debated the relevance of past litigation, contested who owned what, when they owned it, and how they could prove it. Xinuos argued IBM never had a license for SCO code. Big Blue argued that it did nothing wrong. The core issue seems to be whether Xinuos even has the right to litigate the matter, or if some ancient legalese in the original agreements means the window for legal argument has long since expired. The matter continues and appears likely to do so until either the heat death of the universe or the year of Linux on the desktop – whichever comes sooner. ®

Posted in News | Leave a comment