How to escape from your sandbox and from your hardware host

Hmm. Papers [2] and [3] demonstrate an attack starting from a position of executing native code; [4] I didn't read until just now, and that's the one that works within Javascript's semantics.

They had three test machines: a Sandy Bridge laptop, an Ivy Bridge laptop, and a Haswell desktop. The Sandy Bridge laptop seems to have only been used for studying its cache-eviction policy, they don't report a result (positive or negative) for getting it to flip bits. They studied three memory-corruption strategies: in descending order of strength, clflush, evict (native), and evict (JavaScript). The first strategy (clflush) is the previously-discussed strategy using cache-flush instructions, which can only be done from native code with a highly unusual instruction mix. The two evict strategies work by making a pattern of memory accesses which interacts with the processor's caching rules. The clflush version requires executing native code; the evict strategies work if the code is JITted.

All three strategies worked against the Ivy Bridge test machine. None of the strategies worked against the Haswell test machine. (They note that Lenovo released a BIOS update which decreases the memory refresh interval, which would likely make it resistant, which they didn't test). They then went on to change the Haswell's memory refresh interval in the BIOS settings, and compared the rate of bit flips with the three different strategies at different memory refresh intervals (figs. 4 and 5). The eviction-based strategies start causing bit flips at a refresh interval that's slightly more than twice as long as the clflush based strategies; the native and Javascript evict-based strategies started producing bit flips at very close to the same refresh interval.

They did not build a root exploit out of the Javascript version, and to get bit flips at all, they used a modified Javascript interpreter which provides an inverted page table. This is a fairly substantial cheat. They think they could make a root exploit out of this, and I believe them, but the difficulty is quite a lot higher than the clflush-based version and it has not in fact been accomplished.

So to summarize - code running through a JITter is in fact at a large disadvantage when trying to exploit you, just not quite so large a disadvantage that you should feel invulnerable. Stepping back to the bigger picture, assuming RowHammer will be fixed but other vulnerabilities will remain, I expect that language semantics-based sandboxing will protect from many, likely most, but not quite all of them.

A fancy way of saying "don't have a wire or path of wires leading to the internet".

provably secure software mechanisms rely on an idealized model of hardware

In my experience, they also define an attacker model against which to secure. There are no guarantees against attackers with greater access, or abilities, than specified in the model.

I have yet to see any claims of a "secure" system that doesn't state the assumptions and validations of the hardware involved. It may be only my world, but a whole lot of attention is paid to the various boundaries between containers (sandbox, VM, virtualized host, physical host, cluster, airgap), not just to the inner level.

Mostly, "provably secure" means all layers, unless there's a fair bit of fine print with it.

So we can conclude that although David was smart enough to escape his sandbox, he isn't yet at the level of understanding human-style humor.

I don't think the "homomorphic encryption" idea works as advertised in that post--being able to execute arithmetic operations on encrypted data doesn't enable you to execute the operations that are encoded within that encrypted data.

A fully homomorphic encryption scheme for single-bit plaintexts (as in Gentry's scheme) gives us:

• For each public key K a field F with efficient arithmetic operations +F and *F.
• Encryption function E(K, p) = c: p∈{0,1}, c∈F
• Decryption function D(S, c) = p: p∈{0,1}, c∈F where S is the secret key for K.
• Homomorphisms E(K, a) +F E(K, b) = E(K, a ⊕ b) and E(K, a) F E(K, b) = E(K, a b)
• a ⊕ b equivalent to XOR over {0,1} and a * b equivalent to AND over {0,1}

Boolean logic circuits of arbitrary depth can be built from the XOR and AND equivalents allowing computation of arbitrary binary functions. Let M∈{0,1}^N be a sequence of bits representing the state of a bounded UTM with an arbitrary program on its tape. Let binary function U(M): {0,1}^N -> {0,1}^N compute the next state of M. Let E(K, B) and D(S, E) also operate element-wise over sequences of bits and elements of F, respectively. Let UF be the set of logic circuits equivalent to U (UFi calculates the ith bit of U's result) but with XOR and AND replaced by +F and *F. Now D(S, UF^t(E(K, M)) = U^t(M) shows that an arbitrary number of UTM steps can be calculated homomorphically by evaluating equivalent logic circuits over the homomorphically encrypted bits of the state.