eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
773 stars 135 forks source link

Allow solve time granted to be in an env var #50

Open vanhauser-thc opened 3 years ago

vanhauser-thc commented 3 years ago

A critical success factor for symbolic solving is the time given to solve.

currently this is hardcoded in the qsym backend code that is called and is set to 5 secods.

at the start of fuzzing this is an OK setting, however for longer running fuzzing campaigns this becomes useless.

after a few hours and days the shallow paths have all been found and explored and deeper paths would require a longer solving time. at the same time, new paths are found much rarely that would give way more solving time.

Hence so that symcc is not pointless after a few hours of runtime, the solving time needs to be dynamically increased. the fuzzing helper script could do that based on the wait time it took for the next queue entry to be found by the synced afl-fuzz instance and setting that as the solve time, passing that to symcc in an environment variable.

@richinseattle @SweetVishnya

SweetVishnya commented 3 years ago

It sounds very reasonable. When SymQEMU tries to invert deep branches it mostly provides "optimistic" solutions.

sebastianpoeplau commented 3 years ago

Makes a lot of sense. I haven't changed that part of the code because it's in QSYM and I wanted to deviate from the upstream version as little as possible. Do you think we can get the change merged in QSYM? Otherwise I suppose we could put it in our fork.