A symbolic fuzzer that can generate input values symbolically with the following assumptions:
- No recursion
- All variables are annotated with the type information
- The only container used in programs are list of integers with a maximum size of 10
The key idea is as follows: We traverse through the control flow graph from the entry point, and generate all possible paths to a given depth. Then we collect constraints that we encountered along the path, and generate inputs that will traverse the program up to that point.
This tool can:
- Generate and print the path constraints in the program.
- trace each constraint to the part of code that created the constraint.
- Generate the corresponding unsat core and the statements related to an unsatisfiable path.
We used the symbolic fuzzer that is available at The fuzzing book as the basis of our tool.
git clone https://github.com/realsarm/my-symbolic-fuzzer.gitcd .\my-symbolic-fuzzerpython -m venv myvenv.\myvenv\Scripts\activate.batpip install -r requirements.txt
To render the generated DOT source code, you also need to install Graphviz(installation procedure for Windows)
- create your
example.pyfile in examples directory (all files of example directory will be imported tomain.pydynamically using importdir) or use one of the examples that already exist. python main.py- The tool will ask for max_depth(e.g 10), max_tries(e.g 10), max_iter(e.g 10), example_program(e.g a_check_triangle_book_example), and function_from_example_program(e.g a_check_triangle_book_example)
- check the result
- Function call to self-contained void methods.