Comment by josephg

> 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.