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 )
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
self .call( 0x4082E1 , ( 1 , 100 ), 'return_func' )
return dst_addr
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
@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
@proj .hook( 0x40860C , length = 4 )
def hook_next(state):
print ( 'hook delete[]:' , state)
@proj .hook( 0x4085BA )
def hook_test(state):
pass
init_state = proj.factory.blank_state(addr = 0x408329 )
solver = init_state.solver
str_len = 9
message = solver.BVS( 'message' , (str_len + 1 ) * 8 )
message_len = solver.BVV(str_len, 32 )
digest = solver.BVS( 'digest' , 8 * 20 )
message_addr = solver.BVS( "message_addr" , 32 )
digest_addr = solver.BVS( "digest_addr" , 32 )
init_state.memory.store(message_addr, message)
init_state.memory.store(message_addr + 9 , '\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()
if simgr.found:
s = simgr.found[ 0 ]
print ( 'found state:' , s)
print ( 'digest_addr: {}, {}' . format (s.regs.r1, digest_addr))
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符号执行的标准应用应该是:给定一个结果输出集,求到达该结果的输入集(起始点从哪条路径到达结果);通常都是将输入参数都用符号表示。
目前就先到这里,下次有感兴趣的东西再写文章研究下,有任何问题欢迎评论区讨论。
[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入!