Sydr, a dynamic symbolic execution tool
Sydr is an automatic test generation tool for complex programs that finds errors and increases code coverage during testing. Sydr constructs the program’s mathematical model that allows a fuzzer to explore new execution paths that are hard to follow via genetic mutation approaches. The tool advances further the dynamic symbolic execution approach used earlier in Avalanche and Anxiety analyzers developed in ISP RAS. In contrast with similar open source tools, Sydr ensures the correctness of generated input data by checking whether the newly found execution path has the target conditional branches inverted.
- Given an execution path, Sydr inverts all conditional branches that depend on input data. It also supports parallel branches inversion;
- ISP Fuzzer integration to reach the code behind the branches depending on comparisons with constants;
- Reverse engineering automation such as assisting an expert in reaching a given program point or collecting a trace of instructions that depend on input data;
- Support for various input data sources (files, network sockets, environment variables, standard input stream, command line arguments);
- Security predicates that are used to find errors and to generate input data to reproduce them (for division by zero, null pointer dereference, out of bounds access, integer overflow);
- Symbolic execution of multithreaded programs;
- Indirect jumps inversion (in switch statements);
- Formula slicing. Sydr eliminates redundant formulas (not influencing the conditional branch being inverted) from the path predicate. This feature solves the problem of undertainting and speeds up SMT solver work for generated queries.
Scheme of work
- Vishnyakov A., Fedotov A., Kuts D., Novikov A., Parygina D., Kobrin E., Logunova V., Belecky P., Kurmangaleev Sh. Sydr: Cutting Edge Dynamic Symbolic Execution. 2020 Ivannikov ISPRAS Open Conference (ISPRAS), IEEE, 2020. Download presentation