logoalt Hacker News

ryanshrotttoday at 3:23 PM0 repliesview on HN

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.