Proving an Embedded Server from RISC-V to X25519 over UDP
Andres Erbsen
Video
Abstract:
Seriously seeking systematic improvement in security and reliability of computer systems leads us to pursue formal verification of computer systems, which can rule out large classes of bugs. However, the assurances offered by individual verification of computer-systems components are limited because it is exceedingly difficult to specify the correctness of each component in isolation, and subtle bugs can arise from combining of independently defensible components. 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 strategy 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 with optimized cryptographic arithmetic implemented using higher-order functional templates to produce 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, 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 also 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.