[seL4] Re: Conclusions regarding speculation

Sorry Demi, I misunderstood you question about affordability, I guess you are referring to:

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.

My answer is also YES, of course it is affordable seL4 approach. It is reusable solution forever and ever. Once you formally verify something then it is backed by maths and it can be reused on future solutions. It is not only affordable, it is sustainable! Stop building short-term solutions, let's create long-term solution with reusable code. Formally verified code is the most clever security approach we humans have had since we invented computers. El lun, 13 nov 2023 a las 8:50, Hugo V.C. () escribió:

- 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? (remember that this is basically what QubesOS, which I use right now, is doing all the time...). 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. 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.

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

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