-----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-----

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 On Tue, Aug 09, 2022 at 12:46:32PM +0200, Hugo V.C. wrote:

" 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.

Xen Project does indeed have such access, as does Linux. seL4 Foundation should indeed be able to get the same level of access. The Linux Security Team does *not* sign NDAs, so hopefully seL4 Foundation will not need to.

" 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.

Yup!

"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).

I agree. Probably the main reason I do not worry too much about the Linux TCP/IP stack is that if someone does find a reliable 0day in it, then the exploitability of Qubes OS is the least of my worries. I, too, have found nasty vulnerabilities (unauthenticated remote DoS in MIT Kerberos, signature verification bypass in DNF), usually using the same method.

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.

Indeed. Worth noting that the hypervisor is not the only attack surface by any stretch of the imagination. blkback runs in dom0, for instance, and there are a whole slew of Qubes-specific services that are all unverified and can (and have!) had bugs. One way in which an seL4-based Qubes OS can improve is to use layer 3 connections between qubes, rather than layer 2 connections. The Ethernet header serves no useful function in the default configuration, but the associated ARP/NDP processing does introduce attack surface. A much nicer approach would be to simply send IP packets without additional encapsulation. The version field in the header indicates whether the packet is IPv4 or IPv6, so there is no need to distinguish them at the link layer. A layer 2 interface might be needed as well for advanced use-cases, but it should be the exception, not the rule. WireGuard is a widely deployed layer-3 network interface, so it is clear that Linux has good support for this. IP packets are self-delimiting, so it is not even necessary to handle message framing in the connection protocol. Additionally, if you want nested virtualization (you do, Xen not having it is a significant limitation) you might need kernel-mode emulation of at least some instructions to get decent performance. The same goes for some other hot-path parts of the virtualization stack, such as IPI and APIC virtualization. Being able to do these in userspace would be ideal, but performance might require having them run in the kernel, and that means formally verifying them for security. Another annoying Xen limitation is while it has core scheduling, it does not have any form of address space isolation, meaning that SMT must be disabled for security. Hyper-V does not have this limitation, provided that one does not care about within-guest security. Obviously, neither of these are blockers.

And thank you for your comments Demi, openly debate this is a very first step required.

You’re welcome! - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdodNnxM2uiJZBxxxsoi1X/+cIsEFAmLyUPgACgkQsoi1X/+c IsF4cA/8DVfeAt8+vfEtsqDw1+iyj+wWUC7pLK/BiXUwg/lzGTMYtmOtwYnv2Gjd n+EvzVVKjMYt1BP040dyUUQIYZOisfpGVy/9UjwgNbA5u7RzNVZEkGAxW3QV5W1y 0JYEZ2BrMqt4fnsszHVUEx0iRqV7uAjk9BZf+PsHGNjjap6ILY1CDk8HMk0A0COX BTf3yQoET2RtO1ZorzbTmfjZ6RXDi19ZCshu3ysGQsCRHcYp/XDn7pSUJ/4AdQPv CbqskMSEDmArglBz8Xjvyi+EOsnZSLmB8OOYqnFYzdrOXdyoYs4+3kbmjA1vRsgp KoYI0bzkiQr5nJcSILLQ2S0pAv5EtoMjV5gloA5uxjuE3FhOG9n6YsOhp+5PHeWr 3p19FEhvefCbj8RbANFhDyOlfDRuTC406L7oUMWiUfmMpsHG5Fj6MlFXH+LG9WxV g0zTDp3bilxRAU+yku0enu6JjkrVwwDlHBet0Z4BP8W4s2tIPk1128PEK9kAjPxP eEPu/ZP3tGrcR2HGwteZAswUmclP1KwByNpInLfiBPzm/Oj2RN9Wfb0Cq5h/xuVP jsEXneynKwXS2O+AbP0iywtC8W65DRepVqFuoaOi+NSkvlRcede2ff/TjdC7+zYe IP3dDKunEZyqneV7go2I8dwM8earUJyZt5hrXvhmmJiI4MM5u1s= =nzN2 -----END PGP SIGNATURE-----