Towards Tractable Hardware Model Validation Against Real Hardware
TL;DR
This work presents a methodology that lets us validate an abstract formal model against real hardware by generating test cases, executing them on real hardware to capture traces of observable behavior, and employing a synthesis approach to identify the internal microarchitectural steps that explain the observable behavior.
Abstract
Verifying low-level system code requires reasoning about how software interacts with the hardware environment on which it runs. Typically, this means specifying an abstract model of the hardware and verifying the code against it. However, the validity of the verification result depends on the accuracy of the formalized hardware model. Unfortunately, validating the accuracy of the formalized hardware model is hard. It not only requires relating the model's specification to the observable behavior of real hardware, but also involves many invisible internal microarchitectural steps that influence the observable execution of a modern processor. We present a methodology that lets us validate an abstract formal model against real hardware by generating test cases, executing them on real hardware to capture traces of observable behavior, and finally employing a synthesis approach to identify the internal microarchitectural steps that explain the observable behavior. We discuss this methodology for an x86 MMU model of TLB and page-table behavior, using model-specific state reductions to keep test generation and synthesis tractable and to illustrate how similar reduction arguments can apply in other hardware-model contexts.
