Modular Verification of Non-Leakage for Hardware Security Modules with Parfait
Anish Athalye, Henry Corrigan-Gibbs, Frans Kaashoek, Joseph Tassarotti, Nickolai Zeldovich
Materials
Abstract
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.
