Abstracting Architectures: Two Techniques in Formal Hardware Security Verification
Alejandro Sanchez Ocegueda
EECS Department, University of California, Berkeley
Technical Report No. UCB/EECS-2025-169
August 15, 2025
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-169.pdf
Recent years have seen a dramatic increase in cyberattacks that target vulnerable hardware. One of the most effective ways to mitigate such vulnerabilities is to formally verify that hardware designs adhere to security standards. However, in a world with an insatiable need for performance, tight development cycles, and ever-evolving technical demands, verification efforts often fail to keep pace with hardware development. In this work, we present two approaches to making formal verification more efficient.
Our first contribution is a formal model for pointer-encryption schemes, U2. This model serves as a formal foundation for any system that enforces memory safety by using cryptography to protect pointers and data. We implement our model in UCLID5, and prove that it satisfies all desired security properties.
Our second contribution is BtorSec, a security-aware extension of the popular Btor2 format. By adding new cryptographic instructions, BtorSec enables formal reasoning about cryptography in real-world RTL designs. Additionally, we implement a compiler and a proof-of-concept solver for security queries on BtorSec programs.
Together, these contributions advance the state of the art in hardware security verification, enabling earlier detection of vulnerabilities and lowering the barrier to adopting formal methods in modern hardware design.
Advisors: Sanjit A. Seshia
BibTeX citation:
@mastersthesis{Sanchez Ocegueda:EECS-2025-169,
Author= {Sanchez Ocegueda, Alejandro},
Title= {Abstracting Architectures: Two Techniques in Formal Hardware Security Verification},
School= {EECS Department, University of California, Berkeley},
Year= {2025},
Month= {Aug},
Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-169.html},
Number= {UCB/EECS-2025-169},
Abstract= {Recent years have seen a dramatic increase in cyberattacks that target vulnerable hardware.
One of the most effective ways to mitigate such vulnerabilities is to formally verify that hardware designs adhere to security standards.
However, in a world with an insatiable need for performance, tight development cycles, and ever-evolving technical demands, verification efforts often fail to keep pace with hardware development.
In this work, we present two approaches to making formal verification more efficient.
Our first contribution is a formal model for pointer-encryption schemes, U2.
This model serves as a formal foundation for any system that enforces memory safety by using cryptography to protect pointers and data.
We implement our model in UCLID5, and prove that it satisfies all desired security properties.
Our second contribution is BtorSec, a security-aware extension of the popular Btor2 format.
By adding new cryptographic instructions, BtorSec enables formal reasoning about cryptography in real-world RTL designs.
Additionally, we implement a compiler and a proof-of-concept solver for security queries on BtorSec programs.
Together, these contributions advance the state of the art in hardware security verification, enabling earlier detection of vulnerabilities and lowering the barrier to adopting formal methods in modern hardware design.},
}
EndNote citation:
%0 Thesis %A Sanchez Ocegueda, Alejandro %T Abstracting Architectures: Two Techniques in Formal Hardware Security Verification %I EECS Department, University of California, Berkeley %D 2025 %8 August 15 %@ UCB/EECS-2025-169 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-169.html %F Sanchez Ocegueda:EECS-2025-169