Typically cryptographic algorithms are written by Cryptographers, in academic papers in a mathematical notation that is not executable. Implementers then develop “reference implementations” in programming languages or hardware design toolchains that don’t look very much like the math.
Software programmers 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 to ensure the translation did not introduce errors. This process makes the implementation of cryptography time consuming, expensive, and only partially trustworthy.
Our Solution: Cryptol
Cryptol is a domain-specific programming language and toolsuite that allows cryptographers, familiar with the language of cryptography, to specify new (or existing) algorithms. In turn, Cryptol “does the programming”, generating code or hardware designs that are provably correct and faithful to the algorithm as specified by the Cryptographer. This eliminates defects caused by loss of fidelity in the translation between Cryptographer and Software Programmer. It also speeds the implementation process dramatically when optimizations are required.
How it Works
The Cryptol tool suite offers compelling assurance of hardware and software correctness by providing direct compilation of abstract cryptographic algorithms into the industry-standard VHDL and Verilog hardware description languages, as well as software languages such as ‘C.’ Cryptol tools can also verify equivalence of cryptographic 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. 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.
The end result, or output, of using Cryptol is formally specified, formally verified, machine-generated implementation of cryptographic core algorithms that attain a level of assurance unmatched by any other means.
We Admit it, This is Hard
Even with the Cryptol tool suite, developing cryptography for high-assurance systems is not for the faint of heart. That’s where Formaltech comes in. We can:
- Train your team on using Cryptol
- Provide off-the-shelf, verified implementations of cryptographic algorithms
- Assist you in the development, optimization and formal verification of your algorithms
- Assist your team in pursuing FIPS certifications of your implementations