Live data from Hacker News

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

rjlipton.wordpress.com

1–10 of 32 posts

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

#3
post #2

Regarding "keep no state", note also that rand() can not reasonably be implemented without some state being maintained between calls (even if it is maintained by the caller e.g. rand_r()).

Well, yes, but as people are continually rediscovering "randomness" and "provable deterministic behaviour" are really tricky design goals to both meet. At least forcing explicit state makes the caller think slightly about cryptographic randomness. See also the /dev/random vs /dev/urandom wrangling.

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

#5
> Some said that the issue was not about crypto, but about software engineering. So it was someone else’s issue.

So this was my issue on a project once. I had to make sure a certain signing process what the same on an app and the server.

The thing about crypto is there's some things about how it's used that are separate from the mathematical scheme. In ordinary programming we have this as well, but it's relatively easy to look inside the box to see what's happening.

Basically I couldn't be sure the implementations were the same until the Python and Java code were outputting the same using the same inputs. There was a lot of digging in documents involved, and a lot of fine print. For instance, some packages will let you sign a string "blahblah" with your key directly. This hides the fact that you are hashing the string into a number using some agreed hash algo. If your other implementation doesn't have it all conveniently packaged, you have to do the hash ans sign the number yourself. Not rocket science, but hard to figure out until it's done. The nice thing is it's unlikely to come out the same if there's something wrong.

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

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

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

#7

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.

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

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

#8
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).

I heard a talk by a group that is doing exactly this. They built their own language to model crypto primitives, and machine check that a java or c implementation satisfies the specification. It is neat stuff, but unfortunately their system can't model timing differences, which is an important part of crypto implementation.

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

#9

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.

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?

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

#10

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.

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

I did not downvote you. However, can you explain your statement "You can't prove a cryptographic hash function is correct without proving P != NP."
Post reply on HN