符号执行入坑指南

本文主要是介绍符号执行入坑指南，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

0x10 符号执行的定义

符号执行是软件测试行业新型的一个方向，当下较为火热，也给安全测试提供了新的思路，衍生出了诸多安全测试工具。维基百科中定义的符号执行如下

在计算机科学中，符号执行技术指的是通过程序分析的方法，确定哪些输入向量会对应导致程序的执行结果向量的方法。

抛开专业术语的表层，拨云见日，符号执行就是使用符号值代替真实值执行。在计算机程序中，尤其是C语言，符号是指函数名和变量名，在这里，更多的是指变量。符号执行就是说，不给定函数变量（比如入参）特定的值，而是用变量本身来替代，达到模拟输入的效果，即模拟每个路径来产生每一个执行的可能性，将执行语句的结果整合成若干条数学表达式。

符号执行有两篇文章可以参考。其一是2010年David Brumley团队在S&P会议上发表的《All You Ever Wanted to Knowabout Dynamic Taint Analysis and Forward Symbolic Execution (but Might HaveBeen Afraid to Ask)》[1]。这篇文章同时介绍了动态污点分析和前向符号执行的基本概念，作者构造了一种简化的中间语言，用来形式化地描述这两种程序分析技术的根本原理。其二是2011年CristianCadar发表在ACM通讯上的一篇短文《Symbolic execution forsoftware testing: three decades later》[2]，以较为通俗的语言和简单的例子阐述了符号执行的基本原理，并介绍了符号执行技术的发展历程和面临挑战。

0x20 符号执行的分类

符号执行技术是一种白盒的静态分析技术。即，分析程序可能的输入需要能够获取到目标源代码的支持。同时，它是静态的，因为并没有实际的执行程序本身，而是分析程序的执行路径。符号执行根据发展状况可以分为传统的符号执行、动态符号执行和选择性符号执行。

• 传统的符号执行其实是通过解析程序，利用符号值来模拟执行
• 动态符号执行结合真实执行和传统的模拟执行，两者并行，达到真实值以及符号同时执行的效果
• 选择性符号执行则是按照手动划分感兴趣的部分，有选择性的进行符号执行，剩下则用真实值进行执行

0x30 控制流程图-符号执行树

我们以实际的例子来说明。函数代码如下

int d(int x){int y = 2*x;y--;if(y==2)x++;elsex--;return x;
}

该代码很简单，有一个if语句的条件分支，下图就是程序的全部路径运行结果，可以选择对应的赋值来到达对应的运行结果

0x40 实际应用

安全客上有一篇文章，讲解的很好：符号执行——从入门到高速。我更欣赏该文章讲解的实际应用方面。我们知道，由于物联网设备逐渐的大众化，嵌入式设备的漏洞挖掘需求更加显著。那么在嵌入式的环境下，使用符号执行技术挖掘漏洞可行吗？答案是肯定的。但是要解决很多问题，需要解决的问题除了类似于KLEE中出现的与外设交互的系统调用建模以外，还需要解决嵌入式设备中经常出现的混合代码情况。即，给出的嵌入式源代码中，有c语言代码、二进制代码（共享库）和汇编代码。面对这种情况应该如何启用符号执行呢？

举个实际的例子，以下是基于ARMv7架构的一段嵌入式代码。学过嵌入式的人都知道，在嵌入式设备中，仅仅使用C语言往往还是不够的，因为汇编有时候能够更好的与硬件交互，以下代码使用了汇编和C语言的混合编程，能够极大提高效率。

unsigned char msg[] = "world";
int index;void uart_send(unsigned char a)
{__asm volatile("SVC #0");__asm volatile("BX LR");
}void os_uart_send(){...}int main(int argc, char* argv[])
{uart_send(msg[index++]);return 0;
}

该代码的主要作用是通过uart发送消息。函数uart_send()中，通过指令“SVC #0”切换成SVC的寄存器模式之后，将实际上调用函数os_uart_send()发送消息。其中，uart_send函数的参数将直接在os_uart_send()函数中使用。上述代码，通过LLVM转换成LLVM-IR的形式，为下面的代码。

@msg = global [6xi8]c"world0"
@index = global i32 0define void @uart_send(i8 zeroext) #0
{entry:call void asm sideeffect "SVC #0",""()call void asm sideeffect "BX LR",""()unreachable
}define void @os_uart_send(){...}define int @main() #1
{entry:%0 = load i32* @index%inc = add nsw i32 %0, 1store i32 %inc, i32* @index%arrayidx = getelementptr inbounds [6xi8]* @msg, i32 0, i32 %0%1 = load i8* %arrayidxcall void @uart_send(i8 zeroext %1)ret i32 0
}

