3 ms·

So it turns out that the attack "was possible due to the discrepancy between the proof of OCB2 and the actual construction" (according to the paper). That's a

So it turns out that the attack "was possible due to the discrepancy between the proof of OCB2 and the actual construction" (according to the paper). That's a scary thought. I wanted to learn a little bit more about progress towards verified implementations (i.e. deriving the implementation automatically from its proof) and found a nice summary here: https://crypto.stackexchange.com/questions/34304/formal-verification-in-cryptography/34326#34326 https://crypto.stackexchange.com/questions/34304/formal-veri...

hyperpallium 8y ago
This is what makes me so uncomfortable about numerical computing (e.g. CFD): how do you know you got it right? If you implement a fluid simulation, it might look right... but is it right? Of course, there's proof assistants etc that can construct an implementation, but even in this cryptography context, where it's desperately worth it, they're too difficult/too much work. Unless you really understand the maths deeply, it's difficult to be sure you got it right (and even if you do). Especially when it's not easily decomposable into independently verifiable modules. The funny thing is, when you write straightforward code, and try it a few times (even, enshrine those as "tests"), you will feel that it is right. But there's not really that much certainty that you really did get it right. Leading me to believe the crucial thing isn't how difficult it is to get it right, but how much it matters. Software "bug reports" are ubiquitous. Not so for cryptography!
- kiwidrew 8y ago
  > This is what makes me so uncomfortable about numerical computing (e.g. CFD): how do you know you got it right? Indeed. Lack of associativity and distributivity when working with floating point numbers gives the whole thing a feeling of spooky witchcraft. It's precisely the same feeling that I get from Javascript and PHP's weird notions of equality ("==" vs "===").
- mannykannot 8y ago
  It is not my field, but I would guess that in the case of computational physics, the need for the results to be realistic (conforming to conservation and thermodynamic laws, for example) would help in verification.

hyperpallium 8y ago

This is what makes me so uncomfortable about numerical computing (e.g. CFD): how do you know you got it right? If you implement a fluid simulation, it might look right... but is it right? Of course, there's proof assistants etc that can construct an implementation, but even in this cryptography context, where it's desperately worth it, they're too difficult/too much work. Unless you really understand the maths deeply, it's difficult to be sure you got it right (and even if you do). Especially when it's not easily decomposable into independently verifiable modules. The funny thing is, when you write straightforward code, and try it a few times (even, enshrine those as "tests"), you will feel that it is right. But there's not really that much certainty that you really did get it right. Leading me to believe the crucial thing isn't how difficult it is to get it right, but how much it matters. Software "bug reports" are ubiquitous. Not so for cryptography!

kiwidrew 8y ago
> This is what makes me so uncomfortable about numerical computing (e.g. CFD): how do you know you got it right? Indeed. Lack of associativity and distributivity when working with floating point numbers gives the whole thing a feeling of spooky witchcraft. It's precisely the same feeling that I get from Javascript and PHP's weird notions of equality ("==" vs "===").
mannykannot 8y ago
It is not my field, but I would guess that in the case of computational physics, the need for the results to be realistic (conforming to conservation and thermodynamic laws, for example) would help in verification.