Project overview
We are working towards building end-to-end verified hardware/software systems. Our current project is K2, an architecture for formally-verified HSMs. It builds on our past research on Chroniton, a tool for verifying constant-time cryptography at a cycle-precise level, Knox, a framework for verifying HSMs’ correctness and security, Kronos, a system for verifying output determinism for SoCs with multiple clock domains, and Notary, a device for secure transaction approval.
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.
