Python中的符号执行（Symbolic Execution）：使用Angr等工具进行漏洞分析

Python中的符号执行：使用Angr等工具进行漏洞分析

大家好，今天我们来聊聊符号执行，以及如何利用Python和Angr等工具进行漏洞分析。符号执行是一种强大的程序分析技术，它允许我们以符号化的方式执行程序，探索所有可能的执行路径，并发现潜在的错误和漏洞。

1. 什么是符号执行？

传统的程序执行（具体执行）使用具体的输入值来运行程序。而符号执行则不同，它使用符号值（ symbolic values）作为输入，这些符号值代表的是所有可能的输入。在符号执行过程中，程序的状态（包括变量的值、程序计数器等）都用包含符号值的表达式来表示。

例如，如果程序的输入是一个整数 x，具体执行会用一个具体的数值（比如 5）来代替 x，然后执行程序。而符号执行则会用一个符号值（比如 x_0）来代替 x，并在执行过程中维护一个符号表达式，表示 x 的值。

当程序遇到分支语句（例如 if 语句）时，符号执行会创建两个分支，分别对应于 if 条件为真和为假的情况。对于每个分支，符号执行会维护一个路径条件 (path condition, PC)，用于记录到达该分支所需要的条件。路径条件是一个布尔表达式，由符号变量和逻辑运算符组成。

符号执行的目标是探索所有可能的执行路径，并找到满足特定条件的路径。例如，我们可以寻找导致程序崩溃的路径，或者寻找违反安全策略的路径。

2. 符号执行的工作原理

符号执行主要包括以下几个步骤：

• 符号化输入： 将程序的输入替换为符号值。
• 符号化执行： 沿着程序的执行路径，用符号表达式来表示程序的状态。
• 路径条件维护： 对于每个分支，维护一个路径条件，记录到达该分支所需要的条件。
• 求解约束： 当到达目标状态（例如，程序崩溃）时，求解路径条件，找到满足条件的输入值。

我们可以用一个简单的例子来说明符号执行的工作原理：

def vulnerable_function(x):
  if x > 10:
    y = x - 10
    if y < 5:
      print("Vulnerable!")
      # 触发漏洞的地方，例如除以0
      z = 1 / (5 - y)
  else:
    print("Safe!")

如果我们使用符号执行分析这个函数，步骤如下：

1. 符号化输入： 将 x 替换为符号值 x_0。
2. 第一个分支： if x > 10 对应于 x_0 > 10。
   • 如果 x_0 > 10 为真，则 y = x - 10 变为 y = x_0 - 10。
   • 第二个分支： if y < 5 对应于 x_0 - 10 < 5，即 x_0 < 15。
     • 如果 x_0 < 15 为真，则打印 "Vulnerable!"，并执行 z = 1 / (5 - y)。
     • 为了使 z 的计算导致除以 0 的错误，我们需要 5 - y = 0，即 y = 5。
     • 由于 y = x_0 - 10，所以 x_0 = 15。
3. 求解约束： 我们需要求解以下约束：
   • x_0 > 10
   • x_0 < 15
   • x_0 = 15

求解这个约束，我们可以得到 x_0 = 15。这意味着，当 x = 15 时，程序会执行到漏洞代码，导致除以 0 的错误。

3. Angr简介

Angr 是一个强大的、可扩展的二进制分析框架，可以用Python编写，并且支持多种架构（例如 x86, ARM, MIPS 等）。它提供了许多功能，包括：

• 符号执行： 使用 Claripy 符号执行引擎。
• 控制流图分析： 生成和分析程序的控制流图。
• 数据流分析： 分析程序的数据流。
• 漏洞分析： 发现程序中的漏洞。
• 程序修复： 自动修复程序中的漏洞。

Angr 的核心概念包括：

• Project： 表示一个要分析的程序。
• CFG： 控制流图，表示程序的控制流。
• State： 程序的状态，包括内存、寄存器、程序计数器等。
• Path： 程序的执行路径，由一系列状态组成。
• SimulationManager： 用于管理多个执行路径。

