Charles Averill, Ilan Buzzetti (The University of Texas at Dallas), Alex Bellon (UC San Diego), Kevin Hamlen (The University of Texas at Dallas)
LAPSE is a new framework for developing faulttolerant correctness proofs for near-arbitrary native code. It lifts binary code into an intermediate representation (IR) whose operational semantics admit hardware faults. LAPSE implements a machine-verified symbolic execution engine for the resulting IR within the Rocq automated theorem proving framework, creating a proof environment in which the space of possible executions includes all potential fault possibilities. To cope with the increase in proof space, automation tools succinctly describe and reason about the desired fault model. An implementation for 32-bit RISC-V semantics and evaluation on security-critical cryptographic subroutines from OpenSSL and BearSSL demonstrates that fault-aware proofs can be constructed from standard correctness proofs with little additional work, often requiring no novel proof techniques. The results show that developing fault-tolerant correctness proofs is not only feasible, but rote for certain kinds of fault-tolerant programs.