Let's Build a Symbolic Analyser And Automatically Find Bugs

Traditionally, bugs are usually discovered by running your program, and noting where it behaves incorrectly. However, there are other tools for discovering problems that don’t require you to run the code under test. These tools perform static analysis, which involves an analysis of the source code itself, and not an observation of its executed behaviour. The tools that you need to build this in Python are very easy to come by!

There are several methods of performing static analysis. One of them, symbolic execution, “runs” a piece of your code, and develops symbolic variables that represent the possible values and inputs that the code is working with. This means that the test doesn’t necessarily rely on any pre-existing state, or any knowledge of the kind of input that the program will run.

In this talk, we’ll discuss how you can build your own symbolic execution system in Python, using the Z3 solver to perform the heavy mathematical lifting. Along the way, you’ll learn the benefits and drawbacks of this approach, how you can use it in your own projects, and also some formal logic, too!