The security of a software system mainly relies on the security of its software components. To improve its overall security level it is therefore necessary to identify the potential vulnerabilities of these software components and to evaluate the relevance and the efficiency of the whole protection mechanisms.
This task can be assisted by automated code analysis technique, as illustrated by the significant number of existing tools already developed for this purpose. These tools essentially rely on techniques which have been used for a while in the safety or reliability contexts (like abstract interpretation, concolic execution, etc.), possibly with some specific extensions for security purposes. However, existing tools still suffer from several limitations regarding scalability. In addition, they now need to face new attacks models (like Spectre/Meltdown or Rowhammer [5]), leading to increasingly complex vulnerabilities and exploitation schemes. In addition, existing protection mechanisms should also been taken into account when evaluating and ranking some attack scenarios.
The objective of this PhD is to improve existing software vulnerability analysis in two main directions: 1 taking into account some concrete attacker model [4] when looking for exploitable vulnerabilities (i.e., what are his objectives and technical means ?) 2 analyzing and evaluating the possible countermeasures (or protection mechanisms) available inside the software itself, or at the whole execution platform level (with respect to some efficiency vs usefulness trade-off)
More concretely, this PhD could contribute to the following points :
1) countermeasure analysis
The purpose of a countermeasure is to restrict the attacker capabilities by making some vulnerabilities not exploitable (e.g., by early detecting memory errors, or by protecting some memory area using software or hardware mechanisms). A crucial issue is therefore to correctly appreciate the protection level provided by a (set of) countermeasure(s) with respect to some attacker model on a given software. Moreover, when performance criteria do matter (execution time, memory consumption, code size, etc.) it is required to limit as much as possible the impact of these countermeasures. An approach [2,3] has been proposed in the context of fault injection attacks, targeting some subset of possible countermeasures. It consist in specifying the effect of a countermeasure as a property over the code behavior and to validate this property using concolic execution. One objective of this PhD is to leverage this technique to a larger class of countermeasures and attacker models (including combinations of hardware and software countermeasures). This could be achieved thanks to source level annotations allowing to better identify and instrument the protection mechanisms and to guide the concolic execution engine.
2) Exploitability analysis with respect to an attacker model and a countermeasure scheme
The objective here is to evaluate the exploitation level of a given vulnerability, taking into account the attacker model and the available protections. A possible approach is to rely on a binary level symbolic execution extended in the following directions:
- quantitative analysis of the exploitability scenarios, for instance using model-counting facilities provided by some SMT solvers;
- specifying attackers and countermeasure behaviors by means of SMT assertion to be « injected » within the path predicates and concolic execution engine, for instance following some ideas proposed in [6]
Finally, attack combinations (based on multiple vulnerability exploitations) could be handled in a similar way.
3) Tool integration
These analysis proposals will be prototyped within a tool, for instance relying on the BinSeC [1] platform. Target applications will be chosen in the IoT domain (bootloaders, medical devices).
This PhD is funded by the ANR 20-CE25-0009 TAVA project, gathering the CEA LIST, Verimag laboratory and Amossys.
References
[1] BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-level Analysis Robin David , Sébastien Bardin, Thanh Ta, Josselin Feist, Laurent Mounier, Marie-Laure Potet, Jean-Yves Marion - SANER 2016
[2] Lazart: A Symbolic Approach for Evaluating the Robustness of Secured Codes against Control Flow Injections Marie-Laure Potet, Laurent Mounier, Maxime Puys, Louis Dureuil - ICST 2014
[3] Countermeasures Optimization in Multiple Fault-Injection Context. Etienne Boespflug, Cristian Ene, Laurent Mounier, Marie-Laure Potet - FDTC 2020
[4] RowHammer: A Retrospective Onur Mutlu, Jeremie Kim - IEEE TCAD 2020
[5] Weird Machines, Exploitability, and Provable Unexploitability Thomas Dullien - IEEE Transactions on Emerging Topics in Computing, 2019
[6] Compositional fuzzing aided by targeted symbolic execution S. Ognawala, F. Kilger, A. Pretschner (https://arxiv.org/pdf/1903.02981.pdf)
