Description
Hardware execution attacks exploit interactions in the processor microarchitecture. The goal of our research is to use formal verification tools to harden a processor implementation such that certain programs running on the processor are secure against transient execution attacks. In this paper, we formulate the task of hardening as a search problem for a minimal set of ordering constraints.