2.3 语义匹配与符号执行

更新 2026年4月6日

2 min read

2.3.1 符号执行基础 #

核心概念 #

具体执行 vs 符号执行
┌──────────────────────┐        ┌──────────────────────┐
│ 具体执行           │        │ 符号执行             │
│                      │        │                      │
│ 输入: x = 5          │        │ 输入: x = α (符号)   │
│                      │        │                      │
│ y = x + 3            │        │ y = α + 3            │
│ if y > 10:           │        │ if α + 3 > 10:       │
│     z = 1            │        │     Path1: α > 7     │
│ else:                │        │ else:                │
│     z = 0            │        │     Path2: α ≤ 7     │
└──────────────────────┘        └──────────────────────┘
结果: z = 0 (单一结果)          结果: 两条路径的约束

具体执行 vs 符号执行
┌──────────────────────┐        ┌──────────────────────┐
│ 具体执行           │        │ 符号执行             │
│                      │        │                      │
│ 输入: x = 5          │        │ 输入: x = α (符号)   │
│                      │        │                      │
│ y = x + 3            │        │ y = α + 3            │
│ if y > 10:           │        │ if α + 3 > 10:       │
│     z = 1            │        │     Path1: α > 7     │
│ else:                │        │ else:                │
│     z = 0            │        │     Path2: α ≤ 7     │
└──────────────────────┘        └──────────────────────┘
结果: z = 0 (单一结果)          结果: 两条路径的约束

Plaintext

2.3.2 在二进制Diff中的应用 #

验证代码等价性 #

def verify_equivalence_with_se(func1, func2):
    """
    使用符号执行验证两个函数的等价性
    """
    # 创建符号输入
    sym_inputs = create_symbolic_inputs(func1)
    
    # 对func1执行符号执行
    result1 = symbolic_execute_function(func1, sym_inputs)
    
    # 对func2执行符号执行
    result2 = symbolic_execute_function(func2, sym_inputs)
    
    # 检查等价性
    solver = Solver()
    
    for path1 in result1.paths:
        for path2 in result2.paths:
            solver.reset()
            solver.add(path1.constraint)
            solver.add(path2.constraint)
            solver.add(path1.output != path2.output)
            
            if solver.check() == SAT:
                counterexample = solver.model()
                return False, counterexample
    
    return True, None

def verify_equivalence_with_se(func1, func2):
    """
    使用符号执行验证两个函数的等价性
    """
    # 创建符号输入
    sym_inputs = create_symbolic_inputs(func1)
    
    # 对func1执行符号执行
    result1 = symbolic_execute_function(func1, sym_inputs)
    
    # 对func2执行符号执行
    result2 = symbolic_execute_function(func2, sym_inputs)
    
    # 检查等价性
    solver = Solver()
    
    for path1 in result1.paths:
        for path2 in result2.paths:
            solver.reset()
            solver.add(path1.constraint)
            solver.add(path2.constraint)
            solver.add(path1.output != path2.output)
            
            if solver.check() == SAT:
                counterexample = solver.model()
                return False, counterexample
    
    return True, None

Python

识别语义等价的代码变形 #

# 代码变形示例
Original:           Optimized:
mov eax, [rbp-4]    mov eax, [rbp-4]
add eax, 5          lea eax, [eax+5]
mov [rbp-8], eax    mov [rbp-8], eax

语义等价性检查:
输入: [rbp-4] = α (符号)
输出: [rbp-8] = α + 5 (两种情况相同)
结论: 语义等价

# 代码变形示例
Original:           Optimized:
mov eax, [rbp-4]    mov eax, [rbp-4]
add eax, 5          lea eax, [eax+5]
mov [rbp-8], eax    mov [rbp-8], eax

语义等价性检查:
输入: [rbp-4] = α (符号)
输出: [rbp-8] = α + 5 (两种情况相同)
结论: 语义等价

ASM

2.3.3 约束求解 #

SMT求解器 #

求解器	特点	适用场景
Z3	Microsoft开发，功能强大	通用约束求解
CVC4	自动化程度高	验证、类型检查
Yices	高性能	位向量、数组理论
Boolector	针对位向量优化	位向量问题

使用Z3进行约束求解 #

from z3 import *

def check_path_equivalence(path1, path2):
    """
    检查两条路径是否等价
    """
    solver = Solver()
    
    # 定义符号变量
    x = BitVec('x', 32)
    y = BitVec('y', 32)
    
    # 添加路径约束
    solver.add(path1.constraint)
    solver.add(path2.constraint)
    
    # 检查是否可以找到使输出不同的输入
    solver.add(path1.output != path2.output)
    
    if solver.check() == sat:
        return False  # 不等价
    else:
        return True   # 等价

from z3 import *

def check_path_equivalence(path1, path2):
    """
    检查两条路径是否等价
    """
    solver = Solver()
    
    # 定义符号变量
    x = BitVec('x', 32)
    y = BitVec('y', 32)
    
    # 添加路径约束
    solver.add(path1.constraint)
    solver.add(path2.constraint)
    
    # 检查是否可以找到使输出不同的输入
    solver.add(path1.output != path2.output)
    
    if solver.check() == sat:
        return False  # 不等价
    else:
        return True   # 等价

Python