angr_ctf——从0学习angr（二）：状态操作和约束求解

标签：init solver 求解 state ctf angr print 符号

状态操作

angr中提到的状态（state）实际上是一个Simstate类，该类可由Project预设得到。预设完成后，还可以根据需要对某些部分进行细化操作。

一个state包含了程序运行到某个阶段时，内存、寄存器、文件系统、符号变量和符号约束等内容。

寄存器访问

可以通过state.regs.寄存器名来访问和修改寄存器

>>> print(state.regs.eax, state.regs.ebx)
<BV32 0x1c> <BV32 0x0>
>>> state.regs.eax +=1
>>> print(state.regs.eax, state.regs.ebx)
<BV32 0x1d> <BV32 0x0>

栈访问

栈访问涉及两个寄存器：ebp和esp，以及两个指令：push和pop，对于寄存器的访问与其他寄存器相同

push和pop指令可以通过以下方法调用

state.stack_push(value)
state.stack_pop()

内存访问

使用以下两个指令对内存读写：

读内存-state.memory.load(addr, size,endness)

写内存-state.memory.store(data,size,endness)

endness是指使用的大小端，通常应该和程序使用的大小端保持相同，而程序所使用的大小端可以用p.arch.memory_endness查询，因此在对默认值没有把握时，请让endness=p.arch.memory_endness。

此外，上述两个函数的size的单位均为字节，示例如下：

>>> state.memory.store(0x4000,state.solver.BVV(0x0123456789,40))
>>> print(state.memory.load(0x4001,2))
<BV16 0x2345>

其中存入地址0x4000处的数据是一个位向量，之后会介绍。

文件操作

angr提供了一个SimFile类用来模拟文件，通过将SimFile对象插入到状态的文件系统中，在使用angr分析程序时就可以使用该文件

filename = 'test.txt'
simfile = angr.storage.SimFile(name=filename, content=data, size=0x40)
state.fs.insert(filename, simfile)

上述指令能创建一个SimFile对象，文件名为test.txt，内容为data，输入的内容长度为0x40，单位为字节

之后，使用state.fs.insert方法，将SimFile对象插入到状态的文件系统中，在模拟运行程序时就可以使用这个文件了

 

位向量

对于内存、寄存器等进行操作时，不仅可以使用python的int，angr还提供了位向量（Bit Vector，BV）

位向量就是一串比特的序列，这于python中的int不同，例如python中的int提供了整数溢出上的包装。而位向量可以理解为CPU中使用的一串比特流，需要注意的是，angr封装的位向量有两个属性：值以及它的长度

我们先生成几个位向量：

>>> one = state.solver.BVV(1,64)
>>> one_hundred = state.solver.BVV(100,64)
>>> short_nine = state.solver.BVV(9,27)
>>> print(one,one_hundred,short_nine)
<BV64 0x1> <BV64 0x64> <BV27 0x9>

BVV能够生成一个位向量，第二个参数表示该位向量的长度，单位为bit

这些位向量相互之间能够进行运算，但参与运算的位向量的长度必须相同

>>> print(short_nine+1)
<BV27 0xa>
>>> print(one+one_hundred)
<BV64 0x65>
>>> print(one+short_nine)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/kali/angr/venv/lib/python3.9/site-packages/claripy/operations.py", line 50, in _op
    raise ClaripyOperationError(msg)
claripy.errors.ClaripyOperationError: args' length must all be equal

可以看到，当长度不一样时，claripy会提示“length must all be equal”，同时我们也得知，位向量运算的底层模块时claripy，之后会继续说明claripy

如果一定要进行长度不相等位向量之间的运算，可以扩展位向量，使用zero_extend会用零扩展高位，而sign_extend会在此基础上带符号地进行扩展

>>> print(one+short_nine.zero_extend(64-27))
<BV64 0xa>

请注意zero_extend的参数是扩展多少位，而不是扩展到多少位

此外，位向量还可以之间与python的int进行运算：

