Galois is pleased to announce that Cryptol, the language of cryptography, is now available to the public!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.
Domain-specific languages (DSLs) allow subject-matter experts to design solutions in using familiar concepts and constructs. Cryptol, as a DSL, allows domain experts in cryptography to design and implement cryptographic algorithms with a high degree of assurance in the correctness of their design, and at the same time, producing a high performance implementation of their algorithms.Cryptol allows a cryptographer to:
- Create a reference specification and associated formal model.
- Test the specification against published test vectors and formal assertions about state.
- 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 Cryptol site has further documentation and the full language specification. In this release, Galois has made a implementation of the Cryptol language available free of charge for non-commercial uses.
The trial version is available for Linux, MacOS, and Windows installations and can be downloaded at the Cryptol site. The trial version is meant for language exploration. It includes a Cryptol interpreter with QuickCheck capabilities, documentation, and examples. The open version does not compile to VHDL, C/C++, or Haskell, and does not produce the formal models used for equivalence checking.Cryptol is implemented in Haskell.
Contact Galois to obtain a full-featured version for evaluation.