Reverse - Angr angr_ctf

实验题目地址：这里
这套题目也做了两三次了，但是不经常用就老忘，这次记录一下。里面有一些是自己的粗浅理解，有不正确的地方欢迎评论。

Angr介绍

Angr是一个跨平台的二进制分析框架，中间语言使用Valgrind VEX IR。

安装直接pip install angr就行，会看到有很多依赖库，也证明angr内容的繁多。

实际上Angr是一系列功能的集合：

1. CLE实现加载二进制程序 | 加载
2. 中间语言(Vex)转换 | 跨平台
3. 基于Claripy约束求解 | 约束求解
4. Unicorn等模拟程序状态和路径 | 模拟执行
5. SimuVEX实现状态表示 | 符号化

我们最常用的就是它符号执行的部分，当然这也是基于其他功能的。

符号执行概念

符号执行发生在符号变量的抽象域中。当这些系统模拟应用程序时，它们在整个程序执行过程中跟踪寄存器和内存的状态以及对这些变量的约束。

每当到达条件分支时，执行分支并遵循两条路径，将分支条件保存为对采用分支的路径的约束，并将分支条件的逆作为对未采用分支的路径的约束。最终通过约束求解来计算符号量，实现一种自动化分析的效果。

这里尤其指动态下的执行过程，另外一种常见的动态分析手段是以Fuzzing技术为代表的具体执行。

符号执行的局限

既然这样一种自动化的手段目前还没能淘汰逆向工作者，也就证明了它具有不小的局限性。其中最突出的便是路径爆炸。

摘自Wikipedia:

大多数符号执行方法不适用于大型程序：随着程序规模的扩大，程序中有意义的路径成指数级扩大。有些程序中存在无尽循环或递归调用，这更大大增加了有意义路径，提高了符号执行难度。

因此对于符号执行，一个范围较大的循环可能就会使其失效。不过angr和其他符号执行引擎也正逐步的进行优化来缓解这一局限。

angr缓解路径爆炸的策略约有以下几种：
（1）simProcedure：重写一些可能导致状态爆炸的函数。
（2）veritesting：动态符号执行和静态符号执行的结合
（3）Lazy Solve：跳过不必要的函数
（4）Symbion：具体执行和符号执行的结合

	优化方式
auto_load_libs	Project构建时False取消加载自带库
avoid	explorer减支
SimProcedure	Hook 可能路径爆炸的函数
veritesting	设置SimManager策略
Lazy	设置state状态，自动化找洞时候用
Symbion	具体执行和符号执行相互切换

使用Angr的大概流程

使用angr解题的大概步骤

• 进行CLE加载binary获取Project，project对象实际上是一种初始化映像，当需要动态执行时，我们需要一个Simulated Project State。
  SimState内有需要的任何动态数据，包括寄存器，内存，文件系统数据等，其中数据以BV形式描述(unsigned)
• 新建符号量 : BVS (bitvector symbolic ) 或 BVV (bitvector value)
• 把符号量设置到SimState的内存或者其他地方
• 通过Project创建Simulation Managers，确定起始状态，进行路径探索
• 运行，探索满足路径需要的值
• 约束求解，获取执行结果

具体的细节可以参考Angr文档，Angr提供的操作空间还是很大的，想要好好掌握不是一件容易的事情，本篇就仅限于对这套题目的讨论上了。

angr_ctf

每道题都有对应的scaffold.py，可以往脚手架里面填充

SimulationManager.explore()

这三道题目学习给explore选择参数。

00_angr_find

输入经过一个不算complex的complex_function函数再比较

import angr
import sys

def main(argv):
  path_to_binary = r"./00_angr_find"
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.entry_state()
  simulation = project.factory.simgr(initial_state,veritesting=True)
  print_good_address = 0x08048678
  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)

• 第6行加载二进制文件为Project，auto_load_libs使用设置为 True 的话会自动载入依赖的库，然后分析到库函数调用时进入库函数，这样会增加分析的工作量，也有能会跑挂。
• 第8行将生成的入口状态作为符号执行起点创建，veritesting是启用Angr在动态符号执行和静态符号执行的优化措施

