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.
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.
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 :)
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.
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.
> 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.
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.
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...)
> 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.
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).
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.
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.
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.
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
And then how do you know the formal definition you give to Cryptol is correct? How do you know that Cryptol correctly transforms the formal definition to a logic circuit? How do you know it correctly transforms your C/Java/Assembly/VHDL to a logic circuit?
31 comments
[ 3.0 ms ] story [ 69.4 ms ] threadMaybe you could explain how proving a hash function correct implies P!=NP?
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 :)
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.
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.
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
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.
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).
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.
[0] http://blog.erratasec.com/2015/03/x86-is-high-level-language...
[1] https://news.ycombinator.com/item?id=9264195
That sounds like floating point instructions, and cryptography uses integer instructions.
His blog, academic papers, and the paper I linked, have lots of discussions about integer issues.
Recommended if you haven't read it already.
https://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thomp...
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.
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
Its a deep rabbit hole.