Andres Erbsen
October 18, 2023 at 11:00 AM on Zoom / Soda Hall
Proving an Embedded Server from RISC-V to X25519 over UDP
Abstract:
Seriously seeking systematic improvement in security and reliability of computer systems leads us to formal verification, which can indeed rule out large classes of bugs. However, the appropriate notion of correctness for a computer-systems component is exceedingly difficult to specify in isolation, and unrelated verification of adjacent components does not rule out bugs due to their interactions. Instead treating specifications of intricate internal interfaces as proof details on the way to a more elementary specification elegantly bypasses this limitation, but until recently this principle had been realized only for simplified non-interactive systems.
I present a computer-checked mathematical proof of functional correctness for a small but free-standing and relatively conventional embedded system acting as a server with cryptographic authentication. Modular proofs in the Coq proof assistant connect drivers written in a C-like language and optimized cryptographic arithmetic implemented using higher-order functional templates to an application-level whole-system specification in terms of RISC-V machine code and MMIO traces. This result is enabled by the use of novel interface-specification techniques at the assembly and C levels to bypass long-standing challenges in compiler-correctness proofs and program verification. These interface contracts enable modular verification in the presence of underspecification, implementation constraints including undefined behavior, and runtime input. Consequently, the most domain-appropriate tools available in Coq can be used to verify each component, and the code and proofs of individual components support widespread use outside the demonstration system.
Bio: Andres recently received his PhD from MIT. His research interests lie at the intersection of formal verification, computer security, and computer systems. He prefers to seek principled, long-term solutions to practically important problems. His work has led to one of the largest deployments of formally verified code and was recently recognized with the PLDI distinguished paper award.