Modular Verification of Secure and Leakage-Free Systems:
From Application Specification to Circuit-Level Implementation

Anish Athalye, Henry Corrigan-Gibbs, M. Frans Kaashoek, Joseph Tassarotti, Nickolai Zeldovich

Parfait developer workflow and verification approach

Parfait is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by an application specification. Parfait proofs cover the software and the hardware of an HSM, which catches bugs above the cycle-level digital circuit abstraction, including timing side channels. Parfait’s contribution is a scalable approach to proving security and non-leakage by using intermediate levels of abstraction and relating them with transitive information-preserving refinement. This enables Parfait to use different techniques to verify the implementation at different levels of abstraction, reuse existing verified components such as CompCert, and automate parts of the proof, while still providing end-to-end guarantees. We use Parfait to verify four HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. Parfait provides strong guarantees for these HSMs: for instance, it proves that the ECDSA-on-Ibex HSM implementation—2,300 lines of code and 13,500 lines of Verilog—leaks nothing more than what is allowed by a 40-line specification of its behavior.

paper   poster   code [ipr formalization, verified HSMs]

We love answering questions about our work! Send Anish an email at aathalye@mit.edu.

Parfait uses the definition of information-preserving refinement (IPR) and builds on top of the framework from our prior work Knox (OSDI’22). Knox builds on top of the RTL-level verification framework from our prior work Notary (SOSP’19).

Anish’s PhD thesis contains a unified presentation of the ideas contained in the three papers, so that’s a good place to start if you want to understand the complete picture from start to finish. It is also currently the only document that describes the formalization of IPR (Chapter 4).

We took some detours along the way. We built Chroniton (PLARCH’23) for verifying constant-time execution of cryptographic code on hardware. We built K2 (KISV’23), a precursor to Parfait that isn’t verified end-to-end, which uses the RISC-V PMP to isolate sensitive code from persistent memory and I/O.