符号执行与angr

前言

距离第一次接触并使用符号执行CTF——angr使用学习记录_ctf angr-CSDN博客已经三年了，现在再回过头来重温一下

符号执行简述

介绍

符号执行起初应用于基于源代码的安全检测中，它通过符号表达式来模拟程序的执行，将程序的输出表示成包含这些符号的逻辑或数学表达式，从而进行语义分析。符号执行使用符号值作为输入值，根据程序语义利用符号集对程序变量，表达式和语句进行符号翻译，沿着程序路径执行，通过收集条件送往求解器进行求解，最后的输出值可表示为输入值的符号函数。在遇到状态分支时，相应的分叉探索每支路径状态，收集每支路径上的约束条件，通过约束求解器验证约束条件的可满足性问题。若路径约束可满足，则说明路径可达，并生成测试用例，程序执行到该路径；若约束是不可满足的，则该路径不可达，终止分析。

符号变量: 用符号代替实际值，例如将输入变量 x 设为符号变量。

路径条件（PC）: 执行路径上所有分支条件的逻辑与组合，用于约束符号变量的取值。

约束求解器（Constraint Solver）: 用来求解路径条件，验证路径是否可行，并生成测试输入。如z3

静态符号执行与动态符号执行的对比

挑战

主要还面临着以下挑战：探索路径太多——路径爆炸问题，路径条件太难解决——约束求解问题。

程序执行中路径与分支条件的数量呈指数关系，增加分支的数量导致搜索空间会增大，进一步限制了符号执行的性能。因此，采取合适的搜索策略来提高符号执行的覆盖率，以及减少时间开销尤为重要。

约束求解决定着符号执行的效率。约束求解是一种基于数学理论的分析方法，其问题可描述为一个三元组P=<V,D,C>形式，V表示变量集合V={v1,v2,⋯,vn}；D表示中元素的值域集合，即变量的取值范围；C表示约束条件。约束求解问题就是变量在值域范围内取值使得约束条件C可满足的，否则，这约束问题是不可满足的。

angr

一个强大的二进制分析工具。angr 的原理是通过将二进制程序转换为中间表示后，结合符号执行、路径分析和求解器技术，来模拟程序运行。综合了静态分析的结构化视角和动态分析的实时行为追踪能力，能够高效地应对多种复杂的二进制分析任务。官方文档：angr documentation

从angr_ctf练习api的使用

老模板

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

