Fuzzing and Symbolic Execution

Who is the material made for?

This module targets software engineers interested in increasing confidence that existing software projects are free of bugs by means of automated software analysis.

The module assumes some programming background, though not necessarily systems programming (some basic C will be used in the course). A general computer science background is beneficial, though not required.

Introduction

Formal Software Verification are a host of methodologies and tools that can help in the design, development, and maintenance of correct and robust computer programs.

This approach relies on automatic procedures for verifying that software behaves as expected.

7

Software systems are notoriously difficult to get right, and most often contain bugs. Some bugs are obvious and elicited simply by using the software. Some other bugs are less so and require expert knowledge of the inner working of the software to elicit them, by exploring less common unintended code paths, but still account for most of the dangerous and costly bugs, like e.g., memory bugs.

The cost of finding these bugs is usually high due to the level of expertise required, but automated testing methodologies like fuzzing and symbolic execution can help lower these costs.

Fuzzing and symbolic execution are two techniques that are effective in eliciting bugs in software by automatically exploring possible code paths. Fuzzing does so by introducing random changes in the input and can be enhanced in multiple ways to increase code coverage.

Symbolic execution explores different code paths by constructing a symbolic representation of the conditions that lead to a specific code path, then use a constraint solver to find a concrete input that satisfies such constraints and can reach the given path, and repeats this procedure for all paths, in combination with a search strategy that the expert user defines, in order to achieve good code coverage.

After this course you will be able to use both techniques to discover security bugs in existing software. You will be able to assess which methodology and search strategy can improve coverage to elicit the greatest number of bugs.