The foundations of a provably secure operating system (PSOS) (1979) [pdf]

PSOS. Now that was something I never expected to see again.

I'd worked on the previous system, KSOS, mentioned in the article. I wrote the file system and all of the drivers, while at an aerospace company. We'd used formal specifications in SPECIAL. Nobody could prove anything about SPECIAL yet, but I wrote a compiler-like syntax and type checker, so it was at least type valid. It was a good language for writing down invariants. I used it to describe file system consistency and recovery. Another group started work on PSOS, but never got past the design stage. I managed to avoid getting sucked into that, because it looked like a death march.

SRI, which was a think tank, just did abstract designs. It was extreme waterfall. One group wrote a spec, and a contractor implemented it. This did not work too well. They did have Boyer and Moore, and those two made real progress on proof systems. I used their prover for another project, and talked to them a lot. But they were not closely associated with PSOS. Specifications in SPECIAL, which is quantifier-oriented were not compatible with Boyer-Moore theory, which uses constructive mathematics and recursive functions.

The big problem in that era was that the hardware wasn't ready for secure operating systems. KSOS was for the 16-bit PDP-11 line, and it took a cram job to make it fit. The Modula I compiler wasn't very space-efficient. Optimizations had to come out to make it fit, and the result was too slow.

Microprocessors weren't quite ready yet. Neither Intel nor Motorola had a decent MMU. The suitable target machines were all minicomputers, which were on the way out. PSOS never got far enough to pick an implementation target.

Capability-based systems work, but they create a new problem - ticket management. You have lots of tickets which let some piece of software do something, and now you have to track and manage them. It's like physical key control. It's the same reason that Windows access control lists are little used. You also still have the delegation problem - A can't do X, but A can talk to B, which can do X. Most modern attacks involve that approach.

Most of the early secure OS work was funded by NSA. NSA had an internal division in those Cold War days - the important stuff was at Fort Meade, and the less-important stuff was some distance away at FANX, an annex out by Friendship (now BWI) Airport. FANX had personnel ("HR" today), training (including the cryptographic school), safe and lock testing and evaluation, networking, and computer security. Being exiled to FANX was bad for careers. This set back the computer security work.

There was also industry pushback. The operating system testing criteria were borrowed from the safe and lock people. Something submitted for testing got two tries. First try, the evaluators told the vendor what was wrong. Second try was pass/fail with no feedback. That's how locks for vaults were evaluated. Computer vendors (there was not much of a separate OS industry yet) hated this. They eventually got a testing system where "certified labs" did the testing, and a vendor could have as many tries as they were willing to pay for.

Some good secure OSs came out of that, and passed testing. But they were obscure, and for obscure hardware - Prime, Honeywell, etc. If you dig, you can find the approved products list from the 1980s.

What really killed all that was the growth of the computer industry. In the 1960s and 1970s, the government was the biggest purchaser of computers and electronics. As the industry grew, the government became a minor purchaser with a slow update cycle, and could not get design-level attention from major vendors. There was much grumbling about this from military people, especially the USAF, as they were sidelined during the 1980s.

I understand why in 1979 and perhaps until mid 1990s capability OS architecture might have been irrelevant and excessive. But after that, it sounds like the only architecture suitable for the internet age, where you can download and run anything from anywhere. Instead, we're stuck with legacy systems, which now contain layers of layers of abstractions and security measures. User rights, anti-virus software, vetting (signatures, hashes, app-store verification) - all become obsolete or near-obsolete in a capability-based system where a program simply doesn't have access to anything by default. Part of the appeal of virtualization is also due to the fact that it isolates programs (for instance, I only run npm inside Docker container these days, because chances are some package will contain malware at some point).

Part of it is inertia, but part of it is ignorance. Enthusiasts spend tons of money and effort building another GPU enabled terminal or safe programming languages - and maybe that's fine, but I wonder what we could've accomplished if people were simply aware what a well-designed capability OS could be like, because this is literally the only OS paradigm in existence (that I know of) that's even worth any serious effort.

PSOS's capability-based architecture was way ahead of its time. The core idea, tag memory with unforgeable access tokens at the hardware level instead of leaning on software-defined access control lists, is finally getting real implementation, forty-plus years later. seL4 is the obvious modern inheritor. It’s a formally verified microkernel where capabilities are the basic access primitive. The seL4 team proved, in Isabelle/HOL, that the kernel's C implementation matches its formal specification exactly, no buffer overflows, no null pointer derefs, no privilege escalation. That’s the PSOS vision, actually built. CHERI, out of Cambridge and SRI, and a bit ironically building on the same institution's heritage, pushes the idea into hardware: 128-bit fat pointers with encoded bounds and permissions, enforced at the CPU level. ARM's Morello prototype showed this in silicon. A CHERI-extended CPU literally can’t forge a pointer outside its authorized memory region, the hardware traps it. The frustrating part is Miagg's point, we had the blueprint in 1979. What killed capability systems wasn’t technical, it was the Unix monoculture and the network effect of "good enough" security. Now we’re slowly rediscovering capabilities under names like "object capabilities" and "hardware enclaves." Better late than never, tbh, but it’s hard not to wonder what the internet would look like if PSOS's architecture had won.

The difference between ambient authority systems, like Windows and Linux, and capability systems is the difference between a program that only uses global variables and a program that uses local variables and function parameters.

In a capability system, you pass resource capabilitys to subsystems. You can not use resource handles that were not passed to you just like a function can not access variables that were not passed to it (except for explicit global variables.

In ambient authority systems, as a common example, you can just blindly convert what are effectively strings into resource handles (the metaphorical equivalent of casting integers to raw pointers). Your access is mediated by a orthogonal system that tells you which resource handles/pointers you are allowed to use. That is like having a program that runtime checks every pointer access is allowed instead of just preventing you from manufacturing pointers.

You coordinate across subsystems by naming certain resources in the global ambient space in a coordinated fashion (effectively a global variable which is basically just a named memory location in the common memory space). That way the subsystem knows the global you put their parameters/resources in.

While you can still program like that, everybody now knows it is a terrible way to live. Parameter passing and local variables with explicit global variables is almost always the way to go. That same lesson should be learned for operating systems.

The foundations of corporate-authoritarian dystopia.

I don't think the authors had that in mind when they wrote this, but to look back at and imagine a future where such things had taken hold is truly scary.

"The road to hell is paved with good intentions."

I would honestly like to understand why Miagg's comment has been flagged.

If you are interested in this I highly recommend studying SeL4. A practical industrial proven correct micro kernel used by billions of devices worldwide.

My modern take on (un)secure operating system for the future : https://news.ycombinator.com/item?id=48167846

Rebuild everything from scratch, with AI agents. Then make them prove what they wrote.