Andres Erbsen

CV (html)publications (html)GitHubContact
Research Statement (pdf)Teaching Statement (pdf)

I work on building reliable and trustworthy computer systems using computer-checked proofs. Thus I work in formal verification, cryptography engineering, programming languages, security, and type theory. I seek to do applied work with a long time horizon, but some early outputs have already found widespread deployment: Code generated and verified using our research artifacts was likely used by your web browser to secure the connection to this site!

I am currently a PhD student in the lab of Adam Chlipala at MIT CSAIL, far enough along to think about what next.

Selected Research Projects

The bedrock2 'IoT lightbulb' is a small embedded system covered by a single 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 and a streamlined semantics style for modeling nondeterminism.

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.

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.

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.

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

More information on my research can be found in the publication abstracts (html) and Research Statement (pdf).

Old Hacks Not Quite Forgotten Yet

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.