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.
@article{obergsecurity,
title={Security Verification of the OpenTitan Hardware Root of Trust},
author={Oberg, Jason and Rizzo, Cycuity Dominic and Kastner, OpenTitan Ryan and others}
}
https://csdl-downloads.ieeecomputer.org/mags/sp/5555/01/10106105.pdf