-----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 -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdodNnxM2uiJZBxxxsoi1X/+cIsEFAmLyI5AACgkQsoi1X/+c IsGd4RAA3avgKvNZIbwttDyTAF3PTBnxegoZGb0AAcw3B7QIYXZA6/HBaVqeB5r1 WNgbjq2l1Hjbx4SweN9SmcTNnzuRobrv7zRDVKESFvzqccaIKEnVrMTS0YUutNiu BjaWYhqsoeoOxR6W/WaPrqIBteCdo7zwqxUxhV53sMHPFWl6fSLsGZWT8sxQPJj9 CZR9b7uBcdviBHN27cn6MRYJgpK3wTch+Rn/pwnNNhfWX2jkzcRV+fO0mBzf5QV8 FVrDYEsBv6urUr4A0NyHfOoXUOC+p9KQU47ml8vC009Nmsb/wKdeK0VCGU1zC4Uq 4gjGOA1nIxLfS50QQA1AxJK6w3xeyzbYS2cBe1kyb/dj7wQxRx1myoRpmkvo3FHH 4s2t+4QXbpa6UMGnSwcAvi4zHJk2zaL15vBBsnlRsYTc4uFHbmKnEYVlLoBDHlFb 2DimNuf2Qm1v2AI6mitE9YOwWM2eg4M6Oymmej10fwC6VVHUzUZtSb1BjXgeSVPE 7jFWl9AYs9e8pIQbCKmKZzToC5edhsujc++6/cAoV2x2y7aluTcm1H+TlQEzqhp9 o18OckcBQ2QaORYj/jwOEVNDuuYx4VbJuhR7VGGjbbU48CNGWW0J6TRvhX4CWYiN QLQOxke2MhrN/77ikwSSWU1LuF9255Y1gdmfeSEL6XMp7B0KlYA= =hYgV -----END PGP SIGNATURE-----