WARNING | 2022-12-08 17:34:30,264 | angr.storage.memory_mixins.default_filler_mixin | The program is accessing register with an unspecified value. This could indicate unwanted behavior.
......
WARNING | 2022-12-08 17:34:32,332 | angr.storage.memory_mixins.default_filler_mixin | Filling register gs with 4 unconstrained bytes referenced from 0x0 (not part of a loaded object)
b'JXWVXRKX'

01_angr_avoid

函数过大导致不能反编译，发现有一个avoid_me函数被多次调用，我们设置explorer的avoid参数不执行它。

import angr
import sys

def main(argv):
  path_to_binary = r"./01_angr_avoid"
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.entry_state(add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)

  print_good_address = 0x80485E0
  will_not_succeed_address = 0x080485A8
  simulation.explore(find=print_good_address, avoid=will_not_succeed_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)

如果电脑跟我一样拉可以选择安装pypy + 开启state的unicorn选项提速。b'HUJOZMYS'

02_angr_find_condition

IDA提示节点过多，简单看一看感觉是打印节点过多，通过条件而非地址来设置exlporer的参数

import angr
import sys

def main(argv):
  path_to_binary = r"./02_angr_find_condition"
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.entry_state(add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)

  simulation.explore(find=lambda state:b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state:b"Try again" in state.posix.dumps(sys.stdout.fileno()))

  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)

根据一切皆对象的思想直接将定义的函数传进去就行。b'HETOBRCU'

Symbolic

学习怎么在寄存器，栈，堆，文件等处注入符号变量。

03_angr_symbolic_registers

符号化寄存器，感觉从这道题开始才能看出来符号执行的模子，注意学习设置符号的操作。
angr还挺适合这种场景的，大量的运算，少量的循环和判断，符号执行也可以理解就是自动化的约束求解而已。

这道题解题的思路在这段汇编

.text:08048980                 mov     [ebp+var_14], eax
.text:08048983                 mov     [ebp+var_10], ebx
.text:08048986                 mov     [ebp+var_C], edx
.text:08048989                 sub     esp, 0Ch
.text:0804898C                 push    [ebp+var_14]
.text:0804898F                 call    complex_function_1
.text:08048994                 add     esp, 10h
.text:08048997                 mov     ecx, eax
.text:08048999                 mov     [ebp+var_14], ecx
.text:0804899C                 sub     esp, 0Ch
.text:0804899F                 push    [ebp+var_10]
.text:080489A2                 call    complex_function_2
.text:080489A7                 add     esp, 10h
.text:080489AA                 mov     ecx, eax
.text:080489AC                 mov     [ebp+var_10], ecx
.text:080489AF                 sub     esp, 0Ch
.text:080489B2                 push    [ebp+var_C]
.text:080489B5                 call    complex_function_3
.text:080489BA                 add     esp, 10h

