Analyze Cryptographic Specifications: Cryptol

2014-04-25T15:25:10
ID N0WHERE:17392
Type n0where
Reporter N0where
Modified 2014-04-25T15:25:10

Description

The _ Cryptol _ specification language was designed by Galois for the NSA’s Trusted Systems Research Group as a public standard for specifying cryptographic algorithms. A reference specification can serve as the formal documentation for a cryptographic module. Unlike current specification mechanisms, Language is fully executable, allowing designers to experiment with their programs incrementally as their designs evolve.

This release is an interpreter for version 2 of the language. The interpreter includes a :check command, which tests predicates written in Cryptol against randomly-generated test vectors (in the style of QuickCheck . There is also a :prove command, which calls out to SMT solvers, such as Yices, Z3, or CVC4, to prove predicates for all possible inputs.

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 this specification, 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.

Who is using this tool?

Tool 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 this tool, 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.

Building Cryptol From Source

Cryptol builds and runs on various flavors of Linux, Mac OS X, and Windows. We regularly build and test it in the following environments:

  • Mac OS X 10.10 64-bit
  • CentOS 6 32/64-bit
  • Windows 7 32-bit

Prerequisites

Cryptol is developed using GHC 7.10.2 and cabal-install 1.22, though it is still tested with the previous major version of GHC. The easiest way to get the correct versions is to follow the instructions on the haskell.org downloads page .

Some supporting non-Haskell libraries are required to build Cryptol. Most should already be present for your operating system, but you may need to install the following:

You’ll also need Z3 installed when running Cryptol.

Analyze Cryptographic Specifications: Cryptol documentation

Analyze Cryptographic Specifications: Cryptol download