Applications of Mark Miller's thesis to Meltdown/Spectre

[Tony Arcieri]

I can't help but be reminded of Mark Miller's thesis in the wake of Meltdown/Spectre, and wonder about how new approaches to protection domains at the hardware level, perhaps based around an every-word-tagged memory architecture, could prevent these sorts of vulnerabilities by strategically eliminating the entire bugclass.

Very curious what Mark thinks about this, and also Carl as the enthusiastic proponent of "every word tagged" memory architectures.

Perhaps I'll even call into the meeting tomorrow ;)

--

Tony Arcieri

[Dan Connolly]

Side channel attacks like these are particularly scary to me because ocaps, at least in the form of SES or E, don't help. I doubt even seL4 helps.

I was never a fan of x86, but sufficient market forces to replace it look very, very remote. I don't want to pin my hopes on that.

Hmm... perhaps not _so_ remote... mobile passed desktop in various measures a few years ago, and x86 doesn't dominate there...

p.s. the CPU in my first machine was a 6809E and I have never gotten comfortable with relocating linkers...

The 6809 design also focused on supporting reentrant code, code that can be called from various different programs concurrently without concern for coordination between them, or that can recursively call itself.^[4] The design team's prediction was, in reality, incorrect, as the market for ROM modules never materialized: Motorola's only released example of a ROM'd software module was the MC6839 floating-point ROM. (The industry solved the problem of integrating code modules from multiple separate sources by using automatic relocating linkers and loaders—which is still the solution used today—instead of using relocatable ROM modules.) However, the decisions made by the design team yielded a very powerful processor and made possible advanced operating systems like OS-9 and UniFlex, which took advantage of the position-independence, re-entrancy orientated nature of the 6809 to create multi-user multitasking operating systems.

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+unsubscribe@googlegroups.com.
To post to this group, send email to fr...@googlegroups.com.
Visit this group at https://groups.google.com/group/friam.
For more options, visit https://groups.google.com/d/optout.

--

Dan Connolly

http://www.madmode.com/

[Dan Connolly]

Re genode and seL4, there may be some good news:

> * In contrast to monolithic kernels, a microkernel like base-hw, NOVA,
> or seL4 does not deal with any user-level content like cryptographic
> secrets, or the content of files.
>
> In contrast to the Linux kernel, which contains a JIT-based VM in
> the form of the Berkeley Packet Filter, there is no way to
> deliberately inject certain code patterns into a microkernel.

But also:
> It is currently unclear to me, in which ways an
> attacker may exploit this meta data. But given the creativity of
> attackers, we should be pessimistic.

https://sourceforge.net/p/genode/mailman/message/36178974/

>> email to friam+un...@googlegroups.com.

[Tony Arcieri]

On Fri, Jan 5, 2018 at 7:12 PM, Dan Connolly <dc...@madmode.com> wrote:

Side channel attacks like these are particularly scary to me because ocaps, at least in the form of SES or E, don't help. I doubt even seL4 helps.

There was some interesting discussion around that on the seL4 list. While Meltdown/Spectre were still embargoed people on the list were hoping seL4 wouldn't be vulnerable because it doesn't run untrusted code in kernel mode ala BPF/eBPF. But as the details came out it became clear seL4 would be impacted as well. They are presently working on a Meltdown fix. I'm curious if that will involve the whole cycle of implementing it in Haskell, updating their Isabelle proofs to demonstrate the Haskell is correct, updating the C, then proving the C equivalent to the Haskell. If so, wonder how long that will all take.

Clearly good software won't save you from bad hardware. But that's why I was interested in capabilities at the hardware level: the source of the side-channel is the CPU speculating beyond protection domains. One way to close the side-channel is making it impossible for this to happen at a hardware level, e.g. access to memory is gated at the circuit level by a synchronous access check which requires capabilities which are sealed/erased/hidden when the kernel drops to a lower privilege level. Checks similar to this already exist in e.g. RISC-V.

