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

symcc_fuzzing_helper SYMCC_AFL_COVERAGE_MAP doesnt work #49

Open vanhauser-thc opened 3 years ago

vanhauser-thc commented 3 years ago

so that the coverage map generated by afl-showmap and used by symcc is correct the exact same instrumentation has to be in the afl-fuzz binary as in the symcc instrumented binary. in cases where the afl-fuzz + symcc binary is not qemu based (with symqemu) this is hardly ever the case.

all vanilla AFL instrumentations - afl-gcc, afl-llvm-pass and sancov - assign random basic block ids, so the map could never ever match. with afl++ it is possible to match - if non-colliding coverage instrumentation types would be used, and the same clang version and the same compiler optimization options. so basically this would not be the case either. plus I do not know if the symcc instrumentation has an influence over the control path? If so and the coverage map instrumentation is afterwards then this is impossible to ever work.

only with qemu_mode the coverage map will be guaranteed to match. if the map does not match then wrong decisions are made to decide if a new path was found or not.

So what is the solution? I would propose not generating and using the map unless qemu_mode is used.

julihoh commented 3 years ago

I had exactly the same thought, but I think the idea might be to set this configuration to a separate file, to at least let qsym track its own coverage (without necessarily coordinating with afl's map).

sebastianpoeplau commented 3 years ago

I'm not sure I understand. We use afl-showmap exclusively to decide whether to pass a test case to the fuzzer, and we run it with the same binary that the fuzzer uses. So from AFL's point of view it should be correct that a test case for which afl-showmap lists edges that it hasn't listed for previous test cases is interesting.

Then there is the separate concept of SYMCC_AFL_COVERAGE_MAP, which is the QSYM backend's internal mechanism to make branch decisions based on previous explorations. It is modeled after the AFL maps but completely independent from afl-showmap and based only on executions of the SymCC-instrumented binary.