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