DICE*: A Formally Verified Implementation of DICE Measured Boot - Tao, Zhe; Rastogi, Aseem; Gupta, Naman; Vaswani, Kapil; Thakur, Aditya V. (30th Usenix Security Symposium, 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. DICE* is open source at: https://github.com/verified-HRoT/dice-star