DICE*: A Formally Verified Implementation of DICE Measured Boot

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.