@inproceedings{tao2021dice,
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},
year = {2021},
month = {August},
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, 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.

DICE* is open source at: https://github.com/verified-HRoT/dice-star},
url = {http://approjects.co.za/?big=en-us/research/publication/dice-a-formally-verified-implementation-of-dice-measured-boot/},
}