Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code.

We perform a preliminary security analysis of the initial boot stage for the OpenTitan silicon root of trust, including formalisation and verification of relevant security goals using both bounded model checking and (unbounded) model checking. We further report on a potential vulnerability in the platform and show how it can be reproduced using formal modelling and argue that co-verification would be able to detect such vulnerabilities for high assurance projects.