Comment by fovc
2 hours ago
sel4's guarantees break if you have DMA, e.g., from your NIC. It doesn't help with timing attacks. It doesn't cover your network stack. AFAIK, no one has taken up the mantle from Project Everest, so you'll need to write a verified TLS library. Once you've built all that, you can start thinking about your database/application/whatever. Then of course you'll have to verify all your dev's machines and scripts to ensure nobody is misusing a credential that can get stolen.
"So what?" you say. "Making a heavier-than-air metal tube take off and land millions of times per year without a catastrophe is also hard, and we no longer expect most or even many of those tubes to blow up or fall down."
Mother nature is not spending $$$ using AI and HI adversarially trying to find the exact combination of atoms that will cause your device to fail.
> sel4's guarantees break if you have DMA, e.g., from your NIC.
Modern CPUs support IOMMU. If you set that up, your NIC can only DMA to virtual addresses, managed by the operating system.
> It doesn't help with timing attacks. It doesn't cover your network stack
It does help with all this stuff, because your network stack and whatever else can be split off into isolated processes which talk over capabilities. Compromises in those processes are of course terrible. But they don't automatically allow kernel level takeover of the whole machine like on windows / linux.