I work on building reliable and secure computer systems using computer-checked mathematical proofs. By targeting the intersection of leading software-engineering techniques for high-consequence systems and the capabilities of formal verification methodologies, I construct certified implementations of tricky code whose quality is already recognized as important. In particular, I led the development of the first interactive embedded system with a computer-checked correctness proof covering both hardware and software, and the first cryptographic arithmetic library that achieves high performance without hand-specializing implementations to particular parameters. Code generated and verified using our research artifacts was probably used by your web browser to download this document!
The bedrock2 toolchain provides program proof and integration verification facilities for embedded programming in a carefully curated subset of C. We used it to equip a small 'IoT lightbulb' system with a single computer-checked theorem that validates the CPU design, compiler implementation, device drivers, and application software against a neat specification of 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 that sidesteps the main source of incidental proof complexity found in other prominent verified compilers such as CompCert. The correctness proof of this system is the first to capture I/O behavior of a hardware-and-software system, the first to connect compiled code, program data, and I/O devices in the same address space, and the first to provide guarantees of continued operation (albeit the last guarantee does not include the processor implementation). (PLDI'21 above, I am the lead author.)
The Fiat Cryptography library presents novel generic implementations of finite field arithmetic that can be specialized to performance-competitive C code for specifc primes and CPU architectures using the associated certified compiler. Our implementation templates are a natural generalization of the techniques used in world-champion C and assembly code, and we proved in Coq that they compute the correct output for all parameters and run-time inputs. Correct-by-construction code generated by Fiat Cryptography has been deployed by Amazon, Apple, Facebook, Google, Mozilla, and many others, and included in Linux, Go, Rust, and Zig crypto libraries. (S&P'19 above, I am the lead author.)