3 ms·

The rabbit hole goes deeper: how are you sure the compiler is correct? See the paper by John Regehr and his group: http://blog.regehr.org/archives/492 http://bl

by scott_s 11y ago

The rabbit hole goes deeper: how are you sure the compiler is correct? See the paper by John Regehr and his group: http://blog.regehr.org/archives/492 http://blog.regehr.org/archives/492 I'm not just saying this randomly in any subject that is concerned with correctness, as Regehr's work clearly shows that the places where compilers make the most mistakes are the places that cryptographic functions play in: numeric calculations at the boundaries of what is representable. I also want to point out that Lipton's first suggestion is to basically have very smart unit tests - which is a good suggestion. If your result should have known properties, test those.

th0ma5 11y ago
... And then how do we know the CPU's microcode executing these instructions is correct? The tests may reproduce the same error.
- scott_s 11y ago
  It's a valid question, but hardware has much more formal verification than software.
  - _asummers 11y ago
    Modern CPUs do not necessarily correlate assembly to exact machine instructions, due to things like pipelining. [0][1] [0] http://blog.erratasec.com/2015/03/x86-is-high-level-language.html http://blog.erratasec.com/2015/03/x86-is-high-level-language... [1] https://news.ycombinator.com/item?id=9264195 https://news.ycombinator.com/item?id=9264195
    - scott_s 11y ago
      This is true, but not an issue when it comes to this issue. All of that falls under the formal verification for processors.
im3w1l 11y ago
>numeric calculations at the boundaries of what is representable. That sounds like floating point instructions, and cryptography uses integer instructions.
- scott_s 11y ago
  Actually, it's mostly integer instructions. Regehr even has a related post, "Integer Undefined Behaviors in Open Source Crypto Libraries": http://blog.regehr.org/archives/1054 http://blog.regehr.org/archives/1054 His blog, academic papers, and the paper I linked, have lots of discussions about integer issues.
np422 11y ago
Turing award lecture by Ken Thompson, "Reflections on trusting trust". Recommended if you haven't read it already. https://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thompson.pdf https://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thomp...

by scott_s 11y ago

th0ma5 11y ago

... And then how do we know the CPU's microcode executing these instructions is correct? The tests may reproduce the same error.

scott_s 11y ago
It's a valid question, but hardware has much more formal verification than software.
- _asummers 11y ago
  Modern CPUs do not necessarily correlate assembly to exact machine instructions, due to things like pipelining. [0][1] [0] http://blog.erratasec.com/2015/03/x86-is-high-level-language.html http://blog.erratasec.com/2015/03/x86-is-high-level-language... [1] https://news.ycombinator.com/item?id=9264195 https://news.ycombinator.com/item?id=9264195
  - scott_s 11y ago
    This is true, but not an issue when it comes to this issue. All of that falls under the formal verification for processors.

im3w1l 11y ago

>numeric calculations at the boundaries of what is representable. That sounds like floating point instructions, and cryptography uses integer instructions.

scott_s 11y ago
Actually, it's mostly integer instructions. Regehr even has a related post, "Integer Undefined Behaviors in Open Source Crypto Libraries": http://blog.regehr.org/archives/1054 http://blog.regehr.org/archives/1054 His blog, academic papers, and the paper I linked, have lots of discussions about integer issues.

np422 11y ago

Turing award lecture by Ken Thompson, "Reflections on trusting trust". Recommended if you haven't read it already. https://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thompson.pdf https://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thomp...