>>> print(one+1,one*5)
<BV64 0x2> <BV64 0x5>

 

接下来使用BVS（Bit Vectort Symbol）创建一些符号变量

>>> x = state.solver.BVS('x',64)
>>> y = state.solver.BVS('y',64)
>>> z = state.solver.BVS('notz',64)
>>> print(x,y,z)
<BV64 x_42_64> <BV64 y_43_64> <BV64 notz_44_64>

BVS的参数分别是符号变量名和长度，通过z的例子可以看到，BVS中符号变量名参数会影响位向量的名称，但这与你在angr脚本中使用这个符号变量的变量（也就是z）无关。

此时对符号变量进行运算，做比较判断，都不会得到一个具体的值，而是将这些操作统统保存到符号变量中：

　>>> print(x+1)
　<BV64 x_42_64 + 0x1>

 

符号约束与求解

符号约束

每个符号变量本质上可以看做是一颗抽象语法树（AST），之前单独生成的符号变量<BV64 x_42_64>可以看作是只有一层的AST，对它进行操作实际上是在扩展AST，这样的AST的构造规则如下：

• 如果AST只有根节点的话，那么它必定是符号变量或位向量
• 如果AST有多层，那么叶子节点为符号变量和位向量，其他节点为运算符

其中一个节点的左右孩子可以使用args来访问，节点本身存放的信息则使用op来访问。可以通过下面的例子来理解：

>>> ast = (x+5)*(y-1)
>>> print(ast)
<BV64 (x_45_64 + 0x5) * (y_43_64 - 0x1)>

>>> print(ast.op)
__mul__

>>> print(ast.args)
(<BV64 x_45_64 + 0x5>, <BV64 y_43_64 - 0x1>)

>>> print(ast.args[0].op)
__add__

>>> print(ast.args[0].args[0])
<BV64 x_45_64>
>>> print(ast.args[0].args[1])
<BV64 0x5>
>>> print(ast.args[0].args[1].op)
BVV
>>> print(ast.args[0].args[1].args)
(5, 64)
>>> print(ast.args[0].args[0].args)
('x_45_64', None, None, None, False, False, None)
>>> print(ast.args[0].args[0].op)
BVS

可以发现，对单独的节点取op的话，可以得到它的类型（示例中为BVV和BVS）

之前我们使用BVS创建了符号变量，现在如果对该符号变量进行比较判断操作，会得到如下结果：

>>> print(x>0)
<Bool x_42_64 > 0x0>

它现在不是一个位向量了，而是一个符号化的布尔类型

这些布尔类型的值可以通过is_true和is_false来判断，但对于上述有符号变量参与的布尔类型，它永远为false

>>> print(state.solver.is_true(x>0))
False
>>> print(state.solver.is_false(x>0))
False

此外需要注意的是，直接使用比较符号比较两个位向量，通常是默认不带符号的，例子如下：

>>> mfive = state.solver.BVV(-5,64)
>>> one = state.solver.BVV(1,64)
>>> print(one>mfive)
<Bool False>
>>> print(mfive)
<BV64 0xfffffffffffffffb>
>>> print(state.solver.is_true(one>mfive))
False

-5在内存中以0xfffffffffffffffb存储，作为无符号数，它比1要大

 

符号约束是一个和状态相关的概念，或者说一个state除了包含内存、寄存器中的值这些信息外，还包含了符号约束，也就是要到达当前状态符号变量所必须满足的条件。

除了运行程序，SM根据分支收集起来的符号约束之外，也可以自行手动添加约束：

>>> print(x,y)
<BV64 x_45_64> <BV64 y_43_64>
>>> state.solver.add(x>y)
[<Bool x_45_64 > y_43_64>]
>>> state.solver.add(x>5)
[<Bool x_45_64 > 0x5>]
>>> state.solver.add(x<8)
[<Bool x_45_64 < 0x8>]

此时，x必须满足大于5小于8，而y必须满足小于x。

 

符号求解

可以使用state.solver.eval(x)来求解当前状态（即state）中的符号约束下，x的值

