[seL4] Re: Conclusions regarding speculation
That's it. Point "7" is summarizes the goal. In other words, (current) laws of physics do no allow completely isolated systems. Unless you jump into a black hole... were even info can't escape from it. So unless we compute stuff inside a black hole (and the problem would be how to get result info back...) I think we can consider solutions as "good" were the effort required to attack the solution it is not worth. I guess everything we rely on is based on that nowadays... El sáb., 18 nov. 2023 0:02, G. Branden Robinson < g.branden.robin...@gmail.com> escribió: > At 2023-11-17T16:02:28-0500, Demi Marie Obenour wrote: > > On 11/12/23 00:44, Gernot Heiser via Devel wrote: > > > If you want a theoretically sound solution – Welcome to Time > > > Protection! > > > > > > In contrast to your implied claim that time protection is unsound: > > > It’s been formalised, and it’s in the process of being proved > > > correct and complete in an seL4 implementation. Its minimal hardware > > > support also been implemented in RISC-V processors and demonstrated > > > cheap and complete (may even be in silicon by now). > > > > A key storage service _must_ be able to respond to signing and > > decryption requests to be usable at all, and that means that the > > requester _will_ know how long the operation took. One can try to hide > > this information by padding the operation to its worst-case value, > > but this only works if there _is_ a worst-case value. In Qubes OS, > > responding to a request will require heap allocation, fork(), disk > > I/O, and sometimes user interaction. That means that the worst-case > > operation time is _infinite_, so time protection is simply not > > possible and will not be possible for the foreseeable future. > > Can we reëstablish what we mean by "time protection", then? > > A few things seem to me to be true: > > 1. Even on statically configured systems, response times for requested > services can easily exceed the quantum of a schedule slice or "time > protection domain", for exactly the reasons you say. A service may > have highly variable _latency_: to require information retrieval > from a machine register, or local cache, or remote cache, or main > memory, or mass storage, or over the network, or may await human > interaction--as with a user needing to fumble with a physical token > or poke keystrokes into a user interface. Approximately, each of > these is at least one order of magnitude slower than the last. > > 2. The bandwidth of a timing channel attack is strongly and inversely > correlated with the channel's latency. (This statement needs a > proof.) > > 3. Practical time protection is therefore not so much a matter of > achieving zero information leakage; application design may not > permit that. For example, in the key storage service example, one > _can_ draw statistical inferences based on the latency of response; > if the signing or decryption request was fulfilled in less than a > millisecond, then use of the key was probably not authorized > consequent to human interaction. > > 4. The distinction between "static" and "dynamic" systems may become > indistinct here, since even a statically partitioned system may be > operating in a dynamic environment, particularly when taking into > account what data populate caches. > > 5. A "static" system is not necessarily a deterministic one. And > without perfect knowledge of microarchitectural implementations, > something that seems unlikely to eventuate with x86-64 or AArch64 > cores, determinism seems impossible. We have no way of knowing when > a microarchitectural gadget will decide to flush an undocumented > buffer.) > > 6. Because multiple orders of magnitude separate fast accesses from > slow ones, the available bandwidth for exfiltration > decreases exponentially. (This statement also needs a proof.) > > 7. The art and science of time protection will progress on two fronts: > (a) selection by system designers of a "good" time quantum for > high-bandwidth channels that sacrifice little performance while > strangling the bandwidth of information leakage to zero capacity; > and (b) the socialization of knowledge about timing channel attacks > to application designers so that they can estimate the bandwidth of > the timing channels they create, and respond appropriately. > > An analogy that comes to mind is the quality of one-way hashes. We know > that we'll never have a perfect hash function for inputs of arbitrary > length, but we know that the longer the hash, the better we can do. > CRC32 is hopelessly weak for security applications (but still okay for > others); MD5 is regarded as compromised; and BLAKE3 state-of-the-art. > > Time protection strong enough that your exfiltration countermeasures > give your opponent a problem that will outlive them is adequate for most > applications.
[seL4] Re: Conclusions regarding speculation
At 2023-11-17T16:02:28-0500, Demi Marie Obenour wrote: > On 11/12/23 00:44, Gernot Heiser via Devel wrote: > > If you want a theoretically sound solution – Welcome to Time > > Protection! > > > > In contrast to your implied claim that time protection is unsound: > > It’s been formalised, and it’s in the process of being proved > > correct and complete in an seL4 implementation. Its minimal hardware > > support also been implemented in RISC-V processors and demonstrated > > cheap and complete (may even be in silicon by now). > > A key storage service _must_ be able to respond to signing and > decryption requests to be usable at all, and that means that the > requester _will_ know how long the operation took. One can try to hide > this information by padding the operation to its worst-case value, > but this only works if there _is_ a worst-case value. In Qubes OS, > responding to a request will require heap allocation, fork(), disk > I/O, and sometimes user interaction. That means that the worst-case > operation time is _infinite_, so time protection is simply not > possible and will not be possible for the foreseeable future. Can we reëstablish what we mean by "time protection", then? A few things seem to me to be true: 1. Even on statically configured systems, response times for requested services can easily exceed the quantum of a schedule slice or "time protection domain", for exactly the reasons you say. A service may have highly variable _latency_: to require information retrieval from a machine register, or local cache, or remote cache, or main memory, or mass storage, or over the network, or may await human interaction--as with a user needing to fumble with a physical token or poke keystrokes into a user interface. Approximately, each of these is at least one order of magnitude slower than the last. 2. The bandwidth of a timing channel attack is strongly and inversely correlated with the channel's latency. (This statement needs a proof.) 3. Practical time protection is therefore not so much a matter of achieving zero information leakage; application design may not permit that. For example, in the key storage service example, one _can_ draw statistical inferences based on the latency of response; if the signing or decryption request was fulfilled in less than a millisecond, then use of the key was probably not authorized consequent to human interaction. 4. The distinction between "static" and "dynamic" systems may become indistinct here, since even a statically partitioned system may be operating in a dynamic environment, particularly when taking into account what data populate caches. 5. A "static" system is not necessarily a deterministic one. And without perfect knowledge of microarchitectural implementations, something that seems unlikely to eventuate with x86-64 or AArch64 cores, determinism seems impossible. We have no way of knowing when a microarchitectural gadget will decide to flush an undocumented buffer.) 6. Because multiple orders of magnitude separate fast accesses from slow ones, the available bandwidth for exfiltration decreases exponentially. (This statement also needs a proof.) 7. The art and science of time protection will progress on two fronts: (a) selection by system designers of a "good" time quantum for high-bandwidth channels that sacrifice little performance while strangling the bandwidth of information leakage to zero capacity; and (b) the socialization of knowledge about timing channel attacks to application designers so that they can estimate the bandwidth of the timing channels they create, and respond appropriately. An analogy that comes to mind is the quality of one-way hashes. We know that we'll never have a perfect hash function for inputs of arbitrary length, but we know that the longer the hash, the better we can do. CRC32 is hopelessly weak for security applications (but still okay for others); MD5 is regarded as compromised; and BLAKE3 state-of-the-art. Time protection strong enough that your exfiltration countermeasures give your opponent a problem that will outlive them is adequate for most applications. (When it is not, there is always the option of destroying,[1] relocating, or otherwise "losing" the data.[2]) I'd very much welcome correction on any of the foregoing points. Regards, Branden [1] https://academic.oup.com/hwj/article/93/1/95/6535581 [2] https://www.theguardian.com/media/2018/jan/31/cabinet-documents-abc-reveals-top-secret-files-found-in-old-filing-cabinets ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: Conclusions regarding speculation
On 11/12/23 00:44, Gernot Heiser via Devel wrote: > On 11 Nov 2023, at 07:49, Demi Marie Obenour wrote: >> >> On 11/9/23 17:47, Gernot Heiser via Devel wrote: >>> On 10 Nov 2023, at 06:03, Demi Marie Obenour wrote: >>> - Speculative taint tracking provides complete protection against speculative attacks. This is sufficient to prevent leakage of cryptographic key material, even in fully dynamic systems. Furthermore, it is compatible with fast context switches between protection domains. >>> >>> It’s also a point solution, that provides zero guarantees against >>> unforeseen attacks. >> >> Unless I am severely mistaken, it provides complete protection for code >> that has secret-independent timing, such as cryptographic software. It >> is also cheaper than some of the workarounds existing systems must use. > > Well, *if* speculative taint tracking is really completely and correctly > implemented, *and* you have such magic hardware. That’s a strong statement > (for which there’s no proof). But let’s assume it is true. > > Then you may a complete protection against *speculation* attacks. > > Remember, speculation attacks construct a Trojan in otherwise trustworthy > code using speculative execution of gadgets. There are other ways, > specifically control-flow attacks > > So order to be secure, you then “only” need: > - the magic complete and performant implementation of taint tacking, AND > - complete prevention of control-flow attacks, AND > - all secret-handling code being free from algorithmic timing side channels > (i.e. no branching on or indexing by secrets), AND > - no untrusted code, because any untrusted code may contain a Trojan that > actively leaks through caches etc > > If you’re comfortable with all those ifs, fine. I’m not. > >>> - Full time partitioning eliminates all timing channels, but it is >>> possible only in fully static systems, which severely limits its >>> applicability. >>> I’m sorry, but this is simply false. What you need for time protection (I assume this is what you mean with “full time partitioning”) are fixed time slices – ”fixed” in that their length cannot depend on any events in the system that can be controlled by an untrusted domain. It doesn’t mean they cannot be changed as domains come and go. >> >> Based on what information should I set these time slices? > > That’s OS/hypervisor policy. Every system I know assigns time slices, that’s > normal. > > But note, the strictly fixed (in the sense of not influencable by user code) > time slices are only needed if you want to prevent *all* timing channels, in > this case leaking by controlling the timing of context switches. > > This is a relatively low-bandwidth channel, i.e. it will need a minute or tow > to leak an SSL key. If you’re fine with that then there’s no need for fixed > time slices. > - Time protection without time partitioning does _not_ fully prevent Spectre v1 attacks, and still imposes a large penalty on protection domain switches. >>> Time protection does *not* impose a large penalty. Its context-switching >>> cost is completely hidden by the cost of an L1 D-cache flush – as has been >>> demonstrated by published work. And if you don’t flush the L1 cache, you’ll >>> have massive leakage, taint-tracking or not. >>> >>> Where time protection, *without further hardware support*, does have a cost >>> is for partitioning the lower-level caches. This cost is two-fold: >>> >>> 1) Average cache utilisation is reduced due to the static partitioning (in >>> contrast to the dynamic partitioning that happens as a side effect of the >>> hardware’s cache replacement policy). This cost is generally in the >>> single-digit percentage range (as per published work), but can also be >>> negative – there’s plenty of work that uses static cache partitioning for >>> performance *isolation/improvement*. >> >> Static partitioning based on _what_? On a desktop system, the dynamic >> behavior >> of a workload is generally the _only_ information known about that workload, >> so >> any partitioning _must_ be dynamic. > > Again, if you trust all your code to not intentionally leak secrets, then you > don’t have to do this. > > Cache channels are very high bandwidth. Even cache side-channels have high > enough bandwidth to steal encryption keys in minutes. > > If your threat scenario doesn’t care about this, fine. But there’s no way of > preventing cache channels other than flushing or partitioning. > > So, it all depends on your threat scenario. > > If your threat scenario is that: > - your hypervisor/kernel is completely trusted > - all secret-handling code is trusted to >- not have algorithmic timing channels >- not be susceptible to control-flow attacks >- be free of Trojans > … then speculation attacks may be your main worry and you can ignore all the > other timing channels, and you *may* be
[seL4] Re: Conclusions regarding speculation
[re-send 2/2] - Forwarded message from "G. Branden Robinson" - Date: Mon, 13 Nov 2023 04:03:16 -0600 From: "G. Branden Robinson" To: devel@sel4.systems Subject: Re: [seL4] Re: Conclusions regarding speculation Hi Demi, At 2023-11-13T03:39:00-0500, Demi Marie Obenour wrote: > > 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. This is the sort of thing that gets solved by putting together a small team of engineers, some very thick manuals from the manufacturer, a contact inside the vendor to address points "accidentally" omitted or erroneously documented, and a not insignificant amount of money. A Simple Matter of Programming, in other words. > 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. These 3 seem to be what you and Gernot are arguing about and I feel unqualified to get into the middle of that. > 5. Microcode update support. This is like (1) except it will never happen with verifiability and reliability because that would either expose, or enable the replacement of, the "secret sauce", by which the profit margin on the chip is protected. And that is why we need fully open cores subject to third-party correctness verification. I've never even seen an argument that you can combine these properties with binary blobs or trade secrets. And as long as that is true we're sure to keep getting trashed by spec ex attacks or the next great innovation in system compromise. > 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. I may not be completely understanding your argument, but it sounds like you're saying that with Xen/QubesOS you essentially achieve compartmentalization by partitioning one process (in the Unix sense) per processor (in the cores plus shared caches sense). Once you do this, doesn't it start to look a lot like OpenVMS? This would initially be a good way to drive the KVM-switch-in-a-laptop into the market but I think it would run into scaling problems pretty quickly. > 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, ...insanely expensive (5 figures USD) last I looked... And Apple won't give up secret sauce of any kind before the extinction of our species. They still curse John Sculley's name. > and seL4 supports neither. > Apple silicon has lots of nonstandard IOMMUs that seL4 would need to > support, and POWER is not supported at all. For the time being, we are simply screwed. We are the cows from which economic rents are milked; this pleases the Street. The only rescue from our plight is Joseph Schumpeter's "creative destruction", opinions of which seem to vary in a consistent way depending on one's temporal distance from an IPO. > (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.) ! Share a link next time. :) > To be clear: I don’t fault seL4 for focusing on embedded right now. > The reward/effort ratio is vastly more favorable there. That, and I think the larger players in the industry perceive potential risks to the status quo. The promise of lower expenses down the road due to fewer security incidents is a really hard thing to quantify, and much decision making is tied to what can be said in the next quarterly 10-C filing with the SEC. Yes, Heartbleed can give you heartburn big time. But sufficiently large and reliable income streams salve any scald. Quality of implementation is simply not the sort of thing anybody on the financial side of any firm cares about unless it's as dramatic as an airplane falling out of the sky. (I would have said "or life support equipment not being fit for purpose", but that appears not to be the case.[1][2]) > 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,
[seL4] Re: Conclusions regarding speculation
[sending a revised verison of this and one other message; Peter was
able to confirm that the earlier ones got lost somewhere between exim
and mailman--maybe my GPG signature attachment caused problems, so
leaving that off]
- Forwarded message from "G. Branden Robinson"
-
Date: Mon, 13 Nov 2023 02:51:36 -0600
From: "G. Branden Robinson"
To: devel@sel4.systems
Subject: Re: [seL4] Re: Conclusions regarding speculation
At 2023-11-13T08:55:47+0100, Hugo V.C. wrote:
> > One might as well just buy multiple laptops and be able to use them
> > at the same time.
>
> *** You can not easily travel with multiple laptops and it is not a
> comfortable solution, nor you can sell this idea to anyone.
> Instead you can travel with a single laptop with 3 different computing
> platforms inside, basically, the user will never know, it will be
> transparent.
When I was at TS we had a demo system that manifested this sort of
partitioning, but I think it furthermore used a windowing system. The
project was no longer under development while I was working
there--probably it wasn't being actively funded--but the proof of
concept seems to have been delivered. It may have had only two tiers,
"red" and "black", with the former a data sink only (apart from what
your eyeballs could see) and the latter a source and sink. Pretty sure
someone else on the list can correct me and say more.
(I want to say it was called MDDC? "Multi-Domain Display Controller"?]
My other thought is that we're basically talking about putting a KVM
("keyboard/video/mouse", not "kernel virtual machine" :) ) switch inside
a chassis with cores, storage, and peripheral ports. That doesn't seem
like it should be too hard.[0] The physical dimensions of KVMs seem to
be dominated by the sizes of the connectors attached to them. Not an
issue inside a chassis.
Economically there is a reason to expect this to come to pass as well;
with the death of Moore's Law, I submit that we buy multicore CPU
packages not because we use them efficiently--I don't, except when
running "make -j", and that's a tiny fraction of my interaction time--it
is because CPU vendors desire to keep the price point of the minimum
configured processor model for consumer machines around USD 100. I
guess some kind of commodity market dynamics are thought to set in
somewhere below that point, and such dynamics are threatening to the
U.S. consumer-facing semiconductor duopoly.
(Vertical integration is a classic defense against having to participate
in this sort of competition, and is consistent with Apple's in-housing
of CPU design and manufacture.)
As innovations go, this could be a benign one, and a real improvement if
we seize the opportunity on the OS side. (We still need a
capability-based OS and, as Hugo points out, a formally verified network
stack.)
Here's an amusing proof of concept with a mightily retro
hardware/software stack. But if a hobbyist can do this in his garage...
"Meet the ZedRipper – a 16-core, 83 MHz Z80 powerhouse as portable as it
is impractical."
http://www.chrisfenton.com/the-zedripper-part-1/
Aside:
Just over the past couple of weeks, glibc and other libc implementers
have held an open conversation with the Linux man-pages maintainer such
that they're seriously trying to get the best available information to C
programmers about how to perform the seemingly simple operation of
copying strings, and why the silver bullets that have been touted to
date, aren't.[1] For decades our industry has labored under the harmful
myth that the standard C library, even as it existed in ANSI C89, was
perfectly good enough for this, and if you screwed up it was because
you're a bad programmer, not because C's infamously weak type system and
silly selection of return values in its library[2] laid down a minefield
for you to traverse.
Rust has caught fire despite all the money Google has thrown at Go,[3]
and a few people (not just me, I promise) even remember and point out
how Ada got a lot of stuff right 40 years ago that the
"close-to-the-metal"/portable-assembly school of hacking keeps getting
pwn3d by.[4]
gnulib is adding CHERI support as we speak.[5] I don't personally
prefer CHERI to using a better language than C/C++ (and ISA than x86)
from the ground up, but it is a serious and honest attempt to face the
problems with C that code cowboys have waved aside for decades.
Could our industry be--at long, long last--tiring of crap security?
May it be.
By all means put a KVM switch in an 8-package/64-hart RISC-V 64 laptop.
I promise not to block the vent.
Regards,
Branden
[0] This is how you know I'm not a hardware guy.
[1]
https://lore.kernel.org/linux-man/ZU4SDh-Se5gjPny5@debian/T/#mfb5a3fdeb35487dec6f8d9e3d8548bd0d92c4975
[2] https://www.symas.com/post/the-sad-state-of-c-strings
[3] An oft-heard rebuttal to this observatio
[seL4] Re: Conclusions regarding speculation
I had one reply each to Demi and Hugo, but I think they got stuck in a moderation queue. Possibly my GPG signature angers the spam filter. Can someone look into it? Regards, Branden On Mon, Nov 13, 2023 at 2:19 PM Peter Chubb via Devel wrote: > > > "Demi" == Demi Marie Obenour writes: > > Demi> I would love that, but seL4 currently is missing at least five > Demi> critical security features on x86: > > Demi> 1. Interrupt remapping in the IOMMU. > > Can you please take a look at https://github.com/seL4/seL4/pull/1098 > which attempts to add this? It needs more eyes on it. > > -- > Dr Peter Chubbhttps://trustworthy.systems/ > Trustworthy Systems GroupCSE, UNSW > Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm. > ___ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: Conclusions regarding speculation
> "Demi" == Demi Marie Obenour writes: Demi> I would love that, but seL4 currently is missing at least five Demi> critical security features on x86: Demi> 1. Interrupt remapping in the IOMMU. Can you please take a look at https://github.com/seL4/seL4/pull/1098 which attempts to add this? It needs more eyes on it. -- Dr Peter Chubbhttps://trustworthy.systems/ Trustworthy Systems GroupCSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm. ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: Conclusions regarding speculation
El lun, 13 nov 2023 a las 9:39, Demi Marie Obenour () escribió: > 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. > I know since long ago...! And that's why I think your contribution here is so valuable, you are right now a bridge between the academic (seL4) and the real World of Secure Desktop Computing (QubesOS). I've been working with hardened solutions (Grsecurity, Pitbull, etc) since 20 years ago trying to solve the "Desktop problem" and never get a viable solution. Then the virtualization started being more affordable/usable on Desktop systems... and then I knew about QubesOS... and here I saw a big opportunity to join efforts of both solutions. I firmly believe in that. And you are a key piece here, I have not seen anyone else from QubesOS being interested on seL4, but you. So yes, I know who you are and it is very nice you are here debating stuff about seL4 desktop implementation, as this is a path to follow IMHO :-) > > > 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. > *** Wow... this would open a entire new debate out of the scope of this thread which I think it is no worth as I don't want one or the other to be better, but joining efforts to get a superb product that will make the security industry change forever. > > 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 — > >
[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
[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ó: > >> 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
[seL4] Re: Conclusions regarding speculation
El lun, 13 nov 2023 a las 2:48, Demi Marie Obenour () escribió: > On 11/10/23 05:07, Hugo V.C. wrote: > > "If people want to improve the hardware, focussing on generic mechanisms > > such as support for partitioning L2-LL caches would be far more > beneficial > > than point-solutions that will be defeated by the next class of attacks." > > > > The path of partitioning some hardware resourse ends up in full > > partitioning of the computing platform including power supply. It is > > simpler (almost zero design effort) and the only "reasonably" secure > > solution. Whenever you share hardware resources, you open the path to > side > > channels. > > At this point one just has multiple separate systems. > Yes, it is wonderful how simple it is... isn't it? > > > On the other hand, PLUS full computing platform partitioning time > > protection is a must on each isolated computing platform. So here we have > > two problems that need to be addressed by different vendors: > > > > 1) Time protection, CPU/SoC vendors > > 2) Computing platform isolation (laptop/servers vendors). > > > > Figure out how wonderful would be to have a laptop with X full > independent > > computing platforms inside (fun/work/banking...) and each one based on > > CPU/SoC solutions with Time Protection. > > That works until one needs to use all of the cores on the system for a > parallel > VM kernel build or for non-accelerated video encoding. > > > On top of each of those platforms some verified hypervisor/kernel > (seL4?). > > > > BTW, the step 2 is straight forward, just make laptops a bit bigger and > add > > a screen swich to switch each isolated computing platform. > > One might as well just buy multiple laptops and be able to use them at the > same time. > *** You can not easily travel with multiple laptops and it is not a comfortable solution, nor you can sell this idea to anyone. Instead you can travel with a single laptop with 3 different computing platforms inside, basically, the user will never know, it will be transparent. > -- > Sincerely, > Demi Marie Obenour (she/her/hers) > > ___ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems > ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: Conclusions regarding speculation
- 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ó: > 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
[seL4] Re: Conclusions regarding speculation
On 11/10/23 05:07, Hugo V.C. wrote: > "If people want to improve the hardware, focussing on generic mechanisms > such as support for partitioning L2-LL caches would be far more beneficial > than point-solutions that will be defeated by the next class of attacks." > > The path of partitioning some hardware resourse ends up in full > partitioning of the computing platform including power supply. It is > simpler (almost zero design effort) and the only "reasonably" secure > solution. Whenever you share hardware resources, you open the path to side > channels. At this point one just has multiple separate systems. > On the other hand, PLUS full computing platform partitioning time > protection is a must on each isolated computing platform. So here we have > two problems that need to be addressed by different vendors: > > 1) Time protection, CPU/SoC vendors > 2) Computing platform isolation (laptop/servers vendors). > > Figure out how wonderful would be to have a laptop with X full independent > computing platforms inside (fun/work/banking...) and each one based on > CPU/SoC solutions with Time Protection. That works until one needs to use all of the cores on the system for a parallel VM kernel build or for non-accelerated video encoding. > On top of each of those platforms some verified hypervisor/kernel (seL4?). > > BTW, the step 2 is straight forward, just make laptops a bit bigger and add > a screen swich to switch each isolated computing platform. One might as well just buy multiple laptops and be able to use them at the same time. -- Sincerely, Demi Marie Obenour (she/her/hers) ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: Conclusions regarding speculation
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
[seL4] Re: Conclusions regarding speculation
On 11/12/23 00:44, Gernot Heiser via Devel wrote: > On 11 Nov 2023, at 07:49, Demi Marie Obenour wrote: >> >> On 11/9/23 17:47, Gernot Heiser via Devel wrote: >>> On 10 Nov 2023, at 06:03, Demi Marie Obenour wrote: >>> - Speculative taint tracking provides complete protection against speculative attacks. This is sufficient to prevent leakage of cryptographic key material, even in fully dynamic systems. Furthermore, it is compatible with fast context switches between protection domains. >>> >>> It’s also a point solution, that provides zero guarantees against >>> unforeseen attacks. >> >> Unless I am severely mistaken, it provides complete protection for code >> that has secret-independent timing, such as cryptographic software. It >> is also cheaper than some of the workarounds existing systems must use. > > Well, *if* speculative taint tracking is really completely and correctly > implemented, *and* you have such magic hardware. That’s a strong statement > (for which there’s no proof). But let’s assume it is true. > > Then you may a complete protection against *speculation* attacks. > > Remember, speculation attacks construct a Trojan in otherwise trustworthy > code using speculative execution of gadgets. There are other ways, > specifically control-flow attacks > > So order to be secure, you then “only” need: > - the magic complete and performant implementation of taint tacking, AND > - complete prevention of control-flow attacks, AND > - all secret-handling code being free from algorithmic timing side channels > (i.e. no branching on or indexing by secrets), AND > - no untrusted code, because any untrusted code may contain a Trojan that > actively leaks through caches etc The first is a reasonable assumption for hardware with taint tracking, and the rest are reasonable assumptions for cryptographic code. > If you’re comfortable with all those ifs, fine. I’m not. > >>> - Full time partitioning eliminates all timing channels, but it is >>> possible only in fully static systems, which severely limits its >>> applicability. >>> I’m sorry, but this is simply false. What you need for time protection (I assume this is what you mean with “full time partitioning”) are fixed time slices – ”fixed” in that their length cannot depend on any events in the system that can be controlled by an untrusted domain. It doesn’t mean they cannot be changed as domains come and go. >> >> Based on what information should I set these time slices? > > That’s OS/hypervisor policy. Every system I know assigns time slices, that’s > normal. > > But note, the strictly fixed (in the sense of not influencable by user code) > time slices are only needed if you want to prevent *all* timing channels, in > this case leaking by controlling the timing of context switches. > > This is a relatively low-bandwidth channel, i.e. it will need a minute or tow > to leak an SSL key. If you’re fine with that then there’s no need for fixed > time slices. Is this with both sides cooperating or not? Covert channel attacks are out of scope. - Time protection without time partitioning does _not_ fully prevent Spectre v1 attacks, and still imposes a large penalty on protection domain switches. >>> Time protection does *not* impose a large penalty. Its context-switching >>> cost is completely hidden by the cost of an L1 D-cache flush – as has been >>> demonstrated by published work. And if you don’t flush the L1 cache, you’ll >>> have massive leakage, taint-tracking or not. >>> >>> Where time protection, *without further hardware support*, does have a cost >>> is for partitioning the lower-level caches. This cost is two-fold: >>> >>> 1) Average cache utilisation is reduced due to the static partitioning (in >>> contrast to the dynamic partitioning that happens as a side effect of the >>> hardware’s cache replacement policy). This cost is generally in the >>> single-digit percentage range (as per published work), but can also be >>> negative – there’s plenty of work that uses static cache partitioning for >>> performance *isolation/improvement*. >> >> Static partitioning based on _what_? On a desktop system, the dynamic >> behavior >> of a workload is generally the _only_ information known about that workload, >> so >> any partitioning _must_ be dynamic. > > Again, if you trust all your code to not intentionally leak secrets, then you > don’t have to do this. > > Cache channels are very high bandwidth. Even cache side-channels have high > enough bandwidth to steal encryption keys in minutes. How much would this be reduced by a cache that was fully associative, or which emulated full associativity? > If your threat scenario doesn’t care about this, fine. But there’s no way of > preventing cache channels other than flushing or partitioning. Environments that can use cache flushing or partitioning should. However, the cost of
[seL4] Re: Conclusions regarding speculation
"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. El vie, 10 nov 2023 a las 22:02, Demi Marie Obenour () escribió: > On 11/9/23 17:47, Gernot Heiser via Devel wrote: > > On 10 Nov 2023, at 06:03, Demi Marie Obenour > wrote: > > > > - Speculative taint tracking provides complete protection against > > speculative attacks. This is sufficient to prevent leakage of > > cryptographic key material, even in fully dynamic systems. > > Furthermore, it is compatible with fast context switches between > > protection domains. > > > > It’s also a point solution, that provides zero guarantees against > unforeseen attacks. > > Unless I am severely mistaken, it provides complete protection for code > that has secret-independent timing, such as cryptographic software. It > is also cheaper than some of the workarounds existing systems must use. > > > - Full time partitioning eliminates all timing channels, but it is > > possible only in fully static systems, which severely limits its > > applicability. > > > > I’m sorry, but this is simply false. > > > > What you need for time protection (I assume this is what you mean with > “full time partitioning”) are fixed time slices – ”fixed” in that their > length cannot depend on any events in the system that can be controlled by > an untrusted domain. It doesn’t mean they cannot be changed as domains come > and go. > > Based on what information should I set these time slices? > > The system I work with has no idea what workload it is running. It > can’t require the workload to provide it with hints because existing > workloads don’t do that. It can’t ask the user because the user will > have no idea either. The most it can do is adapt based on what the > workload is doing at runtime. > > In Qubes OS, it is completely normal for one VM (effectively a protection > domain) to start using almost the entire system’s CPU resources without > any warning at all. This could happen because the user just started > compiling > a big project. The user might then start another CPU-intensive task (such > as a video call) in another VM, and that might _also_ try to use 100% of > the > system CPU resources. And users will expect that the CPU usage of the > first > workload will decrease when this happens, as some (but not all!) of the CPU > time is allotted to the second workload instead. > > Given this constraint, I see no way to implement time protection. It _is_ > possible to quantize the amount of CPU time allotted to a given vCPU, and > to have a process that uses small, random amounts of CPU to generate noise. > 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. > > > - Time protection without time partitioning does _not_ fully prevent > > Spectre v1 attacks, and still imposes a large penalty on protection > > domain switches. > > > > Time protection does *not* impose a large penalty. Its context-switching > cost is completely hidden by the cost of an L1 D-cache flush – as has been > demonstrated by published work. And if you don’t flush the L1 cache, you’ll > have massive leakage, taint-tracking or not. > > > > Where time protection, *without further hardware support*, does have a > cost is for partitioning the lower-level caches. This cost is two-fold: > > > > 1) Average cache utilisation is reduced due to the static partitioning > (in contrast to the dynamic partitioning that happens as a side effect of > the hardware’s cache replacement policy). This cost is generally in the > single-digit percentage range (as per published work), but can also be > negative – there’s plenty of work that uses static cache partitioning for >
[seL4] Re: Conclusions regarding speculation
On 11 Nov 2023, at 07:49, Demi Marie Obenour wrote: > > On 11/9/23 17:47, Gernot Heiser via Devel wrote: >> On 10 Nov 2023, at 06:03, Demi Marie Obenour wrote: >> >>> - Speculative taint tracking provides complete protection against >>> speculative attacks. This is sufficient to prevent leakage of >>> cryptographic key material, even in fully dynamic systems. >>> Furthermore, it is compatible with fast context switches between >>> protection domains. >> >> It’s also a point solution, that provides zero guarantees against unforeseen >> attacks. > > Unless I am severely mistaken, it provides complete protection for code > that has secret-independent timing, such as cryptographic software. It > is also cheaper than some of the workarounds existing systems must use. Well, *if* speculative taint tracking is really completely and correctly implemented, *and* you have such magic hardware. That’s a strong statement (for which there’s no proof). But let’s assume it is true. Then you may a complete protection against *speculation* attacks. Remember, speculation attacks construct a Trojan in otherwise trustworthy code using speculative execution of gadgets. There are other ways, specifically control-flow attacks So order to be secure, you then “only” need: - the magic complete and performant implementation of taint tacking, AND - complete prevention of control-flow attacks, AND - all secret-handling code being free from algorithmic timing side channels (i.e. no branching on or indexing by secrets), AND - no untrusted code, because any untrusted code may contain a Trojan that actively leaks through caches etc If you’re comfortable with all those ifs, fine. I’m not. >> - Full time partitioning eliminates all timing channels, but it is >> possible only in fully static systems, which severely limits its >> applicability. >> >>> I’m sorry, but this is simply false. >>> >>> What you need for time protection (I assume this is what you mean with >>> “full time partitioning”) are fixed time slices – ”fixed” in that their >>> length cannot depend on any events in the system that can be controlled by >>> an untrusted domain. It doesn’t mean they cannot be changed as domains come >>> and go. > > Based on what information should I set these time slices? That’s OS/hypervisor policy. Every system I know assigns time slices, that’s normal. But note, the strictly fixed (in the sense of not influencable by user code) time slices are only needed if you want to prevent *all* timing channels, in this case leaking by controlling the timing of context switches. This is a relatively low-bandwidth channel, i.e. it will need a minute or tow to leak an SSL key. If you’re fine with that then there’s no need for fixed time slices. >>> - Time protection without time partitioning does _not_ fully prevent >>> Spectre v1 attacks, and still imposes a large penalty on protection >>> domain switches. >>> >> Time protection does *not* impose a large penalty. Its context-switching >> cost is completely hidden by the cost of an L1 D-cache flush – as has been >> demonstrated by published work. And if you don’t flush the L1 cache, you’ll >> have massive leakage, taint-tracking or not. >> >> Where time protection, *without further hardware support*, does have a cost >> is for partitioning the lower-level caches. This cost is two-fold: >> >> 1) Average cache utilisation is reduced due to the static partitioning (in >> contrast to the dynamic partitioning that happens as a side effect of the >> hardware’s cache replacement policy). This cost is generally in the >> single-digit percentage range (as per published work), but can also be >> negative – there’s plenty of work that uses static cache partitioning for >> performance *isolation/improvement*. > > Static partitioning based on _what_? On a desktop system, the dynamic > behavior > of a workload is generally the _only_ information known about that workload, > so > any partitioning _must_ be dynamic. Again, if you trust all your code to not intentionally leak secrets, then you don’t have to do this. Cache channels are very high bandwidth. Even cache side-channels have high enough bandwidth to steal encryption keys in minutes. If your threat scenario doesn’t care about this, fine. But there’s no way of preventing cache channels other than flushing or partitioning. So, it all depends on your threat scenario. If your threat scenario is that: - your hypervisor/kernel is completely trusted - all secret-handling code is trusted to - not have algorithmic timing channels - not be susceptible to control-flow attacks - be free of Trojans … then speculation attacks may be your main worry and you can ignore all the other timing channels, and you *may* be covered by (complete and properly-implemented) speculation taint tracking. That’s a lot of ifs – too many for my comfort. Note, this tracking adds a fair amount of complexity to the processor,
[seL4] Re: Conclusions regarding speculation
On 11/9/23 17:47, Gernot Heiser via Devel wrote: > On 10 Nov 2023, at 06:03, Demi Marie Obenour wrote: > > - Speculative taint tracking provides complete protection against > speculative attacks. This is sufficient to prevent leakage of > cryptographic key material, even in fully dynamic systems. > Furthermore, it is compatible with fast context switches between > protection domains. > > It’s also a point solution, that provides zero guarantees against unforeseen > attacks. Unless I am severely mistaken, it provides complete protection for code that has secret-independent timing, such as cryptographic software. It is also cheaper than some of the workarounds existing systems must use. > - Full time partitioning eliminates all timing channels, but it is > possible only in fully static systems, which severely limits its > applicability. > > I’m sorry, but this is simply false. > > What you need for time protection (I assume this is what you mean with “full > time partitioning”) are fixed time slices – ”fixed” in that their length > cannot depend on any events in the system that can be controlled by an > untrusted domain. It doesn’t mean they cannot be changed as domains come and > go. Based on what information should I set these time slices? The system I work with has no idea what workload it is running. It can’t require the workload to provide it with hints because existing workloads don’t do that. It can’t ask the user because the user will have no idea either. The most it can do is adapt based on what the workload is doing at runtime. In Qubes OS, it is completely normal for one VM (effectively a protection domain) to start using almost the entire system’s CPU resources without any warning at all. This could happen because the user just started compiling a big project. The user might then start another CPU-intensive task (such as a video call) in another VM, and that might _also_ try to use 100% of the system CPU resources. And users will expect that the CPU usage of the first workload will decrease when this happens, as some (but not all!) of the CPU time is allotted to the second workload instead. Given this constraint, I see no way to implement time protection. It _is_ possible to quantize the amount of CPU time allotted to a given vCPU, and to have a process that uses small, random amounts of CPU to generate noise. 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. > - Time protection without time partitioning does _not_ fully prevent > Spectre v1 attacks, and still imposes a large penalty on protection > domain switches. > > Time protection does *not* impose a large penalty. Its context-switching cost > is completely hidden by the cost of an L1 D-cache flush – as has been > demonstrated by published work. And if you don’t flush the L1 cache, you’ll > have massive leakage, taint-tracking or not. > > Where time protection, *without further hardware support*, does have a cost > is for partitioning the lower-level caches. This cost is two-fold: > > 1) Average cache utilisation is reduced due to the static partitioning (in > contrast to the dynamic partitioning that happens as a side effect of the > hardware’s cache replacement policy). This cost is generally in the > single-digit percentage range (as per published work), but can also be > negative – there’s plenty of work that uses static cache partitioning for > performance *isolation/improvement*. Static partitioning based on _what_? On a desktop system, the dynamic behavior of a workload is generally the _only_ information known about that workload, so any partitioning _must_ be dynamic. > 2) Memory utilisation is reduced, as colouring implicitly partitions memory. > This is the most significant cost, and unavoidable without more hardware > support. Intel CAT is one variant of such support (partitions the cache by > ways rather than set, which has not effect on memory utilisation, but only > works on the LLC, and has itself a performance cost due to reduced cache > associativity). Static memory partitioning is completely nonviable for desktop workloads. A VM might go from needing 1/16 of system RAM to requesting over half of it without any warning, and the expected behavior is that unless some other part of the system is using that RAM, the VM will get it. And yes, that does mean that two VMs can communicate by competing for system RAM, just like they can communicate by competing for CPU resources. Covert channels (ones that require cooperation from both ends) are out of scope for Qubes OS and for every other desktop system I am aware of, precisely because the cost of eliminating them is so high. > And, of course, without partitioning the lower-level caches you have leakage > again, and taint tracking isn’t going to help there either. > > If people want to improve the hardware, focussing on
[seL4] Re: Conclusions regarding speculation
"If people want to improve the hardware, focussing on generic mechanisms such as support for partitioning L2-LL caches would be far more beneficial than point-solutions that will be defeated by the next class of attacks." The path of partitioning some hardware resourse ends up in full partitioning of the computing platform including power supply. It is simpler (almost zero design effort) and the only "reasonably" secure solution. Whenever you share hardware resources, you open the path to side channels. On the other hand, PLUS full computing platform partitioning time protection is a must on each isolated computing platform. So here we have two problems that need to be addressed by different vendors: 1) Time protection, CPU/SoC vendors 2) Computing platform isolation (laptop/servers vendors). Figure out how wonderful would be to have a laptop with X full independent computing platforms inside (fun/work/banking...) and each one based on CPU/SoC solutions with Time Protection. On top of each of those platforms some verified hypervisor/kernel (seL4?). BTW, the step 2 is straight forward, just make laptops a bit bigger and add a screen swich to switch each isolated computing platform. Step 1 requires cpu/SoC vendors more effort and there will be some resilience to sell it. El jue., 9 nov. 2023 23:51, Gernot Heiser via Devel escribió: > On 10 Nov 2023, at 06:03, Demi Marie Obenour > wrote: > > - Speculative taint tracking provides complete protection against > speculative attacks. This is sufficient to prevent leakage of > cryptographic key material, even in fully dynamic systems. > Furthermore, it is compatible with fast context switches between > protection domains. > > It’s also a point solution, that provides zero guarantees against > unforeseen attacks. > > - Full time partitioning eliminates all timing channels, but it is > possible only in fully static systems, which severely limits its > applicability. > > I’m sorry, but this is simply false. > > What you need for time protection (I assume this is what you mean with > “full time partitioning”) are fixed time slices – ”fixed” in that their > length cannot depend on any events in the system that can be controlled by > an untrusted domain. It doesn’t mean they cannot be changed as domains come > and go. > > - Time protection without time partitioning does _not_ fully prevent > Spectre v1 attacks, and still imposes a large penalty on protection > domain switches. > > Time protection does *not* impose a large penalty. Its context-switching > cost is completely hidden by the cost of an L1 D-cache flush – as has been > demonstrated by published work. And if you don’t flush the L1 cache, you’ll > have massive leakage, taint-tracking or not. > > Where time protection, *without further hardware support*, does have a > cost is for partitioning the lower-level caches. This cost is two-fold: > > 1) Average cache utilisation is reduced due to the static partitioning (in > contrast to the dynamic partitioning that happens as a side effect of the > hardware’s cache replacement policy). This cost is generally in the > single-digit percentage range (as per published work), but can also be > negative – there’s plenty of work that uses static cache partitioning for > performance *isolation/improvement*. > > 2) Memory utilisation is reduced, as colouring implicitly partitions > memory. This is the most significant cost, and unavoidable without more > hardware support. Intel CAT is one variant of such support (partitions the > cache by ways rather than set, which has not effect on memory utilisation, > but only works on the LLC, and has itself a performance cost due to reduced > cache associativity). > > And, of course, without partitioning the lower-level caches you have > leakage again, and taint tracking isn’t going to help there either. > > If people want to improve the hardware, focussing on generic mechanisms > such as support for partitioning L2-LL caches would be far more beneficial > than point-solutions that will be defeated by the next class of attacks. > > Gernot > ___ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems > ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: Conclusions regarding speculation
On 10 Nov 2023, at 06:03, Demi Marie Obenour wrote: - Speculative taint tracking provides complete protection against speculative attacks. This is sufficient to prevent leakage of cryptographic key material, even in fully dynamic systems. Furthermore, it is compatible with fast context switches between protection domains. It’s also a point solution, that provides zero guarantees against unforeseen attacks. - Full time partitioning eliminates all timing channels, but it is possible only in fully static systems, which severely limits its applicability. I’m sorry, but this is simply false. What you need for time protection (I assume this is what you mean with “full time partitioning”) are fixed time slices – ”fixed” in that their length cannot depend on any events in the system that can be controlled by an untrusted domain. It doesn’t mean they cannot be changed as domains come and go. - Time protection without time partitioning does _not_ fully prevent Spectre v1 attacks, and still imposes a large penalty on protection domain switches. Time protection does *not* impose a large penalty. Its context-switching cost is completely hidden by the cost of an L1 D-cache flush – as has been demonstrated by published work. And if you don’t flush the L1 cache, you’ll have massive leakage, taint-tracking or not. Where time protection, *without further hardware support*, does have a cost is for partitioning the lower-level caches. This cost is two-fold: 1) Average cache utilisation is reduced due to the static partitioning (in contrast to the dynamic partitioning that happens as a side effect of the hardware’s cache replacement policy). This cost is generally in the single-digit percentage range (as per published work), but can also be negative – there’s plenty of work that uses static cache partitioning for performance *isolation/improvement*. 2) Memory utilisation is reduced, as colouring implicitly partitions memory. This is the most significant cost, and unavoidable without more hardware support. Intel CAT is one variant of such support (partitions the cache by ways rather than set, which has not effect on memory utilisation, but only works on the LLC, and has itself a performance cost due to reduced cache associativity). And, of course, without partitioning the lower-level caches you have leakage again, and taint tracking isn’t going to help there either. If people want to improve the hardware, focussing on generic mechanisms such as support for partitioning L2-LL caches would be far more beneficial than point-solutions that will be defeated by the next class of attacks. Gernot ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
