Verifying Hardware Security Modules with Information-Preserving Refinement
For an easy-to-understand but complete example of an HSM verified with Knox, see our “Lockbox” example, a simplified version of PIN-protected backup with a simplified I/O interface, implemented in a single Verilog module.
- Specification:
exposes the
storeandgetoperations. - Implementation: a circuit that exposes a couple data buses and an enable wire.
- Driver: describes how spec-level operations map to wire-level I/O.
- Emulator: captures non-leakage by describing how to mimic wire-level behavior in terms of spec-level operations. This particular emulator is written “from scratch”; rather than using the construction where it uses a copy of the circuit, it directly implements behavior that mimics the circuit. For an emulator for a similar circuit that uses the more common approach, see any other emulator in the repository, such as the emulator for the counter.
paper poster code [knox framework, HSMs]
Knox is a new framework that enables developers to build hardware security modules (HSMs) with high assurance through formal verification. The goal is to rule out all hardware bugs, software bugs, and timing side channels.
Knox’s approach is to relate an implementation’s wire-level behavior to a functional specification stated in terms of method calls and return values with a new definition called information-preserving refinement (IPR). This definition captures the notion that the HSM implements its functional specification, and that it leaks no additional information through its wire-level behavior. The Knox framework provides support for writing specifications, importing HSM implementations written in Verilog and C code, and proving IPR using a combination of lightweight annotations and interactive proofs.
To evaluate the IPR definition and the Knox framework, we verified three simple HSMs, including an RFC 6238-compliant TOTP token. The TOTP token is written in 2950 lines of Verilog and 360 lines of C and assembly. Its behavior is captured in a succinct specification: aside from the definition of the TOTP algorithm, the spec is only 10 lines of code. In all three case studies, verification covers entire hardware and software stacks and rules out hardware/software bugs and timing side channels.
Knox TOTP prototype, running on an FPGA