>>> state.solver.eval(x)
6

求解完x之后，此时如果求解y，则会得到之前求解结果条件下的y，也就是说，y此时必定小于6

此外，很明显能够看到，x应该是有多个值的，可以solver中的其他方法取出来：

• solver.eval(x):给出表达式的一个可能解
• sovler.eval_one(x):给出表达式的解，如果有多个解，将抛出错误
• solver.eval_upto(x,n)给出表达式的至多n个解
• sovler.eval_taleast(x,n):给出表达式的n个解，如果解的数量少于n，则抛出错误
• solver.eval_exact(x,n):给出表达式的n个解，如果解的个数不为n，则抛出错误
• sovler.min(x):给出表达式的最小解
• sovler.max(x):给出表达式的最大解

这些方法还有两个可省略的参数：

• extra_constraints：可以作为约束进行求解，但不会被添加到当前状态
• cast_to：将传递结果转换成指定数据类型，目前只能是int和bytes，例如state.solver.eval(state.solver.BVV(0x41424344, 32), cast_to=bytes) 将返回b'ABCD'

此外，如果将两个互相矛盾的约束加入到一个state当中，那么这个state就会被放到unsat这个stash里面，对这样的state进行求解会导致异常，可以使用state.satisfiable()来检查是否有解

加入到状态中的约束在进行约束求解时的关系是“与”的关系，也就是说必须都得满足，那么如果有其他的关系，比如或之类的关系，该如何表示呢？

事实上，根本不会存在或这样的约束之间的关系，因为angr保存所有分支，因此到达某个状态的条件必然是一层一层都满足的情况下到达的，如果在条件判断时有“或”这样的关系存在，那么这样的解将会出现在另一个state当中，而另一个state当中的符号约束之间也必然都是“与”的关系。

 

实战：03_angr_symbolic_registers

此题用万能脚本也可以解，但出于练习的目的，使用本节讲的内容（angr_ctf作者认为angr在处理多个由scanf接收的输入时表现不好，应该想办法跳过scanf）

首先还是在IDA中逆向分析一下

函数get_user_input()使用scanf在一行中接收三个输入，三个输入之后分别被complex_function混淆后参与if语句的判断

查看汇编指令，发现函数get_usr_input()接收的输入，通过三个寄存器保存在了局部变量当中

因此为了跳过scanf（也就是get_user_input函数），可以考虑让程序在call之后的语句开始模拟运行，同时在三个寄存器中存放三个符号变量，这样程序从mov开始运行时，就会从三个寄存器中分别取出符号变量参与后续运行，也就使用这三个符号变量进行路径选择，保存符号约束，最后在能够到达Good Job的state里求解这三个符号变量即可。

angr脚本如下：

import angr
import claripy

path_to_binary = './dist/03_angr_symbolic_registers'
p = angr.Project(path_to_binary, auto_load_libs=False)
#call get_user_input后的下一条语句
start_addr = 0x08048980
#从目标地址开始模拟运行，而不是程序的入口点
init_state = p.factory.blank_state(addr=start_addr)

#使用claripy创建三个符号变量，之前提到过state有关位向量的底层实现是claripy
passwd_size = 32
passwd0 = claripy.BVS('passwd0', passwd_size)
passwd1 = claripy.BVS('passwd1', passwd_size)
passwd2 = claripy.BVS('passwd2', passwd_size)

#对寄存器进行赋值
init_state.regs.eax = passwd0
init_state.regs.ebx = passwd1
init_state.regs.edx = passwd2

#将初始化后的state添加到SM中
simgr = p.factory.simgr(init_state)

good = 0x080489e9
bad = 0x080489d7

simgr.explore(find=good, avoid=bad)

if simgr.found:
　　#solution_state是能够到达Good Job的状态
    solution_state = simgr.found[0]
