Cryptol version 2: An Open Source Cryptol

Abstract

HCSS participants, in the main, know about Galois' Cryptol language and system and its capabilities.  In short, Cryptol is a domain-specific language for programming, executing, testing, and formally reasoning about streams of bits.  Cryptol particularly excels at specifying and reasoning about cryptographic algorithms.

Galois has decided to "reboot" Cryptol and create, from the ground up, a new Open Source Cryptol release: Cryptol version 2.

Cryptol version 2 is the first Open Source release of the Cryptol system.  Its purpose is to make rigorous applied cryptography available to all.  Moreover, we advocate that Cryptol should be used as the foundation for the specification and verification of past and future cryptographic algorithms standardized via NIST competitions and other similar activities.

The Cryptol system provides: (1) a REPL for experimentation, (2) a parser and typechecker for Cryptol programs, (3) an interpreter for executing Cryptol programs, (4) a validation tool for gaining confidence in the correctness of Cryptol programs via automatic randomized testing, and (5) a verification backend for formally verifying properties of Cryptol programs through the use of SMT solvers.

Presenter Bio

Dr. Joseph Kiniry, a new Principal Investigator at Galois, was most recently a Full Professor at the Technical University of Denmark (DTU). There, he was the Head of DTU's Software Engineering section. He also held a guest appointment at the IT University of Copenhagen. Over the past decade he has held permanent positions at four universities in Denmark, Ireland, and The Netherlands.

Joe has extensive experience in formal methods, high-assurance software engineering, foundations of computer science and mathematics, and information security. Specific areas that he has worked in include software verification foundations and tools, digital election systems and democracies, smart-cards, smart-phones, critical systems for nation states, and CAD systems for asynchronous hardware.

He has over ten years experience in the design, development, support, and auditing of supervised and internet/remote electronic voting systems while he was a professor at various universities in Europe. He co-led the DemTech research group at the IT University of Copenhagen and has served as an adviser to the Dutch, Irish, and Danish governments in matters relating to electronic voting.