A Secure Bootloader for Demonstrating Formal Verification of Hardware-Firmware Interactions on SoCs

Abstract

The of completeness formal verification that provides either a proof of correctness to determine that a checked property holds, or a counterexample that is in violation, is a valu- able asset to security verification, which requires comprehensive testing of all corner cases. While there has been increasing use of model checking as a means of verifying hardware and software separately, unified hardware and software analysis tools are less developed. As integrated circuits become more complex, the prevalence of system-on-chip (SoC) designs with a programmable core that runs rmware to control and interact with hardware accel- erators and other peripheral devices presents a growing need for reliable hardware- rmware coverification. In pursuit of the goal of developing a tool for model checking across the hardware- rmware boundary that is scalable and efficient, we build a realistic testing infras- tructure that can demonstrate the effectiveness of the models that are in development. This task involves adding hardware accelerators to a 8051 microcontroller to create a substantial hardware- rmware interface, developing a secure bootloader that makes use of interactions between hardware and rmware, and identifying system properties of the secure bootloader that cross the hardware- rmware divide and verifying them with formal methods. A subset of these secure boot properties cannot be expressed with temporal logics, so we explore two proposed languages that address this challenge. To perform verification, we abstract the hardware into software, substituting uninterpreted functions in place of complex operations whose details do not affect the properties being checked.