In fact you can perform a birthday attack, which costs on the order of 2^16 calls with n=32. I'm surprised the researchers don't mention this: they're handwaving counter-attacks away because of the "very good digital post-processing, namely AES", but since they use a fixed key it's not actually very powerful.
However, the attack is essentially undetectable with n=128, and it can still be very useful because they force the AES key to be constant: between two reseedings of the conditioner, the output of RDRAND will be entirely deterministic and computable by the attacker. According to http://www.cryptography.com/public/pdf/Intel_TRNG_Report_201... , under heavy load there could be up to 44 64-bit outputs between consecutive reseedings, even assuming a healthy entropy source. The first 2 outputs are unpredictable, and the remaining (up to) 42 outputs can be predicted by the attacker.
Imagine a scenario where a malicious sandboxed application uses the random generator to monitor RDRAND output, while another application generates a cryptographic key. I think that according to Intel, this is safe because RDRAND is designed to be resistant to malicious processes (see the above paper). But if the n=128 attack is used, the malicious process can detect with high reliability when another process uses RDRAND, and can recover the value received by the other process (the exception is that if another process uses RDRAND just before a reseed, it can't be detected). For a 256-bit key and maximal load, that's a 90%+ chance of recovering the key. All with just a simple sandboxed binary.
And I think the broader point of the researchers is not about any particular attack, which can indeed be countered by specific countermeasures: it's that we now know that it's easy to maliciously alter any chip design to add various vulnerabilities, and it's probably going to be very difficult for any chip designer to predict what vulnerabilities this will introduce. I think RDRAND was chosen just because design details were made publicly available by Intel, not because it's the most interesting target. The paper gives another interesting example, which enables side-channel attacks in a side-channel-resistant chip.
> they are using unsigned 64-bit values (which conveniently have defined overflow semantics) for the lengths of the input buffer.
Yes, if you examine the code you can manually prove that it's safe: but that's not proven by their formal computer-checked proof.
As for the rest of your post: you seem to be assuming that what they proved is that b64enc.c behaves correctly. This is not true at all: they just proved that the helper function base64_encode() works correctly for a specific size (this is done in proof/sym_encode.c). This helper function never calls base64_encode_update() twice and is not used by b64enc.c, and that's why we don't know if the multiple-block implementation from b64enc.c actually behaves correctly.
> No variation of the gravitational constant is discernible, (dG/dt) / G = (0.0±1.1)x10–12 /yr
If we're obsessing over details, I'm wondering if 0.0 is indeed the center of the confidence interval, or if this is just a way to say they have bounded |G'/G|. The cited paper ("Lunar laser tests of gravitational physics") just states the result without giving much detail.
It's a flaw in the specification of the theorem, not in the verification.
The way it works is that they choose fixed sizes INLEN and OUTLEN, and prove that when data points to a buffer of INLEN bytes, they can allocate a result buffer and base64_encode(data, INLEN, result) will compute the correct encoding.
So, implied in this statement is the fact that the input buffer is valid (thus not null), and that the output buffer must be valid (and not null) and disjoint from the input buffer.
There are more fundamental classes of bugs that this won't detect:
- behavior for arbitrary sizes, such as integer overflows for large sizes
- bugs when using particular functions of the API, such as base64_encode_update()
The latter problem means that there is no proof that b64enc.c is correct at all, even for a fixed size: it's entirely possible that multiple calls to base64_encode_update() would corrupt the internal state.
It's pretty impressive that this can be done completely automatically (model checking), although the price to pay is that he can only prove the implementation for a fixed input size.
I'm very curious about what would happen if he dropped the safety check in base64_encode_value(). It would probably speed things up a little, but would the proof fail?
However, the attack is essentially undetectable with n=128, and it can still be very useful because they force the AES key to be constant: between two reseedings of the conditioner, the output of RDRAND will be entirely deterministic and computable by the attacker. According to http://www.cryptography.com/public/pdf/Intel_TRNG_Report_201... , under heavy load there could be up to 44 64-bit outputs between consecutive reseedings, even assuming a healthy entropy source. The first 2 outputs are unpredictable, and the remaining (up to) 42 outputs can be predicted by the attacker.
Imagine a scenario where a malicious sandboxed application uses the random generator to monitor RDRAND output, while another application generates a cryptographic key. I think that according to Intel, this is safe because RDRAND is designed to be resistant to malicious processes (see the above paper). But if the n=128 attack is used, the malicious process can detect with high reliability when another process uses RDRAND, and can recover the value received by the other process (the exception is that if another process uses RDRAND just before a reseed, it can't be detected). For a 256-bit key and maximal load, that's a 90%+ chance of recovering the key. All with just a simple sandboxed binary.
And I think the broader point of the researchers is not about any particular attack, which can indeed be countered by specific countermeasures: it's that we now know that it's easy to maliciously alter any chip design to add various vulnerabilities, and it's probably going to be very difficult for any chip designer to predict what vulnerabilities this will introduce. I think RDRAND was chosen just because design details were made publicly available by Intel, not because it's the most interesting target. The paper gives another interesting example, which enables side-channel attacks in a side-channel-resistant chip.