CTF基础知识之符号执行

符号执行

概念及原理介绍

符号执行是程序分析的一种思路，可以类比解方程：我不知道该怎如何确定输入（或感兴趣的变量等）和程序执行路径之间的关系，但我可以把输入设为变量x（此为“符号”），然后对照纸面上的程序，每执行一步，我就记录下来它执行的条件（此为“执行”），作为方程的一部分。如果碰到分支语句，就分为两个方程，一个方程对应一个分支执行条件。如此等到程序结束，我就有了一堆方程，每个方程对应一个执行路径。想分析哪个路径，解对应的方程就行了。通过这样的分析技术，就可以获得让特定区域执行的输入。

符号执行技术是一种白盒的静态分析技术。符号执行(symbolic execution)本身是静态的，因为它只是把具体的输入值(input value)用符号值(symbolic value)替换，然后根据符号值的的约束条件在约束求解器(constraint solver)允许的条件下求解出满足条件的输入值。如果把上述最终状态属性替换成程序形成的bug状态，比如，存在数组越界复制的状态，那么，我们就能够利用此技术挖掘漏洞的输入向量了。

左边的代码中，testme()函数有3条执行路径，组成了右图中的执行树。直观上来看，我们只要给出三个输入就可以遍历这三个路径，即图中绿色的x和y取值。符号执行的目标就是能够生成这样的输入集合，在给定的时间内探索所有的路径。

符号执行通过维护符号状态和路径约束，以便在运行过程中传递信息。

符号状态(symbolic state)：符号执行维护一个符号状态σ，将变量映射到符号表达式。
符号路径约束(symbolic path constraint)：符号路径约束PC，它是符号表达式上无量词的一阶公式。
在执行开始时，将σ初始化为一个空映射，将PC初始化为true；
在符号执行过程中，σ和PC都会更新。
在沿着程序执行路径的符号执行结束时，使用约束求解器对PC进行求解，以生成具体的输入值。如果程序在这些具体的输入值上执行，它将采用与符号执行完全相同的路径，并以相同的方式终止。

对于样例代码，具体的过程如下

初始化：初始化符号状态σ为空，符号路径约束PC为true；
在每个赋值v = e处，符号执行都通过将 v 映射到σ(e)来更新σ，该映射是通过对当前符号状态求值, 而获得的符号表达式。例如：
- main（）函数的前两行（第16-17行）的符号执行导致σ= {x ↦x0，y ↦ y0}，其中x0，y0是两个初始不受约束的符号值；
- 在执行第6行之后，σ = {x ↦x0，y ↦y0，z ↦ 2y0}。
对于每个条件语句：if（e） then S1 else S2。
- 在第7行之后，分别创建了两个符号执行实例，分别具有路径约束x0 = 2y0和x ≠ 2y0;
- 在第8行之后，分别创建两个具有路径约束的符号执行实例（x0 = 2y0）∧（x0 > y0 + 10）和（x0 = 2y0）∧（x0 ≤ y0 + 10）。
- “then”分支： PC被更新为PC ∧ σ(e)；
- “else”分支：生成一个新的PC’, PC’被初始化为：PC∧¬ σ(e)；
- 如果分支的状态σ的PC可满足，则符号执行沿着分支继续，否则路径终止。
  例如:
如果一个符号执行实例碰到了exit或error时，当前符号执行实例就会被终止，并利用一个现成的约束求解器来生成一个可满足当前路径约束的赋值。例如：
- 三条路径按照约束求解后，分别得到我们期望的三组输入：{x=0, y=1}，{x=2, y=1}和{x=30, y=15}。
若代码中包含循环或递归结构，且它们的终止条件是符号化的，则可能导致有无穷多条路径。在实践过程中，需要对路径搜索设置一个限制，例如timeout，限制路径数量，循环迭代次数或探测深度。

经典的符号执行有一个关键的缺点，若符合执行路径的符号路径约束无法使用约束求解器进行有效的求解，则无法生成输入。

Angr一个简单的实践

angr是一个基于python的二进制漏洞分析框架，它将以前多种分析技术集成进来，它能够进行动态的符号执行分析（如，KLEE和Mayhem），也能够进行多种静态分析

基本思路：

①.新建一个Angr工程，并且载入二进制文件
②.创建程序入口点的state
③.将要求解的变量符号化
④.创建SimulationManager进行程序执行管理
⑤.搜索满足我们目标的state
⑥.求解程序执行到state时，符号化变量所需要的约束条件
⑥.解出约束条件，获得目标值

程序

不同的u对应不同的输出，为了找到能输出 “you win”的u，通过符号执行进行分析。

#include <stdio.h>
char u=0;
int main(void)
{
	int i, bits[2]={0,0};
	for (i=0; i<8; i++) {
		bits[(u&(1<<i))!=0]++;
	}
	if (bits[0]==bits[1]) {
		printf("you win!");
	}
	else {
		printf("you lose!");
	}
	return 0;
}

python脚本如下，每行代码的含义见备注

import angr
import claripy

def main():
	#新建一个工程，导入二进制文件，后面的选项是选择不自动加载依赖项
	p = angr.Project('D:/WinAFL/angr-doc/examples/sym-write/issue', load_options={"auto_load_libs": False})
	#函数返回一个代表着程序入口点的state对象，这也就是我们进行符号执行的核心对象，包括了符号信息、内存信息、寄存器信息等
	state = p.factory.entry_state(add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES})
 	#创建一个符号变量，这个符号变量以8位bitvector形式存在，名称为u
	u = claripy.BVS("u", 8)
	#把符号变量保存到指定的地址中，这个地址是和二进制文件相关联的， 0x0804a021
	state.memory.store(0x0804a021, u)
	#创建一个Simulation Manager对象，这个对象和我们的状态有关系
	sm = p.factory.simulation_manager(state)
	# 使用explore函数进行状态搜寻，检查输出字符串是win还是lose
	def correct(state):
		try:
			return b'win' in state.posix.dumps(1)
		except:
			return False
	def wrong(state):
		try:
			return b'lose' in state.posix.dumps(1)
		except:
			return False
	#寻找到满足correct条件且不满足wrong条件的state，即目标state。
	sm.explore(find=correct, avoid=wrong)
     #获得到state之后，运行state.solver.eval(u)求解u的值。
	return sm.found[0].solver.eval_upto(u, 256)

if __name__ == '__main__':
	print(repr(main()))