Moving code analysis from safety to security: attacker model

From bibtex.

Abstract

Major works have delved into program analysis over the last decades, leveraging techniques such as symbolic execution, static analysis, abstract interpretation or bounded model checking, to hunt for software vulnerabilities and bugs in programs, or to prove their absence, leading to industrial adoption in some leading companies. As bugs are an attack entry point, removing them is a first step towards better software security. Yet, they are based on the standard concept of reachability and represent an attacker able to craft smart, legitimate input, through legitimate input sources of the program, exploiting corner cases in the code itself, a rather weak threat model, typically a file formatted to trigger a buffer overflow in data processing. Tools only looking for bugs and software vulnerabilities may deem a program secure while the bar remains quite low for an advanced attacker, able for example to take advantage of attack vectors such as (physical) hardware fault injections, micro-architectural attacks, software-based hardware attacks like Rowhammer, or any combination of vectors.In this thesis, our goal is to devise a technique to automatically and efficiently reason about the impact of an advanced attacker onto a program security properties.We propose adversarial reachability, a formalism extending standard reachability to reason about a program execution in the presence of an advanced attacker. As equipping the attacker with new capacities significantly increases the state space of the program under analysis, we build a new algorithm based on symbolic techniques, named adversarial symbolic execution, to address the adversarial reachability problem from the bug-finding point of view (bounded verification). Our algorithm prevents path explosion thanks to a new forkless encoding of attacker capabilities, modeled as faults. We show it correct and k-complete with respect to adversarial reachability. To improve the performance further, we design two new optimizations to reduce the number of injected faults while keeping the same attacker power: Early Detection of faultSaturation and Injection On Demand.We propose an implementation of our techniques for binary-level analysis, on top of the BINSEC framework. We systematically evaluate its performances against prior work, using a standard fault injection benchmark from physical fault attacks and smart cards. Experiments show a very significant performance gain against prior approaches, for example up to x10 and x200 times on average for 1 and 2 faults respectively - with a similar reduction in the number of adversarial paths. At most, we are x200 times faster for 1 fault and x6000 for 2. Moreover, our approach scales up to 10 faults whereas the state-of-the-art starts to timeout for 3 faults. We also show the use of our method in a number of different security scenarios such as reproducing a BellCoRe attack with one reset fault on CRT-RSA or looking for attacks on a program protected by the SecSwift countermeasure. In addition, we perform a security analysis of the well-tested WooKey bootloader and demonstrate the ability of our analysis to find attacks and evaluate countermeasures in real-life security scenarios. We were especially able to find an attack not mentioned before on a recently proposed patch, and proposed a new patch to the developers.