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

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

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.

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.

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.

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

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.