SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns

Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia

Microarchitectural security verification of software has seen the emergence of two broad classes of approaches. The first is based on semantic security properties (e.g., non-interf…