Modular Verification of Non-Leakage for Hardware Security Modules with K2

K2 is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by its functional specification. K2's proof covers the software and the hardware of an HSM, which enables it to catch all bugs above the cycle-level digital circuit abstraction, including timing side channels. K2's key contribution is a novel approach to proving non-leakage in a modular fashion, using transitive information-preserving refinement. This enables K2 to use different techniques for verifying different layers (software and hardware), reuse existing verified components, and largely automate several parts of the proof, while still providing a single top-to-bottom combined theorem. We use K2 to develop several HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. K2 provides a strong guarantee 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 50-line specification of its behavior.