Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

How do we know if a crypto function is correctly implemented?

rjlipton.wordpress.com

Post reply on HN
Print view View original

21–30 of 32 posts

Re: How do we know if a crypto function is correctly implemented?

#21

Post by th0ma5 »

scott_s wrote: post #20

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 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 wha…

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

Re: How do we know if a crypto function is correctly implemented?

#22

Post by scott_s »

th0ma5 wrote: post #21
scott_s wrote: post #20

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 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 wha…

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

It's a valid question, but hardware has much more formal verification than software.

Re: How do we know if a crypto function is correctly implemented?

#23

Post by _asummers »

scott_s wrote: post #22
th0ma5 wrote: post #21

Earlier quoted context omitted.

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

It's a valid question, but hardware has much more formal verification than software.

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...

[1] https://news.ycombinator.com/item?id=9264195

Re: How do we know if a crypto function is correctly implemented?

#24

Post by crpatino »

Ono-Sendai wrote: post #18
nathan7 wrote: post #13

Earlier quoted context omitted.

You can't prove the hash function is correct, no. But you can prove the hash function is implemented equivalently to its definition. That's what the article is about.

That's true. But if you can't prove that your hash function has the desirable properties you expect/hope for, then I think that is important to acknowledge.

No, those are separate issues. There might be philosophical value on acknowledging the impossibility to prove the correctness of the algorithm, but it has little or no practical value when you want to prove if your implementation of the algorithm is correct.

Your argument is like saying that because there is no way to guarantee your physical product's design is 100% defect free, there is no point to implement quality controls in the manufacturing floor.

Re: How do we know if a crypto function is correctly implemented?

#25

Post by im3w1l »

scott_s wrote: post #20

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 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 wha…

>numeric calculations at the boundaries of what is representable.

That sounds like floating point instructions, and cryptography uses integer instructions.

Re: How do we know if a crypto function is correctly implemented?

#26

Post by RyanZAG »

Isn't it pretty clear why the question wasn't asked much and why nobody there really had an answer? These are cryptologists who are spending their time thinking of the science behind the implementation.

A good analogy would be to go to a conference for traffic planners and asking "How do we know that the car's breaking system is correctly implemented?". Obviously none of the traffic planners would be asking that question and wouldn't have an answer. But if you go ask an automotive engineer, they'll give you the run-down on all the tests they do to ensure it is implemented correctly. Whether cars are breaking correctly or not is obviously incredibly important for traffic planners but it's not their field of expertise.

I'd think it would be the same in this case. If you want to know if a crypto function is correctly implemented then you should go talk to the OpenSSL guys and ask them. I'm sure they have a lot of answers and a lot of ideas here.

Re: How do we know if a crypto function is correctly implemented?

#27

Post by scott_s »

im3w1l wrote: post #25
scott_s wrote: post #20

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 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 wha…

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

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

His blog, academic papers, and the paper I linked, have lots of discussions about integer issues.

Re: How do we know if a crypto function is correctly implemented?

#28

Post by SonOfLilit »

Possible and (relatively) easy.

We write the formal definition of the function in Cryptol, and use the Cryptol toolset to compare it to our implementation.

Cryptol[1] has the amazing ability to verify implementation equivalence between [a large class of] functions written in Cryptol, C, Java, Assembly or VHDL (as far as I recall). Of course this class of functions is not Turing Complete, but it's good enough to verify that two implementations of SHA256 or AES are mathematically identical.

The way Cryptol does this is really interesting: they compile the functions to a logic circuit, and use a SAT solver to prove that the circuit (f(x) == g(x)) always outputs T.

[1] http://www.cryptol.net/, an open source functional language made for Crypto R&D and communication, designed by Galois Inc. on commission from the NSA

Re: How do we know if a crypto function is correctly implemented?

#29

Post by scott_s »

_asummers wrote: post #23
scott_s wrote: post #22

Earlier quoted context omitted.

It's a valid question, but hardware has much more formal verification than software.

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... [1] https://news.ycombinator.com/item?id=9264195

This is true, but not an issue when it comes to this issue. All of that falls under the formal verification for processors.
Post reply on HN