We can’t achieve perfect security (there’s no such thing). What we can achieve is raising the bar for attackers. Simple things like using memory-safe languages for handling untrusted inputs, least-privilege design, defense in depth, etc.
The only perfectly secure computer is one that is off. Security is always about probabilities and trade offs. As you approach perfection cost approaches infinity. It’s similar to adding “nines” to your uptime.
A good security policy balances cost with security and also has plans in place for what to do if security is compromised.
The only correct answer is formal reasoning, as successfully executed by seL4.
This is a useless security nihilism. Xen is much more secure than anything else in terms of hole history. And Qubes relies on hardware virtualization, not software. Most famous escape from it was discovered by the Qubes founder ("Blue Pill").
The size of Linux in dom0 does not matter, because it has no network, does not run any apps and is only used to manage VMs. There is just no way for an attacker to exploit a bug there.
>formal reasoning
I hope this is the future, but unfortunately it's not the present yet.
Qubes devs are welcome to adopt seL4's VMM virtualization solution.
In seL4's virtualization design, VMM handles VM exceptions, and yet has no more privileges (capabilities, enforced by seL4, which is thoroughly formally proven) than the VM itself, thus an escape from VM to VMM would yield no fruit.