QSYM is a concolic execution engine designed to enhance hybrid fuzzing by combining symbolic execution with fuzzing techniques. It targets security researchers and developers seeking to improve software vulnerability discovery in complex programs. The engine aims to overcome limitations of pure fuzzing or symbolic execution by leveraging their respective strengths.

How It Works

QSYM employs a hybrid approach, integrating with fuzzers like AFL. It uses Intel's PIN dynamic binary instrumentation framework to trace program execution and collect path constraints. These constraints are then solved by the Z3 SMT solver to generate new test cases, guiding the fuzzer towards unexplored code paths and complex conditions. This method aims to achieve higher code coverage and uncover deeper bugs than traditional fuzzing alone.

Quick Start & Requirements

• Installation: Via pip install . within a Python virtual environment after running setup.sh. Docker and Vagrant options are also provided.
• Prerequisites: Ubuntu 14.04/16.04 64-bit, Z3 SMT solver, PIN (version not specified but implied by yama/ptrace_scope and pin.log errors), AFL. Requires disabling ptrace_scope.
• Hybrid Fuzzing Setup: Requires setting environment variables AFL_ROOT, INPUT, OUTPUT, AFL_CMDLINE, and QSYM_CMDLINE.
• Testing: cd tests && python build.py && python -m pytest -n $(nproc)
• Documentation: No explicit link provided, but installation and usage instructions are in the README.

Highlighted Details

• Tailored for hybrid fuzzing environments.
• Leverages PIN for dynamic binary instrumentation and Z3 for constraint solving.
• Supports integration with AFL for enhanced fuzzing campaigns.
• Published at USENIX Security Symposium 2018.

Maintenance & Community

The project was authored by researchers from Georgia Tech and Oregon State University. The publication date is 2018, suggesting potential for outdated dependencies or lack of recent updates. No community links (Discord, Slack) or roadmap are provided.

Licensing & Compatibility

The README does not explicitly state a license. Given the academic origin and lack of explicit licensing, users should assume it is not licensed for commercial use or integration into closed-source projects without explicit permission.

Limitations & Caveats

QSYM's reliance on older versions of PIN and its specific Ubuntu version support (14.04/16.04) may indicate compatibility issues with modern systems. The 2018 publication date suggests the project might be unmaintained or have unaddressed compatibility issues with newer tools or operating systems. Troubleshooting notes mention potential issues with Z3 integration if not run within the correct virtual environment.