Cryptol, the language of cryptography, now available

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.

Click to read more ...

Formal Methods in Use at Galois

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.

Click to read more ...

Tech Talk: Mechanically verified LISP interpreters

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.

Click to read more ...

Beautiful Parallelism: Harnessing Multicores with Haskell

Don will be giving a talk SC'08 in Austin, Texas on Monday 17th November, as part of the Bridging Multicore's Programmability Gap workshop (see the schedule here), talking about programming mainstream multicore systems with Haskell, now. Here's the abstract,

Haskell is a general purpose, purely functional programming language. If you want to program a parallel machine, a purely functional language such as Haskell is a good choice: purity ensures the language is by-default safe for parallel execution, (whilst traditional imperative languages are by-default unsafe).This foundation has enabled Haskell to become something of a melting pot for high level approaches to concurrent and parallel programming, all available with an industrial strength compiler and language toolchain, available now for mainstream multicore programming.In this talk I will introduce the features Haskell provides for writing high level parallel and concurrent programs. In particular we'll focus on lightweight semi-explicit parallelism using annotations to express parallelism opportunities. We'll then describe mechanisms for explicitly parallel programs focusing on software transactional memory (STM) for shared memory communication. Finally, we'll look at how Haskell's nested data parallelism allows programmers to use rich data types in data parallel programs which are automatically transformed into flat data parallel versions for efficient execution on multi-core processors.

See Simon Peyton-Jones and Satnam Singh's recent tutorial for more background on multicore Haskell, on which this talk is based.

Click to read more ...

Galois awarded NASA research contract

NASA has awarded Galois, Inc. together with the National Institute of Aerospace (NIA), a research contract to investigate monitor synthesis for software health management (here is NASA's press release). The research team includes myself, Lee Pike as the Principal Investigator,  Cesar Munoz as the Co-PI (NIA), and Alwyn Goodloe as a Research Scientist (NIA). The award runs through the end of 2011, and we are investigating the formal synthesis of online monitors from requirements specifications. The research will focus on safety properties and real-time properties of distributed systems. Here are some slides I gave as part of an invited panel kicking off the project, and here's the press release from Reuters. If you're interested in finding out more about the research or are interested in collaborating, don't hesitate to contact me, or leave a comment!

Click to read more ...