Detecting Spectre Vulnerabilities by Sound Static Analysis

Spectre attacks are critical transient execution attacks affecting a wide range of microprocessors and potentially all software executed on them, including embedded and safetycritical software systems. In order to help eliminating Spectre vulnerabilities at a reasonable human and performance cost, we propose to build on an efficient industrial code analyzer, such as Astrée, which enables an automatic analysis of big complex C codes with high precision. Its main purpose is to discover run time errors, but to do so, it computes precise over-approximations of all the states reachable by a program. We enriched these states with tainting information based on a novel tainting strategy to detect Spectre v1, v1.1 and SplitSpectre vulnerabilities. The selectivity and performance of the analysis is evaluated on the embedded real-time operating system PikeOS, and on industrial safety-critical embedded software projects from the avionics and automotive domain. Keywords–Spectre; taint analysis; abstract interpretation; static analysis; embedded software; operating systems; safety; cybersecurity.