We are working towards building end-to-end verified hardware/software systems. Our current project is Knox, a framework for verifying HSMs’ correctness and security. It builds on our past research on Kronos, a system for verifying output determinism for SoCs with multiple clock domains, and Notary, a device for secure transaction approval.
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.
- Verifying Hardware Security Modules with Information-Preserving Refinement (OSDI ‘22)
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.
- 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 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.