gistfile1.txt

We face a ’chicken-and-egg’ problem, where we need a detailed hardware model to reason
about HSE mechanisms, yet such a model does not exist and requires a tremendous amount of
efforts to be developed, reviewed and validated, which means we need to be reasonably certain
of our modeling choice for those efforts not going to waste. As a consequence, we decided to
develop an ad-hoc x86 hardware model which include the necessary hardware components
—abstracted away in related work— to demonstrate in Chapter 5 how it is possible to leverage
our formal definition of HSE mechanisms presented in Chapter 4 in order to specify and verify
a HSE mechanism implemented by the BIOS. In the process, we learned a lot with regard to
desirable properties a detailed hardware model could have.