Principles of Programming Seminar
— 12:00pm
Location:
In Person
-
Newell-Simon 3002
Speaker:
ADAM CHLIPALA
,
Professor of Computer Science, Programming Languages & Verification Group, Computer Science and Artificial Intelligence Laboratory, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology
http://adam.chlipala.net/
First-Principles Formal Verification of Cryptographic Systems
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.
—
Adam Chlipala'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.
Faculty Host: Jan Hoffman