[seL4] Re: Conclusions regarding speculation

On 11/13/23 02:50, Hugo V.C. wrote:

- Are you sure it is affordable? *** Yes. Creating laptops/servers with independent computing platforms is like putting toghether different laptps/servers inside the same box. Few things in life are so simple.... and simple usually means that it will be affordable or will tend to be affordable (same happened with multi core computing and this is by far a more complex manufacturing problem)

- Can that formally verified software run on desktop-class hardware that I can buy, either now or in the foreseeable future? *** Yes. seL4 is an example. Here the debate is to define what amount of software you want to be verified. To me, an hypervisor/OS like seL4 is more than enough and then, on top of this you need to build other layers of non-verified software. You will always have unverified software on a Desktop, what is important is to have the verified one on critical parts of the solution. What do you need to believe seL4 can run on a laptop? Do you need to see it booting up and running a VM with a standard OS inside?

Yes, and with the same speculation protections Xen provides.

(remember that this is basically what QubesOS, which I use right now, is doing all the time...).

I’m one of the developers of Qubes OS, though I am speaking in a personal capacity here.

The difference is QubesOS do not rely on a verified hypervisor while the hypothetical system I'm talking about it will have seL4 booting, which is a verified piece of code.

I would love that, but seL4 currently is missing at least five critical security features on x86: 1. Interrupt remapping in the IOMMU. 2. Protection against speculative execution attacks the moment the embargo breaks. 3. The ability to either choose the appropriate mitigations itself, or to let userspace choose them. 4. Properly implemented speculative execution mitigations. 5. Microcode update support. Without all five of these, seL4 is _less_ secure than Xen, which defeats the entire purpose of using it. As per the discussion in https://github.com/seL4/seL4/issues/1108 this will not be fixed any time soon. That’s why I asked about desktop-class hardware I can actually buy: the only non-x86 desktop-class hardware I know of are Macs with Apple silicon and POWER9 machines from Raptor, and seL4 supports neither. Apple silicon has lots of nonstandard IOMMUs that seL4 would need to support, and POWER is not supported at all.

Having said that, you can et we will have more and more pieces of verified (or semi-formally verified) software that we will put together like a puzzle to build a more reliable solution. An example is TCP/IP stack, which is a key piece of software I will always encourage people to verify as it will benefit all the Internet, not only Desktops.... but yes, the response is yes, in a foreseeable future we will have such verified software running on desktop-class hardware and the current debate will be part of the Internet History.

That would be amazing. (Fun fact: you probably have some formally verified cryptographic code installed on your system _right now_, since NSS uses fiat-crypto for some of its cryptographic primitives last I checked.)

- Does it have a VMM that can run multi-core Linux guests, and which can schedule those vCPUs across multiple physical CPUs? - Does it support low power states, so that battery life is decent? - Does it allow a privileged guest to create and destroy unprivileged guests? - Does it support PCI passthrough? If not, does it have drivers for every single piece of hardware on the aforementioned desktop-class machine — including the GPU? *** Those can be answered better by seL4 experts, don't dare to give you a wrong answers, anyway, you should understand there are steps in the process of migrating to seL4, do not expect a magical path with everything working like a charm from minute zero. But there's lot of amazing talented people like you that, if working together, can help boosting the process (it will happen after or before). I bet my business and my career on it.

My understanding is that Qubes OS would be happy to _use_ an seL4-based VMM, provided that it met Qubes OS’s requirements and offered a sufficiently compelling advantage over Xen. But Qubes OS simply doesn’t have the resources to _implement_ one. Therefore, the time to talk about integrating seL4 with Qubes OS would be _after_ the features I mentioned are implemented in either the kernel or the supporting userland. Xen provides all of them out of the box, with the sole exception of S0ix ("modern standby"). To be clear: I don’t fault seL4 for focusing on embedded right now. The reward/effort ratio is vastly more favorable there. Servers are significantly harder and I suspect desktops and laptops are the worst-case scenario, because _everything_ is dynamic and subject to the whim of a human who can and will break any simplifying assumptions one has made. And this is even before one starts talking about GPUs and other accelerators, which are a huge attack surface and yet can be the difference between a system being usable and unusable for the tasks people expect of it. There is a reason Qubes OS is going to be supporting GPU acceleration at some point. That’s why I am so pessimistic about time protection on desktop: all of the stuff I have read about it assumes at least some static partitioning, and in the desktop world, static _anything_ simply doesn’t exist.

- Does it protect against speculative execution attacks _without_ requiring static partitioning of _any_ resource? Even with a work-conserving scheduler? *** Those can be answered better by seL4 experts, don't dare to give you a wrong answers, but I think the question is tricky in the way you made it...

- Does it support reassigning memory from VMs that have lots of spare memory to VMs that are short on memory? *** Those can be answered better by seL4 experts, don't dare to give you a wrong answers, anyway, I guess you are referring to the infamous 🙏 (don't want to offend) "memory balancer" of QubesOS that locks you out and forbids you to start news guests when no more memory is available (even if lot of free memory is available on all guests).

No offense taken :). The memory balancer certainly leaves lots to be desired.

If this kind of "reassigning" memory is what you need, I bet this is already viable with seL4, anyway better response will be given by seL4 experts

El lun, 13 nov 2023 a las 2:42, Demi Marie Obenour () escribió:

...

...

"However, ensuring that the CPU time used by one domain is not observable by another domain is not possible, and I do not believe this will ever change."

I usually see infosec people talking about CPU time and cache to cover "modern" hardware based attacks, which is a good starting point, but just a starting point. Share a beer with anyone with know-how on physics and will give you half dozen ways to attack a workload from another workload in a system that is sharing resources. And I'm not talking about covert channels, which are

...

last unicorns to protect, I talk about direct info leaks based on several measurable environmental variables of the medium were those workload are being executed. Even with air gaped systems... so sharing hardware you can figure it out...

I guess I should release some paper about Marvel CPUs (ARM) and how to

...

with those naive hardware partitioning concepts we all are blindly

On 11/12/23 03:57, Hugo V.C. wrote: the play trusting.

...

One thing I absolutely agree with Gernot s to simplyfy hardware as much

as

...

possible and let the (formally verified) software do it's job when it comes to Time Protection. Even if far from perfect, this is an affordable and realistic approach. For any other hardware-based solution where the words "share/sharing" are wrote down somewhere, I would not even read the specs.

- Are you sure it is affordable? - Can that formally verified software run on desktop-class hardware that I can buy, either now or in the foreseeable future? - Does it have a VMM that can run multi-core Linux guests, and which can schedule those vCPUs across multiple physical CPUs? - Does it support low power states, so that battery life is decent? - Does it allow a privileged guest to create and destroy unprivileged guests? - Does it support PCI passthrough? If not, does it have drivers for every single piece of hardware on the aforementioned desktop-class machine — including the GPU? - Does it protect against speculative execution attacks _without_ requiring static partitioning of _any_ resource? Even with a work-conserving scheduler? - Does it support reassigning memory from VMs that have lots of spare memory to VMs that are short on memory?

If the answer to any of these questions is “no”, then it is not realistic in my world.-- Sincerely, Demi Marie Obenour (she/her/hers)