Most projects depend on complex, vulnerable OS's like Linux that nobody knows how to secure. High-assurance security prefers minimalist foundations designed for

Most projects depend on complex, vulnerable OS's like Linux that nobody knows how to secure. High-assurance security prefers minimalist foundations designed for security. Then, those foundations are leveraged by user-facing layers to inherit their properties. It's usually isolation of compromises to specific parts of memory with some support for blocking side channels between partitions. Genode follows that approach using an architecture similar to Nizza and Perseus: https://os.inf.tu-dresden.de/papers_ps/nizza.pdf https://os.inf.tu-dresden.de/papers_ps/nizza.pdf http://www.perseus-os.org/content/pages/Architecture.htm http://www.perseus-os.org/content/pages/Architecture.htm The NOVA microhypervisor, if compared to popular VMM's, is also illustrative of how high-assurance security applies minimalist, privilege-reducing design to the problem: http://hypervisor.org/eurosys2010.pdf http://hypervisor.org/eurosys2010.pdf Although I don't know Genode's assurances, most of the field also tries to make the assurance (confidence level) of the system as high as possible by using techniques that prove it has certain properties and/or rid it of as many vulnerabilities as possible. I have a list of historical and current methods here: https://pastebin.com/uyNfvqcp https://pastebin.com/uyNfvqcp