What is Cryptol?
Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language.
Here is a comparison of a portion of the SHA-1 hash function specification and its representation in Cryptol:
Cryptol SHA-1 implementation
f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z)
| (20 <= t) && (t <= 39) then x ^ y ^ z
| (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
| (60 <= t) && (t <= 79) then x ^ y ^ z
else error "f: t out of range"The Cryptol implementation unambiguously captures both the English description and the mathematical specification below:
SHA-1 specification
From page 10 of NIST 180-4.
Capture and analyze cryptographic specifications
Recent news has highlighted the importance of correct cryptographic implementations 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.
Cryptol version 2 is now released as open source under a 3-clause BSD license. Our goal is that it becomes a widely adopted standard for expressing cryptographic algorithms.
You can see future development plans for Cryptol and other Galois tools here.
Who is using Cryptol?
Cryptol has been used by private companies, educators, and the U.S. Government. It has been used to analyze algorithms and implementations, to generate implementations, and as a learning tool. We would love to hear how you use Cryptol, and with your permission, will add quotes about how Cryptol’s use is growing. Click here (pdf) to read a paper that describes some case studies from version 1 of Cryptol.
This is a big deal
We are proud of Cryptol, and are excited to bring it to the world. Cryptol is representative of what we love to do, and represents over 20 person-years of investment. It also builds on some extremely powerful tools and research from the SAT and SMT communities. With your help, we plan to keep building on it, making it more expressive and powerful.
What are its limitations?
Cryptol was originally designed for expressing the kinds of cryptographic algorithms that can be efficiently implemented in hardware circuits. Cryptol is best suited to implementing core cryptographic routines rather than entire cryptographic protocol suites such as SSL. We have ideas of how to address these limitations, and look forward to working with the community on them. Even with these limitations, Cryptol’s current capabilities have the potential to improve the trustworthiness of many critical cryptographic implementations.