search

eurecom-s3 / symqemu

SymQEMU: Compilation-based symbolic execution for binaries
http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html
Other
317 stars 40 forks source link

Using LD_LIBRARY_PATH #5

Open SweetVishnya opened 3 years ago

SweetVishnya commented 3 years ago

Hi!

I am running symqemu on binary requiring LD_LIBRARY_PATH. Will LD_LIBRARY_PATH=lib SYMCC_INPUT_FILE=file x86_64-linux-user/symqemu-x86_64 ./a.out file work?

I am trying with and without LD_LIBRARY_PATH. It works both ways without any error messages. I cannot tell if it is working correctly.

Also, is there a way to turn off optimistic solving?

SweetVishnya commented 3 years ago

What timeout do you use for solver?

sebastianpoeplau commented 3 years ago

Hi @SweetVishnya,

Not sure about the library search path, I haven't modified anything in that regard. So whatever QEMU's user-mode emulation does applies to SymQEMU as well. I believe it respects your lookup path, and maybe it even has a command-line option to specify a custom path just for the target.

The solver timeout is 10 seconds, inherited from QSYM. As for optimistic solving, there's no switch to disable it, but you can comment out the relevant lines of code in QSYM. (SymCC pulls the QSYM code in via a Git submodule and stores it in runtime/qsym_backend/qsym.)

Hope that helps!

SweetVishnya commented 3 years ago

Thank you for the answers, I will continue evaluating symqemu on Monday. One more question. Do u handle symbolic addresses? Do u generate multiple models for symbolic address as in qsym, they kind of try to solve switch branches that way.

P.S. Also, sent you an email.