PoP Seminar Talk

First-Principles Formal Verification of Cryptographic Systems

Adam Chlipala, Professor of Computer Science, MIT
Friday, 12 April, 2024; 11:00am
NSH 3002
Host: Jan Hoffmann

Abstract

In theory, it has been clear that complete computing stacks (software and hardware) can be proved correct from logical first principles, but in practice, it doesn’t tend to happen very often. I’ll report on our experiences using the Coq theorem prover to establish such theorems for nontrivial pieces of cryptographic functionality. A warm-up with immediate applicability is Fiat Cryptography, a formally verified compiler for finite-field arithmetic, which today is used by every major web browser for TLS, and which is able to set new performance records with automatically generated code for important arithmetic routines. Fiat Cryptography is one part of the larger case study that I’ll talk about, which involves a binary string of RISC-V machine code that runs on a commercial microcontroller (without requiring any other software to be loaded). Its unified proof establishes that it drives the processor to implement a cryptographic protocol that opens or closes a Lego garage door, when an authorized remote party authenticates properly over Ethernet/IP/UDP. These experiences have motivated new ideas in semantics and verification, and they’ve also helped shine light on practical bottlenecks in use of proof assistants based on type theory.

Bio

Adam’s background is in programming languages and formal methods. He is interested in developing simpler and more effective abstractions for building correct, secure, and performant systems – usually taking advantage of machine-checked mathematical proofs somehow. His work applies ideas like object-capability systems, proof-carrying code, transactions, type systems, and whole-program optimizing compilers for high-level languages; with applications in computer architecture, cryptography, databases, and operating systems, including novel designs that span traditional layers.