符号执行原理

一、符号执行过程中对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)为符号执行提供了程序结构上的框架,使得路径探索和条件分叉更加系统和高效。这使得符号执行能够很好地处理复杂程序中的潜在问题和验证程序的行为。

最后编辑于
©著作权归作者所有,转载或内容合作请联系作者
  • 序言:七十年代末,一起剥皮案震惊了整个滨河市,随后出现的几起案子,更是在滨河造成了极大的恐慌,老刑警刘岩,带你破解...
    沈念sama阅读 218,607评论 6 507
  • 序言:滨河连续发生了三起死亡事件,死亡现场离奇诡异,居然都是意外死亡,警方通过查阅死者的电脑和手机,发现死者居然都...
    沈念sama阅读 93,239评论 3 395
  • 文/潘晓璐 我一进店门,熙熙楼的掌柜王于贵愁眉苦脸地迎上来,“玉大人,你说我怎么就摊上这事。” “怎么了?”我有些...
    开封第一讲书人阅读 164,960评论 0 355
  • 文/不坏的土叔 我叫张陵,是天一观的道长。 经常有香客问我,道长,这世上最难降的妖魔是什么? 我笑而不...
    开封第一讲书人阅读 58,750评论 1 294
  • 正文 为了忘掉前任,我火速办了婚礼,结果婚礼上,老公的妹妹穿的比我还像新娘。我一直安慰自己,他们只是感情好,可当我...
    茶点故事阅读 67,764评论 6 392
  • 文/花漫 我一把揭开白布。 她就那样静静地躺着,像睡着了一般。 火红的嫁衣衬着肌肤如雪。 梳的纹丝不乱的头发上,一...
    开封第一讲书人阅读 51,604评论 1 305
  • 那天,我揣着相机与录音,去河边找鬼。 笑死,一个胖子当着我的面吹牛,可吹牛的内容都是我干的。 我是一名探鬼主播,决...
    沈念sama阅读 40,347评论 3 418
  • 文/苍兰香墨 我猛地睁开眼,长吁一口气:“原来是场噩梦啊……” “哼!你这毒妇竟也来了?” 一声冷哼从身侧响起,我...
    开封第一讲书人阅读 39,253评论 0 276
  • 序言:老挝万荣一对情侣失踪,失踪者是张志新(化名)和其女友刘颖,没想到半个月后,有当地人在树林里发现了一具尸体,经...
    沈念sama阅读 45,702评论 1 315
  • 正文 独居荒郊野岭守林人离奇死亡,尸身上长有42处带血的脓包…… 初始之章·张勋 以下内容为张勋视角 年9月15日...
    茶点故事阅读 37,893评论 3 336
  • 正文 我和宋清朗相恋三年,在试婚纱的时候发现自己被绿了。 大学时的朋友给我发了我未婚夫和他白月光在一起吃饭的照片。...
    茶点故事阅读 40,015评论 1 348
  • 序言:一个原本活蹦乱跳的男人离奇死亡,死状恐怖,灵堂内的尸体忽然破棺而出,到底是诈尸还是另有隐情,我是刑警宁泽,带...
    沈念sama阅读 35,734评论 5 346
  • 正文 年R本政府宣布,位于F岛的核电站,受9级特大地震影响,放射性物质发生泄漏。R本人自食恶果不足惜,却给世界环境...
    茶点故事阅读 41,352评论 3 330
  • 文/蒙蒙 一、第九天 我趴在偏房一处隐蔽的房顶上张望。 院中可真热闹,春花似锦、人声如沸。这庄子的主人今日做“春日...
    开封第一讲书人阅读 31,934评论 0 22
  • 文/苍兰香墨 我抬头看了看天上的太阳。三九已至,却和暖如春,着一层夹袄步出监牢的瞬间,已是汗流浃背。 一阵脚步声响...
    开封第一讲书人阅读 33,052评论 1 270
  • 我被黑心中介骗来泰国打工, 没想到刚下飞机就差点儿被人妖公主榨干…… 1. 我叫王不留,地道东北人。 一个月前我还...
    沈念sama阅读 48,216评论 3 371
  • 正文 我出身青楼,却偏偏与公主长得像,于是被迫代替她去往敌国和亲。 传闻我的和亲对象是个残疾皇子,可洞房花烛夜当晚...
    茶点故事阅读 44,969评论 2 355