Zhe Tao, University of California, Davis; Aseem Rastogi, Naman Gupta, and Kapil Vaswani, Microsoft Research; Aditya V. Thakur, University of California, Davis
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, memory-safe, 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.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
author = {Zhe Tao and Aseem Rastogi and Naman Gupta and Kapil Vaswani and Aditya V. Thakur},
title = {{DICE*}: A Formally Verified Implementation of {DICE} Measured Boot},
booktitle = {30th USENIX Security Symposium (USENIX Security 21)},
year = {2021},
isbn = {978-1-939133-24-3},
pages = {1091--1107},
url = {https://www.usenix.org/conference/usenixsecurity21/presentation/tao},
publisher = {USENIX Association},
month = aug
}
