A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity

In recent years, the disclosure of several significant security vulnerabilities has revealed the trust put in some presumed security properties of commonplace hardware to be misplaced. We propose to design hardware systems with security mechanisms, together with a formal statement of the security properties obtained, and a machine-checked proof that the hardware security mechanisms indeed implement the sought-for security property. Formally proving security properties about hardware systems might seem prohibitively complex and expensive. In this paper, we tackle this concern by designing a realistic and accessible methodology on top of the Kôlka Hardware Description Language for specifying and proving security properties during hardware development. Our methodology is centered around a verified compiler from high-level and inefficient to work with Kôlka models to an equivalent lower-level representation, where side effects are made explicit and reasoning is convenient. We apply this methodology to a concrete example: the formal specification and implementation of a shadow stack mechanism on an RV32I processor. We prove that this security mechanism is correct, i.e., any illegal modification of a return address does indeed result in the termination of the whole system. Furthermore, we show that this modification of the processor does not impact its behaviour in other, unexpected ways.