USENIX Security2021Top-tier venue
DICE*: A Formally Verified Implementation of DICE Measured Boot
Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, Aditya V. Thakur
Abstract
Measured boot is an important class of boot protocols that ensure that each layer of firmware and software in a device's chain of trust is measured, and the measurements are reliably recorded for subsequent verification. This paper presents DICE , a formal specification as well as a formally verified implementation of DICE, an industry standard measured boot protocol. DICE is proved to be functionally correct, memorysafe, and resistant to timing-and cache-based side-channels. A key component of DICE is a verified certificate creation library for a fragment of X.509. We have integrated DICE into the boot firmware of an STM32H753ZI micro-controller. Our evaluation shows that using a fully verified implementation has minimal to no effect on the code size and boot time when compared to an existing unverified implementation.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 065d4c93-983d-4007-ae8c-d60616b5f185Cited by top-tier papers5
- PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed ProgramsGabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier et al.PLDI 2025 · 8 citations
- Towards Neural Synthesis for SMT-Assisted Proof-Oriented ProgrammingSaikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury et al.ICSE 2025 · 4 citations
- SoK: Integrity, Attestation, and Auditing of Program ExecutionMahmoud Ammar, Adam Caulfield, Ivan De Oliveira NunesS&P 2025
- Towards Practical, End-to-End Formally Verified X.509 Certificate Validators with VerdictZhengyao Lin, Michael McLoughlin, Pratap Singh, Rory Brennan-Jones et al.USENIX Security 2025
- Secret State Leakage Attacks and Their Impacts on EMV Contactless Payment AppsJesse Chen, Rubin Yuchan Yang, Ahmad Musa, Syed Rafiul Hussain et al.S&P 2026
Builds on6
- HACL*: A Verified Modern Cryptographic LibraryJean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin BeurdoucheCCS 2017 · 258 citations
- EverCrypt: A Fast, Verified, Cross-Platform Cryptographic ProviderJonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel et al.S&P 2020 · 114 citations
- Formal verification of a constant-time preserving C compilerGilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin et al.POPL 2020 · 77 citations
- EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message FormatsTahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy et al.USENIX Security 2019 · 70 citations
- Dominance as a New Trusted Computing Primitive for the Internet of ThingsMeng Xu, Manuel Huber, Zhichuang Sun, Paul England et al.S&P 2019 · 61 citations
Related papers
- Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSETahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil SwamyCCS 2025
- Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernelLuke Nelson, Jacob Van Geffen, Emina Torlak, Xi WangOSDI 2020 · 72 citations
- The Last Mile: High-Assurance and High-Speed Cryptographic ImplementationsJosé Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire et al.S&P 2020 · 67 citations
- DICE: Automatic Emulation of DMA Input Channels for Dynamic Firmware AnalysisAlejandro Mera, Bo Feng, Long Lu, Engin KirdaS&P 2021 · 81 citations
- EC: Embedded Systems Compartmentalization via Intra-Kernel IsolationArslan Khan, Dongyan Xu, Dave Jing TianS&P 2023
