Provably Correct, Secure, and Leakage-Free Systems

I see someone posted this before I was able to do it :)

Hi HN! For the last six years, I've been working on techniques to build high-assurance systems using formal verification, with a focus on eliminating side-channel leakage. I'm defending my PhD thesis next week, where I'll talk about our approach to verifying hardware security modules with proofs covering the entire hardware and software system down to the wire-I/O-level. In terms of the artifacts we verify: the biggest example is an ECDSA signature HSM, implemented in 2,300 lines of C code and 13,500 lines of Verilog, and we verify its behavior (capturing correctness, security, and non-leakage) against a succinct 50-line specification.

One of the components that I'm most excited about is how we formally define security for a system at the wire-I/O-level --- we do this with a new security definition called "information-preserving refinement," inspired by the real/ideal paradigm from theoretical cryptography.

HN has been a huge part of my life since I started undergrad about 10 years ago (I post occasionally but mostly read). I would love to see some of the HN community there, whether in-person or over Zoom --- PhD thesis defense talks are open to the public, and my talk is aimed at a general CS/systems audience!