The Cryptol language comes with an integrated verification tool-set that can automatically perform equivalence and safety checking on Cryptol programs. Recently, we have presented a paper on this topic at PLPV’09: “Programming Languages Meets Program Verification” workshop. (Slides are also available.)

Briefly, equivalence checking refers to the problem of proving that two functions have the exact same input/output behavior. Typically, these functions are versions of the same algorithm; one being a reference implementation and the other being an optimized version. Cryptol automatically establishes that the optimized version is precisely equivalent to the original. If the functions are not equivalent, Cryptol provides a counter-example where they disagree; aiding greatly in development/debugging.

Safety checking refers to the problem of proving that the execution of a function cannot raise any exceptions; such as division by zero; index out-of-bounds, etc. When the safety checker says that a function is safe, you will know for sure that such conditions will never arise at run-time. (Similarly, you will get a concrete counter-example from Cryptol if this is not the case.)

Cryptol uses symbolic simulation to translate equivalence and safety checking problems to equivalent problems using the bit-vector logic of SMT-Lib. Furthermore, Cryptol has built-in connections to several SAT/SMT solvers. It automatically calls these provers and presents the results to the user in original Cryptol terms; providing a seamless verification environment for the end-user.

The full paper and slides on equivalence checking in Cryptol are available for download.

Cryptol now has a mailing list for discussions: The language, the tool set, programming idioms, everthing and anything related to Cryptol. Looking forward to seeing you join us!

Following on from the MD6-in-Cryptol posting, let’s consider another very interesting candidate from the (deep) pool of SHA-3 submissions; Skein 

 http://www.skein-hash.info/ http://www.schneier.com/skein.html

by the merry band of Ferguson, Lucks, Schneier, et al.The expression of their reference implementation comes out, we think, fairly cleanly in Cryptol. The digest output size is a variable parameter to the algorithm, but we’ll focus on the 512-bit version here — the submission’s primary candidate for SHA-3.In order to avoid duplicating the introductory material on Cryptol, we suggest the reader go through the MD6 writeup to get a grounding in Cryptol, its idioms, and syntax.

NIST is currently running a competition to come up with the next generation message hashing function that it intends to standardize and FIPS recommend upon completion (assuming one good candidate is left standing and well at the conclusion of the evaluation process):

 http://csrc.nist.gov/groups/ST/hash/sha-3/index.html

Apart from the need to come up with better alternatives to its current recommendation, the SHA-2 family of hashing functions, this competition draws inspiration from the success that the AES competition had a couple of years ago in engaging the community in coming up with a replacement for the DES block cipher. As then, a lot of new innovation has resulted.As with block ciphers, many common types of hashing functions lend themselves well to expression in Cryptol. To demonstrate some of the features of Cryptol and how it could be used to express SHA-3 candidates, here’s one of the submissions, MD6 from the CSAIL group at MIT, headed by Ronald L. Rivest:

 http://groups.csail.mit.edu/cis/md6/

The goal of this writeup is twofold:

• Introduce you to the MD6 hashing algorithm and its construction.
• Expose you to the Cryptol language, and how it lends itself to expressing MD6.

Ideally, you’ll come away with enthusiasm on both accounts!

If you get IEEE Computer, check out the article on page 108 of the January, 2009 issue: Rosetta: Standardization at the System Level.  The author, Perry Alexander , is a professor at the University of Kansas.  Perry describes Rosetta, a language for designing and modeling systems.  The language is undergoing IEEE standardization, and there’s even a book describing the language.Perry collaborates with me and others at Galois, Inc. and has used Rosetta on one of our joint formal methods projects.

The Principles of Programming Languages conference, POPL 09, and its surrounding workshops is kicking off this week in Savannah, Georgia. Galwegians will be attending most of the conferences: you might be able to find Levent at VMCAI or the Twelf Tutorial, or Iavor at TLDI or POPL, and Jeff Lewis (now at Signali) will be giving a keynote at PADL. Step up and say “hello!”.

Signali Corp is the latest technology commercialization spinout from Galois, chartered with commercialization of hardware IP core design technology aimed at the FPGA and ASIC markets.  Engineers at Galois and Signali have used the proprietary technology to deliver to government prime contractors the highest performing FPGA implementations in the world for a set of common cryptographic algorithms.With this technology, Signali is well-placed to make a significant impact on the IP core market with their ability to re-tune their cores to meet the customer’s design constraints, whether speed, or power, or area. The technology is especially well suited for optimizing hardware designs of computationally complex functions such as those common in digital signal processing and cryptographic systems.Galois enlisted the experience of Brian Moore, a seasoned design engineer and lab director from Intel, to lead Signali. Moore brings over 25 years of experience in the semiconductor and energy research industries. Galois co-founder Jeff Lewis, is leading the technology development as Chief Technology Officer. Signali is currently co-located with Galois in the historic Commonwealth Building in downtown Portland, Oregon. The company is engaged with Achronix Semiconductor to develop a portfolio of very high performance IP cores for their next-generation FPGAs. Sample performance and utilization numbers for IP cores running on the Achronix Speedster FPGA can be found on the Signali website.

Don did an interview with Michael Wrinn and Aaron Tersteeg from Intel’s Multicore Software Development podcast about Haskell, multicore and parallel programming, and the use of functional programming at Galois and in industry in general. Listen to the full interview! (15 minutes).

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.

This summer I attended the International Joint Conference on Automated Reasoning (IJCAR 2008) in cold, cold Sydney, to give a tutorial on Formal Methods in Use at Galois. The overview slides of the tutorial are available for download, for people interested in seeing some industrial applications of formal methods. Incidentally, while I was at the conference, I entered the automatic theorem prover competition with my ML prover Metis, and finished respectably mid-table.