Collecting constraints of real-world program

[tiedaoxiaotubie]

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: #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]

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.