The protection domains in use by most other CPU architectures today feel like several extremely complicated systems coordinating to enforce a logical model, all within a highly concurrent system doing very complicated things like speculative execution, out-of-order execution, etc. Bad interactions with these parts of the CPU and the multitude of access control enforcement mechanisms lead to unforeseen circumstances where the CPU was speculating outside of the logical protection domains. The lack of a unified, physically enforced access control model in a complicated concurrent system seems like a recipe for disaster.

I was never a fan of x86, but sufficient market forces to replace it look very, very remote. I don't want to pin my hopes on that.

I'm not sure we'll see a bona fide x86 replacement any time soon, but as Apple's T1 and T2 chips have demonstrated you can do a lot of interesting things with a security-oriented companion processor, and if you have a secure place to keep your secrets outside of the primary CPU, the insecurity of x86 matters less. It'd also be generally nice to have a security-oriented CPU that performs in the same ballpark as x86 for those willing to go off the beaten path ISA-wise in hopes of building more secure systems.

I think RISC-V is in a great position to implement next-generation speculative execution features which leverage the existing capability-esque protections to allow for "safe speculation". Right now pretty much all RISC-V CPUs are "immune" to Meltdown/Spectre because they do not have any speculative execution features. However, adding speculative execution to RISC-V is an open research area and presently being worked on. They have a great foundation and are now greenfielding these features with 20/20 hindsight of what went wrong in previous CPUs.

Maybe they'll be able to pull it off securely. 

--

Tony Arcieri

[Chris Hibbert]

https://xkcd.com/1938/

Conclusion: Install updates to your software. :-)

Chris
--
protecting privacy in the computer age is
like trying to change a tire on a moving car.
--Colin Bennett

Chris Hibbert
hib...@mydruthers.com
Blog: http://www.pancrit.org
http://mydruthers.com

[Raoul Duke]

that ol' adage to live by, "First, make it fast. Then, under public/economic duress, patch like hell to make it appear like you also care about it being right."

[Bill Frantz]

On 1/6/18 at 11:24 PM, dc...@madmode.com (Dan Connolly) wrote:

>But also:
>>It is currently unclear to me, in which ways an
>>attacker may exploit this meta data. But given the creativity of
>>attackers, we should be pessimistic.
>
>https://sourceforge.net/p/genode/mailman/message/36178974/

Genode seems to be like CapROS in keeping most normal OS
functions out of the kernel. (I had not heard of it before.) I
couldn't quickly figure out if it runs with user pages
accessable in the kernel map or unmapped. If it runs in either
of these modes, then the Meltdown attack can be used to read
secrets from user pages.

Given the work down to identify cryptographic keys in memory
dumps -- they have higher entropy than normal data -- there may
be a problem.

Cheers - Bill

-------------------------------------------------------------------------
Bill Frantz | When it comes to the world | Periwinkle
(408)356-8506 | around us, is there any choice | 16345
Englewood Ave
www.pwpconsult.com | but to explore? - Lisa Randall | Los Gatos,
CA 95032

[Tony Arcieri]

On Sat, Jan 6, 2018 at 9:03 AM, Tony Arcieri <bas...@gmail.com> wrote:

I think RISC-V is in a great position to implement next-generation speculative execution features which leverage the existing capability-esque protections to allow for "safe speculation". Right now pretty much all RISC-V CPUs are "immune" to Meltdown/Spectre because they do not have any speculative execution features. However, adding speculative execution to RISC-V is an open research area and presently being worked on. They have a great foundation and are now greenfielding these features with 20/20 hindsight of what went wrong in previous CPUs.

Seems like the RISC-V foundation agrees! (and also confirms no RISC-V CPUs are vulnerable) 

https://riscv.org/2018/01/more-secure-world-risc-v-isa/

"The RISC-V community has an historic opportunity to 'do security right' from the get-go with the benefit of up-to-date knowledge."

--

Tony Arcieri

[Bill Frantz]

This 2007 rant about processor bugs from Theo de Raadt is worth reading:
<https://marc.info/?l=openbsd-misc&m=118296441702631&w=2>

