Open vanhauser-thc opened 3 years ago
@vanhauser-thc this is most likely because our symbolic understanding of libc is incomplete. So when you call strncmp
, SymCC can't trace the computations that happen in the function. There are several ways to address the issue:
strncmp
and strcmp
to the collection of wrapped libc functions and register the wrapper in the compiler. This is quick and easy, but it doesn't scale if your target uses many libc functions on symbolic data.strncmp
is self-contained, so you can just add it to your build (e.g., symcc -o test test.c /path/to/musl/src/string/strncmp.c
).Suggestions how to make such situations easier to deal with are highly welcome :)
I think string compare functions make sense to add (so solution 1) as these are a limited number of common functions. 2 sounds like too much overhead and 3) should only be needed to be done for very specific cases (e.g. a third party library that is binary only),
KLEE's libc may also be a good starting point for 1 and/or 3: https://github.com/klee/klee/tree/master/runtime/klee-libc
Has anyone already tried 2)? If all it takes to get full support of libc functions is to compile uclibc with SymCC from scratch then I don't mind the extra work. Are there any additional steps required to set up the instrumented libc that I'm missing?
This example file:
the abort() can be triggered with:
echo -en 'ABCD1234EFGHIJKLDEADBEEF\0'|./test
when I compile the test.c with symcc, and feed the most advanced input it finds, it can not get past "ABCD1234EFGHAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", so it cannot solve the last strcmp with
DEADBEEF\0
- I guess this is a bug? or is this too complex to solve?