Verifying Hardware Security Modules with Information-Preserving Refinement

Explore a groundbreaking framework for building highly secure hardware security modules (HSMs) through formal verification in this OSDI '22 conference talk. Dive into the Knox framework, which aims to eliminate hardware bugs, software bugs, and timing side channels in HSMs. Learn about the novel concept of information-preserving refinement (IPR) and how it relates an implementation's wire-level behavior to a functional specification. Discover the framework's support for writing specifications, importing Verilog and C code implementations, and proving IPR using annotations and interactive proofs. Examine three case studies, including an RFC 6238-compliant TOTP token, to understand how verification covers entire hardware and software stacks. Gain insights into the challenges and benefits of creating HSMs with high assurance, and explore the potential impact on the future of hardware security.