引用angr开发者的话
angr 是一个python编写的二进制分析框架,它结合了静态与动态符号分析,适用于各种任务。
它功能很多,但是学习曲线陡峭,并不是因为其功能繁杂,而是因为缺少学习资料与路径。事实上,有很多ctf writeup之类的东西写道它,但是从学习者的角度太看,这些远远不够。
回到angr,乍一看它真正吸引人的地方是它的符号执行引擎。简言之,符号执行意味着在不实际执行程序的情况下,就可以分析哪些输入经历了哪些代码路径。最常见的例子就是一个程序根据输入的一个字符串跟自身生成的字符串作比较来打印一些东西。符号执行允许我们像对待方程一样分析一个程序,解这个方程然后告诉我们正确的输入。
在angr_ctf repo 里面有写slides,因此我把学术这部分留给您。通过这些你需要知道它被称为符号执行的原因:因为程序的某些部分(本例中为输入)不是具体的值,而是符号,就像方程中的 x ,我们称它为路径约束符号
int x; scanf("%d", &x); if ((x > 1) && (x < 10)) { puts("Success!!"); } else { puts("Fail."); }
在这个代码里面, if 状态约束了变量 x 的值。假设我们对打印 Success 的代码路径感兴趣,我们知道 x 必须大于1小于10,这是成功执行该路径的约束。符号执行引擎注入一个符号 (λ), 然后向后遍历执行以找到一个合适约束的 λ 值。
这里我们真正想表达的是:除非特别要求,符号执行引擎并不会真正执行程序。还有很重要的一点,符号执行会评估代码中所有分支,这就意味着当我们分析一个有很多的分支的庞大程序时会发生“路径爆炸”。某些情况下,分析的总时间会很长。发生这种情况是因为每个分支都会使符号执行引擎必须分析的状态数量加倍。
下面根据题目进行介绍
克隆 angr_ctf 的仓库,打开 dist文件夹,里面18个题目与scafflodXX.py文件,这些py文件时包含了解决这些问题的基本框架。我们第一个挑战是 00_angr_find 这是一个非常简单的二进制文件,输入一个字符串,然后打印是否正确,我们对能打印 Good Job 的路径感兴趣
传统方法就是逆向分析 complex_function 函数,但这并不是个好主意。
这次我们用angr解决这个问题。
先看一下 scaffold00.py 文件
import angr import sys def main(argv): path_to_binary = ??? project = angr.Project(path_to_binary) initial_state = project.factory.entry_state() simulation = project.factory.simgr(initial_state) print_good_address = ??? simulation.explore(find=print_good_address) if simulation.found: solution_state = simulation.found[0] print solution_state.posix.dumps(sys.stdin.fileno()) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
我们逐行分析这个文件,然后编辑它以解决这个问题
前两行导入 angr 跟 sys 库,sys 库用于解析打印到标准输出的内容。
def main(argv): path_to_binary = ??? # (1) project = angr.Project(path_to_binary) # (2) initial_state = project.factory.entry_state() # (3) simulation = project.factory.simgr(initial_state) # (4)
在(1)处声明了要分析的程序的位置,之后将在(2)处创建一个 Project 对象实例。在(3)处脚本创建了一个程序入口点状态(类似于快照),最后通过传入参数 initial_state 调用 simgr 函数创建 Simulation Manager 对象。这就基本上告诉符号执行引擎同程序的入口点开始符号执行,因此我们要做的第一件事就是编辑程序的位置。
path_to_binary = "./00_angr_find" # (1)
来看下两行
print_good_address = ??? (1) simulation.explore(find=print_good_address) # (2)
这些是关键。 print_good_address 保存的是可以打印 Good Job 块的地址,我们可以通过反汇编找到这个地址。
用红色方框中的值替代 ???
。在(2)处意思是告诉引擎找一条到该地址的路径。最后几行:
if simulation.found: # (1) solution_state = simulation.found[0] # (2) print solution_state.posix.dumps(sys.stdin.fileno()) # (3) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
在(1)处会检查 found 这个list(包含了所有可以到达目标地址的状态)是否为空。在这个例子中,如果有输入出发了正确的路径,在(2)处会将状态分配给 solution_state 并在(3)打印到标准输出。剩下几行就是如果没有状态可以到达约束的地址,就会执行这里。
现在就可以执行这个脚本
完整的脚本
import angr import sys def main(argv): path_to_binary = "./00_angr_find" # path of the binary program project = angr.Project(path_to_binary) initial_state = project.factory.entry_state() simulation = project.factory.simgr(initial_state) print_good_address = 0x8048678 # :integer (probably in hexadecimal) simulation.explore(find=print_good_address) if simulation.found: solution_state = simulation.found[0] solution = solution_state.posix.dumps(sys.stdin.fileno()) print("[+] Success! Solution is: {}".format(solution.decode("utf-8"))) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
这是第一部分的内容,下一部分将会介绍如何解决路径爆炸问题,以及如何将符号缓冲区注入到程序
上一部分介绍了如何对一个简单的二进制文件进行基本的符号执行,这次我们讨论 symbolic bitvectors (符号位向量)以及如何避免不必要的状态以减少执行时间。
我们准备跳过 00_angr_avoid , 这个跟第一个很像,不过你还要指定avoid 分支: explore()方法允许用不想分析的代码地址作为avoid参数。
这个题目教给我们如何让angr根据程序的输出判断avoid或者keep哪些状态。反汇编这个题目就会发现有大量的代码块输出 Good Job or Try again.
,因此,要想记录下这些代码的地址会非常麻烦。幸运的是我们可以告诉angr 根据打印到标准输出的内容保持或丢弃某些状态。首先打开 scaffold02.py 文件。
import angr import sys def main(argv): path_to_binary = argv[1] project = angr.Project(path_to_binary) initial_state = project.factory.entry_state() simulation = project.factory.simgr(initial_state) # Define a function that checks if you have found the state you are looking # for. def is_successful(state): # Dump whatever has been printed out by the binary so far into a string. stdout_output = state.posix.dumps(sys.stdout.fileno()) # Return whether 'Good Job.' has been printed yet. # (!) return ??? # :boolean # Same as above, but this time check if the state should abort. If you return # False, Angr will continue to step the state. In this specific challenge, the # only time at which you will know you should abort is when the program prints # "Try again." def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) return ??? # :boolean # Tell Angr to explore the binary and find any state that is_successful identfies # as a successful state by returning True. simulation.explore(find=is_successful, avoid=should_abort) if simulation.found: solution_state = simulation.found[0] print solution_state.posix.dumps(sys.stdin.fileno()) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
首先编辑程序路径
path_to_binary = "./02_angr_find_condition"
现在看一下 is_successful() 函数,这个函数应该是判断当前状态能否使程序输出 Good Job,然后返回 True or False,
def is_successful(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) # (1) if b'Good Job.' in stdout_output: # (2) return True # (3) else: return False
在(1)我们把标准输出赋值给 stdout_output ,注意:那不是字符串而是一个bytes 对象,意味着在(2)我们需要使用 b'Good Job.' 替代 Good Job. 检查是否输出了字符串 Good Job. 。在(3)根据是否得到目标字符串返回 ture 或者 false。用同样的方法判断输出是否为 Try Again 。
def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Try again.' in stdout_output: return True else: return False
定义好这两个函数以后,告诉angr我们感兴趣的代码路径以及要避免的代码路径。
simulation.explore(find=is_successful, avoid=should_abort)
find 跟 avoid 参数可以是一个你已经确定感兴趣或要避免的地址(或者是地址列表)或者是一个可以动态选择“是否感兴趣”的函数。在这个例子里,因为有太多的状态可以打印我们感兴趣的字符串,所以我们采用两个函数。
之后就是检查结果是不是我们想要的。
if simulation.found: solution_state = simulation.found[0] solution = solution_state.posix.dumps(sys.stdin.fileno()) print("[+] Success! Solution is: {}".format(solution.decode("utf-8"))) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
代码有点像 scaffold00.py 里的代码,它会检查是否有状态能打印 Good Job ,并打印一个可以到达约束路径的输入(可能会有很多,但是我们选择第一个)。下面是完整的脚本:
import angr import sys def main(argv): path_to_binary = "./02_angr_find_condition" project = angr.Project(path_to_binary) initial_state = project.factory.entry_state() simulation = project.factory.simgr(initial_state) def is_successful(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Good Job.' in stdout_output: return True else: return False def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Try again.' in stdout_output: return True else: return False simulation.explore(find=is_successful, avoid=should_abort) if simulation.found: solution_state = simulation.found[0] solution = solution_state.posix.dumps(sys.stdin.fileno()) print("[+] Success! Solution is: {}".format(solution.decode("utf-8"))) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
如果我们不确定avoid参数,只用find参数执行会发生什么?在这个挑战里一点也不要紧,因为这个程序很小,没有太多的分支。如果是更复杂的程序呢?然我们看下一个挑战。
现在我们开始真正的接触angr了。但是首先我要告诉你一件事情:当调用 scanf()的时候,angr无法处理复杂的格式。因此我们通过这个学习如何将符号值注入寄存器。
首先,我们先看一下 main 函数。
有一个 get_user_input函数,还有三个 complex_function_1, complex_function_2, complex_function_3 函数用于操纵 get_user_input函数的输出。我们看一下 get_user_input 的内容,看看它是如何解析输入的。
angr最大的敌人就是复杂格式的字符串,在调用 scanf 之前就可以看到程序将 "%x %x %x" 地址压栈,意味着程序以3个16进制数作为输入。
通过红框内可知,三个16进制数被放进了三个寄存器 :eax
,ebx
,edx
。最好注意一下。现在我们已经掌握了程序如何解析输入的内容,现在看一下 scaffold03.py 脚本。
import angr import claripy import sys def main(argv): path_to_binary = argv[1] project = angr.Project(path_to_binary) # Sometimes, you want to specify where the program should start. The variable # start_address will specify where the symbolic execution engine should begin. # Note that we are using blank_state, not entry_state. # (!) start_address = ??? # :integer (probably hexadecimal) initial_state = project.factory.blank_state(addr=start_address) # Create a symbolic bitvector (the datatype Angr uses to inject symbolic # values into the binary.) The first parameter is just a name Angr uses # to reference it. # You will have to construct multiple bitvectors. Copy the two lines below # and change the variable names. To figure out how many (and of what size) # you need, dissassemble the binary and determine the format parameter passed # to scanf. # (!) password0_size_in_bits = ??? # :integer password0 = claripy.BVS('password0', password0_size_in_bits) ... # Set a register to a symbolic value. This is one way to inject symbols into # the program. # initial_state.regs stores a number of convenient attributes that reference # registers by name. For example, to set eax to password0, use: # # initial_state.regs.eax = password0 # # You will have to set multiple registers to distinct bitvectors. Copy and # paste the line below and change the register. To determine which registers # to inject which symbol, dissassemble the binary and look at the instructions # immediately following the call to scanf. # (!) initial_state.regs.??? = password0 ... simulation = project.factory.simgr(initial_state) def is_successful(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) return ??? def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) return ??? simulation.explore(find=is_successful, avoid=should_abort) if simulation.found: solution_state = simulation.found[0] # Solve for the symbolic values. If there are multiple solutions, we only # care about one, so we can use eval, which returns any (but only one) # solution. Pass eval the bitvector you want to solve for. # (!) solution0 = solution_state.se.eval(password0) ... # Aggregate and format the solutions you computed above, and then print # the full string. Pay attention to the order of the integers, and the # expected base (decimal, octal, hexadecimal, etc). solution = ??? # :string print solution else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
首先,我们先补全程序路径,然后告诉angr我们不想从程序开头开始执行,因为我们要跳过 scanf 函数。所以开始地址只能是 call scanf 之后的指令地址,意味着我们可能需要从 ADD ESP , 0X10 开始执行,因为这条指令清理了 scanf 函数接收的数据,但是我们并没有调用该函数。。。
这就意味着我们需要跳过这条指令,设置 start_address 为 MOV ECX, DWORD [EBP - 0x18] 指令的地址 0x08048937 。
但是还有一个问题:如果从 0x08048937 开始执行的话程序无法正常工作,因为没有开辟栈空间,要这样做的话,首先需要开辟栈空间,但是作者没有这么做。为了使程序工作,我决定从 call get_user_input 的下一条指令开始分析(也就是 MOV DWORD [EBP - 0x14], EAX @0x8048980 ),这不会改变任何东西,因为我们只是跳过该功能并直接设置寄存器的值。
start_address = 0x8048980 initial_state = project.factory.blank_state(addr=start_address)
注意,我们这次使用 blank_state() 方法替代了 entry_state() 。通过把 addr=start_address 传递给 blank_state() ,实际上是告诉angr在这个特定的地址创建一个新状态。
还记得 get_user_input 解析我们的输入,并把三个值分别赋给三个寄存器吗?现在开始制作输入,以便程序能到达我们要去的地方。为此我们需要创建三个符号位向量,如注释中所述,符号位向量是angr用于将符号值注入程序的数据类型。这些位向量作为angr求解的方程的 x 。我们用 claripy 通过 BVS() 方法生成三个位向量。这个方法需要两个参数:第一个参数表示符号名,第二个参数表示这个符号的长度 单位bit。因为符号值都保存在寄存器里,并且寄存器都是32位的,所以位向量的大小也需要是32位的。
password_size_in_bits = 32 password0 = claripy.BVS('password0', password_size_in_bits) password1 = claripy.BVS('password1', password_size_in_bits) password2 = claripy.BVS('password2', password_size_in_bits)
现在我们已经创建了三个符号位向量,现在就把他们赋值给 eax
,ebx
,edx
。我准备修改先前创建的状态 initial_state,并更新寄存器的内容,幸运的是,angr提供了一个非常智能的方法:
initial_state.regs.eax = password0 initial_state.regs.ebx = password1 initial_state.regs.edx = password2
现在我们准备跟以前一样定义 find
, avoid
状态。
simulation = project.factory.simgr(initial_state) def is_successful(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Good Job.\n' in stdout_output: return True else: return False def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Try again.\n' in stdout_output: return True else: return False simulation.explore(find=is_successful, avoid=should_abort)
所有事情都准备好了,下面就是打印解了。
if simulation.found: solution_state = simulation.found[0] # Solve for the symbolic values. If there are multiple solutions, we only # care about one, so we can use eval, which returns any (but only one) # solution. Pass eval the bitvector you want to solve for. # (!) NOTE: state.se is deprecated, use state.solver (it's exactly the same). solution0 = format(solution_state.solver.eval(password0), 'x') # (1) solution1 = format(solution_state.solver.eval(password1), 'x') solution2 = format(solution_state.solver.eval(password2), 'x') # Aggregate and format the solutions you computed above, and then print # the full string. Pay attention to the order of the integers, and the # expected base (decimal, octal, hexadecimal, etc). solution = solution0 + " " + solution1 + " " + solution2 # (2) print("[+] Success! Solution is: {}".format(solution)) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
需要解释一下:
下面是完整的方法:
import angr import claripy import sys def main(argv): path_to_binary = "./03_angr_symbolic_registers" project = angr.Project(path_to_binary) start_address = 0x08048980 # address right after the get_input function call initial_state = project.factory.blank_state(addr=start_address) password_size_in_bits = 32 password0 = claripy.BVS('password0', password_size_in_bits) password1 = claripy.BVS('password1', password_size_in_bits) password2 = claripy.BVS('password2', password_size_in_bits) initial_state.regs.eax = password0 initial_state.regs.ebx = password1 initial_state.regs.edx = password2 simulation = project.factory.simgr(initial_state) def is_successful(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Good Job.\n' in stdout_output: return True else: return False def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Try again.\n' in stdout_output: return True else: return False simulation.explore(find=is_successful, avoid=should_abort) if simulation.found: solution_state = simulation.found[0] solution0 = format(solution_state.solver.eval(password0), 'x') solution1 = format(solution_state.solver.eval(password1), 'x') solution2 = format(solution_state.solver.eval(password2), 'x') solution = solution0 + " " + solution1 + " " + solution2 # :string print("[+] Success! Solution is: {}".format(solution)) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
下一节,我们将会学习如何构造栈帧,并在函数内直接跳转。
上面我们学习了如何使用angr将符号位向量注入到寄存器中以及如何避免不必要的代码路径,但是我们跳过了如何在函数内直接执行,现在不得不从头为函数构造栈帧,下面将会讲如何做到这一点。
首先看一下这个挑战
看一下 handle_user 函数,
在调用 scanf 把格式化字符串压入栈之前,先会把两个局部变量地址入栈:[EBP - 0x10], [EBP - 0xC]。
与上个挑战不同的是,这次的变量保存在栈上,而不是寄存器,这就意味着我们必须用一些栈技巧,在程序不崩溃的情况下推送符号缓冲区。回顾一下我们现在所知道的:
[EBP - 0x10]
和[EBP - 0xC]
现在我们对程序做了什么有了一定了解,现在看一下 scaffold04.py 文件。
import angr import claripy import sys def main(argv): path_to_binary = argv[1] project = angr.Project(path_to_binary) start_address = ??? initial_state = project.factory.blank_state(addr=start_address) initial_state.regs.ebp = initial_state.regs.esp password0 = claripy.BVS('password0', ???) ... padding_length_in_bytes = ??? # :integer initial_state.regs.esp -= padding_length_in_bytes initial_state.stack_push(???) # :bitvector (claripy.BVS, claripy.BVV, claripy.BV) ... simulation = project.factory.simgr(initial_state) def is_successful(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) return ??? def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) return ??? simulation.explore(find=is_successful, avoid=should_abort) if simulation.found: solution_state = simulation.found[0] solution0 = solution_state.se.eval(password0) ... solution = ??? print solution else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
我们首先应当先想好一个策略而不是立即就对这个脚本进行修改。我们需要确定angr应当从哪里开始。因为我们需要跳过 scanf 函数,因此我们可能需要从 0x8048697 地址开始。所以直接跳过指令 ADD ESP, 0x10 ,
因为它的作用是在 scanf 函数返回以后清理栈空间,但是我们没有调用它,因此不需要清理任何东西。
现在我们需要了解,我们跳过的那些指令是如何调整栈空间的,我们要注入的符号位向量的确切的位置。从前面的分析可知,我们要注入的位置是 [EBP - 0x10]
, [EBP - 0xC]
,因此在压栈前我们我要填充栈,但是我们首先应当告诉 ebp 它应该是指向内存的什么位置。因此我们要用angr处理函数开头(我们跳过的部分): MOV EBP, ESP 。之后我们需要减小帧指针的值(译者注:这里应该是模拟 sub esp, XXX
)并压入我们的值。但是我们需要填充多少字节?
我们知道,两只值中地址最小的是 [EBP - 0xC],因为它是四字节的值,所以它将会占据一下内存:| 0xC | 0xB | 0xA | 0x9 |
,一共两个值意味着我们需要在压入它们之前填充8个字节。之后向栈上压入我们的值,现在看一下如何修改脚本
def main(argv): path_to_binary = "04_angr_symbolic_stack" project = angr.Project(path_to_binary) start_address = 0x8048697 initial_state = project.factory.blank_state(addr=start_address)
修改程序位置,并将 start_address 的值修改为前面分析的地址。现在开始构造栈,首先用下面的方法执行 MOV EBP, ESP 指令
initial_state.regs.ebp = initial_state.regs.esp
然后就是栈指针地址减8以提供填充空间。因为程序需要两个接收两个无符号整数,所以符号位向量的大小就应该是32bit。
password0 = claripy.BVS('password0', 32) password1 = claripy.BVS('password1', 32) initial_state.stack_push(password0) initial_state.stack_push(password1)
之后与前面的脚本基本相同,只要求解符号位向量并打印他们。
if simulation.found: solution_state = simulation.found[0] solution0 = (solution_state.solver.eval(password0)) solution1 = (solution_state.solver.eval(password1)) print("[+] Success! Solution is: {0} {1}".format(solution0, solution1)) else: raise Exception('Could not find the solution')
下面是完整的脚本:
import angr import claripy import sys def main(argv): path_to_binary = "04_angr_symbolic_stack" project = angr.Project(path_to_binary) start_address = 0x8048697 initial_state = project.factory.blank_state(addr=start_address) initial_state.regs.ebp = initial_state.regs.esp password0 = claripy.BVS('password0', 32) password1 = claripy.BVS('password1', 32) padding_length_in_bytes = 0x08 initial_state.regs.esp -= padding_length_in_bytes initial_state.stack_push(password0) initial_state.stack_push(password1) simulation = project.factory.simgr(initial_state) def is_successful(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) #print(stdout_output) if b'Good Job.\n' in stdout_output: return True else: return False def should_abort(state): stdout_output = state.posix.dumps(sys.stdout.fileno()) if b'Try again.\n' in stdout_output: return True else: return False simulation.explore(find=is_successful, avoid=should_abort) if simulation.found: solution_state = simulation.found[0] solution0 = (solution_state.solver.eval(password0)) solution1 = (solution_state.solver.eval(password1)) print( solution0, solution1) else: raise Exception('Could not find the solution') if __name__ == '__main__': main(sys.argv)
angr_ctf : https://github.com/jakespringer/angr_ctf
原文地址:
https://blog.notso.pro/2019-03-20-angr-introduction-part0/
https://blog.notso.pro/2019-03-25-angr-introduction-part1/
https://blog.notso.pro/2019-03-26-angr-introduction-part2/