Doctoral thesis in Mathematics and Computer Science, defended on June 24, 2020 in front of a committee consisting of:
[ manuscript.pdf | defense.pdf | tel.archives-ouvertes.fr ]
Symbolic Execution is a formal verification technique which consists in modeling program executions by logical formulas in order to prove that these executions verify a given property. Very effective, Symbolic Execution led to the development of analysis tools and to the discovery of many new bugs. The question is now how to use it in other contexts than bug finding, for example in vulnerability analysis. Applying Symbolic Execution to vulnerability analysis fundamentally differs from bug finding on at least two aspects:
First, finding a bug does not imply having found a vulnerability, and differentiating between the two requires to move from source-level analysis to binary-level analysis. But binary-level semantics are not only less structured than source-level semantics, they are also far more verbose.
Second, interactions with the environment are not modeled in the same way for vulnerability analysis than for bug finding. Indeed in vulnerability analysis, the environment model will depend on the attacker model we choose, as to conclude that a vulnerability is a real one, we need to prove the vulnerability manifests itself for all the configurations that components not controlled by the attacker can take.
These two differences have a profound impact on logical formulas generated by Symbolic Execution and their resolution:
Logical formulas generated during an analysis quickly become gigantic, and more and more difficult to solve. If this problem is not specific to vulnerability analysis, it is reinforced in this context, because of the verbosity of semantics used in binary-level analysis.
Modeling some security properties is likely to involve quantifiers whose use made generated logical formulas nearly impossible to solve. This is the case in vulnerability analysis about interactions with the environment, according to whether an attacker does or does not control a component.
Therefore this thesis focuses on two issues arising from the field of decision procedures, namely the simplification of logical formulas to limit their size explosion during the analysis, and the extension of solvers to quantified logic in order to allow finer models, required for vulnerability analysis.