Andres Erbsen

CV (html) – publications (html) – GitHub – Contact

I lead the ISE Formal team at Google. Previously, I was a PhD student in the lab of Adam Chlipala at MIT CSAIL.

I work on building reliable and trustworthy computer systems using computer-checked proofs. The aim is to virtually eliminate bugs by mechanizing the engineering disciplines behind computer infrastructure along with the justification of their adequacy and compatibility, evolving proofs and code in tandem. The challenge lies in explicating domain-expert intuition into workable and appropriate formal models that help rather than hinder development. I see my efforts as applied work with a long time horizon, sometimes showing off parts of the stack in separate large-scale deployments: Code generated and verified using our research artifacts was likely used by your web browser to secure the connection to this site!

Selected Research Projects

The bedrock2 'IoT lightbulb' is a small embedded system covered by a record-setting Coq theorem that ties together the CPU design, compiler implementation, device drivers, and application software to a neat specification about input-output traces. Novel ingredients leading up to the end-to-end proof include a lightweight formalization of the RISC-V ISA (ICFP '23) and a smooth method for formalizing intentional underspecification (TOPLAS '23).

📖 Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala. Integration Verification Across Software and Hardware for a Simple Embedded System. Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21). June 2021.

📖 Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Adam Chlipala, Clément Pit-Claudel. Foundational Integration Verification of a Cryptographic Server. Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'24). To appear.

Fiat Cryptography is a library of reusable implementations of cryptographic arithmetic carefully generalized from expert-optimized C and assembly code. The templates are proven correct in Coq and specialized to particular elliptic-curve parameters using a certified compiler. Code generated from our templates has since been deployed by Facebook, Amazon, Apple, Mozilla, Google, and many others. We also set some ECC speed records by applying verified proof-generating superoptimization to Fiat-Crypto code, earning the PLDI'23 Distinguished Paper award and the HUMIES Gold award.

📖 Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala. Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises. Proceedings of the IEEE Symposium on Security & Privacy 2019 (S&P'19). May 2019.

🧩 The two systems combine into a case study featuring total-correctness proofs about cryptographic authentication performed by a lightweight microcontroller at the edge of performance constraints (dissertation).

Old Hacks Not Quite Forgotten Yet

Reification by Parametricity (ITP '18) is a two-line trick for feeding Coq goals into certified procedures.

dename, coname - Decentralized cryptographic identity in the anytrust model (two sllightly different tradeoffs within Zooko’s triangle of digital identity).

torch is an embeddable Tor client library with flexible rendezvous support, it's written in Go.

voteserver,voteclient - An auditable online voting system implementation based on linkable anonymous group signatures.

sipb-pgpsign - Automatic PGP certification for MIT students.

scalabiliry of cjdns - A discouraging simulation of the original cjdns route-finding scheme.

verilog implementation of curve25519 for Virtex-6 and similar FPGAs.

efficient base converter - to and from bases [2..256], with unnecessarily fancy optimizations.

engcode - An encoding for binary data designed to be easy for humans to remember.