TY - GEN
T1 - Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code
AU - Møller, Bjarke Hilmer
AU - Søndergaard, Jacob Gosch
AU - Jensen, Kristoffer Skagbæk
AU - Pedersen, Magnus Winkel
AU - Bøgedal, Tobias Worm
AU - Christensen, Anton
AU - Poulsen, Danny Bøgsted
AU - Larsen, Kim Guldstrand
AU - Hansen, René Rydhof
AU - Rosted Jensen, Thomas
AU - Juvoll Madsen, Heino
AU - Uhrenfeldt, Henrik
PY - 2021/12/10
Y1 - 2021/12/10
N2 - 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.
AB - 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.
KW - Co-verification
KW - Formal methods
KW - Hardware modelling
KW - Security
UR - http://www.scopus.com/inward/record.url?scp=85119856071&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-91625-1_11
DO - 10.1007/978-3-030-91625-1_11
M3 - Article in proceeding
SN - 978-3-030-91624-4
T3 - Lecture Notes in Computer Science
SP - 192
EP - 211
BT - Secure IT Systems
A2 - Tuveri, Nicola
A2 - Michalas, Antonis
A2 - Brumley, Billy Bob
PB - Springer
T2 - 26th Nordic Conference on Secure IT Systems, NordSec 2021
Y2 - 29 November 2021 through 30 November 2021
ER -