首页
社区
课程
招聘
[原创]angr符号执行和逆向分析的思考:angr的实际应用在哪里?
发表于: 2024-4-28 08:43 3180

[原创]angr符号执行和逆向分析的思考:angr的实际应用在哪里?

2024-4-28 08:43
3180

angr有什么用?

这是我对angr的最大疑问,即使看angr CTF挑战题我也很难看出什么特别的作用,尽管第一次运行类似的示例会觉得特别神奇。如果仅用于解决这种CTF题开发这么复杂的符号执行引擎未免有点太费脑子了,因为这些例子比较特殊,个人看来这不需要angr也能快速解决。另外,angr遇到每个分支都会产生新的后继状态,即使是简单的for循环,它也会在for循环的判断中不断产生新的状态,就等同trace代码一样每执行一次都会记录一次,而且有时也不好处理,这样就会造成状态爆炸,这么看来,如果一个函数非常复杂,而我们想要angr模拟整个函数,处理起来还是挺头痛的。
angr使用Claripy进行约束求解,但是有时也会遇到:“claripy.errors.UnsatError: unsat”,非常头痛。总体感觉各方面都不完美,各种问题,各种限制,打破了我对angr的完美想象。不过想想,也没什么是完美的,也有可能是我对angr还不够了解,毕竟angr还是很复杂的。angr是一个很漂亮的工具,写这篇文章是想重新思考一下,在有限的范围内分析一下angr的实际应用,看看它如何有助于逆向分析。

angr的基本示例

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
import angr
import claripy
 
proj = angr.Project('./assets/libangr.so', load_options={'auto_load_libs': False})
m = proj.loader.main_object
func1_addr = m.get_symbol('_Z5func1ii').rebased_addr
 
state = proj.factory.blank_state(addr=func1_addr)
solver = state.solver
x = solver.BVS('x', 32)
y = solver.BVS('y', 32)
 
simgr = proj.factory.simgr(state)
simgr.explore(find=0x408301)
 
if simgr.found:
    s = simgr.found[0]
    print(s.solver.eval(s.regs.r0))

这是angr的一般使用代码,首先加载二进制文件,接着创建一个初始状态,创建模拟管理器(SimulationManager),然后调用explore探索路径,最后获取求解目标值。
首先得吐槽一下angr的api设计,个人的编程习惯偏向Java和C/C++,感觉使用把大部分东西放在Project里面就很有歧义,各种东西混杂在Project就挺乱的,官方文档说是这样方便。另外angr经过几次更新,代码接口风格变化也是很大。
上面这个例子不同于一般的CTF题例子,我看很多angr CTF例子都有使用到标准输入输出(state.posix.dumps(0|1)),感觉这样的例子不好,因为一般分析的二进制文件标准输入输出可是几乎不会存在。
虽然以上的代码很短,但是还是涉及的概念挺复杂的,那么应该从何谈起呢?

加载二进制文件


当然首先就是要解析二进制文件了,二进制分析中,最常见的就是PE文件和ELF文件,angr使用PyELFTools解析ELF文件,而类似pyelftools的工具在angr中称为后端,CLE加载器会根据文件类型自动选择恰当的后端。所以,原理上你是可以使用angr来操作原始二进制文件的,当然了单独使用pyelftools不就好了。
对于加载文件要注意的一个地方是依赖库的加载,一般情况下建议不要加载依赖库(使用auto_load_libs设置),因为它会造成符号执行非常慢,对于那些依赖其他库的变量或函数,angr提供方法解决:你手动提供实现替换一下就行了。对于变量,可以通过继承SimData实现,对于函数可以通过继承SimProcedure,需要hook的话也是使用SimProcedure。
对于加载文件,没有更多需要说的,如果要理解更清晰,需要懂得ELF文件结构、PE文件结构、重定位和内存映射等。

angr的基本数据:一切都是AST

