Angr中未约束状态与已找到状态地址相同的问题排查

问题场景 #

目标代码 #

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

int main(void)
{
    int x;   // 未初始化，符号执行中可视为符号变量
    if (x % 2 == 0)
        printf("Even");
    else
        printf("Odd");
    return 0;
}

编译与反汇编 #

64位机器上用gcc odd_even.c -o odd_even编译后，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}

控制流图显示：分支指令jne 0x40115d分出的两条路径，最终都会到达0x40116c。

Angr脚本与异常现象 #

使用Angr的simulation_manager.explore()尝试捕获所有到达0x40116c的状态，结果found和active stash各有一个指向0x40116c的状态：

>>> 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                            # 设置栈环境
>>> 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和found状态地址相同
>>> 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()后，active状态变为unconstrained，原因是返回地址未初始化导致ret指令执行时出现未约束状态。

原因分析 #

1. explore()的执行逻辑 #

Angr的simulation_manager.explore()默认行为是：一旦检测到某个状态满足find条件，就立即将该状态移至found stash，其他未满足条件的状态继续在active中执行。本场景中两个分支到达0x40116c的时间不同：

• 奇数分支（jne跳转路径）执行printf后直接落到0x40116c，先被检测到符合find条件，进入found；
• 偶数分支执行printf后通过jmp跳转至0x40116c，此时explore尚未完成遍历，该状态刚到达目标地址，还未来得及被移入found，因此留在active中。

若要将所有到达目标地址的状态都收集到found，可在explore()执行后手动将active中地址匹配的状态移至found，或使用simgr.move()方法筛选状态。

2. 符号变量的位宽不匹配 #

原代码中x是32位int，但脚本创建了64位符号变量x = s.solver.BVS("x",64)，并通过stack_push(x)压入8字节到栈中。而反汇编中mov eax, dword [rbp-0x4]读取的是栈上4字节数据，对应符号变量x的高32位（栈向下增长，压入的8字节中高地址区域是数据的低字节部分，rbp-0x4指向的是压入数据的高32位），这就是约束中出现x_40_64[39:32]的原因。正确做法是创建32位符号变量，通过s.mem[rbp-0x4].dword = x写入栈的对应位置，而非使用stack_push。

3. 未约束状态的产生 #

执行simgr.step()后状态变为unconstrained，是因为脚本从0x401142开始执行时，未正确初始化栈上的返回地址。当执行到retn指令时，需要从栈上读取返回地址，但该地址未被约束，导致Angr将其标记为unconstrained状态。

内容的提问来源于stack exchange，提问作者Rinkesh P