zlacker

>>feross+(OP)
The only practical security is security through isolation, like what Qubes OS provides. Security through correctness is impossible.

>>fsflov+Vp
Stupid question: how do you know your isolation is correct?

>>ttymck+Rr
Not stupid question at all. Nothing is 100% correct. Instead, you look at the attack surface, which for Qubes is extremely small: no network in AdminVM, only 100k lines of code in Xen supervisor, hardware virtualization with extremely low number of discovered escapes and so on.

>>fsflov+dv
Xen is bloated and has a security hole history. This also ignores the size of the Linux acting as dom0, that is.

The only correct answer is formal reasoning, as successfully executed by seL4.