Security verification for hardware is literally foundational: hardware resides on technology’s ground floor, so attacks on it can impact every floor above it, including
- operating systems,
- applications, and
- communications.
To examine technology’s hardware foundation, a group of researchers recently used simulation-based hardware information-flow tracking (IFT) for hardware security verification.
IFT uses knowledge of design assets to define
- security requirements,
- objectives, and
- boundaries.
The researchers used IFT—as embodied in Cycuity’s Radix—to run a security verification on OpenTitan, an open-source hardware root of trust (RoT). Their effort focused on a key component of OpenTitan security: its one-time programmable (OTP) memory controller.
The OTP plays a pivotal role in OpenTitan’s security because it holds data for three key operations:
- Secure boot
- Lifecycle provisioning
- Attestation
The researchers discuss this project in the IEEE Security & Privacy article, “Security Verification of the OpenTitan Hardware Root of Trust.” The article includes a step-by-step description of the security verification on OpenTitan’s OTP and how it
- formalized the security property,
- identified a potential weakness,
- debugged the root cause, and
- repaired the flaw.
Here, we offer a brief overview of the article.
OpenTitan Overview
OpenTitan performs security-critical functionalities including secure boot, operation mode configurations, and sensitive data management. It comprises the following components:
- A security-enhanced RV32IMCB RISC-V Ibex core
- Security peripherals such as Advanced Encryption Standard, Keccak Message Authentication Code, and Hash-based Message Authentication Code
- Multiple memories, including ROM, FLASH, static random-access memory, and one-time programmable memory
- Dedicated controllers for access control and scrambling purposes
Different input–output peripherals
OpenTitan’s threat model, which describes security assets, potential attacker profiles, attack surfaces, and methods, is used to derive relevant security requirements. The security model it defines includes
- device provisioning and run-time operations,
- secure hardware design guidelines, and
- functional guarantees.
For its target users—enterprises, platform providers, and chip manufacturers—OpenTitan can serve as a platform integrity module, universal second-factor security key, and a trusted platform module.
The OpenTitan RoT comprises testing plans, testbench architecture, a security countermeasure verification framework, and design guides, and it integrates with both formal and simulation-based verification tools.
IFT Security Verification
Using IFT, verification engineers can reason about noninterference expressed as a hyperproperty; this provides a more concise, expressive representation of the confidentiality, integrity, and availability that are crucial for hardware security verification.
Simulation-based hardware IFT analysis offers two key benefits:
- It quickly moves knowledge about design assets to define security requirements, security objectives, and security boundaries.
- It enables concise specification of security properties related to confidentiality, integrity, and availability.
The OpenTitan Verification and Its Findings
The researchers used Radix, an IFT-enhanced simulation tool, to formalize and verify OpenTitan’s OTP security requirements.
The article describes in detail how the researchers derived requirements for this asset and its operation, wrote formal properties that specified the requirements, and then verified them in a step-by-step process.
The effort uncovered a potential weakness in OpenTitan, which the researchers disclosed—along with a proposed solution—to the OpenTitan team; it then issued a patch to mitigate the leakage.
Dig Deeper
The article reporting on this project illustrates how IFT can turn human knowledge of assets and security requirements into formal, verifiable properties.
To read more about this project and the six-step security verification of the OpenTitan OTP memory controller, check out “Security Verification of the OpenTitan Hardware Root of Trust,” by Andres Meza, Francesco Restuccia, Jason Oberg, Dominic Rizzo, and Ryan Kastner.
