The '80s never died: automata theory for reversing modern CPUs - Pepe Vila [RootedCON2020-EN]

The '80s never died: automata theory for reversing modern CPUs
Understanding the timing behavior of modern CPUs is crucial for optimizing code and for ensuring timing-related security and safety properties. Unfortunately, the timing behavior of modern processors depends on subtle and poorly documented details of their microarchitecture, which has triggered laborious efforts to reverse-engineer microarchitectural details. Cache replacement policies have received special attention, because they control the content stored in the memory hierarchy and hence heavily influence execution time.
In this talk we present an end-to-end solution for automatically learning cache replacement policies from real-time measurements on hardware. Our approach relies on two main contributions: (1) a tool, called CacheQuery, that provides an abstract interface to any individual cache set in the cache hierarchy, liberating the user from dealing with intrincate details such as address translation, index mapping, slicing, cache level interference, or measurement noise; and (2) an algorithm, called Polca, that provides an abstract interface to the cache replacement policy, and exploits several symmetries that make automata learning techniques applicable to the problem. Furthermore, we use program synthesis to automatically derive human-readable descriptions of the learned replacement policy.
In our experiments, we are successful in learning the cache replacement policies used in recent Intel processors, including 2 previously undocumented policies.
Pepe Vila