angr中最基本的数据应视为AST(抽象语法树),或可一般称为:符号(类似代数式),例如:
x = claripy.BVS('x', 32)
y = claripy.FPV(3.14, claripy.FSORT_FLOAT)
x和y变量都是一个符号,如果x有一个具体值,有时又称为位向量:具有一定长度的二进制位。有点乱,那么统称为AST,就是代数式那样的东西。
angr的符号数据是由Claripy支持的,符号的相关操作都可以在其api文档中找到:https://api.angr.io/projects/claripy/en/latest/api.html。
接触汇编分析都知道,计算机只会处理数字,不管是什么东西,它终究是数字,只是这个数字可能是整数也可能是浮点数,一个数可能是一个地址也可能是实际数据。所以AST符号是能够满足表示计算机的一般数据的,如BV是针对整数的,FP是针对浮点数的。
给定一个函数F,参数集为X,表达式为g(x),在数学可表示为F(X)=g(x)。由于angr提供了使用符号表示数据,那么一个程序的函数执行也可以这样表示,只是没有数学中的那样直观。
例如一个计算从a到b的和的函数可能表示为f(a)=c+k*a,当然,这不是乱举例的,是真的可以这样表示。
那么寄存器、内存和文件呢?寄存器中的数据是符号,内存中的数据是符号,文件数据也是符号——全是代数式(angr的CTF例子中有这三种数据的模拟操作)。如此一来,那我们是不是可以通过符号模拟执行一个md5函数就可以拿到它的符号表达式了?原理上是的,但是实际上会有各种问题,其中一个问题就是太复杂的函数执行起来效率非常低,更多的问题下面也会谈到一些。

angr被分析对象的数据结构:SimState、Block

angr最常用的是针对SimState进行分析,但是不止状态,还有Block,Block称为基本代码块或基本块。其中SimState表示程序某一时刻的所有瞬时状态数据,包括寄存器、内存和文件系统数据,而Block表示一个没有分支跳转的代码块,angr不少地方的处理都是以基本块为单元进行处理的,例如step(),每执行一次step()执行完一个基本块中的所有指令,此时你去获取active中的状态的地址会发现等于基本块的起始地址。
所有的基本块组成一个图(Graph),所以程序的指令是图进行组织的,准确来说是一个有向图,也就是程序控制流程图。所有的SimState构成也可以看成一个图,当前的状态也可以通过history进行回溯,只是一个SimState还有各种插件,其中history也被视为插件。

状态模拟管理器(SimulationMnager)

其中最主要的方法是step、run和explore,这三个方法都是模拟器执行,step默认每次单步执行一个基本块;run和explore执行到指定位置或直至结束。
另外,step和run默认是按照BFS广度优先进行执行的:先处理完下一层的所有分支,再进行深入执行。而explore是按照DFS深度优先执行的:从起始地址一直执行到结束,然后再更换分支。对于explore,如果找到目标状态,会把目标状态添加到found中,这样你就可以从found状态列表中获取状态进一步处理。
另外要说的一个是状态集合(stash),官方文档是称为stash,实际上是一个集合或列表,是对状态的分类集:不同类型的状态放到不同的集合中。对于即将要解析执行的状态会被放到active中,一般来说active每个状态的地址就等于基本块的起始地址,当active列表为空时,就表示模拟执行已经全部处理完成。至于其它类型的状态集可以参考官方文档看看。

angr符号求解:Claripy约束求解器

一般的符号求解代码如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
import claripy
 
