Contents

1. 符号执行
2. 污点分析
1. 2.1. 静态污点分析
2. 2.2. 动态污点分析
3. angr
1. 3.1. angr_ctf

符号执行

给一个结果，求输入。

根据发展状况,可以将符号执行分为经典符号执行、动态符号执行和选择性符号执行

经典符号执行

经典符号执行的核心思想是通过使用符号值来代替具体值作为程序输入，并用符号表达式来表示与符号值相关的程序变量的值。经典符号执行并不真实地执行,而是基于解析程序，通过符号值模拟执行。

int twice(int v){
	return 2*v;
}

void testme(int x, int y){
	z = twice(y);
	if (z == x){
		if (x > y+10)
			ERROR;
	}
}   

int main(){
	x = sym_input();
	y = sym_input();
	testme(x, y);
	return 0;
}

符号执行使用符号值代替具体值，在符号执行过程中，符号执行引擎始终保持一个状态信息(pc, π, σ)，其中：

1）pc 指向需要处理的下一条程序语句，其可以是赋值语句、条件分支语句或者是跳转语句。

2）π 指代路径约束信息，表示为执行到程序特定语句需要经过的条件分支，以及各分支处关于符号 α_i 的表达式。在分析的过程中，将其初始定义为 π = true。

3）σ 表示与程序变量相关的符号值集，包括含有具体值和符号值 α_i 的表达式

据此分析上述代码段：

开始执行

符号变量σ : α, β

初始状态为σ : {x → α, y → β}; π＝true

执行到第6行

σ : {x → α, y → β, z → 2∗β}; π＝true

执行到第7行，延伸出两个分析状态

true路径：if z == x → σ : {x → α, y → β, z → 2∗β}; π: 2∗β == α

true路径：if x > y+10 → σ : {x → α, y → β, z → 2∗β}; π: {2∗β == α ∩ α > β+10}

false路径：if x > y+10 → σ : {x → α, y → β, z → 2∗β}; π: {2∗β == α ∩ α <= β+10}

false路径：if z != x → σ : {x → α, y → β, z → 2∗β}; π: 2∗β != α

传统符号执行在原理上是可以对程序路径进行全覆盖的,而且可以针对每一路径都生成符合该路径的测试用例。

执行路径（execution path）true false序列
执行树（execution tree）

动态符号执行

符号执行在发展过程中出现了一种叫做动态符号执行的方法（concrete and symbolic， concolic）。动态符号执行是以具体数值作为输入来模拟执行程序代码，与传统静态符号执行相比，其输入值的表示形式不同。动态符号执行使用具体值作为输入，同时启动代码模拟执行器，并从当前路径的分支语句的谓词中搜集所有符号约束。然后修改该符号约束内容构造出一条新的可行的路径约束，并用约束求解器求解出一个可行的新的具体输入，接着符号执行引擎对新输入值进行一轮新的分析。通过使用这种输入迭代产生变种输入的方法，理论上所有可行的路径都可以被计算并分析一遍。
动态符号执行相对于静态符号执行的优点是每次都是具体输入的执行，在模拟执行这个过程中，符号化的模拟执行比具体化的模拟执行的开销大很多；并且模拟执行过程中所有的变量都为具体值，而不必使用复杂的数据结构来表达符号值，使得模拟执行的花销进一步减少。但是动态符号执行的结果是对程序的所有路径的一个下逼近，即其最后产生路径的集合应该比所有路径集合小，但这种情况在软件测试中是允许的。

正向的符号执行

正向的符号执行用于全面地对程序代码进行分析，可分为过程内分析和过程间分析。

过程内分析：只对单个函数的代码进行分析
过程间分析（或全局分析）：对整个软件代码进行上下文敏感的分析，在当前函数入口点要考虑当前函数的调用信息和环境信息等

逆向的符号执行

逆向的符号执行用于对可能存在漏洞的部分代码进行有针对性的分析。通过分析这些程序语句，可以得到变量取值满足怎样的约束表示程序存在漏洞，将这样的约束记录下来，在之后的分析中，通过逆向分析判断程序存在漏洞的约束是否是可以满足的。通过不断地记录并分析路径条件，检查程序是否可能存在带有程序漏洞的路径。

缺点

路径状态空间爆炸问题：由于每一个条件分支语句都可能会使当前路径再分出一条新的路径，特别是遇到循环分支时，每增加一次循环都将增加一条新路径，因此这种增长是指数级的。

解决：比如规定每个过程内的分析路径的数目上限，或者设置时间上限和内存上限等来进行缓解。

污点分析

