DICE*: A Formally Verified Implementation of DICE Measured Boot

Tao, Zhe and Rastogi, Aseem and Gupta, Naman and Vaswani, Kapil and Thakur, Aditya V.
30th USENIX Security Symposium (USENIX Security ’21 Fall), 2021

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.

PDF    

@inproceedings{USENIX2021,
  author = {Tao, Zhe and Rastogi, Aseem and Gupta, Naman and Vaswani, Kapil and Thakur, Aditya V.},
  title = {DICE*: A Formally Verified Implementation of DICE Measured Boot},
  booktitle = {30th {USENIX} Security Symposium (USENIX Security '21 Fall)},
  year = {2021}
}