[xorcist]

Good point. The other argument is also true; Security and correctness is not a single metric.

With modern (buggy) hardware and DMA access, when your driver and/or hardware fails all bets are off. Some hardware may be possible to reboot (much as you'd reinitialize a kernel module in Linux), but sometimes your best course of action is a complete reboot.

As for security, you also need to take a long hard look at the the operating systems your operating system relies on, such as the ones powering your disks, nic, pci-controller etc. There are some potential tricky security interactions with them.

[techdragon]

SMM and other such ring "-1" type "services" in modern CPUs make your point quite clear to anyone who digs deep enough.

When trying to secure a system, we have reached the point where you have to sometimes as "is this CPU opcode safe?" Sometimes it just feels like modern hardware complexity is reaching some kind of critical mass threshold for "stupid shit"

[nickpsecurity]

That point was reached back in 90's when first security evaluations of Intel architecture were done, found tons of black boxes like SMM, and said to ditch it for security or virtualization. Invisible Things did a good job demonstrating an old risk but people should've ditched it long ago.

If you want verifiable hardware, look up the VAMP processor as it has everything from design descriptions to formal proofs of correctness. Not sure about its availability. SPARC and RISC-V are very open with open-source implementations available with Linux and compiler support. So, there's a solution if people ever want to put the work in.