PhD Defense: Yaëlle Vinçont

Dec 14 14:00 ₂₀₂₁

Abstract: The automatic generation of tests is a major issue in software engineering and security. Test suites created this way can efficiently explore the code, and find potential bugs, and therefore vulnerabilities.

In this thesis, we were interested in two of the said techniques: symbolic execution and fuzz testing. Symbolic execution uses methodical exploration of the execution paths, and for each one generates a constraint on the program input. A solution to this predicate, which follows the same execution path, is then created using an SMT solver. At the same time, fuzz testing quickly generates test cases, with varying knowledge about the program, following the idea that executing the program on many test cases will lead to exhaustive exploration. Whereas symbolic execution can, in theory, explore all paths, but is limited by the high number of paths in a program, fuzzing is quick to explore but can be blocked by a path condition it failed to solve.

In this thesis, we combine those two techniques, in order to use symbolic execution's reasoning power to solve such conditions, and fuzzing's efficient test case generation to explore the program as a whole. To achieve this, we combined two ideas:

• Lighweight Symbolic Execution (LSE) is a variant of symbolic execution where the analysis targets a condition on a path, rather than a full path, and the target constraint language is restricted to an easily-enumerable fragment of the usual one. As a consequence, deriving (correct) path predicates in this language is more complicated, but test cases following a given path are then easy to enumerate, without using any off-the-shelf constraint solver.
• Constrained Fuzzing operates over a test case and an easily-enumerable constraint in order to quickly generate test cases which follow the intended path, up to the targeted condition.

Overall, LSE will lead the exploration past difficult conditions and towards interesting parts of the code, while the constrained fuzzer will efficiently create test cases, including solutions to the constraints. This allows us to explore the program without systematically relying on symbolic analysis, and removes the need for an SMT solver to create test cases satisfying the constraints. We evaluated the performances of the resulting tool, called ConFuzz, on a standard fuzzing benchmark, and found that we improved upon the performance of standard fuzzing and symbolic execution tools.

Jury:

• Jean-Yves MARION, Ecole Nationale Supérieure des Mines de Nancy, Reviewer
• Michail PAPADAKIS, Université de Luxembourg, Reviewer
• Emmanuelle ENCRENAZ, Sorbonne Université, jury member
• Mihaela SIGHIREANU, ENS Paris-Saclay, jury member
• Sylvain CONCHON, Université Paris-Saclay, PhD Supervisor
• Sébastien BARDIN, CEA Saclay, co-supervisor