How does S2E implement selective symbolic execution?

298 views

Skip to first unread message

cdboot

unread,

Mar 27, 2012, 7:38:39 AM3/27/12

to S2E Developer Forum

Hi,
We know from your paper that S2E can do selective symbolic execution.
That is to say it can analyze a program in symbolic mode and explore
its libraries concrete by getting a legal value for a symbolic
variable with a constraint solver. My question is how does S2E achieve
this? How does S2E know when calling the library functions? Does it
monitor the library functions and stub in them?

And also another question: can we add the function
"s2e_make_symbolic()" twice in a program?

Hope for your help, thanks!

Jonas Wagner

unread,

Mar 28, 2012, 4:10:33 AM3/28/12

to s2e...@googlegroups.com

Hello,

> We know from your paper that S2E can do selective symbolic execution.
> That is to say it can analyze a program in symbolic mode and explore
> its libraries concrete by getting a legal value for a symbolic
> variable with a constraint solver. My question is how does S2E achieve
> this? How does S2E know when calling the library functions? Does it
> monitor the library functions and stub in them?

There are two parts to your question:
1) How does S2E know whether some code belongs to the application under
test and when it belongs to a library?
This is operating system specific. On Linux, you can use the init_env
library to automatically select an application's code, see [1]. On
Windows, you can use the WindowsMonitor plugin together with the
ModuleExecutionDetector, see [2]

[1] https://s2e.epfl.ch/embedded/s2e/Howtos/init_env.html
[2]
https://s2e.epfl.ch/embedded/s2e/Windows/DriverTutorial.html#selecting-the-driver-to-execute

2) How to switch between symbolic and concrete execution?
If code is encountered that should not be tested (such as library code)
S2E turns off forking. This means that data is still processed
symbolically, but only one path will be followed at every branching
point. This is better than concretizing the entire execution state,
because when the execution re-enters your program under test, execution
can continue symbolically.

> And also another question: can we add the function
> "s2e_make_symbolic()" twice in a program?

Sure. You pass a pointer to the data that you want to make symbolic.
Thus, call the function once per variable or buffer that you wish to
make symbolic.