Kawa: An Abstract Language for Scalable and Variable Detection of Spectre Vulnerabilities

Since the discovery of Spectre attacks, various detection methods for speculative vulnerabilities have been developed. Sound static analyses based on symbolic execution give precise results but lack scalability, while pattern-based analyses can accommodate large code bases but may be unsound and require manually crafted patterns for each microarchitecture. We introduce Kawa, an abstract language designed to model control and data flows, allowing efficient analysis of Spectre vulnerabilities. Kawa's abstract nature also enables interpretation as schemata to capture entire classes of concrete programs with speculative leaks.