符号执行原理

一、符号执行过程中对IR代码的分析

符号执行通过对IR代码的逐步解析和分析,来模拟程序的各种可能执行路径。这包括处理程序中的每个基本块、条件分支、循环等控制流结构。以下是符号执行过程中如何分析IR代码的详细说明。

二、步骤详解

1、生成并读取IR代码:
* 使用编译器前端(如Clang)将源代码编译成IR代码。例如,将C/C++代码转化为LLVM IR。
* 符号执行引擎读取IR代码,以便后续分析和处理。

2、构建控制流图(CFG):
*控制流图是符号执行的核心,因为它可以显示程序的所有基本块及其控制流关系。这是通过分析IR中的分支和跳转指令来完成的。
*基本块(basic block)是顺序执行的代码片段,不含分支。
*分析出所有基本块,并依据控制跳转指令(如br、switch等)连接基本块,形成控制流图。

3、初始化符号状态:
*输入变量被初始化为符号变量,表示其所有可能的值。
* 初始化全局符号状态,记录程序当前的符号变量和路径条件。

4、符号模拟执行:
*遍历控制流图,从入口基本块(entry block)开始,逐个解析和模拟基本块,以及其中的每条指令。
*对每条IR指令进行处理,更新符号状态。这包括:
--算术指令:如add、sub,通过操作符创建新的符号表达式。
--布尔指令:如icmp比较指令,生成新的符号条件。
--分支指令:如br,依据比较结果构建新的路径条件并分支。
--内存指令:如load、store,符号化内存操作。
*每条指令都可能产生新的符号表达式,这些表达式被添加到当前路径的符号状态中。

5、路径条件管理和分叉:
*遇到条件分支时(如br指令),符号执行引擎根据布尔条件生成不同的路径。
*每条新路径继承当前路径的符号状态,并附加额外的路径条件。
*使用约束求解器(如Z3)来验证路径条件的可行性。如果条件不可满足,该路径被剪枝。

6、示例:LLVM IR 符号执行
考虑如下简单的C函数:
c

int test(int x, int y) {
    int z = x + y;
    if (z > 10) {
        return 1;
    } else {
        return 0;
    }
}

对应的LLVM IR代码:

llvm
define i32 @test(i32 %x, i32 %y) {
entry:
    %z = add i32 %x, %y
    %cmp = icmp sgt i32 %z, 10
    br i1 %cmp, label %if.then, label %if.else

if.then:
    ret i32 1

if.else:
    ret i32 0
}

三、符号执行步步解析:

1、初始化输入符号变量:

i32 %x  ->  SymX
i32 %y  ->  SymY

2、符号模拟执行基本块entry:

%z = add i32 %x, %y  ->  z = SymX + SymY
%cmp = icmp sgt i32 %z, 10  ->  cmp = (SymX + SymY) > 10
br i1 %cmp, label %if.then, label %if.else

*符号表达式:z = SymX + SymY
*符号条件:cmp = (SymX + SymY) > 10
*基于条件cmp,路径分叉:
3、路径分叉模拟:

*路径1(if.then基本块):

z > 10  ;路径条件:PC = (SymX + SymY) > 10
ret i32 1
   ----路径条件可行(由约束求解器验证)。

*路径2(if.else基本块):

z <= 10  ;路径条件:PC = (SymX + SymY) <= 10
ret i32 0
    ----路径条件可行(由约束求解器验证)。

4、记录和报告路径状态:
*在每条路径上记录输入条件和产生的符号表达式。
*在发现潜在错误或漏洞时(如不可满足的路径条件、异常值等)生成报告。

四、小结

在符号执行过程中,确实要对IR代码进行详细的解析和处理。通过对每个基本块和每条指令的分析,符号执行引擎能够生成和维护符号状态和路径条件,从而探索所有可能的执行路径。在分析IR代码时,控制流图(CFG)为符号执行提供了程序结构上的框架,使得路径探索和条件分叉更加系统和高效。这使得符号执行能够很好地处理复杂程序中的潜在问题和验证程序的行为。

最后编辑于
©著作权归作者所有,转载或内容合作请联系作者
平台声明:文章内容(如有图片或视频亦包括在内)由作者上传并发布,文章内容仅代表作者本人观点,简书系信息发布平台,仅提供信息存储服务。