4. 使用Angr进行符号执行

下面我们通过一个简单的例子，演示如何使用 Angr 进行符号执行。我们仍然使用上面的 vulnerable_function 函数，但这次我们将它编译成一个二进制文件，并使用 Angr 分析它。

首先，我们需要将 Python 代码编译成二进制文件。可以使用 pyinstaller 工具：

pyinstaller --onefile vulnerable_function.py

这将生成一个可执行文件 dist/vulnerable_function（或者类似的名称）。

接下来，我们可以使用 Angr 分析这个二进制文件：

import angr
import claripy

# 加载二进制文件
project = angr.Project("dist/vulnerable_function", auto_load_libs=False)

# 创建初始状态
initial_state = project.factory.entry_state()

# 创建 SimulationManager
simulation = project.factory.simulation_manager(initial_state)

# 探索程序，寻找到达特定地址的路径
# 假设我们知道漏洞代码的地址是 0x400676 (需要根据实际情况调整)
# 可以使用 objdump 或 gdb 等工具查看二进制文件的汇编代码，找到目标地址
target_address = 0x400676

# 定义一个找到目标的函数
def found(state):
  return state.addr == target_address

# 定义一个避免错误的函数 (除以零)
def avoid(state):
  # 这里需要根据实际情况调整，判断是否会发生除以零的错误
  # 通过检查寄存器或内存中的值来判断
  # 比如，检查RBP-0x8处的值是否为5
  return state.solver.eval(state.memory.load(state.regs.rbp-0x8, 4)) == 5

# 使用探索模式寻找目标
simulation.explore(find=found, avoid=avoid)

if simulation.found:
  # 找到了一条路径
  solution_state = simulation.found[0]

  # 获取输入值
  input_arg = solution_state.posix.stdin.content[0]  # 假设输入是标准输入
  print("Found vulnerable input:", solution_state.solver.eval(input_arg))
else:
  print("No vulnerable input found.")

这段代码首先加载二进制文件，然后创建一个初始状态。接下来，它创建一个 SimulationManager，用于管理程序的执行。simulation.explore 函数会沿着程序的执行路径探索，寻找到达 target_address 的路径。find 参数指定了要寻找的目标地址，avoid参数指定了要避免的状态（例如，可能导致除以 0 错误的状态）。found 和 avoid 函数需要根据实际情况进行调整，具体需要分析二进制文件的汇编代码，找到目标地址和可能导致错误的状态。

如果找到了到达目标地址的路径，代码会打印出导致程序执行到该路径的输入值。

5. Angr的高级用法

Angr 提供了许多高级功能，可以用于更复杂的漏洞分析：

• 插桩： 可以使用插桩技术来收集程序执行过程中的信息，例如，可以记录每个指令的执行次数，或者记录每个变量的值。
• 污点分析： 可以使用污点分析技术来跟踪敏感数据的传播，例如，可以跟踪用户输入的数据，并判断它是否会影响程序的控制流。
• 符号执行引擎定制： Angr 使用 Claripy 作为符号执行引擎，可以定制 Claripy 的行为，例如，可以添加新的符号操作，或者修改现有的符号操作。

6. 符号执行的局限性

虽然符号执行是一种强大的程序分析技术，但它也存在一些局限性：

• 路径爆炸： 随着程序复杂度的增加，可能的执行路径数量会呈指数级增长，导致符号执行无法完成。
• 循环： 循环会导致无限多的执行路径，使得符号执行无法终止。
• 外部调用： 符号执行难以处理外部调用，例如，调用操作系统 API 或第三方库。
• 浮点数运算： 符号执行对浮点数运算的支持有限。

为了解决这些问题，研究人员提出了许多改进的符号执行技术，例如：

• 混合执行 (Concolic Execution)： 结合具体执行和符号执行，利用具体执行的结果来指导符号执行，减少路径爆炸。
• 路径合并： 将多个相似的执行路径合并成一个，减少需要分析的路径数量。
• 函数摘要： 对外部调用进行摘要，用一个简单的模型来代替实际的函数调用。

