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

Bjarke Hilmer Møller; Jacob Gosch Søndergaard; Kristoffer Skagbæk Jensen; Magnus Winkel Pedersen; Tobias Worm Bøgedal; Anton Christensen; Danny Bøgsted Poulsen; Kim Guldstrand Larsen; René Rydhof Hansen; Thomas Rosted Jensen; Heino Juvoll Madsen; Henrik Uhrenfeldt

doi:10.1007/978-3-030-91625-1_11

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

Bjarke Hilmer Møller, Jacob Gosch Søndergaard, Kristoffer Skagbæk Jensen, Magnus Winkel Pedersen, Tobias Worm Bøgedal, Anton Christensen^*, Danny Bøgsted Poulsen, Kim Guldstrand Larsen, René Rydhof Hansen, Thomas Rosted Jensen, Heino Juvoll Madsen, Henrik Uhrenfeldt

^*Corresponding author for this work

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

1 Citation (Scopus)

Abstract

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.

Original language	English
Title of host publication	Secure IT Systems : 26th Nordic Conference, NordSec 2021, Virtual Event, November 29–30, 2021, Proceedings
Editors	Nicola Tuveri, Antonis Michalas, Billy Bob Brumley
Number of pages	20
Publisher	Springer
Publication date	10 Dec 2021
Pages	192-211
ISBN (Print)	978-3-030-91624-4
ISBN (Electronic)	978-3-030-91625-1
DOIs	https://doi.org/10.1007/978-3-030-91625-1_11
Publication status	Published - 10 Dec 2021
Event	26th Nordic Conference on Secure IT Systems, NordSec 2021 - Virtual, Online Duration: 29 Nov 2021 → 30 Nov 2021

Conference

Conference	26th Nordic Conference on Secure IT Systems, NordSec 2021
City	Virtual, Online
Period	29/11/2021 → 30/11/2021

Series	Lecture Notes in Computer Science
Volume	LNCS 13115
ISSN	0302-9743

Keywords

Co-verification
Formal methods
Hardware modelling
Security

Access to Document

10.1007/978-3-030-91625-1_11

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

Møller, B. H., Søndergaard, J. G., Jensen, K. S., Pedersen, M. W., Bøgedal, T. W., Christensen, A., Poulsen, D. B., Larsen, K. G., Hansen, R. R., Rosted Jensen, T., Juvoll Madsen, H., & Uhrenfeldt, H. (2021). Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code. In N. Tuveri, A. Michalas, & B. B. Brumley (Eds.), Secure IT Systems: 26th Nordic Conference, NordSec 2021, Virtual Event, November 29–30, 2021, Proceedings (pp. 192-211). Springer. https://doi.org/10.1007/978-3-030-91625-1_11

Møller, Bjarke Hilmer ; Søndergaard, Jacob Gosch ; Jensen, Kristoffer Skagbæk et al. / Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code. Secure IT Systems: 26th Nordic Conference, NordSec 2021, Virtual Event, November 29–30, 2021, Proceedings. editor / Nicola Tuveri ; Antonis Michalas ; Billy Bob Brumley. Springer, 2021. pp. 192-211 (Lecture Notes in Computer Science, Vol. LNCS 13115).

@inproceedings{16cec89e036d435ca30ef4b9ffcaf90e,

title = "Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code",

abstract = "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.",

keywords = "Co-verification, Formal methods, Hardware modelling, Security",

author = "M{\o}ller, {Bjarke Hilmer} and S{\o}ndergaard, {Jacob Gosch} and Jensen, {Kristoffer Skagb{\ae}k} and Pedersen, {Magnus Winkel} and B{\o}gedal, {Tobias Worm} and Anton Christensen and Poulsen, {Danny B{\o}gsted} and Larsen, {Kim Guldstrand} and Hansen, {Ren{\'e} Rydhof} and {Rosted Jensen}, Thomas and {Juvoll Madsen}, Heino and Henrik Uhrenfeldt",

year = "2021",

month = dec,

day = "10",

doi = "10.1007/978-3-030-91625-1_11",

language = "English",

isbn = "978-3-030-91624-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "192--211",

editor = "Nicola Tuveri and Antonis Michalas and Brumley, {Billy Bob}",

booktitle = "Secure IT Systems",

address = "Germany",

note = "26th Nordic Conference on Secure IT Systems, NordSec 2021 ; Conference date: 29-11-2021 Through 30-11-2021",

}

Møller, BH, Søndergaard, JG, Jensen, KS, Pedersen, MW, Bøgedal, TW, Christensen, A, Poulsen, DB , Larsen, KG , Hansen, RR, Rosted Jensen, T, Juvoll Madsen, H & Uhrenfeldt, H 2021, Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code. in N Tuveri, A Michalas & BB Brumley (eds), Secure IT Systems: 26th Nordic Conference, NordSec 2021, Virtual Event, November 29–30, 2021, Proceedings. Springer, Lecture Notes in Computer Science, vol. LNCS 13115, pp. 192-211, 26th Nordic Conference on Secure IT Systems, NordSec 2021, Virtual, Online, 29/11/2021. https://doi.org/10.1007/978-3-030-91625-1_11

Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code. / Møller, Bjarke Hilmer; Søndergaard, Jacob Gosch; Jensen, Kristoffer Skagbæk et al.
Secure IT Systems: 26th Nordic Conference, NordSec 2021, Virtual Event, November 29–30, 2021, Proceedings. ed. / Nicola Tuveri; Antonis Michalas; Billy Bob Brumley. Springer, 2021. p. 192-211 (Lecture Notes in Computer Science, Vol. LNCS 13115).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

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 -

Møller BH, Søndergaard JG, Jensen KS, Pedersen MW, Bøgedal TW, Christensen A et al. Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code. In Tuveri N, Michalas A, Brumley BB, editors, Secure IT Systems: 26th Nordic Conference, NordSec 2021, Virtual Event, November 29–30, 2021, Proceedings. Springer. 2021. p. 192-211. (Lecture Notes in Computer Science, Vol. LNCS 13115). doi: 10.1007/978-3-030-91625-1_11

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

Abstract

Conference

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Cite this