x = claripy.BVS('x', 32# 定义AST
y = claripy.BVS('y', 32)
exp = x * y + x / y + 100  # 符号表达式
solver = claripy.Solver()  # 获取求解器
solver.add(exp == 300# 添加表达式符号约束
print(solver.eval(x * y, 2))  # 求解
print(solver.eval(x / y, 2))
 
a = claripy.FPV(3.14, claripy.FSORT_DOUBLE)
b = claripy.FPS('b', claripy.FSORT_DOUBLE)
print(a - b)
solver.add(a + 0.1 <= b)
print(solver.eval(b, 1)[0])

其中solver.add是添加符号约束,参数通常是符号比较表达式。solver.eval是求解函数,用于求解一个表达式或符号的可能值,第二个参数是解的个数,返回值可能包含多个解。
这里不深入求解器的原理,对于使用来说,符号求解其实就等于解方程,只是有可能无解就是。
以上基本介绍了angr的基本内容,其它还有两个重点是:探索技术(angr.exploration_techniques)和分析技术(project.analyses),前者是针对模拟执行过程的处理,后者是一些专门分析的技术,分析技术中,其中有控制流程图、值流程图、数据依赖图、后向切片等,以后有机会再讨论,现在我们先针对angr的符号执行。
下面我们开始尝试使用angr的符号执行进行更自由的使用,首先来看一个最简单的例子:

计算整数列和

对于这个例子,我一开始学angr就写了这个例子,因为很简单,CTF那种例子实在太特殊、太有限制了,我想试图尝试更自由的使用。但是执行完似乎不像预期想的那样,遇到各种问题,一度让我怀疑angr是不是就只会处理非常简单的问题。
首先,数列和的数学表示为:s = a + (a+1) + (a+2) + … + (b-1),其中a<b-1。
现在我们来看一般的情形:

1
2
3
4
5
6
7
8
extern int func1(int a, int b) {
    if (a >= b) return 0;
    int s = 0;
    for(int i = a;i < b;i++) {
        s += i;
    }
    return s;
}

这个函数用于计算从a到b的数列和,我们的目标是获取函数的符号表达式,也就是将函数使用接近数学表达式的方式表示,这也是我写这篇文章的原因。我想看看是否可以做到针对普遍的函数,是否能够将一个程序函数计算为一个符号表达式。
如果函数是用于计算两个整数的和,很显然是可以做到的。但是如果函数的实现更复杂,是否还能够实现呢?例如上面这个函数,或者是hex、md5等其它加密解密函数呢?
将以上函数复制到JNI代码中,编译程序libangr.so库,然后编写angr代码分析该文件,代码如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
import angr
import claripy
 
proj = angr.Project('./assets/libangr.so', load_options={'auto_load_libs': False})
m = proj.loader.main_object
func1_addr = m.get_symbol('_Z5func1ii').rebased_addr
 
init_state = proj.factory.blank_state(addr=func1_addr)
solver = init_state.solver
x = solver.BVS('x', 32)
y = solver.BVS('y', 32)
init_state.regs.r0 = x
init_state.regs.r1 = y
print('x:', x)
print('y:', y)
 
simgr = proj.factory.simgr(init_state)
 
simgr.explore(find=0x408301, num_find=1)
s = simgr.found[0]
print('result:', s.solver.eval(s.regs.r0))

其中,对于函数的输入我们使用符号表示,符号需要使用BVS,而浮点符号使用FPS。然后将两个参数赋值给r0和r1寄存器作为函数的传入参数。find=0x408301是函数执行结束的地方,到找到到达该地址的状态后,explore停止执行,s.regs.r0是从该位置的状态中读取r0函数返回值。
函数的执行输出如下:

1
2
3
x: <BV32 x_0_32>
y: <BV32 y_1_32>
result: 0

这可不是我需要的结果!
先去看看函数的汇编指令:

1
2
3
.text:000082C6                 CMP             R0, R1
.text:000082C8                 BLT             loc_82D2
.text:000082CA                 B               loc_82CC

其中loc_82CC是a>=b时直接返回0的跳转,而explore是按照DFS执行的,所以我想这是因为angr找到第一个符合条件的状态就返回了,而第一个符合条件的则是a>=b的情况,下面我们来验证一下,看看是不是这样。

1
2
for addr in s.history.bbl_addrs:
    print('-', hex(addr))

增加以上代码输出如下:

1
2
3
4
- 0x4082bd
- 0x4082cb
- 0x4082cd
- 0x4082ff

其中第一个地址是函数的起始基本块的起始地址,也就是函数开始执行的地址,最后一个地址是函数结束基本块的地址。
果然是这样,explore只要找到第一个符合条件的就会停止执行,这是很自然的,只是这不是我们想要的,我们想要的是计算整数数列和的符号表达式。
接着,我们可以在avoid参数中添加这条路径的地址,过滤掉这条路径,代码如下:

1
2
3
4
5
6
simgr.explore(find=0x408301, avoid=0x4082cb, num_find=1)
s = simgr.found[0]
print('r0:', s.regs.r0)
print('result:', s.solver.eval(s.regs.r0))
for addr in s.history.bbl_addrs:
    print('-', hex(addr))

其中num_find表示探索解的个数,针对我们的目标,只需要一个就够了,另外这里求解r0是不准确的,如果r0是一个符号,显然求解的值会不确定,所以目前我们先不用关注它的值,只需要关注它的符号表示,以上代码执行输出如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
x: <BV32 x_0_32>
y: <BV32 y_1_32>
r0: <BV32 x_0_32>
result: 0
- 0x4082bd
- 0x4082d3
- 0x4082dd
- 0x4082e5
- 0x4082e7
- 0x4082f1
- 0x4082dd
- 0x4082f9
- 0x4082ff

你可以看到,r0等于x,这说明仅执行一次循环就退出了,因为for循环中也有一个条件判断i<b,以上执行走了i>=b的路径。
当angr执行到一个条件判断的时候,如果进行判断的变量是一个符号,这里的i初始值等于x,所以是一个符号;angr会同时执行两个分支:i>=b和i<b,同时生成两个分支的后继状态继续执行。由于我们需要跳出循环,所以并不能简单地去除跳出循环的分支简单地过滤掉这个地址。
接着该如何解决?a到b的数列和,a<b,原理上explore会执行完所有路径,针对当前分析的函数的情况,如果num_find=1, r0=x,循环执行一次;当num_find=2时,r0=2x+1,循环执行两次,以此类推。但是由于b是一个符号,除了a<b,还可以约束a>0,b>0,即使如此,b的取值范围原则上可以最大到无穷大。而就目前的情形,数列的项数刚好就等于num_find。感觉有些不完美,因为这个意味着我们需要手动指定一个实际的项数值,由此也可以看出程序和数学符号的区别,程序计算比数学符号更具体,而局限性更大,数学符号更抽象,涵括的范围更大。例如任意整数数列可以表示为无限形式s+(s+1)+(s+2)+…+(s+n),而程序表示更多情况只能表示无限数列的其中一段。这也启发我们使用angr的时候,要注意是否会遇到无限循环,如果遇到就需要将其限制为有限循环。
这里我取项数n=99,此时代码执行的输出为:

1
2
3
x: <BV32 x_0_32>
y: <BV32 y_1_32>
r0: <BV32 0x12f3 + 0x63 * x_0_32>

由于1到99的数列和为4950,对比r0表达式,可以算出x=1;也可以在代码中实现求解:

1
2
3
4
5
6
7
8
9
10
11
start_time = time.time()
n = 99
simgr.explore(find=0x408301, avoid=0x4082cb, num_find=n)
s = simgr.found[n - 1]
r0 = s.regs.r0
print('r0:', r0)
s.solver.add(r0 == 4950)
print('result:', s.solver.eval(x))
end_time = time.time()
execution_time = end_time - start_time
print("time:", execution_time, "s")

就目前模拟执行这个简单的循环,计算的时间为29秒,真是灾难!因为这个例子太简单了,虽然找到了99条路径,但是指令很少,分支也很少,如果函数稍微再复杂一些,这可怎么搞。
这个例子先到止为止,其中关键点在于for循环中的条件分支,angr每次执行到该位置都会产生两个分支,这就造成路径爆炸。假设一个函数的参数为x,而x作为函数中一个for循环的上限(while循环也是一样),如果我们不去分析和处理,这意味着要不提前退出了循环,要不进入无限循环。如果我们指定x的值为具体值,那么angr就变成了仅仅使用unicorn的实际值模拟执行,而不是符号执行,针对这个问题,欢迎感兴趣的朋友在下方评论和讨论。
如下代码就是实际值的模拟执行:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
proj = angr.Project('./assets/libangr.so', load_options={'auto_load_libs': False})
m = proj.loader.main_object
func1_addr = m.get_symbol('_Z5func1ii').rebased_addr
 
init_state = proj.factory.blank_state(addr=func1_addr)
solver = init_state.solver
x = solver.BVV(1, 32)
y = solver.BVV(100, 32)
init_state.regs.r0 = x
init_state.regs.r1 = y
print('x:', x)
print('y:', y)
 
simgr = proj.factory.simgr(init_state)
 
simgr.explore(find=0x408301)
s = simgr.found[0]
r0 = s.regs.r0
print('r0:', r0)
print('result:', s.solver.eval(r0))

而此时,我们不需要去处理for循环,结果为4950,它会正确地执行,此时不是符号执行。
让我们回到面向一般汇编函数的情形,对于我们最感兴趣的情形就是:这个函数是一个关键函数,函数接受一些输入参数,提供特定的输出,这个函数可能是加密或解密函数,而我们的目标是:它的算法是怎么样的?从输入参数到结果的计算过程是怎么样的?是否可以使用符号执行,使得最终使用符号表示这个算法?

angr符号执行、算法分析和循环语句

编程语言之间的语句类型基本是等同的,针对angr符号执行,其中最特殊的就是循环语句,如果这个循环语句的上界和下界都是具体值,我们自然不需要担心,但是如果上下界至少有一个是符号或AST,这就让情况变得非常棘手了。我目前也没有想到什么解决办法,可能angr中有相关解决该问题的支持或者有其他辅助方法,知道的朋友可以回应一下。目前这里只能是被迫将循环语句的上下界指定位置具体值。
但是如何符号都被迫使用具体值,这就让使用angr失去了意义——那不如使用unicorn或基于unicorn的框架。假设我们的目标是为了获取算法,如果我们能够得到一个使用angr符号表示的算法那就算完成了目的,但是都有可能会遇到循环上下界是符号的情况,总之我们尽可能让输入参数都是符号。否则我们就需要考虑具体值执行的情况,毕竟目标是分析算法,目标并不是强制要求angr如何有神奇的功能,如果不能解决那就需要想其他方法了。
目前发现这文章的方向成了:如何使用angr获取算法的符号表达式?我还没看过类似的用法,但是符号执行的技术让我觉得或多或少应该能够实现一些目的,这也算一个关于angr应用的分析和尝试。

尝试使用angr计算SHA1算法表达式

目前使用的SH1算法函数签名是:

1
void sha1(const uint8_t *message, size_t message_len, uint8_t *digest)

其中message是一个字符串指针,第二个参数是字符串的长度,第三个是返回值,长度固定为20。
函数有点长,这里先不贴出来,有需要的朋友可以回复问一下,到时需要再贴在评论区。
在这个函数中有一个for循环的是和函数第二个参数有关的,也就是循环的上下界都是符号变量,依据上面的分析,我们最好指定一下第二个参数为具体值。

1
2
3
for (size_t i = message_len + 1; i < padded_len - 8; i++) {
    padded_message[i] = 0x00;
}

如果我们不指定,当仅探索一条目标路径的时候,它一般不执行完就跳出循环了,不过也可以再尝试下使用符号会是什么情况。
先把SHA1函数复制到JNI中,编译生成libangr2.so,然后开始编写angr分析代码。程序首先遇到的第一个问题就是函数中使用到了memcpy函数,这个函数来自其他库,对于这种问题,我们可以使用angr hook解决。

angr hook的用法和问题

angr hook和一般类似frida hook不太一样,和hook类似的还有变量或符号替换,不过这里不展开讨论,就是上面说到的,如果这个符号依赖于其他库,就需要手动注册符号的实现。
angr hook操作实现有两种,使用上是不同的:第一种是继承SimProcedure,实现run实例方法,除了self参数,参数按顺序依次为原函数的参数,如run(self, arg1, arg2, arg3…),run的返回值就是原函数的返回值。当我们使用SimProcedure hook一个目标函数后,目标函数默认不会再被执行,可以使用project.hook或project.hook_symbol进行hook。
如果我们想在run中再次调用函数,可以使用self.call调用其它函数或自身,这就类似在frida中的Interceptor.replace调用自身。使用SimProcedure hook的示例代码如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
class AEABIMemcpy(SimProcedure):
    def run(self, dst_addr, src_addr, size):
        print('memcpy: ', dst_addr, src_addr, size)
        self.state.memory.copy_contents(dst_addr, src_addr, size)
        print('memcopy class hooked')
        self.state.regs.r0 = dst_addr
 
        # hook内部调用函数: 可用于调用其它函数或自身,类似frida中的Interceptor.replace
        # 第一个参数是目标函数地址,第二个参数目标函数的参数列表,第三个参数是当前类中的函数名称,
        # 执行完目标函数就会执行这个函数
        self.call(0x4082E1, (1, 100), 'return_func')
        return dst_addr
 
    # 函数返回值可以在该函数的self.state中获取
    # 该函数的参数必须和run的参数一样
    def return_func(self, a, b, c):
        print('end func:', self.state.regs.r0)
 
proj.hook(0x407CC4, AEABIMemcpy())

第二种是使用@project.hook(hook_addr, length=n),hook_addr是目标函数地址,默认情况下,hook函数会先执行hook_addr,然后返回到这个地址继续执行,它默认不会跳过hook_addr这个位置的指令;除非你使用length指定返回后跳过的地址字节数,例如跳过4字节,也就是跳过hook_addr这个位置的指令继续执行,示例代码如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
@proj.hook(0x4083D7, length=4)
def aeabi_memcpy(state):
    dst_addr = state.regs.r0
    src_addr = state.regs.r1
    size = state.regs.r2
    print(dst_addr, src_addr, size)
    state.memory.copy_contents(dst_addr, src_addr, size)
    print('aeabi_memcpy hooked: ', state)
    state.regs.r0 = dst_addr  # 使用r0或遵循函数返回值约定的寄存器的值作为函数返回值
    # 函数返回值是后继状态列表,用于控制执行流程
 
 
@proj.hook(0x40860C, length=4)
def hook_next(state):
    print('hook delete[]:', state)
 
 
@proj.hook(0x4082E6)
def hook_next(state):
    print('hook func1:', state.regs.r0, state.regs.r1)

而在上一节中,我们想使用angr hook来解决memcpy函数的问题,这里提供的hook示例代码也就解决了这个问题。
angr hook的作用也正如frida hook,你可以使用它完成各种事情,但angr hook其中一个针对的是解决依赖函数的问题,一般就是用上面的方式——还有一切皆符号的思想。
我们可以注意到,一般情况下最好还是要用hook处理来自其它库的函数,如果函数非常多,这将会非常麻烦,我们可以预想到如果一个目标函数非常复杂,使用angr也是感觉鞭长莫及。另外这种hook类似什么?就是一般模拟执行中的补环境。

angr模拟执行获取SHA1算法表达式

像上面说的,我们需要的是使用一个表达式表示一个算法,那么angr中使用的表达式是怎么样的?angr使用VEX IR中间语言来统一所有平台的机器指令表示,使用的相关库是PyVEX,感兴趣的可以去github看看。IR是中间表示语言,例如smali,它比机器码阅读性更强,但是不及源代码。VEX IR也是类似,它比一般的ARM/X64指令更容易阅读,自然也比不上直接阅读C/C++代码。
VEX IR其实挺好阅读的,前面说的基本块其实就是VEX IR的IR超级块(IR Super Block),你可以使用proj.factory.block获取一个基本块,或使用state.block获取当前状态指向的基本块,block.vex就是一个IRSB。
angr中的一切皆符号——而这些符号表达式就是VEX IR表达式,有时你输出一个符号的时候可能会遇到莫名其妙的表示,不要紧张,这些都是VEX IR表达式,这些符号不是随便拼凑的,有一定的语法格式,看不懂就去官方文档看就行了。
而我们模拟执行得到的表达式就是VEX IR表达式,进一步的说,它们都是AST树——都是一棵树,因为在这个例子中,我们将会遇到非常复杂的表达式,甚至python控制台长时间都无法输出,这是头痛。但是你知道表达式就是一个AST,你可以选择性的简单遍历一下AST树看看。
先看看angr模拟执行获取SHA1算法表达式的代码:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
import angr
import claripy
import time
 
proj = angr.Project('./assets/libangr2.so', load_options={'auto_load_libs': False})
 
@proj.hook(0x4083D7, length=4)
def aeabi_memcpy(state):
    dst_addr = state.regs.r0
    src_addr = state.regs.r1
    size = state.regs.r2
    print(dst_addr, src_addr, size)
    state.memory.copy_contents(dst_addr, src_addr, size)
    print('aeabi_memcpy hooked: ', state)
    state.regs.r0 = dst_addr  # 使用r0或遵循函数返回值约定的寄存器的值作为函数返回值
    # 函数返回值是后继状态列表,用于控制执行流程
 
@proj.hook(0x40860C, length=4)
def hook_next(state):
    print('hook delete[]:', state)
 
@proj.hook(0x4085BA)
def hook_test(state):
    pass
    # print('hook test:', state.regs.r0)
    # print('hook test1:', state.regs.r1 - state.regs.r2, state.memory.load(state.regs.r1 - state.regs.r2, 64))
    # print('hook test2:', state.regs.r0, state.memory.load(state.regs.r1 - 8, 1))
 
init_state = proj.factory.blank_state(addr=0x408329)
 
solver = init_state.solver
str_len = 9  # 指定具体值,因为这个值在for循环边界会用到,字符串长度为9
message = solver.BVS('message', (str_len + 1) * 8# 长度+1表示包含字符串结尾的'\0'
message_len = solver.BVV(str_len, 32)
digest = solver.BVS('digest', 8 * 20# sha1签名字节结果
message_addr = solver.BVS("message_addr", 32# 可以使用固定地址如: 0x10000000
digest_addr = solver.BVS("digest_addr", 32# 也可以使用固定地址,如0xf0000000
init_state.memory.store(message_addr, message)  # 将输入数据保存到指定地址的内存中
init_state.memory.store(message_addr + 9, '\0'# 将最后一个字节填充为'\0'
init_state.memory.store(digest_addr, digest)
init_state.regs.r0 = message_addr
init_state.regs.r1 = message_len
init_state.regs.r2 = digest_addr
print('message:', message)
print('message_len:', message_len)
print('digest:', digest)
 
simgr = proj.factory.simgr(init_state)
 
start_time = time.time() 
# 0x4086B9
# 目标函数签名为: void sha1(const uint8_t *message, size_t message_len, uint8_t *digest)
if simgr.found:
    s = simgr.found[0]
    print('found state:', s)
    print('digest_addr: {}, {}'.format(s.regs.r1, digest_addr))  # r1是digest字节数组的地址, 等于digest_addr
    # for i in range(20):
    #     print('byte:', s.memory.load(s.regs.r1 + i, 1))
    # print('digest:', s.memory.load(digest_addr, 20))  # 输出完整的表达式会等待很久
    digest_byte_array = s.memory.load(s.regs.r1, 20)
    print('digest_ast:', digest_byte_array.shallow_repr(max_depth=2))
    print('digest:', digest_byte_array.op)
 
    end_time = time.time()
    execution_time = end_time - start_time
    print("time: {}s".format(execution_time))
else:
    print('Not Found.')

其中shallow_repr方法就是用来简单看看运算结果的,因为目前没法完整输出整个表示,如果有知道的朋友可以在评论区说一下,这个我暂时还不大清楚,只是看下简单表示大概确定一下没问题就行,如果以上代码或分析有任何问题,也欢迎评论区指出。
下面是AST深度为8的算法表达式截图,既然完整的都无法一下子输出,我想这个表达式应该很大,或者应该计算一下它的复杂度。

以上截图都是VEX IR表达式,其中类似[81:81](闭区间)的表示字节范围,就是一个字节,而..表示拼接,<…>则是一种缩写,因为目前以非完全的方式输出,所以会有这种缩写,它还可以展开的。
没想到吧,这是真复杂啊!即使我得出这个表达式了,但是这表达式比我写的这篇文章还长,也不能看懂用来测试,似乎作用不大,这似乎意味着我的尝试失败了,这——么长的表达式好像对于我分析算法并没有太直接的作用对不对?而很多加密解密算法都有循环语句的,而过多的循环会导致表达式过长,或者其它原因,总之看来angr的局限性挺大的。

总结

目前看来,angr只能非常有限地使用,其中最重要的标志就是目标代码中的循环,循环决定了复杂度,一旦有循环,特别是想要符号化的变量也参与循环边界,不但难以符号化,而且也会导致表达式过于复杂。所以针对复杂循环的情况,最好可能是按代码块进行分析,就是说我把一次分析的范围缩小,例如缩小为一个for循环;而angr是可以从任意位置开始执行的,只要你能够补好模拟环境就行了。其实我还想讨论一个简单算法的例子的(主要是循环),因为某些情况还是能够很好表示一个算法的。
我认为angr的符号执行是非常好的,但是它的效率让我觉得好像单独用pyelftools、claripy、unicorn似乎也没大区别,我是希望它能够有更多的扩展应用。
angr符号执行的标准应用应该是:给定一个结果输出集,求到达该结果的输入集(起始点从哪条路径到达结果);通常都是将输入参数都用符号表示。

目前就先到这里,下次有感兴趣的东西再写文章研究下,有任何问题欢迎评论区讨论。


[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入!

收藏
免费 6
支持
分享
最新回复 (3)
雪    币: 3535
活跃值: (31011)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
2
感谢分享
2024-4-28 09:28
1
雪    币: 10
能力值: ( LV1,RANK:0 )
在线值:
发帖
回帖
粉丝
3
感谢分享
2024-4-28 09:29
0
雪    币: 1229
活跃值: (1765)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
4
tql 感谢分享
2024-4-28 19:23
0
游客
登录 | 注册 方可回帖
返回
//