Cryptol is a domain-specific language (DSL) and tool suite that simplifies the specification of a cryptographic algorithm and then compiles the specification into VHDL, an industry-standard chip layout language. This approach is compelling to developers because it ensures a clean, direct path from the designer’s intentions to its final implementation in hardware, as well as provides a compelling assurance argument. Developed in consultation with expert cryptographers, Cryptol enables the construction of cryptographic software with ease, reliability, and high assurance. Cryptol is currently used by the Intelligence Community (IC) and has been licensed to several universities.
Cryptol Language and Compiler
The Cryptol specification language was designed by Galois for the NSA as a public standard for specifying cryptographic algorithms. A Cryptol reference specification can serve as the formal documentation for a cryptographic module, eliminating the need for separate and voluminous English descriptions. Cryptol is fully executable, allowing designers to experiment with their programs incrementally as their designs evolve. Cryptol compilers can generate C, C++, and Haskell software implementations, and VHDL or Verilog HDL hardware implementations. These tools significantly reduce overall life-cycle costs by addressing the key cost drivers in the deployment of cryptographic solutions. For example, Cryptol allows engineers and mathematicians to program cryptographic algorithms on FPGAs as if they were writing software.
In addition to generating implementations of cryptographic algorithms, Cryptol tools can verify the faithfulness of an implementation to a reference specification, at each stage of the toolchain. Equivalence can be demonstrated between a reference Cryptol specification and a refinement of that specification, and between a Cryptol specification and a VHDL implementation, even if that VHDL was not produced by the Cryptol tools. This enables the designer to incrementally refine an implementation to trade off space, time, and other performance metrics, while ensuring correctness of each refinement.
- Browning, S. and Weaver, P. Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In Design and Verification of Microprocessor Systems for High-Assurance, David S. Hardin, Editor. Springer 2010
- Colby Hoffman, Jeff Lewis, Brad Martin, Sally Browning, A Complete Design Flow for MILS in a Single High Assurance FPGA, European Reconfigurable Radio Technologies Workshop, 2010
- Levent Erkök, Magnus Carlsson, and Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol. In Formal Methods in Computer Aided Design Conference, FMCAD'09, Austin, TX, November 2009, IEEE.
- Levent Erkök, John Matthews. High assurance programming in Cryptol. In CSIIRW'09: Proceedings of the 5th Annual Workshop on Cyber Security and Information Intelligence Research, Oak Ridge, TN, April 2009, ACM.
- Levent Erkök and John Matthews. Pragmatic Equivalence and Safety Checking in Cryptol. PLPV 2009: 73-81.
- Lee Pike, Mark Shields, John Matthews: A verifying core for a cryptographic language compiler. ACL2 2006: 1-10
Collaborate with Us
Licensing - Obtain a license for one of our advanced technologies.
Research & Development - Solve your toughest problems by exploring new approaches with us.
Training - Learn how to use cutting-edge tools to increase trustworthiness in your critical systems.