L1E6N0A2

监督自己不断学习

0%

每日一题3-1

发表于 更新于
本文字数： 5.5k 阅读时长 ≈ 5 分钟

CTF_Angr

github: https://github.com/jakespringer/angr_ctf. 可以看到有每一个题目的文件夹（题目生成包，用来生成可执行文件，只需刷题的话大概没用），还有dist和solutions两个文件夹。

dist里有：

  1. XX_xxxx：每道题的elf。
  2. scaffoldXX.py：解题脚本挖空范例（题面，需要填空，注释用来解释语句的作用很详细）。

solutions里各道题的文件夹里有：

  1. XX_xxxx：每道题的elf。
  2. scaffoldXX.py：解题脚本挖空范例（同上）。
  3. solveXX.py：解题脚本（正确答案=v=）。

这里面都是典型的angr使用方法，这里仅以第一个范例进行演示，剩下的可以按照相同的思路求解。

0X00-angr_find

使用IDA打开dist/00_angr_find,F5转化为伪C代码

1

程序输入password，经过complex_function函数处理，如果最终等于“JACEJGCS”就输出Good Job。

complex_fuction函数判断了输入的取值范围。

2

本题使用传统的“爆破”方法也可以解决，一位一位拼出符合题意的输入（“JXWVXRKX”）。脚本如下：

1
2
3
4
5
6
7
8
9
10
11
str1 = "JACEJGCS"
flag = ""
def complex_function(a1,a2):
    return (3 * a2 + a1 - 65) % 26 + 65
if __name__ == "__main__":
    for i in range(len(str1)):
        for j in range(64,90):      
            if ord(str1[i]) == complex_function(j,i):
                flag += chr(j)
                break            
    print(flag)

知道目标输出，构造合适的输入，可以使用Angr这个符号执行工具解题。

①.新建一个Angr工程，并且载入二进制文件

1
2
path_to_binary = 'D:\WinAFL\angr_ctf\dist\00_angr_find'
project = angr.Project(path_to_binary, auto_load_libs=False)

②.创建程序入口点的state

1
state = p.factory.entry_state(add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES})

③.将要求解的变量符号化

本题目中可以省略这步操作(当然也可以保留，但后面就不能用dump，要用eval)，因为不是手动设置的输入，是在程序运行时用户任意输入的。

详细解释见下“注”。

1
2
u = claripy.BVS("u", 8)
initial_state.memory.store(0x080485C7, u)  //main地址

④.创建SimulationManager进行程序执行管理

1
sm = p.factory.simulation_manager(state)

⑤.搜索满足我们目标的state

目标state是”good job”, IDA中确定地址为0x8048678

3

1
print_good_address = 0x8048678

⑥.求解程序执行到state时，符号化变量所需要的约束条件

1
sm.explore(find=print_good_address)

⑥.解出约束条件，获得目标值

solution_state.posix.dumps(0)代表该状态执行路径的所有输入

solution_state.posix.dumps(1)代表该状态执行路径的所有输出 

1
2
3
4
5
if sm.found:
    solution_state = sm.found[0]
    print(solution_state.posix.dumps(0))
else:
    raise Exception('Could not find the solution')

完整代码见 "./angr_ctf/solutions/00_angr_find/solve00.py", 与爆破得到的结果一致。

注：本题中不是手动设置的输入，而是程序运行过程中进行的输入，因此可以使用dump(0) dump标准输入来得到输入。但如果题目修改为char s1[9]="00000000",并去掉scanf，这时就要将输入符号化，使用angr求解器（solver）提供的eval函数，得到满足条件的可能的输入。

solver.eval（）函数详细说明：https://blog.csdn.net/doudoudouzoule/article/details/79394447

baby-re（DEFCON 2016 quals）

github：https://github.com/angr/angr-doc/tree/master/examples，这里有很多例子，之前已经实践过sym_write，这次选择一个复杂点的，defcon2016quals_baby-re，作为一道经典的CTF真题，《从0到1 CTFer成长之路》一书也对这个例子进行了详细的分析。

首先IDA打开二进制文件，F5查看C伪代码，了解程序逻辑。输入13个字符，然后通过CheckSolution判断输入字符是否满足约束条件。（截图为部分程序代码）

9

分析可知成功的地址是0x4028E9，失败的地址是0x402941

6

7

然后用最朴素的方式构造payload，代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
import angr
import claripy
import re
import math

proj = angr.Project('./baby-re', auto_load_libs=False)
state = proj.factory.entry_state(add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES})
sm = proj.factory.simulation_manager(state)
sm.explore(find=0x4028E9, avoid=0x402941)
if sm.found:
    solution_state = sm.found[0]
    text = solution_state.posix.dumps(0).decode("utf-8")  #bytes转化为string
    str = re.findall(r'.{%d}' % int(10), text)   #每10位进行切割，asc码转字符串，拼接组成flag
    flag = ''
    for i in str:
        flag += (chr(int(i)))
    print(flag)
