Share

Integration of active attacker models into security program analysis

#ANSSI #BINSEC #Cybersecurity
Crédit : Flatart / Freepik
CEA-List and Université Grenoble Alpes have developed the first-ever software security analysis technique capable of simulating a powerful attacker at scale. An implementation in CEA-List’s BINSEC analysis software was validated on a security component at ANSSI (France’s national information systems security agency).

Today’s software security analysis methods can simulate so-called “weak” attackers capable only of introducing bad data into software. A “powerful” attacker can affect more than just data with attacks like:

  • Fault injection attacks, originally developed to target high-security components like smart cards, exploit the physical phenomena inside a system to disrupt the environment in which a program is running.
  • Software-induced fault injection attacks (such as rowhammer attacks) and attacks exploiting processor microarchitectures expand the attack surface significantly.

Powerful attackers cannot be represented in the reachability analyses generally used to determine the existence of a path to an identified system vulnerability. The first challenge is to design an environment for effective automated reasoning about a powerful attacker’s impact on a program. The second challenge is to design an efficient algorithm to determine a program’s vulnerability to a given attacker model while avoiding combinatorial explosion, especially in the event of multiple attacks. Today’s techniques cannot be scaled up and do not provide a formalization of the underlying problem.

Figure 1 : Experimental Evaluation – Path explosion

 

Figure 2 : Fault injection attacks everywhere

 

Our original algorithm, Adversarial Symbolic Execution (ASE), can analyze a program’s execution paths in the presence of a powerful attacker by extending the symbolic execution used in standard code analysis and the conventional concept of reachability. Unlike state-of-the-art techniques, a new “forkless” vulnerability injection technique does not create additional paths to explore, preventing combinatorial explosion. The algorithm was implemented as a new module (BINSEC/ASE) of our BINSEC code analysis software.

Tests completed with BINSEC revealed major improvements in performance, both in terms of the number of paths explored and in terms of analysis time.