7. 其他符号执行工具

除了 Angr，还有其他一些符号执行工具，例如：

• KLEE： 基于 LLVM 的符号执行引擎。
• SAGE： Microsoft Research 开发的符号执行工具，主要用于测试 Windows 操作系统。
• Mayhem： ForAllSecure 开发的符号执行工具，主要用于 CTF 比赛。

8. 一些使用Angr进行漏洞分析的例子

这里提供几个更具体的Angr使用例子，涉及到常见的漏洞类型。

8.1 缓冲区溢出漏洞

假设有如下C代码，存在一个简单的栈缓冲区溢出漏洞：

#include <stdio.h>
#include <string.h>

int main() {
    char buffer[10];
    char input[100];

    printf("Enter some text: ");
    fgets(input, sizeof(input), stdin);

    strcpy(buffer, input); // Vulnerability: buffer overflow

    printf("You entered: %sn", buffer);
    return 0;
}

使用Angr分析这个程序：

import angr
import claripy

def find_buffer_overflow(binary_path):
    proj = angr.Project(binary_path, auto_load_libs=False)
    entry_state = proj.factory.entry_state()
    sim_manager = proj.factory.simulation_manager(entry_state)

    # 假设我们知道溢出点在strcpy调用之后，栈地址的某个偏移处，我们想让这个地址可控
    # 这里只是一个示例，实际中需要通过分析汇编代码来确定目标地址
    overflow_address = 0x401176 # 需要根据实际情况调整

    def crash_on_overflow(state):
        return state.addr == overflow_address  # 假设溢出影响到这个地址

    sim_manager.explore(find=crash_on_overflow)

    if sim_manager.found:
        found_state = sim_manager.found[0]
        input_arg = found_state.posix.stdin.content[0]
        print("Found vulnerable input:", found_state.solver.eval(input_arg, cast_to=bytes))
    else:
        print("No overflow found.")

# 替换为实际的二进制文件路径
binary_path = "./overflow_example" # 编译后的二进制文件
find_buffer_overflow(binary_path)

8.2 格式化字符串漏洞

假设有如下C代码，存在格式化字符串漏洞：

#include <stdio.h>

int main(int argc, char *argv[]) {
    char format_string[256];

    if (argc != 2) {
        printf("Usage: %s <format_string>n", argv[0]);
        return 1;
    }

    snprintf(format_string, sizeof(format_string), argv[1]);  // Vulnerability: Format string vulnerability
    printf(format_string); // Vulnerability: Format string vulnerability

    return 0;
}

使用Angr分析这个程序：

import angr
import claripy

def find_format_string_vuln(binary_path):
    proj = angr.Project(binary_path, auto_load_libs=False)

    # 创建符号参数argv[1]
    arg1 = claripy.BVS("format_string", 256 * 8) # 最大长度256字节

    # 创建初始状态，并设置命令行参数
    initial_state = proj.factory.entry_state(args=[binary_path, arg1])
    sim_manager = proj.factory.simulation_manager(initial_state)

    # 假设我们想找到一种方式来改变程序的执行流程，例如修改某个内存地址
    # 这里只是一个示例，实际中需要通过分析汇编代码来确定目标地址
    # 通常，格式化字符串漏洞可以用来覆盖返回地址或者GOT表
    target_address = 0x401186 # 需要根据实际情况调整

    def reach_target(state):
      return state.addr == target_address

    sim_manager.explore(find=reach_target)

    if sim_manager.found:
        found_state = sim_manager.found[0]
        input_arg = found_state.posix.argv[1]
        print("Found vulnerable input:", found_state.solver.eval(input_arg, cast_to=bytes))
    else:
        print("No format string vulnerability found.")

# 替换为实际的二进制文件路径
binary_path = "./format_string_example" # 编译后的二进制文件
find_format_string_vuln(binary_path)

8.3 整数溢出漏洞

假设有如下C代码，存在整数溢出漏洞：

#include <stdio.h>
#include <stdlib.h>