else:
    raise Exception('Could not find the solution')

程序输出正确的结果，但用时较长，下面要想办法优化。

8

  • LAZY_SOLVES

    在LAZY_SOLVES打开的情况下，只要路径在基本块的末尾分支为几个，angr就不会主动检查每个成功的状态是否可以满足。相反，angr认为他们都是可以满足的，并且继续创造成功的路径。LAZY_SOLVES指在不运行的时候检查当前的条件是否能够成功到达目标位置。这样无法避免一些无解的情况，但是可以显著提高脚本的运行速度，是在路径爆炸（创建更多路径）和花费在约束求解上的时间之间的平衡。

    在早期angr版本中默认LAZY_SOLVES是开启的，它可以加快我们分析的速度，因为它不会对每个状态都进行判断。新版本可通过下面的语句开启：

    1
    sm.one_active.options.add(angr.options.LAZY_SOLVES

    经过实践，时间大大缩短，从449.51s降低到15.78s

  • blank_state

    有些时候程序的输入数据被分类很多组，或者程序获取输入的逻辑实现的很复杂，严重干扰了angr分析，这时候就要跳过那些输入指令，加载程序，提高符号执行效率。创建initial_state时，使用factory的blank_state方法，传入地址，表示从该地址的状态开始，实现任意位置加载程序。

    1
    state = proj.factory.blank_state(addr=0x4025E7) #main函数地址

  • hook

    在scanf函数前面存在fflush函数，它的功能是清空缓冲区，将输入写入stream。注意到在每次输入时，都会调用printf和fflush这两个对程序关键算法分析没有帮助的函数浪费时间，因此hook这两个函数，让他们直接return。

    1
    2
    proj.hook_symbol('printf',angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](return_value=0), replace = True)
    proj.hook_symbol('fflush',angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](return_value=0),replace = True)

    优化scanf：用自己的my_scanf()来代替__isoc99_scanf，我们在保持scanf功能不变的情况下，将我们的符号变量存储进去。

    1
    2
    3
    4
    5
    6
    7
    8
    9
    class my_scanf(angr.SimProcedure):
        def run(self, fmt, des):  # 参数为 (self + 该函数实际参数)
            simfd = self.state.posix.get_fd(0) # 创建一个标准输入对对象
            data, real_size = simfd.read_data(4) # 从标准输入中读取一个整数，返回值第一个是读到的数据内容 第二个数内容长度
            self.state.memory.store(des, data) # 将数据保存到相应参数内
            return 1 # 返回原本函数该返回的东西

    proj.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)
    # 这里%d对应int 是4个字节 但是读取到一个int所以返回1  所以这完全是模拟的原来的函数

    因为我们这里Scanf是要向内存写入数据的，于是我们利用使用 state.memory.store(addr, val) 接口将数据保存到相应参数内。

    优化scanf就可以达到和控制返回值类似的效果，对于速度提升效果明显，时间缩短到4.86s

  • Claripy

    angr中通过claripy模块手动构造输入，claripy.BVS可以直接创建符号变量，第一个参数为变量名，第二个参数是位数，可以这样创建用户输入，然后把这些变量保存在内存地址。

    1
    flag_chars = [claripy.BVS('flag_%d' % i, 32) for i in range(13)]
    1
    2
    3
    4
    5
    class my_scanf(angr.SimProcedure):
    	def run(self, fmt, ptr): 
    		self.state.mem[ptr].dword = flag_chars[self.state.globals['scanf_count']]
    		self.state.globals['scanf_count'] += 1
    proj.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)
    1
    simulation.one_active.globals['scanf_count'] = 0

    这样程序每次调用scanf时，其实就是在执行my_scanf就会将flag_chars[i]存储到self.state.mem[ptr]当中，这其中ptr参数，其实就是本身scanf函数传递进来的。为了控制下标，我们设置了一个全局符号变量scanf_count记录scanf函数的数目，存储在state.globals里面，使得第i个scanf函数的state.mem赋值第i个符号变量。

    这种优化方式时间缩短，效果不明显，平均5.02s

    综合上述分析优化，完整程序代码见./angr-doc/examples/defcon2016quals_baby-re/solve.py

参考资料

https://blog.csdn.net/doudoudouzoule/article/details/79977415

https://b0ldfrev.gitbook.io/note/symbolic_execution/angr-jin-jie

https://www.anquanke.com/post/id/214288

https://xz.aliyun.com/t/4137

https://blog.csdn.net/doudoudouzoule/article/details/79394447