Security Verification of the OpenTitan Hardware Root of Trust
Andres Meza, Francesco Restuccia, Jason K. Oberg, Dominic Rizzo, Ryan Kastner · IEEE Security & Privacy · 2023
We describe the security verification of OpenTitan. We illustrate how information flow tracking turns human knowledge of assets and security requirements into formal security properties verified using Cycuity’s Radix. The verification uncovered weaknesses and helped produce hardware fixes to eliminate vulnerabilities.