这道题就不使用预定义的entry_state了，定义一个blank_state，自行设置符号量eax,ebx,edx，主要原因是当调用 scanf（）的时候，angr无法处理复杂的格式。(但是实际上Angr如今已经实现了对一些格式化输入的支持，所以直接设置entry_state来跑是没问题的.....，这里就纯粹为了学习使用blank_state）

import angr
import sys
import claripy
def main(argv):
  path_to_binary = r"./03_angr_symbolic_registers"
  angr_entry = 0x08048980
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.blank_state(addr=angr_entry,add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)
  
  arg_eax = claripy.BVS("aeax",32)
  arg_ebx = claripy.BVS("aebx",32)
  arg_edx = claripy.BVS("aedx",32)
  initial_state.regs.eax = arg_eax
  initial_state.regs.ebx = arg_ebx
  initial_state.regs.edx = arg_edx
  
  simulation.explore(find=lambda state:b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state:b"Try again" in state.posix.dumps(sys.stdout.fileno()))

  if simulation.found:
    solution_state = simulation.found[0]
    print("%X %X %X" % (solution_state.solver.eval(arg_eax),solution_state.solver.eval(arg_ebx),solution_state.solver.eval(arg_edx)))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

state.solver.eval()是位向量域下的求解，例如
state.solver.eval(state.solver.BVV(0x41424344, 32),cast_to=bytes) # 转换结果 b'ABCD'

输出：B9FFD04E CCF63FE8 8FD4D959

04_angr_symbolic_stack

和上一题类似，这道题目的符号量需要设置在栈内存中。

.text:08048682                 lea     eax, [ebp+var_10]
.text:08048685                 push    eax
.text:08048686                 lea     eax, [ebp+var_C]
.text:08048689                 push    eax
.text:0804868A                 push    offset aUU      ; "%u %u"
.text:0804868F                 call    ___isoc99_scanf
.text:08048694                 add     esp, 10h
.text:08048697                 mov     eax, [ebp+var_C]
.text:0804869A                 sub     esp, 0Ch
.text:0804869D                 push    eax
.text:0804869E                 call    complex_function0
.text:080486A3                 add     esp, 10h
.text:080486A6                 mov     [ebp+var_C], eax
.text:080486A9                 mov     eax, [ebp+var_10]
.text:080486AC                 sub     esp, 0Ch
.text:080486AF                 push    eax
.text:080486B0                 call    complex_function1
.text:080486B5                 add     esp, 10h

特别留意栈内符号的注入

import angr
import sys
def main(argv):
  path_to_binary = r"./04_angr_symbolic_stack"
  angr_entry = 0x08048697
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.blank_state(addr=angr_entry,add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)
  
  var_10 = initial_state.solver.BVS("var_10",32)
  var_C = initial_state.solver.BVS("var_C",32)
  
  initial_state.mem[initial_state.regs.ebp-0xC].uint32_t = var_C
  initial_state.mem[initial_state.regs.ebp-0x10].uint32_t = var_10
  
  simulation.explore(find=lambda state:b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state:b"Try again" in state.posix.dumps(sys.stdout.fileno()))

  if simulation.found:
    solution_state = simulation.found[0]
    print("%X %X" % (solution_state.solver.eval(var_C ),solution_state.solver.eval(var_10)))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

65954334 8DFFA41F
这里也可以模拟压栈过程来注入符号,程序使用cdecl，关键代码如下：

  var_10 = initial_state.solver.BVS("var_10",32)
  var_C = initial_state.solver.BVS("var_C",32)
  
  padding  = 8
  initial_state.regs.ebp = initial_state.regs.esp
  initial_state.regs.esp -= padding
  
  initial_state.stack_push(var_C)
  initial_state.stack_push(var_10)

05_angr_symbolic_memory

符号化bss段内存，思路上和上一道题目一样，这里用了下initial_state.memory.store。

import angr
import sys
import claripy

def main(argv):
  path_to_binary = r"./05_angr_symbolic_memory"
  angr_entry = 0x08048601
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.blank_state(addr=angr_entry,add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)
  
  user_input = claripy.BVS("user_input", 64)
  unk_A1BA1C8 = claripy.BVS("unk_A1BA1C8", 64)
  unk_A1BA1D0 = claripy.BVS("unk_A1BA1D0", 64)
  unk_A1BA1D8 = claripy.BVS("unk_A1BA1D8", 64)
 
  initial_state.memory.store(0x0A1BA1C0, user_input)
  initial_state.memory.store(0x0A1BA1C8, unk_A1BA1C8)
  initial_state.memory.store(0x0A1BA1D0, unk_A1BA1D0)
  initial_state.memory.store(0x0A1BA1D8, unk_A1BA1D8)
  
  simulation.explore(find=lambda state:b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state:b"Try again" in state.posix.dumps(sys.stdout.fileno()))

  if simulation.found:
    solution_state = simulation.found[0]
    print("%s %s %s %s" %(solution_state.solver.eval(user_input, cast_to=bytes),
                          solution_state.solver.eval(unk_A1BA1C8, cast_to=bytes),
                          solution_state.solver.eval(unk_A1BA1D0, cast_to=bytes),
                          solution_state.solver.eval(unk_A1BA1D8, cast_to=bytes)))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

输出b'NAXTHGNR' b'JVSFTPWE' b'LMGAUHWC' b'XMDCPALU

state.memory.store(0x083E0DB4, addr1)Angr在内存中存储整数使用大端序,加上参数endness=proj.arch.memory_endness可以以小端序存储。
使用initial_state.mem[0x0A1BA1C0].uint64_t = user_input直接注入进去要注意字节序的问题，转成bytes之后要[::-1]。

06_angr_symbolic_dynamic_memory

符号化堆内存，关键在于怎么获得内存地址。思路是伪造一个未被使用的内存地址，并修改数据指针指向该地址。这个就非常像游戏外挂找基地址时候的人造指针。
我们让buffer0和buffer1指向我们确定的地址，一般直接在BSS段里面找就行。

import angr
import sys
import claripy

def main(argv):
  path_to_binary = r"./06_angr_symbolic_dynamic_memory"
  angr_entry = 0x08048699
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.blank_state(addr=angr_entry,add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)
  
  data_0 = claripy.BVS("data0", 64)
  data_1 = claripy.BVS("data1", 64)
  
  addr0 = 0x0ABCC700
  addr1 = 0x0ABCC710
  
  initial_state.mem[0x0ABCC8A4].uint32_t = addr0
  initial_state.mem[0x0ABCC8AC].uint32_t = addr1
  
  initial_state.memory.store(addr0,data_0)
  initial_state.memory.store(addr1,data_1)
  
  simulation.explore(find=lambda state:b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state:b"Try again" in state.posix.dumps(sys.stdout.fileno()))

  if simulation.found:
    solution_state = simulation.found[0]
    print("%s %s" %(solution_state.solver.eval(data_0,cast_to=bytes),solution_state.solver.eval(data_1,cast_to=bytes) ))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

输出b'UBDKLMBV' 'UNOERNYS'

07_angr_symbolic_file

这道题要符号化一个打开的文件，Angr在state的插件(state的大多数属性都被视为插件，如mem,regs...)中包含了虚拟的文件系统fs，我们只要在其打开文件之前在fs中插入自己创建好的符号文件替换原本要打开的文件即可。

import angr
import sys
import claripy

def main(argv):
  path_to_binary = r"./07_angr_symbolic_file"
  angr_entry = 0x080488E7
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.blank_state(addr=angr_entry,add_options=angr.options.unicorn)
  
  filename = "OJKSQYDP.txt"
  filesize = 0x40
  flag = claripy.BVS("flag",filesize * 8)
  txtfile = angr.storage.SimFile(filename,content=flag,size=filesize)
  initial_state.fs.insert(filename,txtfile)
  
  simulation = project.factory.simgr(initial_state,veritesting=True)
  simulation.explore(find=lambda state:b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state:b"Try again" in state.posix.dumps(sys.stdout.fileno()))

  if simulation.found:
    solution_state = simulation.found[0]
    print("%s" %(solution_state.solver.eval(flag,cast_to=bytes)))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

留意一下创建符号文件的地方和插入文件系统的部分

b'AZOMMMZM\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x01\x00\x00\x00\x00'

Hook

开始学怎么避免路径爆炸了，其实个人感觉hook，simProcedure，手动约束的思想都差不多。

08_angr_constraints

这里要学会的是手动约束。

check_equals_AUPDNNPROEZRJWKB函数的功能是我们已知的，我们可以对其进行手动约束，避免路径爆炸(16个字符逐个比较会有2^16个分支,字符串比较常常导致路径爆炸)。

直接find Good Job会抛异常。

import angr
import sys
import claripy

def main(argv):
  path_to_binary = r"./08_angr_constraints"
  angr_entry = 0x08048625
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.blank_state(addr=angr_entry,add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)

  flag = claripy.BVS("flag",8 * 16)
  buffer_addr = 0x0804A050
  initial_state.memory.store(buffer_addr,flag)
  
  simulation.explore(find=0x08048565)

  if simulation.found:
    solution_state = simulation.found[0]
    solution_state.add_constraints(solution_state.memory.load(buffer_addr,16) == "AUPDNNPROEZRJWKB")
    print("%s" %(solution_state.solver.eval(flag,cast_to=bytes)))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

这里的约束不再是find输出，而是我们定义的在0x08048565地址时，buffer_addr需要满足等于"AUPDNNPROEZRJWKB"，然后solution_state.solver.eval自动求解。
b'LGCRCDGJHYUNGUJB'

09_angr_hooks

这道题在到达了check地址之后还会执行，使用hook来做更方便一些。

import angr
import sys
import claripy

def main(argv):
  path_to_binary = r"./09_angr_hooks"
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.entry_state(add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)

  buffer_addr = 0x0804A054
  
  @project.hook(addr=0x080486B3,length=5)# skip call
  def check(state):
    data = state.memory.load(buffer_addr,16) 
    state.regs.eax = claripy.If(data == "XYMKBKUHNIQYNQXE",
                      claripy.BVV(1,32),
                      claripy.BVV(0,32))
    
  simulation.explore(find=lambda state: b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state: b"Try again" in state.posix.dumps(sys.stdout.fileno()))
  
  if simulation.found:
    solution_state = simulation.found[0]
    print("%s" %(solution_state.posix.dumps(sys.stdin.fileno())))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

另外，本题接收的输入为字符串，直接用entry_state就行
b'ZXIDRXEORJOTFFJNWUFAOUBLOGLQCCGK'

10_angr_simprocedures

仔细看是对check_equals_ORSDDWXHZURJRBDH的大量重复调用，hook这个符号就好，这里用到simProcedures对check_equals_ORSDDWXHZURJRBDH来重写。

simProcedures的编写相对之前的两种方法有点繁琐，需要定义一个类然后继承angr.simProcedures

该函数的第一个参数是比较地址，第二个参数比较长度，我们在自己的函数里面也定义这两个参数。

import angr
import sys
import claripy

def main(argv):
  path_to_binary = r"./10_angr_simprocedures"
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.entry_state(add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)


  class SimCheckEqual(angr.SimProcedure):
    def run(self, str_addr,str_len):
      data = self.state.memory.load(str_addr,str_len)
      return claripy.If(
        data == "ORSDDWXHZURJRBDH",
        claripy.BVV(1,32),
        claripy.BVV(0,32)
      )
    
  check_symbols = 'check_equals_ORSDDWXHZURJRBDH'
  project.hook_symbol(check_symbols, SimCheckEqual())  
  simulation.explore(find=lambda state: b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state: b"Try again" in state.posix.dumps(sys.stdout.fileno()))
  
  if simulation.found:
    solution_state = simulation.found[0]
    print("%s" %(solution_state.posix.dumps(sys.stdin.fileno())))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

输出b'MSWKNJNAVTTOZMRY'

从这三道题目可以总结出：

• 路径爆炸函数在最后可以考虑find地址然后手动约束
• 路径爆炸函数之后还有约束，hook比较方便
• 多次调用路径爆炸函数可以用SimProcdure来hook符号

思想其实比较类似

11_angr_sim_scanf

用SimProcdure来hook scanf的话关键就是构建如下代码,hook之后就可以利用entry_state了（还是说现在已经可以直接跑了( ）

    class SimProcScanf(angr.SimProcedure):
        def run(self, format_string, scanf0_address, scanf1_address):
            scanf0 = claripy.BVS("scanf0", 32)
            scanf1 = claripy.BVS("scanf1", 32)
            self.state.memory.store(
                scanf0_address, scanf0, endness=project.arch.memory_endness
            )
            self.state.memory.store(
                scanf1_address, scanf1, endness=project.arch.memory_endness
            )
            self.state.globals['solutions'] = (scanf0, scanf1)

    scanf_symbol = "__isoc99_scanf"
    project.hook_symbol(scanf_symbol, SimProcScanf(), replace=True)

这里使用了一个globals全局变量，因为scanf的结果需要保存，使用时候再从全局变量中取用就好。

Veritesting

12_angr_veritesting

这个选项其实之前的脚本一直都开着，这里就CV下原理（

符号执行，一种是动态符号执行（Dynamic Symbolic Execution，简称DSE），另一种是静态符号执行（Static Symbolic Execution，简称SSE）。
动态符号执行会去执行程序然后为每一条路径生成一个表达式。在生成表达式上引入了很多的开销，然而生成的表达式很容易求解。
而静态符号执行将程序转换为表达式，每个表达式都表示任意条路径的属性生成表达式容易，但是表达式难求解。
veritesting就是在这二者中做权衡，使得能够在引入低开销的同时，生成较易求解的表达式。

脚本就是一个常规的脚本，angr使用的时候常常是在逆向的最后，优化完代码逻辑后跑，可能碰不到之前这么多的情况。当然也可以一上来就梭angr( 。

import angr
import sys

def main(argv):
  path_to_binary = r"./12_angr_veritesting"
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":False})
  initial_state = project.factory.entry_state(add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)

  simulation.explore(find=lambda state: b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state: b"Try again" in state.posix.dumps(sys.stdout.fileno()))
  
  if simulation.found:
    solution_state = simulation.found[0]
    print("%s" %(solution_state.posix.dumps(sys.stdin.fileno())))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

Library

13_angr_static_binary

和00_angr_find唯一的区别是二进制文件被编译为静态二进制文件,我们主动替换库函数避免路径爆炸和加速。
angr提供了写好的SimProcdure，我们直接索引到对应的函数然后hook就行。

import angr
import sys

def main(argv):
  path_to_binary = r"./13_angr_static_binary"
  project = angr.Project(path_to_binary,load_options={"auto_load_libs":True})
  initial_state = project.factory.entry_state(add_options=angr.options.unicorn)
  simulation = project.factory.simgr(initial_state,veritesting=True)
  project.hook(0x0804ED40, angr.SIM_PROCEDURES['libc']['printf']())
  project.hook(0x0804ED80, angr.SIM_PROCEDURES['libc']['scanf']())
  project.hook(0x0804F350, angr.SIM_PROCEDURES['libc']['puts']())
  project.hook(0x08048D10, angr.SIM_PROCEDURES['glibc']['__libc_start_main']())
  simulation.explore(find=lambda state: b"Good Job" in state.posix.dumps(sys.stdout.fileno()),
                     avoid=lambda state: b"Try again" in state.posix.dumps(sys.stdout.fileno()))
  
  if simulation.found:
    solution_state = simulation.found[0]
    print("%s" %(solution_state.posix.dumps(sys.stdin.fileno())))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

输出b'PNMXNMUD'

14_angr_shared_library

题目依赖lib14_angr_shared_library.so，这里学习怎么符号执行so文件的代码

14_angr_shared_library中用到了外部函数validate，在so文件中找到文件偏移为000006D7h

动态链接库的代码可以在任意位置执行，且动态链接库中必然不能有绝对地址，与之相伴的技术实现叫做位置无关代码PIC

我们指定下共享库的基地址加上偏移就能定位到validate。这里用到一个新的内置state：call_state

1. .blank_state()：空白状态，其大部分数据未初始化。 访问未初始化的数据时，将返回一个不受约束的符号值。
2. .entry_state() ：构造一个准备在主二进制文件入口点执行的状态。
3. .full_init_state()：通过需要在主二进制文件入口点之前运行的任何初始化程序构造一个准备执行的状态
4. .call_state()：构造一个准备好执行给定函数的状态。

脚本如下：

import angr
import sys
import claripy

def main(argv):
  path_to_binary = r"./lib14_angr_shared_library.so" 
  
  base = 0x4000000
  project = angr.Project(path_to_binary, load_options={
    'main_opts' : {
      'custom_base_addr' : base
    }
  })
  
  buffer_pointer = claripy.BVV(0x3000000, 32)
  func_address = base + 0x6d7
  initial_state = project.factory.call_state(func_address, buffer_pointer, claripy.BVV(8, 32))
  flag = claripy.BVS('flag', 8*8)
  initial_state.memory.store(buffer_pointer, flag)
  
  simulation = project.factory.simgr(initial_state,veritesting = True)
  func_end = base + 0x783
  simulation.explore(find=func_end)
  
  if simulation.found:
    solution_state = simulation.found[0]
    solution_state.add_constraints(solution_state.regs.eax != 0)
    print(solution_state.solver.eval(flag, cast_to=bytes))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

解题中没有用到14_angr_shared_library，实现了函数的独立运行，直接得到了结果b'PGXSNWTS'

Overflow

Angr在栈溢出中的使用，三道题目分别是任意读，任意写，简单ROP。

15_angr_arbitrary_read

import angr
import sys
import pwn
def main(argv):
  path_to_binary = r"./15_angr_arbitrary_read" 
  project = angr.Project(path_to_binary, load_options={"auto_load_libs" : False})
  initial_state = project.factory.entry_state(add_options=angr.options.unicorn)
  
  avoid_addr = 0x0804852F
  find_addr = 0x08048524
  simulation = project.factory.simgr(initial_state,veritesting = True)
  simulation.explore(find=find_addr,avoid=avoid_addr)
  if simulation.found:
    solution_state = simulation.found[0]
    solution_state.add_constraints(solution_state.regs.eax == 0x484F4A47)
    print(solution_state.posix.dumps(sys.stdin.fileno()))
  else:
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

输出b'0041810812 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00GJOH'

16_angr_arbitrary_write

import angr
 
def main():
    proj = angr.Project(r'./16_angr_arbitrary_write')
    init_state = proj.factory.entry_state()
 
    def check_strncpy(state):
        strncpy_dest = state.memory.load(state.regs.esp+4, 4, endness=proj.arch.memory_endness)
        strncpy_src = state.memory.load(state.regs.esp+8, 4, endness=proj.arch.memory_endness)
        strncpy_len = state.memory.load(state.regs.esp+12, 4, endness=proj.arch.memory_endness)
 
        src_contents = state.memory.load(strncpy_src, strncpy_len)
 
        if state.solver.symbolic(strncpy_dest) and state.solver.symbolic(src_contents):
 
            password_string = "NDYNWEUJ"
            buffer_address = 0x57584344
 
            does_src_hold_password = src_contents[-1:-64] == password_string
            does_dest_equal_buffer_address = strncpy_dest == buffer_address
 
            if state.satisfiable(extra_constraints=(does_src_hold_password, does_dest_equal_buffer_address)):
                state.add_constraints(does_src_hold_password, does_dest_equal_buffer_address)
                return True
            else:
                return False
        else:
            return False
 
    simulation = proj.factory.simgr(init_state)
 
    def success(state):
        strncpy_addr = 0x08048410
 
        if state.addr == strncpy_addr:
            return check_strncpy(state)
        else:
            return False
 
    simulation.explore(find=success)
 
    if simulation.found:
        solution_state = simulation.found[0]
        print(solution_state.posix.dumps(0))
 
if __name__ == '__main__':
    main()

感觉这里也可以使用SimProcdure来hook strncpy符号，通过全局变量来保存约束条件。
b'0011604995 NDYNWEUJ\x00\x00\x00\x00\x00\x00\x00\x00DCXW'

17_angr_arbitrary_jump

一个简单的ROP，通过read_input跳转到print_good函数中。

这里的符号执行推进的方式不再是高度封装的explore，而采用了step步进
SimManager将State以Stash的形式存储，当一个状态遇到符号分支条件时，两个后继状态都会出现在 stash 中，并且可以将它们同步步进，会步进的状态只有active列表中的stash。

当一个指令有很多分支的可能性时，称为不受约束的状态,比如这里输入决定了EIP的位置。在启用save_unconstrained选项下，不受约束的状态会被放置在unconstrained列表中。否则会被弃置。我们利用不受约束状态来进行ROP。

import angr
import claripy
import sys
 
def main():
    proj = angr.Project('./17_angr_arbitrary_jump',load_options={"auto_load_libs":False})
    init_state = proj.factory.entry_state(add_options=angr.options.unicorn)
    
    simulation = proj.factory.simgr(
        init_state,
        save_unconstrained=True,
        stashes={
            'active':[init_state],
            'unconstrained': [],
            'found': []
        },
        veritesting = True
    )
 
    def has_found_solution():
        return simulation.found
 
    def has_unconstrained():
        return simulation.unconstrained
 
    def has_active():
        return simulation.active
 
    while( has_active() or has_unconstrained() ) and (not has_found_solution()) :
        simulation.move('unconstrained','found')
        simulation.step()
 
    if simulation.found:
        solution_state = simulation.found[0]
        solution_state.add_constraints(solution_state.regs.eip == 0x42585249)
        print(solution_state.posix.dumps(sys.stdin.fileno()))
    else:
        raise Exception('Could not find the solution')
 
if __name__ == '__main__':
  main()

输出b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00IRXB\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'

题目到这里就结束了，但是angr还远没有结束，Symbion技巧和很多细节还没有体现出来，等学的更深入之后再补一些吧。