Links

• My Github Repositories

  My Github page contains git repositories of publicly released software, including the open-source Secure Virtual Architecture software and the KCoFI proofs written in Coq.

• The LLVM Compiler Infrastructure

  I began working with LLVM in 2003 at the University of Illinois. It's a very nice compiler infrastructure, and I've used it in nearly all of my research projects.

• Secure Virtual Architecture

  I am the lead developer on the Secure Virtual Architecture (SVA). SVA enforces safety properties on commodity operating system kernels.

• KCoFI Pudding

  As part of my work on control-flow integrity for operating system kernels, I developed semantics and proofs vetting my design. Those proofs, written in Coq, are available at the above URL.

• University of Rochester

  My current employer.

• University of Illinois

  My alma mater and previous employer.

Menu