为什么要转换成LLVM-IR的代码呢。LLVM-IR是LLVM的一种中间的语言表达形式，也是一种汇编语言的形式。现有的KLEE工具就是LLVM-IR工具实现的符号执行虚拟机。在解释上面的代码之前，简单介绍几个LLVM-IR的基础语法，以便更清楚的理解。

LLVM-IR的变量有三种，通过前缀@或者%的形式区分，其中@表示全局变量，%表示局部变量：

1. %或者@接数字，表示的是临时变量，在一个函数中，从0开始编号使用。比如%0，%1，。。
2. %或者@接字符串，表示有名字的变量，可以任意使用；
3. 第三类就是立即数

@msg = global [6xi8]c"world0"
@index = global i32 0

上述代码初始化了全局变量msg和index。

entry:
%0 = load i32* @index
%inc = add nsw i32 %0, 1
store i32 %inc, i32* @index

上述代码中，i32表示是32位的类型，i32表示的指向i32类型的指针类型。%0 = load i32 @index表示将全局变量index的值赋值给局部变量%0. Add nsw是有符号的相加。再加完之后，又把数值存储回了全局变量index。

%arrayidx = getelementptr inbounds [6xi8]* @msg, i32 0, i32 %0
%1 = load i8* %arrayidx
call void @uart_send(i8 zeroext %1)

上述代码中，[6xi8] 这种形式表示的是数组类型，这里就是含有6个8位的元素的数组。Getelementptr inbounds即使获得数组对应元素的指针。之后利用语句%1 = load i8* %arrayidx获取指针指向的8位的值，在传入到函数uart_send中执行。

可以发现，如果按照已有的KLEE方法，在转换成LLVM-IR代码之后，由于代码中含有arm架构的汇编，而该arm代码中没有明显的调用参数的代码和方式，使得符号数值的传递再次中断，导致KLEE方法不能执行。因此，我们需要对上述含有混合LLVM-IR代码的内存进行再次转化，使得含有低级语意的arm汇编也能够被KLEE的符号执行虚拟机分析。

通过程序分析的方式，将混合由高级语言和低级语言的代码同时转化成KLEE能够分析的语言，从而执行符号执行的分析。根据Inception里面的思想，上述LLVM-IR转化之后，可以有下面的表达形式：

@msg = global [6xi8]c"world0"
@index = global i32 0; stack is stored in global variables
@R0 = global i32 0, align 4
@SP = global i32 0, align 4 
@_SVC_fe = global i32 0, align 4 
@LR = global i32 0, align 4 
@.stack = global [8202xi4] zeroinitializer define void @uart_send(i8) #0
{; pass the parameters from high level to the low level.entry:%1 = zext i8 %0 to i32store i32 %1, i32* @R0br label %"uart_send+0" ; jmp to the actual code"uart_send+0":%SP1 = load i32* @SP ; load the stack pointerstore i32 0, iew* @_SVC_festore i32 268436580, i32* @PC ; store pointer executioncall void (...)* @_sv_call()call void (...)* os_uart_send()    ; invoke uart send function and  using the value from the R0%LR1 = load i32* @LR1              ;load return addressret void
}define void @os_uart_send(){...}define int @main() #1
{entry:%0 = load i32* @index%inc = add nsw i32 %0, 1store i32 %inc, i32* @index%arrayidx = getelementptr inbounds [6xi8]* @msg, i32 0, i32 %0%1 = load i8* %arrayidxcall void @uart_send(i8 zeroext %1)ret i32 0
}

可以发现，相比于之前的LLVM-IR。函数uart_send中多了一部分内容。更多内容参考之前提到的文章就行了。

0x50 总结

鉴于代码覆盖率越高越好，符号执行的要求如下

• 尽可能的覆盖所有的可能的执行路径.
• 速度尽可能快.

因为这样才能达到测试所有代码的目的，当然这是理论上的想法，实际过程中，项目庞大而复杂。例如对于一组分支组成的树形结构，最少有O(n)O(n)O(n)种指派方案可以覆盖到所有路径，也就是说最小的复杂度是线性的，最多有O(2n)O(2^n)O(2 n )种指派方案，是指数增长类型。这就是路径爆炸。

所以，需要找到一个平衡点。符号执行实质是通过限制路径搜索空间来进行程序遍历，运行时间与所需要遍历的路径空间大小成正比。利用可靠的程序分析技术来减小路径爆炸的复杂度，利用启发式搜索搜索最佳路径，这些都是符号执行追求的终极目标。

这篇关于符号执行入坑指南的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！

---