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.

This Galois Tech Talk, the first for 2009, was our very own Joe Hurd talking about package management for theories. You can read the slides

Interactive theorem has grown beyond toy examples in mathematics and program verification, as demonstrated by recent successes such as the Gonthier’s formal proof of the four colour theorem and Leroy’s verified compiler from a realistic subset of C into PowerPC assembly code. As the construction of large programs led to the development of software engineering techniques, there is now a need for theory engineering techniques to support these major verification efforts.In this talk I will present the OpenTheory project, which has defined a simple ‘article’ format to represent theories of higher order logic. Theories in article format can be written by one higher order logic theorem prover, compressed by a standalone tool, stored and read by a different theorem prover. Articles naturally support theory interpretations, which leads to more efficient developments of standard theories, and also provides one approach to handling difficult constructs such as monads without extending the underlying logic. Finally, the grand vision of the OpenTheory article repository is painted, with fully automatic installation and dependency resolution.

• Date: Tuesday, January 13, 2008
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

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.

This week’s tech talk will be Magnus Myreen from Cambridge talking about mechanically verified Lisp interpreters. It will be held at the irregular time of 2pm, Friday Nov 14.

This talk describes work on constructing verified interpreters for a small LISP-like language using the interactive theorem prover HOL4.  The LISP interpreters have been proved correct with respect to detailed x86, ARM and PowerPC processor models (written by Sarkar, Fox and Leroy). New techniques for expressing correctness of machine code were developed, as well as new techniques for proof-producing decompilation and compilation to/from HOL4 functions. A copying garbage collector (a Cheney collector) was verified and subsequent proofs were built upon its verified specification.

Formal Methods in Computer Aided Design (FMCAD’08) is the preeminent conference in formal methods for hardware and systems, and this year, it’ll be held in downtown Portland, November 17-20. The advance program has been announced, and the lineup of technical papers, invited tutorials, invited speakers, and panel discussion looks awesome.Registration is open, so be sure to get your spot soon!Galois is sponsoring this year’s conference, along with Cadence, IBM, Intel, NEC, and Synopsis.  If you attend, stop by Galois; we’re only a few blocks from the conference hotel.

This Galois Tech Talk was held on Tuesday September 16th, 10.30am, with John Harrison, Principal Engineer at Intel, talking about theorem proving for formal verification. (You can also check out his Handbook of Practical Logic and Automated Reasoning). (.pdf slides, proof demo)

Abstract

The theorem proving approach to verification involves modelling a system in a rich formalism such as higher-order logic or set theory, then performing a human-driven interactive correctness proof using a proof assistant. In a striking contrast, techniques like model checking, by limiting the user to a less expressive formalism (propositional logic, CTL etc.), can offer completely automated decision methods, making them substantially easier to use and often more productive. With this in mind, why should one be interested in the theorem proving approach? In this tutorial I will explain some of the advantages of theorem proving, showing situations where the generality of theorem proving is beneficial, allowing us to tackle domains that are beyond the scope of automated methods or providing other important advantages. I will talk about the state of the art in theorem proving systems and and give a little demonstration to give an impression of what it’s like to work with such a system.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.