Cryptol
The Cryptol domain-specific language tool suite offers compelling assurance of hardware correctness by providing direct compilation of abstract cryptographic algorithms into the industry-standard VHDL and Verilog hardware description languages. Cryptol tools can also verify equivalence of crypto algorithm specifications, and equivalence of HDL and Cryptol descriptions.
Designing cryptographic hardware correctly, while trading off time, space, and power, is expensive and time-consuming. Verifying that a hardware implementation implements a cryptographic algorithm specification correctly is equally challenging.
Correct cryptographic implementations are important for everyone. Previously, the challenge has been that cryptographic algorithms are written in academic papers in a mathematical notation that is not executable. Someone often writes a “reference implementation” which doesn’t usually look very much like the math. People then use (or optimize) that reference implementation in their applications, but there hasn’t been an easy way to check those implementations against the mathematical specification.
Using a specification in Cryptol, programmers can generate their own test vectors, prove theorems, and (using other tools) verify equivalence to their own programs, or even generate code or hardware from the specification.
