[RetroTechie]

Capabilities-based OSes aren't magic. Their robustness still depends on underlying assumptions, which may or may not hold. See eg relevant disclaimers in seL4 whitepaper(s).

And hardware glitches are a thing (edit: and supply chain attacks).

But I do agree that verified correct software can offer very strong guarantees that go well beyond those of commonly deployed software. We could have been in a much better place today.

[saidnooneever]

their robustness lives in hardware capabilities. amd64 and intel x86_64 have quite good features but people dont use them well. For example you can have your microkernel be at the hypervisor level and thoroughly isolate devices etc through IOMMU and have almost no attack surface to get access deep enough to make significant changes to the security posture.

still not immune to be hacked ofc. I think the last step would be making it common place again to build these things custom. that way they'd have to have more specific information available as threat actors to exploit you. It'd be harder to have generic methods affecting millions of systems.

regardless there are no silverbullets, and tradecraft/opsec will always be a thing. most compromises are because people hand out keys unwittingly rather than 0days and crazy sploits. (they do happen though, but its more expensive than fishing and just loggin on under some dudes credentials)

[RetroTechie]

To clarify: capabilities-based OS != verified correct software.

But there's much synergy there. Each enhances the other.