I haven't heard that modern processors are more bug free than
the ones of 10 years ago.

The Mill might be better than other CISC processors since it
depends on the compiler to do the cache preloads.

Cheers - Bill

---------------------------------------------------------------------------
Bill Frantz | Re: Computer reliability, performance, and security:
408-356-8506 | The guy who *is* wearing a parachute is
*not* the
www.pwpconsult.com | first to reach the ground. - Terence Kelly

[Mark Miller]

Hi Tony, I finally feel ready to start answering your question. Here's Part 1:

I often find the standard top-level taxonomy of security useful; the division into integrity, confidentiality, and availability. A basic engineering principle I learned from KeyKOS, that AFAIK is followed by everything in the KeyKOS family including seL4, and that we followed in E, Joe-E, Caja, and Dr.SES:

    Whenever possible, integrity should not depend on confidentiality.

Further, for interactions between mutually suspicious entities sharing a mutually trusted platform, such as a single machine, this is always possible. In that context, the recommendation becomes an absolute:

   (Among things on a shared TCB)

   Integrity must never depend on confidentiality

The Gedanken experiment that I've used to think about this is:

   Start with a KeyKOS system. Now imagine we add to the architecture a user-mode instruction for reading any word of physical memory. On such a system, it is no longer possible to keep secrets, so cryptography is impossible. But among processes running on one shared KeyKOS kernel, integrity is not compromised in the slightest.

In my previous discussion of this Gedanken experiment, I missed the issue of login authentication. The strong statement is still correct, in that it is an interaction with suspicious agents outside the shared TCB, i.e., an alleged human at a keyboard. However, this is not an avoidable problem for the utility of KeyKOS as originally conceived.

This separation was mostly implicit in the local E design, but I cannot think of any exceptions. I think local E follows this perfectly.

This separation became explicit during the Joe-E design, where we were careful about the principle:

    None of Joe-E's security claims depends on any party's lack of knowledge. Even if any party might be omniscient, all Joe-E's security claims would still hold.

For local E, with one exception, all my strong claims have been about integrity only. I knew that E was not in a position to make strong claims about availability. With one exception, I knew that E was not in a position to make claims about confidentiality. Least authority and defensive consistency are only about integrity. See section 5.7 of my thesis "A Practical Standard for Defensive Programming" for the criteria used for the claims "By convention, unless stated otherwise, E and its libraries are engineered to achieve and support the following forms of robustness. The examples and mechanisms presented in this dissertation should be judged by this standard as well."

The one exception, which I don't think is anywhere mentioned in the thesis, E is designed to support "loggable fail-stop non-determinism". This means that the spawner of a confined E computation can ensure that two runs of the same computation, from the same logs of inputs, if neither fails, must take the same conditional branches and produce the same overt outputs. E does allow non-deterministic failure, such as by memory exhaustion, where one replica might fail while another does not. This property enables some claims about confidentiality:

Such computation cannot read non-overt (covert and side) channels, unless those channels are already encoded into its loggable inputs. In other words, the confiner knows that they only need to worry about the same inputs that the confiner knows to worry about logging.

These new attacks, Meltdown and Spectre, are a closer approximation to my KeyKOS Gedanken experiment than anything I ever imagined might be possible. However, the attacks directly only reveal information, and only to those that can somehow measure time. These attacks are severe! Although for local E, I avoided making a strong confidentiality claims that are invalidated by these attacks, I certainly built E to achieve a measure of confidentiality that now needs to be re-evaluated. I am not in any realistic sense claiming that local E is practically immune to these attacks. But I do find it very satisfying that this stratification of security claims was robust against this unexpected class of new attacks.

