Symbolic Engine | New Dynamic Symbolic Execution module

[ilebrero]

Details

Currently, there's a DSE algorithm built on top of the Genetic algorithm broadly used in the tool. Here we write an independent DSE module. See [Project.1] for work timelines and organization and [Project.2] for the thesis report with all the details (Only Spanish for now). For each change detail please check the PR link provided in each change.

Update: Merge against #311

Merge changes can be seen in this commit and the changes impact on the symbolic engine can be seen here plus this PR adaptation to the changes doc here and commit here.

Exploration Algorithm

• The exploration algorithm is based on SAGE's implementation [Exploration.1] from which the critical sections like path generation and next path selection strategies are abstracted. The default implementations of these are the SAGE's implementations, but they can be extended for new ones.
• Path divergence check is based on checking that the expected path is a prefix of the actual one [Exploration.3]
• Experiments are based on the benchmarks and general ideas from [Exploration.4]

Arrays support

• The first implementation is made in a similar fashion to java pathfinder [Arrays.1]. On the solver side we are using arrays theory.
• The second implementation sees the arrays as a bag of variables that are dynamically generated as needed, see the PR below for more info.

Experimentation

• See info in the PR below. Artifacts based on [Experiments.1].

Changes

Bugfixs

• DSE cache

Minor Changes

• Refactors of the current DSE algorithm.
• Small Refactor of concolic engine

DSE Module Rework + New Exploration Algorithm

• Medium refactor of the concolic engine and basic structure of the new DSE Algorithm.
• Added high level fitness functions and stopping conditions
• Added test strategies.
• Added path divergence check
• Important: Changed the DSE algorithm to be based on the SAGE general idea implementation. See references on PR.
• Added Scoring function for next path selection and fitness functions.
  • fix forgotten constructor.
  • Scoring penalty on path divergences
• Code cleanup
• Completed stopping conditions
• Switched the DSE algorithm to the new one + fixed bugs
• Tests and algorithm worklist fix
• Added statistics
• Counter-exampe constraint cache improve

Experiments

• New algorithm experiments

Arrays support

• Two Implementations of arrays.

References

Project

1. Work organization Trello board.
2. Thesis report Overleaf doc.

Exploration

1. Automated Whitebox Fuzz Testing
2. A Survey of Symbolic Execution Techniques
3. An empirical investigation into path divergences for concolic execution using CREST
4. Improving Search-based Test Suite Generation with Dynamic Symbolic Execution.

Arrays

1. Symbolic Arrays in Symbolic PathFinder

Experimentation

1. Improving search-based test suite generation with dynamic symbolic execution

[gofraser]

Looks fine, and seems to work, will merge -- thanks!