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

Possible and (relatively) easy.<p>We write the formal definition of the function in Cryptol, and use the Cryptol toolset to compare it to our implementation.<p>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&#x27;s good enough to verify that two implementations of SHA256 or AES are mathematically identical.<p>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.<p>[1] <a href="http:&#x2F;&#x2F;www.cryptol.net&#x2F;" rel="nofollow">http:&#x2F;&#x2F;www.cryptol.net&#x2F;</a>, an open source functional language made for Crypto R&amp;D and communication, designed by Galois Inc. on commission from the NSA

The rabbit hole goes deeper: how are you sure the <i>compiler</i> is correct? See the paper by John Regehr and his group: <a href="http:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;492" rel="nofollow">http:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;492</a><p>I&#x27;m not just saying this randomly in any subject that is concerned with correctness, as Regehr&#x27;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.<p>I also want to point out that Lipton&#x27;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.

&gt; Some said that the issue was not about crypto, but about software engineering. So it was someone else’s issue.<p>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.<p>The thing about crypto is there&#x27;s some things about how it&#x27;s used that are separate from the mathematical scheme. In ordinary programming we have this as well, but it&#x27;s relatively easy to look inside the box to see what&#x27;s happening.<p>Basically I couldn&#x27;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 &quot;blahblah&quot; 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&#x27;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&#x27;s done. The nice thing is it&#x27;s unlikely to come out the same if there&#x27;s something wrong.

Isn&#x27;t it pretty clear why the question wasn&#x27;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.<p>A good analogy would be to go to a conference for traffic planners and asking &quot;How do we know that the car&#x27;s breaking system is correctly implemented?&quot;. Obviously none of the traffic planners would be asking that question and wouldn&#x27;t have an answer. But if you go ask an automotive engineer, they&#x27;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&#x27;s not their field of expertise.<p>I&#x27;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&#x27;m sure they have a lot of answers and a lot of ideas here.

I think that it&#x27;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.<p>Remember, the liberal arts aren&#x27;t <i>just</i> the humanities: they are the humanities <i>and</i> the sciences. The mediæval liberal arts were grammar &amp; rhetoric (both part of mastering one&#x27;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).

&gt; 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.<p>Sometimes there&#x27;s no substitute for rolling up the sleeves and reading the darn thing. Even if it&#x27;s the machine code and the higher levels have to be reverse engineered.<p>&gt; Further it makes this happen in a subtle manner, which is extremely hard to detect by code inspection. How would we discover this?<p>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.<p>Sometimes the solution can&#x27;t avoid the involvement of an expert.<p>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&#x27;s more effective, developing more for the general tests or just testing the target, for given circumstances. There&#x27;s no &quot;one-size-fits-all&quot; for that.

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

Regarding &quot;keep no state&quot;, 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()).

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