eurecom-s3
SymQEMU does not explore all possible paths.
Using an example from another project (Triton)
serj@debtest:~/GITHUB/symqemu/build$ echo AAAAAAAAAAAAAAAAAAAAAA | ./qemu-x86_64 /home/serj/GITHUB/Triton/src/examples/python/ctf-writeups/cm002/cm002
This is SymCC running with the QSYM backend
Enter password:
[STAT] SMT: { "solving_time": 0, "total_time": 43966 }
[STAT] SMT: { "solving_time": 3871 }
[STAT] SMT: { "solving_time": 3871, "total_time": 48288 }
[STAT] SMT: { "solving_time": 4680 }
[STAT] SMT: { "solving_time": 4680, "total_time": 49952 }
[STAT] SMT: { "solving_time": 16049 }
[STAT] SMT: { "solving_time": 16049, "total_time": 61933 }
[STAT] SMT: { "solving_time": 16623 }
[STAT] SMT: { "solving_time": 16623, "total_time": 63323 }
[STAT] SMT: { "solving_time": 17397 }
[INFO] New testcase: /tmp/output/000000
[STAT] SMT: { "solving_time": 17397, "total_time": 67232 }
[STAT] SMT: { "solving_time": 18046 }
[INFO] New testcase: /tmp/output/000001
Wrong password!
Inspecting the output files I see that it does not generate the solution to the challenge. SymQEMU does not actually explore all possible states. In contrast tritondse script for the same binary produces this output
(venv) serj@debtest:~/GITHUB/tritondse$ python3 ./bla.py
symbol __gmon_start__ imported but unsupported
calling __gmon_start__ which is unsupported
Enter password:
Wrong password!
symbol __gmon_start__ imported but unsupported
calling __gmon_start__ which is unsupported
Enter password:
calling __gmon_start__ which is unsupported
Enter password:
calling __gmon_start__ which is unsupported
Enter password:
calling __gmon_start__ which is unsupported
Enter password:
calling __gmon_start__ which is unsupported
Enter password:
calling __gmon_start__ which is unsupported
Enter password:
calling __gmon_start__ which is unsupported
Enter password:
calling __gmon_start__ which is unsupported
Enter password:
You found the password: "����M"��� ����"
8
The � characters are symbolic non concreted values.
https://github.com/quarkslab/tritondse The binary https://github.com/JonathanSalwan/Triton/tree/master/src/examples/python/ctf-writeups/cm002
So running SymQEMU a few times in a row using the last generated output will eventually get to the correct password.
Indeed, this is because SymQEMU is a concolic executor more than a symbolic executor. Just like SymCC, see : https://github.com/eurecom-s3/symcc/issues/14 It would be possible it make it a symbolic executor (i.e. forking states like s2e or klee), but this would be much easier on the system mode, and would require significant work. Definitely a nice to have feature and something we have in mind at some point, but no timeline :)
