Groups keyboard shortcuts have been updated
Dismiss
See shortcuts

Re: [s2e-dev] Issue about state switching

31 views
Skip to first unread message

Vitaly Chipounov

unread,
Oct 26, 2023, 9:23:01 AM10/26/23
to s2e...@googlegroups.com
Hi,

Use the S2EExecutionState::Yield() api if you want to switch states from the execution loop.

Vitaly


On Thu, Oct 26, 2023 at 10:58 AM Wenkang <hwk...@gmail.com> wrote:
Hi Vitaly, I'd like to develop a searcher plugin that enables switching the state when the S2E is running at a specific pointer counter(PC) or basic block.

I found that the default S2E searcher supports state switch at a certain timer as shown in function stateSwitchTimerCallback
snippet 1
```cpp
void S2EExecutor::stateSwitchTimerCallback(void *opaque) { S2EExecutor *c = (S2EExecutor *) opaque; assert(env->current_tb == nullptr); if (g_s2e_state) { c->doLoadBalancing(); S2EExecutionState *nextState = c->selectNextState(g_s2e_state); if (nextState) { g_s2e_state = nextState; } else { // Do not reschedule the timer anymore return; } } libcpu_mod_timer(c->m_stateSwitchTimer, libcpu_get_clock_ms(host_clock) + 100); }
```
Thus, I wrote a simliar function in my plugin so as to swith the state at specific point as shown in the following snippet. Note that I implemented the function setCpuExitRequest which leverages the kvm vCPU request to force suspending current state execution.
snippet 2
```cpp
// --- myPlugin --- void ValidPathSearcher::triggerSelfSwitch() { env->current_tb = nullptr; // validPathSearcherStateSwitchCallback and stateSwitchTimerCallback are almost the same. s2e()->getExecutor()->validPathSearcherStateSwitchCallback(s2e()->getExecutor()); // exit current state so that s2e continues with the selected state. s2e()->getExecutor()->setCpuExitRequest(); } // --- declared in s2e\libs2ecore\include\s2e\S2EExecutor.h --- void setCpuExitRequest(void); // --- definede in s2e\libs2ecore\src\S2EExecutor.cpp --- void S2EExecutor::setCpuExitRequest() { s2e_kvm_cpu_exit_request(); } // --- declared in s2e\libs2ecore\include\s2e\cpu.h --- void s2e_kvm_cpu_exit_request(void); // --- definede in s2e\libs2e\src\s2e-kvm-vcpu.cpp --- void s2e_kvm_cpu_exit_request(void) { s2e::kvm::s_vcpu->requestExit(); }
```
However, when I test my plugin with demo program the execution will be stuck after state swith.
For example as shown in the following demo .
snippet 3
```cpp
void demo(short a, short b, short c) { if ((a & 0xC == 4) || (a & 0xC == 8) && ((b & 0x40000) != 0)) { ... } else { a = 0x50001; } func(); ... }
```
I assign a, b and c as symbols and perform concolic execution. I try to switch the state after return of func().
My logs indicate the following:
  • When the program reaches a & 0xC == 4, S2E triggers a fork event, creating state 0 and state 1
    • state 0 -> a & 0xC == 4 is false
    • state 1 -> a & 0xC == 4 is true
  • Then, the program reaches a & 0xC == 8, S2E triggers a fork event again, creating state 0 and state 2
    • state 0 -> a & 0xC == 8 is false
    • state 2 -> a & 0xC == 8 is true
  • Based on my plugin, after func, S2E switches to state 2.
  • The issue arises when the program reaches b & 0x40000) != 0, S2E aborts at Executor::fork. I find g_s2e_state' id is different from param current_state 's id. current_state is a param of Executor::fork.

I feel like switching back in order to explore more information from the other path, so that I can select the better one through comparsion.
In summary, what I'd like to seek advice is as follows:
  • What could be the possible reasons?
  • Have you ever written such a feature before? If not, What advice do you have for implementing this feature and ensuring correct path switching?

--
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/84e41767-e8ee-4ab5-a89c-bd6bc7dd9291n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages