{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:53:11Z","timestamp":1743065591611,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030916244"},{"type":"electronic","value":"9783030916251"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91625-1_11","type":"book-chapter","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T00:03:08Z","timestamp":1636761788000},"page":"192-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code"],"prefix":"10.1007","author":[{"given":"Bjarke Hilmer","family":"M\u00f8ller","sequence":"first","affiliation":[]},{"given":"Jacob Gosch","family":"S\u00f8ndergaard","sequence":"additional","affiliation":[]},{"given":"Kristoffer Skagb\u00e6k","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Magnus Winkel","family":"Pedersen","sequence":"additional","affiliation":[]},{"given":"Tobias Worm","family":"B\u00f8gedal","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9430-603X","authenticated-orcid":false,"given":"Anton","family":"Christensen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9623-0748","authenticated-orcid":false,"given":"Danny B\u00f8gsted","family":"Poulsen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5953-3384","authenticated-orcid":false,"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5688-6432","authenticated-orcid":false,"given":"Ren\u00e9 Rydhof","family":"Hansen","sequence":"additional","affiliation":[]},{"given":"Thomas Rosted","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Heino Juvoll","family":"Madsen","sequence":"additional","affiliation":[]},{"given":"Henrik","family":"Uhrenfeldt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Andrews, J.R.: Co-verification of Hardware and Software for ARM SoC Design. Elsevier (2005)","DOI":"10.1016\/B978-075067730-1\/50007-4"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Casper, W.D., Papa, S.M.: Root of trust. In: Encyclopedia of Cryptography and Security, 2nd Ed, pp. 1057\u20131060. Springer (2011). https:\/\/doi.org\/10.1007\/978-1-4419-5906-5_789","DOI":"10.1007\/978-1-4419-5906-5_789"},{"key":"11_CR3","unstructured":"Gigerl, B., Hadzic, V., Primas, R., Mangard, S., Bloem, R.: Coco: Co-design and co-verification of masked software implementations on CPUs. In: Proceedings of the 30th USENIX Security Symposium (USENIX Security 2021). pp. 1469\u20131468 (Aug 2021), https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/gigerl"},{"key":"11_CR4","unstructured":"Google: Advisory: Security issue with Bluetooth Low Energy (BLE) Titan security keys. Google Security Blog (May 2019), https:\/\/security.googleblog.com\/2019\/05\/titan-keys-update.html, web page, last accessed 21 august 2021"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Huang, B., Ray, S., Gupta, A., Fung, J.M., Malik, S.: Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. In: Proceedings of the 55th Annual Design Automation Conference (DAC 2018). pp. 91:1\u201391:6 (2018). https:\/\/doi.org\/10.1145\/3195970.3196055","DOI":"10.1145\/3195970.3196055"},{"key":"11_CR6","unstructured":"Huang, B., Zhang, H., Subramanyan, P., Vizel, Y., Gupta, A., Malik, S.: Instruction-level abstraction (ILA): A uniform specification for system-on-chip (SoC) verification. CoRR abs\/1801.01114 (2018), http:\/\/arxiv.org\/abs\/1801.01114"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Kroening, D., Tautschnig, M.: CBMC - C bounded model checker. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). Lecture Notes in Computer Science, vol. 8413, pp. 389\u2013391 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Larsen, K., Pettersson, W., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer 1 (1997)","DOI":"10.1007\/s100090050010"},{"key":"11_CR9","unstructured":"Mukherjee, R., Joshi, S., O\u2019Leary, J., Kroening, D., Melham, T.: Hardware\/software co-verification using path-based symbolic execution. arXiv CoRR abs\/2001.01324 (2020), http:\/\/arxiv.org\/abs\/2001.01324"},{"key":"11_CR10","unstructured":"M\u00f8ller, B., Pedersen, M., B\u00f8gedal, T.: Formally Verifying Security Properties for OpenTitan Boot Code with Uppaal. Master\u2019s thesis, Aalborg University (2021), https:\/\/projekter.aau.dk\/projekter\/files\/422795285\/P10__24_.pdf"},{"key":"11_CR11","unstructured":"M\u00f8ller, B.H., S\u00f8ndergaard, J.G., Jensen, K.S., Pedersen, M.W., B\u00f8gedal, T.W.: Evaluation of Tools for Formal Verification of OpenTitan Boot Code. Project report, Aalborg University (2020), https:\/\/github.com\/Tutter\/OpenTitan-Formal-Verification\/blob\/d830c\/P9-EvaluationOfToolsForFormalVerificationOfOpenTitan.pdf"},{"key":"11_CR12","unstructured":"Nunes, I.D.O., Eldefrawy, K., Rattanavipanon, N., Steiner, M., Tsudik, G.: VRASED: A verified hardware\/software co-design for remote attestation. In: 28th USENIX Security Symposium (USENIX Security 2019). pp. 1429\u20131446 (2019), https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/de-oliveira-nunes"},{"key":"11_CR13","unstructured":"OpenTitan: HMAC HWIP technical specification, https:\/\/docs.opentitan.org\/hw\/ip\/hmac\/doc, web page, last accessed 2021\u201326-08"},{"key":"11_CR14","unstructured":"OpenTitan: hmac.sv, https:\/\/github.com\/lowRISC\/opentitan\/blob\/dcdadc72072\/hw\/ip\/hmac\/rtl\/hmac.sv#L121, web page, last accessed 2021\u201326-08"},{"key":"11_CR15","unstructured":"OpenTitan: Identities and root keys, https:\/\/docs.opentitan.org\/doc\/security\/specs\/identities_and_root_keys\/, web page, last accessed 2021\u201319-08"},{"key":"11_CR16","unstructured":"OpenTitan: Key manager hwip technical specification, https:\/\/docs.opentitan.org\/hw\/ip\/keymgr\/doc\/, web page, last accessed 2021\u201325-08"},{"key":"11_CR17","unstructured":"OpenTitan: OpenTitan logical security model, https:\/\/docs.opentitan.org\/doc\/security\/logical_security_model\/, web page, last accessed 2021\u201317-08"},{"key":"11_CR18","unstructured":"OpenTitan: Opentitan secure boot, https:\/\/docs.opentitan.org\/doc\/security\/specs\/secure_boot\/, web page, last accessed 2021\u201319-08"},{"key":"11_CR19","unstructured":"Roche, T., Lomn\u00e9, V., Mutschler, C., Imbert, L.: A side journey to Titan. In: Proceedings of the 30th USENIX Security Symposium (USENIX Security 2021). pp. 231\u2013248 (Aug 2021), https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/roche"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Subramanyan, P., Vizel, Y., Ray, S., Malik, S.: Template-based synthesis of instruction-level abstractions for SoC verification. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2015). pp. 160\u2013167 (2015)","DOI":"10.1109\/FMCAD.2015.7542266"},{"key":"11_CR21","unstructured":"S\u00f8ndergaard, J., Jensen, K.: Formally Verifying the Correctness and Safety of OpenTitan Boot Code using CBMC. Master\u2019s thesis, Aalborg Univeristy (2021), https:\/\/projekter.aau.dk\/projekter\/files\/422795280\/P10__23_.pdf"},{"key":"11_CR22","unstructured":"Yubico: Security advisories. Yubico web page, https:\/\/www.yubico.com\/support\/security-advisories\/, security advisories relating to Yubi key. Last accessed 21 august 2021"}],"container-title":["Lecture Notes in Computer Science","Secure IT Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91625-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,19]],"date-time":"2021-11-19T00:12:54Z","timestamp":1637280774000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91625-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030916244","9783030916251"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91625-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"13 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NordSec","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nordic Conference on Secure IT Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nordsec2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/events.tuni.fi\/nordsec2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.83","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.47","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}