Quantifying Programs' Robustness Against Multi-Fault Control-Flow Attacks by Static Analysis

From bibtex.

Abstract

Multi-fault attacks consist of multiple hardware disruptions targeting a single execution of a program; they can bypass security countermeasures by altering both program logic and its protections. Due to repetition and internal program complexity, the search space for these attacks is immense and few tools can analyze them either at scale or with completeness guarantees. Gicquel et al.'s SAMVA analyzer can construct control-flow attacks with large numbers of faults, but relies on heuristics and suffers from unpredictable performance. This paper replaces SAMVA's path search and fault positioning algorithms to fix its variable performance and give it completeness guarantees. Our reworked SAMVA finds all control-flow attacks (within a well-defined class) that achieve a user-provided attack plan, and enumerates them by increasing fault count. Finding optimal attacks directly quantifies the target program's robustness against the fault model for the chosen attack plan, to our knowledge, the first analysis of its kind at this scale. We demonstrate these capabilities by mapping out the robustness of eight PIN verification programs against a bypass of the PIN check with variable-width instruction skips, assessing the efficacy of each countermeasure. SAMVA analyzes all attacks of less than 10 faults and finds tens of thousands of optimal fault sequences within minutes.