Strange Loop

Intro to Cryptol and High-Assurance Crypto Engineering

Cryptol is an open source pure functional language for expressing and reasoning about bit-precise computations, particularly cryptographic algorithms. Like Haskell, it is built upon a polymorphic, static type system, and offers similar mathematical function and sequence comprehension notation. The type system features size polymorphism and arithmetic type predicates designed to express the constraints that naturally arise in cryptographic specifications.

The advanced type system and restricted domain of Cryptol enables a theorem-driven development style: correctness properties can be expressed directly in the language in tandem with the development of a specification. As the specification evolves, these properties can be continually fuzz-tested with random QuickCheck-style testing, and even sent to external SAT and SMT solvers for a mathematical proof of correctness.

In this workshop, We’ll introduce the Cryptol language from the ground up. We will implement several classical cryptosystems to learn the basic syntax and semantics of the language, building up to an model of the Enigma machine. Along the way, we will express and check correctness properties about our implementations using QuickCheck. Finally, We will demonstrate a Cryptol specification of the ZUC stream cipher used in 4G LTE communications, and show how the theorem-driven development approach reveals a bug in a previous version of the cipher.

Joe Kiniry

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.

Adam Foltzer

Galois

Adam was lucky enough to begin programming in Scheme when he was quite young, and has since then had a passion for functional and denotational programming. While getting a B.S. and M.S. in Computer Science from Indiana University, he began using Haskell while studying the theory, design, and implementation of programming languages; parallel and concurrent programming; and quantum and reversible computing. Prior to studying Computer Science, he studied Russian language and literature, archaeology, and how to fly small aircraft.

Dylan McNamee

Galois

Dylan McNamee is a member of the technical staff at Galois, where he leads Galois’ assured platforms program. At Galois, he designed a file system for cross- domain systems, and has written Cryptol specifications for a number of cryptographic algorithms. Before joining Galois, Dylan was an assistant professor of computer science at the Oregon Graduate Institute, and subsequently co-founded two startup companies in the early 2000’s. He received his MS and PhD in Computer Science from University of Washington (in Seattle), and his BA in Computer Science from UC Berkeley.