Home // CYBER 2019, The Fourth International Conference on Cyber-Technologies and Cyber-Systems // View article

Detecting Spectre Vulnerabilities by Sound Static Analysis

Authors:
Daniel Kästner
Laurent Mauborgne
Christian Ferdinand
Henrik Theiling

Keywords: Spectre; taint analysis; abstract interpretation; static analysis; embedded software; operating systems; safety; cybersecurity

Abstract:
Spectre attacks are critical transient execution attacks affecting a wide range of microprocessors and potentially all software executed on them, including embedded and safety-critical 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.

Pages: 29 to 36

Copyright: Copyright (c) IARIA, 2019

Publication date: September 22, 2019

Published in: conference

ISSN: 2519-8599

ISBN: 978-1-61208-743-6

Location: Porto, Portugal

Dates: from September 22, 2019 to September 26, 2019