search

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

Collecting constraints of real-world program #62

Closed tiedaoxiaotubie closed 3 years ago

tiedaoxiaotubie commented 3 years ago

Hi, I wonder if it is doable to use SymCC to collect real-world program's path constraints? Supposing we have a CVE and the corresponding poc, we want to collect the constraints along the execution trace.

I know the libc interaction will be a serious problem, and I have also noticed this: https://github.com/eurecom-s3/symcc/issues/23, so what if I add all the necessary libc wrappers, may I manage to collect the complete constraints then?

For adding libc wrappers approach, the developed of SymCC has said like this:

 it doesn't scale if your target uses many libc functions on symbolic data

What the meaning of scale? Just time-consuming? If it can collect the constraints successfully, time-cost won't be a serious problem. (For example, the automatic exploit generation guys don't care about the speed much)

aurelf commented 3 years ago

Hi,

That looks like perfectly possible to extract constraints along the execution of the program (I imagine SYMCC_LOG_FILE should log that), and yes the libc will need to be instrumented if you want to propagate the symbolic execution to that layer.

I assume that the problem with scaling mentioned in #23 is mainly because of manual work to add wrappers. The best option would be to have a separate libc for the analyzed program and for the instrumentation.