-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512
On Tue, Aug 09, 2022 at 08:11:04AM +0200, Hugo V.C. wrote:
"From a Qubes OS perspective, the approach I would prefer is to first get Qubes OS working on seL4, with the control plane running in a Linux VM as it does now. This is definitely less than optimal, but it is likely the quickest way to get Qubes on seL4 working at all, and therefore the solution that is the most likely to actually be finished. "
I agree. The main goal here is to have something that can run.
Indeed it is. In particular, this means that seL4 has to have acceptable performance while being resistant to speculative execution vulnerabilities. It might mean that significant amounts of code will need to be verified that currently are not, and it will definitely require interrupt remapping support. Lack of interrupt remapping was part of Qubes Security Bulletin #1, all the way back in 2011. I suspect one of the hardest parts will be getting pre-disclosure notifications of embargoed CPU vulnerabilities.
" Over time, more and more of the code can be replaced by native seL4 components as those components become available. "
Absolutely. In fact, this is the most painful and time consuming task.
That it is, but it is also not necessary to get a significant benefit. - From my perspective, the most important win would be replacing Xen, which has had serious security flaws in the past, with formally verified code.
"For instance, the firewall is currently based on Linux, but it is a stand-alone component that already has an alternative implementation based on MirageOS. Therefore, it would be an excellent candidate for replacement with a firewall running natively on seL4."
Yes. Sounds very good as the firewall is huge attack surface (due to TCP/IP stack) and running it natively in seL4 looks like one of the very first steps.
The Linux TCP/IP stack is a very large attack surface, but it is also heavily fuzzed and extremely mature. If it _did_ have a reliably exploitable remote code execution vulnerability, the consequences would dwarf those of Heartbleed, ShellShock, or even Log4Shell. To the best of my knowledge, there have been no such vulnerabilities in the past decade. GRO Packet of Death does not count, as it requires GRO to be enabled on a UDP socket and no Qubes OS component does that. - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab