[Zigurd]

It's either verifiably secure or it isn't, and that makes an enormous difference. Also, the issue of hardware bugs purports to be addressed by verifiably secure CPU designs.

Of course that leaves the multitude of programmable peripheral devices. But starting with hardware and software that are implemented to be provably secure is a big change. It is table stakes for systems to be vastly harder to penetrate.

[jtgans]

Absolutely, and this is specifically why I chose to start with seL4 and use Rust for the userland we built. seL4 has a verification framework already in place, so we can use it to ensure our system design and implementation is good. We've spent this time working with the seL4 guys to find a good middle ground in these changes, and we're going to see about verifying the design as we go, but we wanted to get these things out sooner rather than waiting because it affords more chances for feedback and collaboration. My only regret is not being able to open the entire source tree at once yet. We'll get there, but this is a good start in the meantime.

We do not have our changes formally verified yet, but that is definitely on our roadmap -- otherwise, what's the point of starting from this set of options? Likewise, this is why we chose Rust -- there are several projects already in progress to produce formal verification tools for Rust, so we can hopefully use those as additional proofs.

[Sirened]

are there any formally verified CPUs that support any of the constructs needed for anything more than microcontrollers? Like, I have not yet found a formally verified CPU which supports virtual memory or caching