" 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." This is out of my know-how comfort zone... maybe someone from seL4 core team can add some comments here... "I suspect one of the hardest parts will be getting pre-disclosure notifications of embargoed CPU vulnerabilities." I have no idea how to deal with this. Does Xen has access to those pre-disclosure notifications? If not then we are in same situation. If Xen does have access, then I guess seL4 Foundation (now backed by Google too) can get same access level. " From my perspective, the most important win would be replacing Xen, which has had serious security flaws in the past, with formally verified code." 100% agree. And that is where IMHO main effort should go if this lovely partnership between QubesOS and seL4 ever starts. "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." This is my know-how comfort zone... As far I have realized, vulnerabilities involving TCP/IP stacks of massive deployed devices are handled with extremely secrecy and few details are made public. I was somewhat involved in the Urgent/11 vulnerability research, exploitation, patching and disclosure on a derivative of VxWorks that affected the VxWorks’ TCP/IP stack (IPnet) and could see the impact of such issues. TCP/IP stacks are tested with ancient techniques (even modern fuzzing techniques are "old school" security from my point view). Modern vulnerability research involve manual analysis of the code logic and exploitation of corner side scenarios or configs or uncommon protocols. I have found some really nasty remote vulnerabilities (i.e. an UDP IKE single packet "ping of death") following this method so I guess that more skilled and resource capable adversaries (like govs) can do magic too, much better than me, on VxWorks, Linux, Windows, iOS and most OSs around there. TCP/IP stacks are too complex for humans and we are trying to automate all testing but this simply do not works (IMHO). And the Linux TCP/IP stack... yes, I agree it is very well tested and lot of eyes are there watching, but still is the main (remote) entry point, so I think it makes sense to think about having it ported to seL4 native some day in the future. But of course, this is not a priority, as you mentioned above, or even this may never happen, who knows... not my concern right now, my concern is about VM isolation guarantees (hypervisor), and this is where seL4 fits very well, and where QubesOS and seL4 can have a nice friendship. And thank you for your comments Demi, openly debate this is a very first step required. El mar, 9 ago 2022 a las 11:06, Demi Marie Obenour (< demi@invisiblethingslab.com>) escribió:
-----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-----