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.

Intro
HSMs: powerful tools for securing s
HSMs suffer from bugs
Goal: HSMs without security vulnera
Approach: formal verification
Example: PIN-protected backup HS
How to relate implementation to spe
Information-preserving refinement
IPR: driver
IPR: emulator construction
IPR transfers security properties from spe
Knox framework
Evaluation: case studies
Subtle bug involving persistence and
Real implementations have similar c