Cryptol Language for Cryptography
Cryptol is a domain specific language for the design, implementation and verification of cryptographic algorithms, developed over the past decade by Galois for the United States National Security Agency. It has been used successfully in a number of projects, and is also in use at Rockwell Collins, Inc.
…
Cryptol allows a cryptographer to:
- Create a reference specification and associated formal model.
- Quickly refine the specification, in Cryptol, to one or more implementations, trading off space, time, and other performance metrics.
- Compile the implementation for multiple targets, including: C/C++, Haskell, and VHDL/Verilog.
- Equivalence check an implementation against the reference specification, including implementations not produced by Cryptol.
The trial version & docs are here.
First, I think this is really cool. I like domain specific languages, and crypto is hard. I really like equivalence checking between models and code. I had some questions, which I’m not yet able to answer, because the trial version doesn’t include the code generation bits, and in part because I’m trying to vacation a little.
My main question came from the manual, which First off the manual states: “Cryptol has a very flexible notion of the size of data.” (page number 11, section 2.5) I’d paste a longer quote, but the PDF doesn’t seem to encode spaces well. Which is ironic, because what I was interested in is “does the generated code defend against stack overflows well?” In light of the ability to “[trade] off space, time [etc]” I worry that there are a set of options which translate, transparently, into something bad in C.
I worry about this because as important as crypto is, cryptographers have a lot to consider as they design algorithms and systems. As Michael Howard pointed out [link to http://blogs.msdn.com/sdl/archive/2008/11/18/secure-coding-secrets.aspx#comments no longer works], the Tokeneer system shipped with a library that may be from 2001, with 23 possible vulns. It was secure for a set of requirements, and if the requirements for Cryptol don’t contain “resist bad input,” then a lot of systems will be in trouble.
I met with several people from Galois last summer. If I recall correctly, they have one can define data sizes parametrically in the code, but the actual implementation is compiled to fix-sized buffers. They are mainly targeting Cryptol to compile to Verilog or VHDL for running on FPGAs.
For verification, they make two implementations: a high-level inefficient implementation that should be close to the theoretical encryption algorithm, and a low-level pipelined algorithm that may be very complicated. These two implementations are checked for equivalence using a custom combination of SMT solvers and inductive theorem proving techniques. They could also do more convential techniques like fuzz testing as well.
By having two implementation and doing equivalence testing, I think they should have a good chance of catching all the implementation correctness bugs. Their approach won’t catch bugs in the high-level implementation or in the underlying algorithm. I also suspect they could miss information leakage due to timing attacks, but they may have a solution to that.
In any case, this approach of a domain specific language and static verification has been successful in other areas, and seems like a good approach here.
Frankly, Tokeneer seemed slightly overhyped to me. I read through the docs back when they were released, and I seem to recall something like the following:
In the big glossy print, they claimed the code had been formally verified; later, in the fine print, they revealed that their verification had gaps. For instance, they told their theorem prover to assume that integers couldn’t overflow, but they didn’t verify this assumption. Many years after they originally delivered the software (I think it may have been when they were preparing the code for release?) they discovered a security bug that arose due to integer overflow.
That’s my memory. I might be misremembering or misquoting.
I worry about things like this. What is the point in proving the mathematics and protocol to the Nth degree of purity and essence, when the requirements are wrong?