High Assurance Cryptography Synthesis with Cryptol

Presented as part of the 2015 HCSS conference.

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. As summarized last year at HCSS, Galois has "rebooted" Cryptol and created, from the ground up, a new Open Source Cryptol release: Cryptol version 2.

A new major feature under development within Cryptol 2 and the Galois Software Assurance Workbench (SAW) is a set of new backends capable of synthesizing formally verified implementations and test benches for arbitrary cryptographic algorithms.  Within Cryptol 1 we were previously able to synthesize C, JVM, and VHDL implementations, but without any additional artifacts to provide evidence of the implementations' correctness.  Cryptol's new backends will target (at least) C (directly and via LLVM), JVM, VHDL, and (System) Verilog, along with Cryptol-independent evidence of the synthesized code's correctness.

In particular, we are developing a new subsystem called the "Structured VC Generator" that produces evidence in a form amenable to analysis by other tools.  More specifically, it accepts as input a set of Cryptol properties and a Cryptol specification.  Using the SAW symbolic interpreter it generates, for each Cryptol function reachable from the properties, a complete set of verification conditions characterized as input-output relations on said function. This is a particularly powerful technique for guaranteeing functional correctness because top-level theorems, which are expressed as universally quantified sentences, derive new theorems at function application boundaries. This results in a enormously rich set of input-output relations useful for runtime verification.

The generated VCs, which are encoded in the IR of SAW, can then be pushed through the backends to automatically generate test benches, amenable to runtime or static verification, for both software and hardware implementations.  Theorems about implementations are stated in the natural fashion given the backend in question; C specifications are captured in ACSL, JVM specifications in JML, and VHDL/(System) Verilog specifications in HDL assertions.  Consequently all generated implementations have full formal specifications and complete test benches for validation and verification, and their correctness and security properties can be independently analyzed using other tools capable of reasoning about C, LLVM, JVM, VHDL, and System Verilog.

Biography:

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.