污点分析可以抽象成一个三元组<sources,sinks,sanitizers>的形式

source ：污点源，代表直接引入不受信任的数据或者机密数据到系统中；

sink：污点汇聚点，代表直接产生安全敏感操作(违反数据完整性)或者泄露隐私数据到外界(违反数据保密性)；

sanitizer：无害处理，代表通过数据加密或者移除危害操作等手段使数据传播不再对软件系统的信息安全产生危害。

污点分析是一种跟踪并分析污点信息在程序中流动的技术。在漏洞分析中，使用污点分析技术将所感兴趣的数据（通常来自程序的外部输入）标记为污点数据，然后通过跟踪和污点数据相关的信息的流向，可以知道它们是否会影响某些关键的程序操作，进而挖掘程序漏洞。即将程序是否存在某种漏洞的问题转化为污点信息是否会被 Sink 点上的操作所使用的问题。

显式信息流：通过数据依赖传播的信息流

[...]
scanf("%d", &x);    // Source 点，输入数据被标记为污点信息，并且认为变量 x 是污染的
[...]
y = x + k;          // 如果二元操作的操作数是污染的，那么操作结果也是污染的，所以变量 y 也是污染的
[...]
x = 0;              // 如果一个被污染的变量被赋值为一个常数，那么认为它是未污染的，所以 x 转变成未污染的
[...]
while (i < y)       // Sink 点，如果规定循环的次数不能受程序输入的影响，那么需要检查 y 是否被污染

隐式信息流：通过控制依赖传播的信息流

if (x > 0)			// 变量 y 的取值依赖于变量 x 的取值，如果变量 x 是污染的，那么变量 y 也应该是污染的。
    y = 1;
else
    y = 0;

静态污点分析

静态污点分析系统首先对程序代码进行解析，获得程序代码的中间表示，然后在中间表示的基础上对程序代码进行控制流分析等辅助分析，以获得需要的控制流图、调用图等。在辅助分析的过程中，系统可以利用污点分析规则在中间表示上识别程序中的 Source 点和 Sink 点。最后检测系统根据污点分析规则，利用静态污点分析检查程序是否存在污点类型的漏洞。

基于数据流的污点分析。在不考虑隐式信息流的情况下，可以将污点分析看做针对污点数据的数据流分析。根据污点传播规则跟踪污点信息或者标记路径上的变量污染情况，进而检查污点信息是否影响敏感操作。

基于依赖关系的污点分析。考虑隐式信息流，在分析过程中，根据程序中的语句或者指令之间的依赖关系，检查 Sink 点处敏感操作是否依赖于 Source 点处接收污点信息的操作。

动态污点分析

动态污点分析是在程序运行的基础上，对数据流或控制流进行监控，从而实现对数据在内存中的显式传播、数据误用等进行跟踪和检测。动态污点分析与静态污点分析的唯一区别在于静态污点分析技术在检测时并不真正运行程序，而是通过模拟程序的执行过程来传播污点标记，而动态污点分析技术需要运行程序，同时实时传播并检测污点标记。识别出污点数据后，需要对污点进行标记。污点生命周期是指在该生命周期的时间范围内，污点被定义为有效。污点生命周期开始于污点创建时刻，生成污点标记，结束于污点删除时刻，清除污点标记。

angr

CLE（CLE Load Everything）：可执行文件和库的加载器

负责装载二进制对象以及它所依赖的库，将自身无法执行的操作转移给angr的其它组件，最后生成地址空间，表示该程序已加载并可以准备运行。
archinfo：描述各种架构的库
PyVEX：关于二进制代码转换VEX的python包装器

angr需要处理不同的架构，所以它选择一种中间语言来进行它的分析，angr使用Valgrind的中间语言——VEX来完成这方面的内容。VEX中间语言抽象了几种不同架构间的区别，允许在他们之上进行统一的分析。
SimuVEX：中间语言VEX执行的模拟器

它允许你控制符号执行
Claripy：抽象的约束求解包装器

专注于将变量符号化，生成约束式并求解约束式，符号执行的核心所在。
Angr：程序分析套件
以上：上层封装好的接口

angr_ctf

00_angr_find

In [1]: import angr

In [2]: p = angr.Project("./00_angr_find")		# 打开要执行的二进制文件

In [3]: init_state = p.factory.entry_state()	# 创建空白的执行上下文环境

In [4]: smg = p.factory.simulation_manager(init_state)		# 创建模拟器