Distributed E of course depends on cryptography. Due to the influence of client utility, live distributed E uses the distributed c-list technique, which avoids depending on the unguessability of *transmitted* secrets, i.e., swiss numbers. However, the transition from offline to live does depend on this: for dereferencing either captp uris or sturdy refs. CapCert was never implemented, but like SPKI/SDSI, never depends on the unguessability of transmitted secrets, period. I believe that E's captp uris and sturdy refs could be replaced with something more like the CapCert introduction, but I have not explored it. Possibly, client utility already demonstrates a logically equivalent case. Alan?

--

  Cheers,
  --MarkM

[Alan Karp]

As I recall, Client Utility could have accepted a certificate as the credential used to establish a connection, but I don't believe it was ever implemented. The E-speak product did, however.

--------------
Alan Karp

--

You received this message because you are subscribed to the Google Groups "friam" group.

To unsubscribe from this group and stop receiving emails from it, send an email to friam+unsubscribe@googlegroups.com.

[Bill Frantz]

Current Distributed E depends on the secrecy of it's VAT's
private key. If that key were in an enclave or preferably in a
separate computer, it might be possible to keep it secret even
in the fact of Meltdown and Spectre style attacks. (I worry
about enclaves since they share physical elements with the main
CPU and we now know there are serious bugs in current CPUs.)

Since we still have integrity, we can control which parts of the
E system can have things signed by the separate computer. Since
it doesn't have the private key in shared memory, that key is
still protected.

The SPKI kind of capability might be in the correct direction.

Cheers - Bill

-----------------------------------------------------------------------
Bill Frantz | There's nothing so clear as | Periwinkle
(408)356-8506 | a design you haven't written | 16345
Englewood Ave
www.pwpconsult.com | down. - Dean Tribble | Los Gatos,
CA 95032

[Mark Miller]

On Tue, Jan 9, 2018 at 1:42 PM, Mark Miller <eri...@gmail.com> wrote:

Hi Tony, I finally feel ready to start answering your question. Here's Part 1:

I often find the standard top-level taxonomy of security useful; the division into integrity, confidentiality, and availability. A basic engineering principle I learned from KeyKOS, that AFAIK is followed by everything in the KeyKOS family including seL4, and that we followed in E, Joe-E, Caja, and Dr.SES:

    Whenever possible, integrity should not depend on confidentiality.

Further, for interactions between mutually suspicious entities sharing a mutually trusted platform, such as a single machine, this is always possible. In that context, the recommendation becomes an absolute:

   (Among things on a shared TCB)

   Integrity must never depend on confidentiality

The Gedanken experiment that I've used to think about this is:

   Start with a KeyKOS system. Now imagine we add to the architecture a user-mode instruction for reading any word of physical memory. On such a system, it is no longer possible to keep secrets, so cryptography is impossible.

Correction. Even on a system that's fully transparent, like this Gedanken experiment, there is still one form of cryptography that still works. Cryptographic hashes. Cryptohashes still depend on unguessability: the infeasability to guess another plaintext that hashes to the same hash value. Cryptohashes would be destroyed by a hypothetical technology that gave us vast computational speedups of everything (as some people mistakenly worry quantum computation might do). But cryptohashes are not destroyed by transparency, because the secret that must remain unguessable is a secret that no one and no thing ever knew.

(Thanks Mike Samuel for triggering this insight)

Thus, such uses of cryptohashes are still robust in the face of meltdown and spectre.

 

But among processes running on one shared KeyKOS kernel, integrity is not compromised in the slightest.

In my previous discussion of this Gedanken experiment, I missed the issue of login authentication. The strong statement is still correct, in that it is an interaction with suspicious agents outside the shared TCB, i.e., an alleged human at a keyboard. However, this is not an avoidable problem for the utility of KeyKOS as originally conceived.

This separation was mostly implicit in the local E design, but I cannot think of any exceptions. I think local E follows this perfectly.

This separation became explicit during the Joe-E design, where we were careful about the principle:

    None of Joe-E's security claims depends on any party's lack of knowledge. Even if any party might be omniscient, all Joe-E's security claims would still hold.

