Angr 无约束状态与找到的状态具有相同的地址

Question

我正在研究一个简单的符号执行问题。代码如下

// odd_even.c
#include <stdio.h>

int main(void)
{
    int x;   //yes x is uninitialized here, but that won't matter during symbolic execution would it?
    if (x % 2 == 0)
        printf("Even");
    else
        printf("Odd");
    return 0;
}

在64位机器上用

gcc odd_even.c -o odd_even

编译并使用二进制ninja后，这里是

main

的cfg

拆解

main()

00401136  int32_t main(int32_t argc, char** argv, char** envp)

00401136  f30f1efa           endbr64 
0040113a  55                 push    rbp {__saved_rbp}
0040113b  4889e5             mov     rbp, rsp {__saved_rbp}
0040113e  4883ec10           sub     rsp, 0x10
00401142  8b45fc             mov     eax, dword [rbp-0x4 {var_c}]
00401145  83e001             and     eax, 0x1
00401148  85c0               test    eax, eax
0040114a  7511               jne     0x40115d

0040114c  bf04204000         mov     edi, 0x402004  {"Even"}
00401151  b800000000         mov     eax, 0x0
00401156  e8e5feffff         call    printf
0040115b  eb0f               jmp     0x40116c

0040115d  bf09204000         mov     edi, 0x402009
00401162  b800000000         mov     eax, 0x0
00401167  e8d4feffff         call    printf

0040116c  b800000000         mov     eax, 0x0
00401171  c9                 leave    {__saved_rbp}
00401172  c3                 retn     {__return_addr}

我的目标是到达地址

0x0040116c

。我可以在 angr 的

explore()

上使用

simulation_manager

方法，并且它确实有效，除了它以 2 个存储结束，

found

和

active

最终变成

unconstrained

，两者的地址都是

0x0040116c

.

这是我的 angr 脚本，在 python 解释器中

>>> import angr
>>> p = angr.Project('odd_even')
>>> s = p.factory.blank_state(addr = 0x401142, add_options={angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY
,angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS})
>>> x = s.solver.BVS("x",64)
>>> s.regs.rbp = s.regs.rsp                            //setting up the stack
>>> s.stack_push(x)
>>> simgr = p.factory.simulation_manager(s,save_unconstrained = True)
>>> simgr.explore(find= 0x40116c)
<SimulationManager with 1 active, 1 found>
>>> simgr.active
[<SimState @ 0x40116c>]                                //active and found states have same address
>>> simgr.found
[<SimState @ 0x40116c>]
>>> simgr.found[0].solver.constraints
[<Bool (x_40_64[39:32] & 1) != 0>]
>>> simgr.active[0].solver.constraints
[<Bool (x_40_64[39:32] & 1) == 0>]
>>> simgr.step()
WARNING  | 2024-11-12 16:57:01,371 | angr.engines.successors | Exit state has over 256 possible solutions
. Likely unconstrained; skipping. <BV64 mem_7ffffffffff0008_42_64{UNINITIALIZED}>
<SimulationManager with 1 unconstrained, 1 found>
>>> simgr.unconstrained[0]
<SimState @ <BV64 mem_7ffffffffff0008_42_64{UNINITIALIZED}>>
>>> simgr.unconstrained[0].solver.constraints
[<Bool x_40_64[32:32] == 0>]
>>> simgr.unconstrained[0].solver.eval(x)
0x0
>>> simgr.found[0].solver.eval(x)
0x100000000

我预计 found 存储中有

2 个状态

，这两个状态分别代表奇数和偶数分支。这种行为的原因可能是什么？

Answer 1

来自

angr.sim_manager.SimulationManager.explore

的源代码

向前勾选 stash“stash”（最多“n”次或直到找到“num_find”状态），寻找条件“find”， 避免条件“避免”。将找到的状态存储到“find_stash”中，并将避免的状态存储到“avoid_stash”中。

如前所述，使用

simgr.explore(find= 0x40116c, num_find = 2)

会在

found

存储中产生 2 个状态，每个状态代表各自的约束。

或者，多次调用

simgr.explore(find= 0x40116c)

最终也会达到相同的结果。