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. (<skydive...@gmail.com>) 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 (<demioben...@gmail.com>) > escribió: > >> On 11/12/23 03:57, Hugo V.C. wrote: >> > "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 >> the >> > 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 >> play >> > with those naive hardware partitioning concepts we all are blindly >> 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) >> >> _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