For local E, with one exception, all my strong claims have been about integrity only. I knew that E was not in a position to make strong claims about availability. With one exception, I knew that E was not in a position to make claims about confidentiality. Least authority and defensive consistency are only about integrity. See section 5.7 of my thesis "A Practical Standard for Defensive Programming" for the criteria used for the claims "By convention, unless stated otherwise, E and its libraries are engineered to achieve and support the following forms of robustness. The examples and mechanisms presented in this dissertation should be judged by this standard as well."

The one exception, which I don't think is anywhere mentioned in the thesis, E is designed to support "loggable fail-stop non-determinism". This means that the spawner of a confined E computation can ensure that two runs of the same computation, from the same logs of inputs, if neither fails, must take the same conditional branches and produce the same overt outputs. E does allow non-deterministic failure, such as by memory exhaustion, where one replica might fail while another does not. This property enables some claims about confidentiality:

Such computation cannot read non-overt (covert and side) channels, unless those channels are already encoded into its loggable inputs. In other words, the confiner knows that they only need to worry about the same inputs that the confiner knows to worry about logging.

These new attacks, Meltdown and Spectre, are a closer approximation to my KeyKOS Gedanken experiment than anything I ever imagined might be possible. However, the attacks directly only reveal information, and only to those that can somehow measure time. These attacks are severe! Although for local E, I avoided making a strong confidentiality claims that are invalidated by these attacks, I certainly built E to achieve a measure of confidentiality that now needs to be re-evaluated. I am not in any realistic sense claiming that local E is practically immune to these attacks. But I do find it very satisfying that this stratification of security claims was robust against this unexpected class of new attacks.

Distributed E of course depends on cryptography. Due to the influence of client utility, live distributed E uses the distributed c-list technique, which avoids depending on the unguessability of *transmitted* secrets, i.e., swiss numbers. However, the transition from offline to live does depend on this: for dereferencing either captp uris or sturdy refs. CapCert was never implemented, but like SPKI/SDSI, never depends on the unguessability of transmitted secrets, period. I believe that E's captp uris and sturdy refs could be replaced with something more like the CapCert introduction, but I have not explored it. Possibly, client utility already demonstrates a logically equivalent case. Alan?

--

  Cheers,
  --MarkM

--

  Cheers,
  --MarkM

[Mike Stay]

On Tue, Jan 23, 2018 at 8:13 PM, Mark Miller <eri...@gmail.com> wrote:
> Correction. Even on a system that's fully transparent, like this Gedanken
> experiment, there is still one form of cryptography that still works.
> Cryptographic hashes. Cryptohashes still depend on unguessability: the
> infeasability to guess another plaintext that hashes to the same hash value.
> Cryptohashes would be destroyed by a hypothetical technology that gave us
> vast computational speedups of everything (as some people mistakenly worry
> quantum computation might do). But cryptohashes are not destroyed by
> transparency, because the secret that must remain unguessable is a secret
> that no one and no thing ever knew.
>
> (Thanks Mike Samuel for triggering this insight)
>
> Thus, such uses of cryptohashes are still robust in the face of meltdown and
> spectre.

This kind of transparent system is precisely the situation we've got
with computations on the RChain blockchain. We can do hashes,
signature verification, and encrypting under a public key. Because we
have unforgeability, we can use sealers and unsealers, but the
contents of a sealed box are visible, so we can still only do the
operations corresponding to signature verification and encrypting
under a public key. I suppose it's technically possible to do fully
homomorphic encryption if you keep the keys off chain, but even with
recent advances it's still terribly slow.

This remains my favorite way of protecting code from reverse
engineering: https://www.youtube.com/watch?v=HlUe0TUHOIc
--
Mike Stay - meta...@gmail.com
http://www.math.ucr.edu/~mike
http://reperiendi.wordpress.com

[Mark S. Miller]

Hi Mike, yes. Computation replicated on public blockchains is transparent in just this way. Computation written to run securely for this transparency worst case will remain secure when run on normal hardware, non replicated, under normal tcb assumptions modified for worst case worries about Meltdown and Spectre.

The parallelism is fascinating!