Benjamin Farinier

Decision Procedures for Vulnerability Analysis

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 ]

Abstract

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:

These two differences have a profound impact on logical formulas generated by Symbolic Execution and their resolution:

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.