Cryptographic components are increasingly being integrated into hardware and software systems to improve information assurance and security. Because of this, several serious challenges arise:

• Test and verification of systems incorporating cryptography
• Unambiguous specification of cryptographic algorithms
• Rapid and safe retargeting of cryptographic implementations to new hardware and software platforms

Attempted solutions to these challenges are only hindered by conventional techniques using imperative languages such as Java and C.

Cryptol is the answer to these challenges. Based on solid mathematical foundations, and moving beyond traditional approaches, Cryptol is a specialized language and tool suite for developing, compiling, and validating cryptographic software. Engineers from Galois developed Cryptol in consultation with expert cryptographers. The Cryptol language enables construction of cryptographic software with ease, reliability, and high assurance. Cryptographers can express essential cryptographic concepts in Cryptol directly and formally.

Cryptol provides significant benefits to:

• Developers that write cryptographic implementations for deployment on a variety of hardware and software platforms
• High-assurance systems developers incorporating embedded cryptographic components
• Cryptographers that explore new cryptographic approaches
• Verification laboratories which use formal models to verify implementations
• Customers of high-assurance systems responsible for validation and test

One Specification, Many Uses

The Language of Cryptography - Using high-level Cryptol to express the same concepts and idioms found in published algorithms, developers can quickly implement pre-existing algorithms or develop new ones. Developers are freed to focus on the cryptography itself, not distracted by machine-level details such as word size. For example, Cryptol specification can be written using words that are 97 bits wide just as easily as using words that are 32 bits wide. Cryptol automatically ensures that the right implementation is generated for the target machine.

Authoritative Reference for Validation - Cryptol is positioned to become the standard language for cryptography. A growing number of both public and non-public algorithms are under development. Standard Cryptol specifications can be used to validate new cryptographic implementations by generating test vectors of user-selectable intermediate values.

Framework for Verification - For embedded systems developers who need to deploy high assurance applications, Cryptol facilitates construction of formal models, increasing the confidence in the development. Cryptol supports the eventual development of model checking tools.

Platform for Generation - Cryptol specifications are inherently portable. Retargeting the deployment platform doesn't involve recoding the algorithm. Cryptol is intended for use with various platforms, including embedded systems and smart cards. Currently Galois is working with industry partners towards deployment of Cryptol specifications to specialized cryptography platforms such as FPGAs.

The Cryptol Toolbox

The current Cryptol Toolbox contains a development environment for Cryptol specifications. An interpreter supports interactive experimentation with specifications, a tracing tool extracts intermediate values for validation, and a compiler generates C code.

Aspects of the Cryptol Language

Simple and Regular: The Cryptol language is essentially a language of sequences. This simple notion structures all data in Cryptol. A computer word is just a sequence of bits, a block is a sequence of words, and a stream is a sequence of blocks. The simplicity and consistency of this model leads to a simplicity and consistency in Cryptol specifications.

Expressive and Safe: Because Cryptol understands cryptography, it provides useful immediate feedback during creation of the specification regarding the cryptographic functions and data used. Cryptol can generate much of this information automatically, and enforce constraints and restrictions. Cryptol helps you get it right the first time. Whole classes of errors involving mismatch of data and functions are eliminated. Cryptol supports reasoning about intermediate values by providing information about the construction and use of those values.

Declarative: Cryptol specifications say what the form of the result will be, and do not specify the sequence of operations required to achieve the result. This facilitates the customization of implementations to the strengths of various platforms, and makes Cryptol suitable for highly-parallel target environments, such as FPGAs.