　　在该状态中求解三个符号变量即可
    solution0 = hex(solution_state.solver.eval(passwd0))
    solution1 = hex(solution_state.solver.eval(passwd1))
    solution2 = hex(solution_state.solver.eval(passwd2))

    print(solution0, solution1, solution2)

else:
    raise Exception('Could not find')

 

实战：04_angr_symbolic_stack

此题与03一样，需要绕过scanf函数，然而上一题中输入的参数被保存在寄存器当中之后再转移到局部变量。此题则是直接保存在局部变量当中了，因此创建的符号变量需要存放在栈上。

那么进行动态调试，查看执行完scanf后的栈结构（我输入了1234 5678，对应16进制为4d2 162e）：

可以发现，输入进去的数字被保存在了距离ebp 0xc的位置上，那么我们只要将两个符号变量压入这个位置即可。

angr脚本：

import angr
import claripy

path_to_binary = './dist/04_angr_symbolic_stack'
p = angr.Project(path_to_binary, auto_load_libs=False)
#call scanf的下一个汇编指令
start_addr = 0x08048694
init_state = p.factory.blank_state(addr=start_addr)

good = 0x080486e4
bad = 0x080486d2

v1 = claripy.BVS('v1', 32)
v2 = claripy.BVS('v2', 32)
#tmp保存当前esp的内容，以便待会还原
tmp = init_state.regs.esp
#-减8而不是减12的原因在于，esp保存了当前不为空的栈顶，push时esp先+4再存放内容
init_state.regs.esp = init_state.regs.ebp - 0x8
init_state.stack_push(v1)
init_state.stack_push(v2)
#还原esp，维持堆栈平衡
init_state.regs.esp = tmp

#之后的步骤同3
simgr = p.factory.simgr(init_state)
simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution_state = simgr.found[0]
    s0 = solution_state.solver.eval(v1)
    s1 = solution_state.solver.eval(v2)

    print(s0, s1)

else:
    raise Exception('Could not find')

 

实战：05_angr_symbolic_memory

此题逻辑与前两个也一样，区别在于这次输入的东西被保存在了.bss段作为全局变量存放了

那么只需要创建符号变量，并保存在对应的地址处就可以了，使用state.memory.store方法进行内存写。

angr脚本：

import angr
import time
import claripy


def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False


time_start = time.perf_counter()
p = angr.Project('./dist/05_angr_symbolic_memory')
start_addr = 0x080485FE
init_state = p.factory.blank_state(addr=start_addr)

passwd_size_in_bits = 8 * 8
password0 = claripy.BVS('password0', passwd_size_in_bits)
password1 = claripy.BVS('password1', passwd_size_in_bits)
password2 = claripy.BVS('password2', passwd_size_in_bits)
password3 = claripy.BVS('password3', passwd_size_in_bits)

# 四个变量地址连续，向其中写入符号变量即可
password0_address = 0x0A1BA1C0
init_state.memory.store(password0_address, password0)
init_state.memory.store(password0_address + 0x08, password1)
init_state.memory.store(password0_address + 0x10, password2)
init_state.memory.store(password0_address + 0x18, password3)
simgr = p.factory.simgr(init_state)

simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution = simgr.found[0]
    solution0 = solution.solver.eval(password0, cast_to=bytes).decode('utf-8')
    solution1 = solution.solver.eval(password1, cast_to=bytes).decode('utf-8')
    solution2 = solution.solver.eval(password2, cast_to=bytes).decode('utf-8')
    solution3 = solution.solver.eval(password3, cast_to=bytes).decode('utf-8')
    print(solution0, solution1, solution2, solution3)
else:
    raise Exception("Could not find solution")

print('program last:', time.perf_counter() - time_start)

 

实战：06_angr_symbolic_dynamic_memory

和前三题一样，只是此题将输入进来的数据保存到了malloc申请来的内存空间当中了

 