import angr
import claripy 
#载入文件，auto_load_libs设置为false，大概是启用angr自带的函数定义，避免一些逻辑过于复杂，机器跑不出来。
p = angr.Project('./test',load_options={"auto_load_libs":False})
#我们使用claripy这个模块来定义抽象的数据，claripy的BVS函数可以创建一个指定长度的抽象数据
#BVS函数要求两个参数，第一个参数为变量名，第二个参数为变量长度。符号化变量；
arg = claripy.BVS(‘arg1′, 8)
#entry_state()函数接收一个list作为程序的命令行参数并且返回程序入口的状态
state = p.factory.entry_state(args=argv)
# 表示从标准输入读取一个字节 
state.posix.files[0].read_from(1)
#创建一个 blank_state 对象，这个对象里面很多东西都是未初始化的，当程序访问未初始化的数据时，会返回一个不受约束的符号量
st = p.factory.blank_state(addr=)
#表示从state这个地址开始执行。
sm = p.factory.simulation_manager(state)
#当探索到find地方，就是想要的答案，avoid就是需要避免的地方。
sm.explore(find=0x400676,avoid=[0x40073d])
#最后的输出
sm.found.posix.dumps(1) 
#found的输入
sm.found.posix.dumps(0) 
#使用约束求解引擎获取命令行参数，类型为字符串，
sm.found.solver.eval(arg1,cast_to = str）

在使用符号变量后，不能通过posix.dump来获取标准输入，而应该获取符号变量的值，simgr.one_found.solver.eval函数可以获取符号变量的值

angr.Project

SimState

angr.SimState 类是 angr 框架的核心组件之一，表示符号执行过程中的程序状态。它包含寄存器、内存、约束、文件 I/O 等信息，能够模拟程序的执行流程，追踪路径上的符号化变量以及相应的约束条件。

示例：栈的符号化：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

import angr
import claripy
import sys
def main(argv):
    p = angr.Project('')
    def good(state):
        return b'Good Job.' in state.posix.dumps(1)
    def bad(state):
        return b'Try again.' in state.posix.dumps(1)
    #创建开始状态
    start_addr = 0x08048697  #scanf之后的地址，之所以是这儿，是因为上一行'add  esp,10h'的作用是清理scanf的栈空间
    state = p.factory.blank_state(addr=start_addr)
 
    #因为跳过了scanf函数，所以我们需要模拟它的整个操作(对栈的操作)
    #state.stack_push(state.regs.ebp)
    state.regs.ebp = state.regs.esp    #初始化ebp、esp
    space = 0x8                         #一个变量占4个空间，所以两个就是8
    state.regs.esp -= space   #模拟scanf时栈的情况(剔除了对空间的浪费，即只开辟了两个变量的空间)
    ps1 = claripy.BVS('ps1',32)       #符号化两个输入
    ps2 = claripy.BVS('ps2',32)
    state.stack_push(ps1)     #将符号化的输入入栈
    state.stack_push(ps2)
    #至此对scanf的模拟过程就完成了
    
    #创建模拟管理器
    simulation = p.factory.simgr(state)
    
    #开始探索
    simulation.explore(find=good,avoid=bad)
    if simulation.found:
        solution_state = simulation.found[0]
        flag1 = solution_state.solver.eval(ps1)
        flag2 = solution_state.solver.eval(ps2)
        print('{} {}'.format(flag1,flag2))
  
 
if __name__ == '__main__':
    main(sys.argv)

SimulationManager

angr.SimulationManager 是 angr 框架中用于管理和操作多个程序执行路径（SimulationState 对象）的核心组件。它提供了一种高层抽象，用于对符号化执行进行路径分类、过滤、探索以及管理，是分析和控制程序路径执行的强大工具。

两种写法等效

1
2

proj.factory.simgr(state)
proj.factory.simulation_manager(state)

angr.SimulationManager 类中使用率较高的重要 API 函数及其功能的详细表格：

Claripy

Claripy 是 angr 中用于符号化计算和约束求解的关键库，它为符号执行提供了强大的表达式表示、符号求解、符号计算、以及符号约束管理功能。Claripy 处理和操作符号化数据（如变量和内存地址）并提供求解器接口，用于符号计算、约束求解和路径分析。对于我们而言一般不需要直接与其进行交互，但通常我们会使用其提供的一些接口

bitvector - 位向量

位向量（bitvector）是 angr 求解引擎中的一个重要部分，其表示了 一组位 （a sequence of bits）。

以下是优化和扩展后的 Claripy 常用函数和属性表格，增加了详细的描述、常见的使用场景以及新内容：

Claripy ，涵盖了符号表达式的符号计算、符号约束和求解等关键操作。

hook

在 angr 中，hook 允许用户为程序的特定地址或函数提供自定义的处理逻辑。通过 hook，用户可以拦截程序的控制流，并用自定义的代码替代原有的函数或指令。

常用 hook 函数表格

示例：

1
2
3

p.hook(addr=0x08048485, hook=hook_demo, length=2)

p.hook_symbol('想要被hook的函数名', 自己定义的替换函数名，replace=True）

addr 为待 hook 指令的地址

hook 为 hook 的处理函数，在执行到 addr 时，会执行 这个函数，同时把 当前的 state 对象作为参数传递过去

length 为 待 hook 指令的长度，在 执行完 hook 函数以后，angr 需要根据 length 来跳过这条指令，执行下一条指令

优化：

simgr.one_active.options.add(angr.options.LAZY_SOLVES)

对simgr开启LAZY_SOLVES选项，该选项可不在运行时实时检查当前条件能否到达目标位置。虽然这样无法规避一些无解的情况，但可以显著提高效率

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

#!/usr/bin/env python
# coding=utf-8
import angr
import claripy
def hook_demo(state):
    state.regs.eax = 0
    state.regs.ebx = 0xdeadbeef
p = angr.Project("./examples/sym-write/issue", load_options={"auto_load_libs": False})
p.hook(addr=0x08048485, hook=hook_demo, length=2) # 使用 p.hook 把 0x08048485 处的 2 字节的指令 为 hook_demo，之后执行 0x08048485就会去执行 hook_demo
state = p.factory.blank_state(addr=0x0804846B, add_options={"SYMBOLIC_WRITE_ADDRESSES"})#创建一个 state , 因为要往内存里面设置 符号量 （ BVS ），设置SYMBOLIC_WRITE_ADDRESSES
u = claripy.BVS("u", 8)
state.memory.store(0x0804A021, u) #新建一个 8 位长度的符号量，并把它存到 0x0804A021 (全局变量 u 的位置)
sm = p.factory.simgr(state)
sm.explore(find=0x080484DB)
st = sm.found[0]
print hex(st.se.eval(st.regs.ebx))

SimFile和SimPackets

SimProcedure

angr.SimProcedure 类是 angr 提供的一个用于模拟程序中的函数过程的类，它可以用来模拟文件中的某些函数的行为，尤其是在符号执行过程中。通过继承并重写 SimProcedure 类的 run() 方法，用户可以定义自定义的函数行为，这对于替换或模拟二进制程序中调用的特定函数非常有用

SimProcedure 主要 API 函数表格

Stash

在 angr 中，Stash 是一种状态分类机制，用于将不同类型的符号执行状态组织到 SimulationManager 的不同列表中，以便进行有针对性的分析。每种 Stash 都表示一种特定的状态集合，并支持对状态的筛选、转移、合并、步进等操作。这种设计提高了符号执行的灵活性和效率。

常见的 Stash 类型

Stash 操作