In [5]: smg.explore(find=0x8048675)			# 探索到目标地址
WARNING | 2021-10-15 05:06:35,829 | angr.storage.memory_mixins.default_filler_mixin | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | 2021-10-15 05:06:35,830 | angr.storage.memory_mixins.default_filler_mixin | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | 2021-10-15 05:06:35,830 | angr.storage.memory_mixins.default_filler_mixin | 1) setting a value to the initial state
WARNING | 2021-10-15 05:06:35,830 | angr.storage.memory_mixins.default_filler_mixin | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | 2021-10-15 05:06:35,830 | angr.storage.memory_mixins.default_filler_mixin | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to suppress these messages.
WARNING | 2021-10-15 05:06:35,830 | angr.storage.memory_mixins.default_filler_mixin | Filling register edi with 4 unconstrained bytes referenced from 0x80486b1 (__libc_csu_init+0x1 in 00_angr_find (0x80486b1))
WARNING | 2021-10-15 05:06:35,832 | angr.storage.memory_mixins.default_filler_mixin | Filling register ebx with 4 unconstrained bytes referenced from 0x80486b3 (__libc_csu_init+0x3 in 00_angr_find (0x80486b3))
WARNING | 2021-10-15 05:06:38,184 | angr.storage.memory_mixins.default_filler_mixin | Filling memory at 0x7ffeff60 with 4 unconstrained bytes referenced from 0x818ac20 (strcmp+0x0 in libc.so.6 (0x8ac20))
Out[5]: <SimulationManager with 1 active, 16 deadended, 1 found>		# 找到一个结果

In [6]: found_state = smg.found[0]

In [7]: found_state.posix.dumps(0)
Out[7]: b'JXWVXRKX'

01_angr_avoid

Options -> General -> Line prefixes(graph) 调出Graph框地址

目标

同时为了节省算时，我们不想到达avoid_me处

In [2]: import angr

In [3]: p = angr.Project("./01_angr_avoid")

In [4]: init_state = p.factory.entry_state()

In [5]: smg = p.factory.simulation_manager(init_state)

In [6]: smg.explore(find=0x080485E0, avoid=0x080485A8)		# find目标地址 avoid排除地址
WARNING | 2021-10-15 07:04:50,906 | angr.storage.memory_mixins.default_filler_mixin | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | 2021-10-15 07:04:50,906 | angr.storage.memory_mixins.default_filler_mixin | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | 2021-10-15 07:04:50,906 | angr.storage.memory_mixins.default_filler_mixin | 1) setting a value to the initial state
WARNING | 2021-10-15 07:04:50,906 | angr.storage.memory_mixins.default_filler_mixin | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | 2021-10-15 07:04:50,906 | angr.storage.memory_mixins.default_filler_mixin | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to suppress these messages.
WARNING | 2021-10-15 07:04:50,906 | angr.storage.memory_mixins.default_filler_mixin | Filling register edi with 4 unconstrained bytes referenced from 0x80d4591 (__libc_csu_init+0x1 in 01_angr_avoid (0x80d4591))
WARNING | 2021-10-15 07:04:50,908 | angr.storage.memory_mixins.default_filler_mixin | Filling register ebx with 4 unconstrained bytes referenced from 0x80d4593 (__libc_csu_init+0x3 in 01_angr_avoid (0x80d4593))
WARNING | 2021-10-15 07:04:55,068 | angr.storage.memory_mixins.default_filler_mixin | Filling memory at 0x7ffeff3d with 11 unconstrained bytes referenced from 0x818b210 (strncmp+0x0 in libc.so.6 (0x8b210))
WARNING | 2021-10-15 07:04:55,068 | angr.storage.memory_mixins.default_filler_mixin | Filling memory at 0x7ffeff60 with 4 unconstrained bytes referenced from 0x818b210 (strncmp+0x0 in libc.so.6 (0x8b210))
Out[6]: <SimulationManager with 1 active, 16 deadended, 1 found, 8 avoid>

In [7]: found_state = smg.found[0]

In [8]: found_state.posix.dumps(0)
Out[8]: b'HUJOZMYS'

02_angr_find_condition

目标

import angr
import sys

def main(argv):
    p = angr.Project("./02_angr_find_condition")
    init_state = p.factory.entry_state()
    sim = p.factory.simgr(init_state)
    
    sim.explore(find=0x0804900D)
    
    if sim.found:
        found_state = sim.found[0]
        print(found_state.posix.dumps(0))
    else:
        raise Exception('Could not find the solution!')
    
if __name__ == '__main__':
    main(sys.argv)

Reference:

符号执行研究综述

angr学习(angr_ctf)

ctf all in one 5.1&5.5

p1Kk's World!

艺无止境，功不唐捐。

符号执行&污点分析简述