双击进入buffer0和buffer1，对应的地址分别是.bss:0x0abcc8ac和.bss:0x0abcc8ac，这两个地址将来会存放由malloc申请来的地址，而malloc申请来的地址当中，将存放输入的字符串，也就是说，我们需要将符号变量保存在buffer中保存的指针指向的地方，而我们并不会清楚malloc具体会申请到哪个地址，因此考虑直接跳过malloc语句，往buffer中填入一个不影响程序运行的地址，然后在该地址中存放符号变量

这里是一个多重指针，熟悉堆管理方式的朋友应该不会陌生，它们的调用关系如下：

buffer -> malloc申请到的地址 -> 字符串保存的地址

angr脚本如下：

import angr
import claripy

def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False

p = angr.Project('./dist/06_angr_symbolic_dynamic_memory')
# scanf后的第一条汇编指令
start_addr = 0x08048699
init_state = p.factory.blank_state(addr=start_addr)

# fake_addr为不影响程序运行的任意地址
fake_addr1 = 0x085fa000
fake_addr2 = 0x085fa010
buffer1 = 0x0abcc8a4
buffer2 = 0x0abcc8ac

# 注意设置大小端
init_state.memory.store(buffer1, fake_addr1, endness=p.arch.memory_endness)
init_state.memory.store(buffer2, fake_addr2, endness=p.arch.memory_endness)

v1 = claripy.BVS('v1', 64)
v2 = claripy.BVS('v2', 64)

# 符号变量不是具体的值，不需要考虑大小端
init_state.memory.store(fake_addr1, v1)
init_state.memory.store(fake_addr2, v2)


simgr = p.factory.simgr(init_state)

simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution_state = simgr.found[0]
    s1 = solution_state.solver.eval(v1, cast_to=bytes).decode()
    s2 = solution_state.solver.eval(v2, cast_to=bytes).decode()
    print(s1, s2)
    
else:
    raise Exception("Could not find solution")

 

实战：07_angr_symbolic_file

此题逻辑也一样，只是这次需要从文件中读取输入了

 

因此我们需要创建一个SimFile对象，该对象是个模拟文件，然后将符号变量存放在模拟文件中并将模拟文件插入到state中，这样在模拟运行时，程序就会从我们模拟的文件中读取符号变量作为输入的参数进行后续的运行。

import angr
import claripy
import time


def good(state):
    tag = b'Good' in state.posix.dumps(1)
    return True if tag else False


def bad(state):
    tag = b'Try' in state.posix.dumps(1)
    return True if tag else False


time_start = time.perf_counter()

p = angr.Project('./dist/07_angr_symbolic_file', auto_load_libs=False)
# memset的后一条指令
start_addr = 0x080488e7
init_state = p.factory.blank_state(addr=start_addr)

v = claripy.BVS('v', 0x40*8)
filename = 'OJKSQYDP.txt'
# 创建SimFile对象
simfile = angr.storage.SimFile(name=filename, content=v, size=0x40)
# 将SimFile插入到state的文件系统中
init_state.fs.insert(filename, simfile)

simgr = p.factory.simgr(init_state)
simgr.explore(find=good, avoid=bad)

if simgr.found:
    solution_state = simgr.found[0]
    s = solution_state.solver.eval(v, cast_to=bytes)
    print(s)

else:
    raise Exception("Could not find solution")

print('program last: ', time.perf_counter() - time_start)

需要注意的是，我们只是模拟了文件，并没有直接将符号变量存在buffer中，因此程序还是需要从文件中读取符号变量的，所以我们blank_state中的初始地址不能超过fopen函数。

此外，由于参与混淆和比较的字符串被保存在了buffer当中，也可以使用之前的方式将符号变量直接保存在buffer中，然后跳过所有的文件操作开始运行程序。

该题也可以通过万能脚本完成，但是通过计算程序实际运行的时间，发现使用模拟文件的方式要更快一些，前者大约是5秒半，后者大约3秒，这也是angr脚本的意义——通过更详细的设置angr状态和路径搜索策略，提高angr的效率。

 

标签：init,solver,求解,state,ctf,angr,print,符号
From： https://www.cnblogs.com/level5uiharu/p/16932453.html