int main() {
    int size;
    char *buffer;

    printf("Enter the size of the buffer: ");
    scanf("%d", &size);

    // Vulnerability: Integer overflow can lead to small allocation
    buffer = (char*) malloc(size * sizeof(int));

    if (buffer == NULL) {
        printf("Memory allocation failed.n");
        return 1;
    }

    printf("Buffer allocated. Enter data: ");
    // 假设这里后续使用了buffer，并且假设后续的操作会导致越界访问
    // 例如，使用一个比实际分配空间更大的索引访问buffer
    buffer[size * sizeof(int) / 2] = 'A';  // 假设这里造成越界访问

    free(buffer);
    return 0;
}

使用Angr分析这个程序：

import angr
import claripy

def find_integer_overflow(binary_path):
    proj = angr.Project(binary_path, auto_load_libs=False)

    # 创建符号变量作为输入
    size = claripy.BVS("size", 32) # size是32位的整数

    # 创建初始状态，并设置输入
    initial_state = proj.factory.entry_state(stdin=size)  # size作为标准输入

    sim_manager = proj.factory.simulation_manager(initial_state)

    # 假设溢出导致程序崩溃，或执行到某个特定地址
    # 这里需要通过分析汇编代码来确定目标地址
    overflow_address = 0x4011A6 # 需要根据实际情况调整

    def crash_on_overflow(state):
      return state.addr == overflow_address

    sim_manager.explore(find=crash_on_overflow)

    if sim_manager.found:
        found_state = sim_manager.found[0]
        input_arg = found_state.posix.stdin.content[0]
        print("Found vulnerable input:", found_state.solver.eval(input_arg))
    else:
        print("No integer overflow vulnerability found.")

# 替换为实际的二进制文件路径
binary_path = "./integer_overflow_example" # 编译后的二进制文件
find_integer_overflow(binary_path)

请注意，这些代码示例是简化版本，实际的漏洞分析可能需要更复杂的设置和更深入的分析。你需要根据具体程序的汇编代码来确定目标地址、溢出条件、避免条件等。并且，需要仔细分析Angr的状态信息，才能找到真正的漏洞。

9. 如何选择合适的符号执行工具？

选择合适的符号执行工具取决于你的具体需求和目标。以下是一些选择工具时需要考虑的因素：

• 支持的架构： 确保工具支持你所要分析的程序的架构。
• 易用性： 选择一个易于学习和使用的工具。
• 性能： 符号执行的性能是一个重要的考虑因素，特别是对于复杂的程序。
• 功能： 不同的工具提供不同的功能，选择一个满足你需求的工具。
• 社区支持： 选择一个拥有活跃社区的工具，可以获得更多的帮助和支持。

工具	优点	缺点
Angr	功能强大，可扩展性强，Python接口	学习曲线陡峭，配置复杂
KLEE	基于LLVM，性能较好，支持多种语言	配置和使用相对复杂
SAGE	擅长处理Windows程序，大规模测试能力	闭源，使用受限
Mayhem	自动化程度高，适合CTF比赛	商业软件，价格昂贵

10. 总结一下

符号执行是一种强大的程序分析技术，可以用于发现程序中的漏洞。Angr 是一个流行的符号执行框架，可以用 Python 编写，并且提供了许多功能，可以用于漏洞分析。虽然符号执行存在一些局限性，但通过结合其他技术，可以有效地提高分析效率。希望今天的讲解能够帮助你更好地理解符号执行，并开始使用 Angr 进行漏洞分析。

对程序的深入理解是关键

成功运用符号执行进行漏洞分析的关键在于对目标程序有深入的理解。这包括理解程序的控制流、数据流、以及潜在的漏洞点。只有深入理解程序，才能有效地利用符号执行工具，找到隐藏的漏洞。

实践是掌握符号执行的最好方式

理论学习是基础，但实践才是掌握符号执行的最好方式。通过实际操作，分析不同的程序，尝试发现各种类型的漏洞，才能真正掌握符号执行技术。尝试从简单的例子开始，逐步挑战更复杂的程序，不断积累经验。

更多IT精英技术系列讲座，到智猿学院