Security Verification of the OpenTitan Hardware Root of Trust
Andres Meza, Francesco Restuccia, Jason Oberg, Dominic Rizzo, Ryan Kastner
Abstract
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.
Topics & Concepts
Computer scienceComputer securityIntelligent verificationFormal verificationRoot (linguistics)Information flowProgramming languageSoftwareLinguisticsSoftware systemSoftware constructionPhilosophySecurity and Verification in ComputingAdvanced Malware Detection TechniquesCloud Data Security Solutions