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
771 stars 137 forks source link

Add support to LAVA-M dataset #107

Open Yhcrown opened 1 year ago

Yhcrown commented 1 year ago

fix #102. I add more intercepted functions so that the lava-m programs can properly get input tainted. If the code is not quite standardized, I hope to get your test and modification. Thanks & Best regards.

Yhcrown commented 1 year ago

Some functions are difficult for me to write test cases for (like getutent). I’m still learing it. 😢

aurelf commented 1 year ago

Thanks for the changes! Would be great if the test is possible to add for that function too... Do you think you can add it ?

Yhcrown commented 1 year ago

Thanks for the changes! Would be great if the test is possible to add for that function too... Do you think you can add it ?

It may be a bit difficult for me now 😭 , I haven't figured out how symcc testing works yet. It would be great to have your help!.

sebastianpoeplau commented 1 year ago

I haven't figured out how symcc testing works yet.

We have some documentation here: https://github.com/eurecom-s3/symcc/blob/master/docs/Testing.txt. Let us know if you have questions!

zhou1615 commented 1 year ago

Sorry for trouble but this PR does not seem to work in the current version of SymCC. It seems that g_config.fullyConcrete has been removed from Config.cpp. I am not quite familiar with SymCC, thus I am not sure how to make it work.

Maybe a possible change is use maybeSetInputFile like this commit d5891b02e1f9a662e19aa2e516c30a1d43828a7e

sebastianpoeplau commented 1 year ago

Sorry for trouble but this PR does not seem to work in the current version of SymCC. It seems that g_config.fullyConcrete has been removed from Config.cpp. I am not quite familiar with SymCC, thus I am not sure how to make it work.

I can take it over, but I've got a question about the symbolic version of getutent. If I understand correctly, it treats the data returned from this libc function as symbolic input. Is this intended? In other words, do you expect SymCC to generate alternate contents of /var/run/utmp? Users can't write this file anyway, so wouldn't it make more sense to treat any data read from there as concrete?

I don't have a LAVA-M setup to check :frowning_face:

aurelf commented 7 months ago

I'm trying to look at this PR, @Yhcrown in case you can give me push access to your branch that would save me quite some time :) It's quite manual now... I seem to be only able modify your pr from the online editor.