Project overview
We are working on building systems that are free of correctness bugs, security bugs, and timing side channels using formal verification. Our most recent project is Parfait (SOSP ‘24), a scalable approach to verifying HSMs’ correctness and security. It builds on our past research on K2 (KISV ‘23), an architecture for formally-verified HSMs; Chroniton (PLARCH ‘23), a tool for verifying constant-time cryptography at a cycle-precise level; Knox (OSDI ‘22), a framework for verifying HSMs’ correctness and security; Kronos (CARRV ‘21), a system for verifying output determinism for SoCs with multiple clock domains; and Notary (SOSP ‘19), a device for secure transaction approval.
Parfait
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.
Publications
- Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation (SOSP ‘24)
- Code: IPR theory, verified HSMs
- Talk (slides)
- Formally Verifying Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation (PhD thesis)
K2
K2 is a new architecture and verification approach for hardware security modules (HSMs). The K2 architecture’s rigid separation between I/O, storage, and computation over secret state enables modular proofs and allows for software development and verification independent of hardware development and verification while still providing correctness and security guarantees about the composed system. For a key step of verification, K2 introduces a new tool called Chroniton that automatically proves timing properties of software running on a particular hardware implementation, ensuring the lack of timing side channels at a cycle-accurate level.
Publications
Chroniton
We propose abandoning leakage models for verifying timing properties of cryptographic software, instead directly verifying software with respect to a hardware implementation at the RTL level. Early experiments include verifying that an Ed25519 implementation running on a 6-stage pipelined processor executes in a constant number of cycles. Many challenges remain, including scaling up to modern out-of-order speculative cores and extending the approach to reason about library code outside the context of a whole application.
Publications
- Leakage models are a leaky abstraction: the case for cycle-level verification of constant-time cryptography (PLARCH ‘23)
Knox
Knox is a framework for building correct and secure hardware security modules (HSMs) through formal verification spanning an implementation’s hardware and software. One key challenge addressed by Knox is defining what it means for an HSM to be secure. With information-preserving refinement (IPR), we capture the idea that an HSM implementation (spanning hardware and software), modeled at the level of wires and cycles, leaks no more information beyond what is allowed by its functional specification.
Publications
- Verifying Hardware Security Modules with Information-Preserving Refinement (OSDI ‘22)
- Code: Knox framework, HSMs
- Talk (slides)
Kronos
Kronos is a system for verifying output determinism of SoCs with multiple clock domains. Output determinism says that after a reset (+ running initialization code), a SoCs externally-observable behavior does not depend on its pre-reset state, including microarchitectural state.
Publications
- rtlv: push-button verification of software on hardware (CARRV ‘21)
- Kronos: Verifying leak-free reset for a system-on-chip with multiple clock domains (MEng thesis)
Notary
Notary is a new hardware and software architecture for running isolated approval agents in the form factor of a USB stick with a small display and buttons. Approval agents allow factoring out critical security decisions, such as getting the user’s approval to sign a Bitcoin transaction or to delete a backup, to a secure environment. The key challenge addressed by Notary is to securely switch between agents on the same device. Prior systems either avoid the problem by building single-function devices like a USB U2F key, or they provide weak isolation that is susceptible to kernel bugs, side channels, or Rowhammer-like attacks. Notary achieves strong isolation using reset-based switching, along with the use of physically separate systems-on-a-chip for agent code and for the kernel, and a machine-checked proof of both the hardware’s register-transfer-level design and software, showing that reset-based switching leaks no state. Notary also provides a trustworthy I/O path between the agent code and the user, which prevents an adversary from tampering with the user’s screen or buttons.
