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++;
else
x--;
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 0
define 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, 1
store i32 %inc, i32* @index
%arrayidx = getelementptr inbounds [6xi8]* @msg, i32 0, i32 %0
%1 = load i8* %arrayidx
call void @uart_send(i8 zeroext %1)
ret i32 0
}
为什么要转换成LLVM-IR的代码呢。LLVM-IR是LLVM的一种中间的语言表达形式,也是一种汇编语言的形式。现有的KLEE工具就是LLVM-IR工具实现的符号执行虚拟机。在解释上面的代码之前,简单介绍几个LLVM-IR的基础语法,以便更清楚的理解。
LLVM-IR的变量有三种,通过前缀@或者%的形式区分,其中@表示全局变量,%表示局部变量:
- %或者@接数字,表示的是临时变量,在一个函数中,从0开始编号使用。比如%0,%1,。。
- %或者@接字符串,表示有名字的变量,可以任意使用;
- 第三类就是立即数
@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 i32
store i32 %1, i32* @R0
br label %"uart_send+0" ; jmp to the actual code
"uart_send+0":
%SP1 = load i32* @SP ; load the stack pointer
store i32 0, iew* @_SVC_fe
store i32 268436580, i32* @PC ; store pointer execution
call 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 address
ret void
}
define void @os_uart_send(){...}
define int @main() #1
{
entry:
%0 = load i32* @index
%inc = add nsw i32 %0, 1
store i32 %inc, i32* @index
%arrayidx = getelementptr inbounds [6xi8]* @msg, i32 0, i32 %0
%1 = load i8* %arrayidx
call 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 )种指派方案,是指数增长类型。这就是路径爆炸。
所以,需要找到一个平衡点。符号执行实质是通过限制路径搜索空间来进行程序遍历,运行时间与所需要遍历的路径空间大小成正比。利用可靠的程序分析技术来减小路径爆炸的复杂度,利用启发式搜索搜索最佳路径,这些都是符号执行追求的终极目标。