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

11–20 of 32 posts

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

#11

Post by Ono-Sendai »

FeepingCreature wrote: post #9
Ono-Sendai wrote: post #7

Earlier quoted context omitted.

Does anyone want to write why they disagree instead of just downvoting me?

I'm not sure, but it seems like you're making a connection to P vs. NP that is at the least very non-obvious, so people default to thinking that you have no idea what you're talking about. Maybe you could explain how proving a hash function correct implies P!=NP?

Sure thing. I'll write a blog post about it later tonight (am on work time right now)

Brief summary however: The point of a crypto hash function is that you need to try on the order of 2^n inputs (n being length in bits of digest) to find a collision. (greater than polynomial time) However you can check any input in polynomial time. This makes it in NP. (decision problem is computable in polynomial time). I'm probably missing some details which I will think about later :)

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

#12

Post by matthavener »

leni536 wrote: post #6

Can proof assistants help (like coq)? My best bet is the specification of crypto algorithms are essentially the algorithm themselves, so maybe not. Of course if you want to avoid state than maybe you want to program your crypto in a functional language, although there could be non-trivial attack vectors too (like timing).

Cryptol does something pretty similar. You implement your functions in Cryptol and then verify them with SAT/SMT solvers, or generative testing. Its less about verifying the C/C++ implementations and more about verifying properties of the algorithms themselves. (Example: https://github.com/GaloisInc/cryptol/blob/master/examples/ZU...)

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

#13

Post by nathan7 »

Ono-Sendai wrote: post #4

You can't prove a cryptographic hash function is correct without proving P != NP. So I don't think anyone has proven their implementations of hash functions correct at least.

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.

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

#14

Post by Herpyderp666 »

Ono-Sendai wrote: post #11
FeepingCreature wrote: post #9

Earlier quoted context omitted.

I'm not sure, but it seems like you're making a connection to P vs. NP that is at the least very non-obvious, so people default to thinking that you have no idea what you're talking about. Maybe you could explain how proving a hash function correct implies P!=NP?

Sure thing. I'll write a blog post about it later tonight (am on work time right now) Brief summary however: The point of a crypto hash function is that you need to try on the order of 2^n inputs (n being length in bits of digest) to find a collision. (greater than polynomial time) However you can check any input in polynomial time. This makes it in NP. (decision problem is computable in polynomial time). I'm probabl…

Watch Dan Boneh's coursera cryptography course where he at least mentions that provably secure cipher systems require that P != NP. Combine that with the wikipedia article on cryptographic hash functions which tells you that you can build ciphers from hash functions. Done.

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

#15

Post by giech »

leni536 wrote: post #6

Can proof assistants help (like coq)? My best bet is the specification of crypto algorithms are essentially the algorithm themselves, so maybe not. Of course if you want to avoid state than maybe you want to program your crypto in a functional language, although there could be non-trivial attack vectors too (like timing).

It can, but it is highly non-trivial. Here are a couple of 2015 papers on OpenSSL verification from the same group at Princeton:

SHA verification (ACM TOPLAS): https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf

HMAC verification (Usenix Security): http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf

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

#16

Post by acqq »

> How can we know? We can look at the code and check that it really works as claimed, but that is messy and time consuming. Worse it defeats the whole purpose of having a library of crypto functions.

Sometimes there's no substitute for rolling up the sleeves and reading the darn thing. Even if it's the machine code and the higher levels have to be reverse engineered.

> Further it makes this happen in a subtle manner, which is extremely hard to detect by code inspection. How would we discover this?

The date-dependency can be exhaustive tested for the dates in which the software is expected to be used (e.g. up to 2100). The every-expected millisecond dependency would be harder to test, but possibly doable for the fast routines. Otherwise, it certainly has to be spotted by reading the code. The code of the primitives should not be date or time dependent, and the answer to the first question applies. Somebody has to roll up the sleeves and read.

Sometimes the solution can't avoid the involvement of an expert.

Standardization of the components and the description languages and the tools which would use these can make some tests mechanical. Exhaustive tests and the random-probe tests can be very effective. And the engineering problem is what's more effective, developing more for the general tests or just testing the target, for given circumstances. There's no "one-size-fits-all" for that.

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

#17

Post by Ao7bei3s »

Ono-Sendai wrote: post #11
FeepingCreature wrote: post #9

Earlier quoted context omitted.

I'm not sure, but it seems like you're making a connection to P vs. NP that is at the least very non-obvious, so people default to thinking that you have no idea what you're talking about. Maybe you could explain how proving a hash function correct implies P!=NP?

Sure thing. I'll write a blog post about it later tonight (am on work time right now) Brief summary however: The point of a crypto hash function is that you need to try on the order of 2^n inputs (n being length in bits of digest) to find a collision. (greater than polynomial time) However you can check any input in polynomial time. This makes it in NP. (decision problem is computable in polynomial time). I'm probabl…

O(2^(n/2)) actually, due to the birthday attack.

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

#18

Post by Ono-Sendai »

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

You can't prove a cryptographic hash function is correct without proving P != NP. So I don't think anyone has proven their implementations of hash functions correct at least.

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.

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

#19

Post by wtbob »

I think that it's great the the question was raised by a performing arts professor—it really goes to show why the liberal arts ideal is so important.

Remember, the liberal arts aren't just the humanities: they are the humanities and the sciences. The mediæval liberal arts were grammar & rhetoric (both part of mastering one's own language); logic, geometry and arithmetic (mathematics, the core of science); astronomy (the major science of its day); and music (the marriage of art and science).

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

#20

Post by scott_s »

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

Post reply on HN