Questions about s2e taint analysis

[Insu Yun]

Hi, all.

I have a question about s2e's taint analysis.

I saw that s2e uses memory helper for checking whether it is symbolic or not.

If symbolic, it calls switch_to_symbolic to run symbolic execution.

I have questions.

1. When it hits symbolic memory, will it go back to basic block start? or the instruction in LLVM IR?

2. If it go back to the basic block start, how can s2e recover the value changed in the basic block?

3. Could you let me know which code should I take a look?

Thanks. 

[Vitaly Chipounov]

Hi,

Le 30.11.2017 à 21:27, Insu Yun a écrit :
>
> 1. When it hits symbolic memory, will it go back to basic block start?
> or the instruction in LLVM IR?

No, it will abort the current instruction, exit the CPU loop, then
re-execute the current instruction in symbolic mode. This may involve
re-translating to LLVM instructions starting from the aborted instruction.

> 2. If it go back to the basic block start, how can s2e recover the
> value changed in the basic block?

It does not go to the start, because it's impossible to recover state in
general.

> 3. Could you let me know which code should I take a look?

It's here:
https://github.com/S2E/libs2ecore/blob/master/src/S2EExecutor.cpp#L1913

Vitaly

[Insu Yun]

Thanks a lot. I missed https://github.com/S2E/libs2ecore/blob/master/src/S2EExecutor.cpp#L2639.

2017년 11월 30일 목요일 오후 3시 34분 42초 UTC-5, Vitaly Chipounov 님의 말: