OpenTitan Security Verification: An Information Flow Tracking (IFT) Approach

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 secu­rity 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 secu­rity 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 Authen­tication Code, and Hash-based Message Authentication Code
• Multiple memories, including ROM, FLASH, static random-access memory, and one-time program­mable memory
• Dedicated controllers for access control and scrambling purposes Different input–output peripherals

OpenTitan’s threat model, which describes security assets, poten­tial 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 guide­lines, 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 coun­termeasure verification framework, and design guides, and it integrates with both formal and simulation-based verifica­tion tools.

IFT Security Verification

Using IFT, veri­fication 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, secu­rity 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.