学习一下angr符号执行…

符号执行

基本概念

符号执行 （Symbolic Execution）是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。

使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。

符号执行技术是一种白盒的静态分析技术。即，分析程序可能的输入需要能够获取到目标源代码的支持。同时，它是静态的，因为并没有实际的执行程序本身，而是分析程序的执行路径。

详细移步看雪

python虚拟环境

在windows和linux中我都装的是anaconda来配置python虚拟环境。建议搭配pycharm使用

常用命令：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
# 创建一个名为py38的python3.8版本的虚拟环境：
conda create -n py38 python=3.8  

# 启动环境
conda activate py38

# 查看已经安装的包
pip list

# 退出环境
conda deactivate py38

# 删除虚拟环境中的包
conda remove --name py38  package_name

# 删除环境 py38
conda remove -n py38 --all

用pycharm使用虚拟环境或者自带环境来新建项目，只需要找到其Python的解释器即可

举例我用anconda创建了一个py27的虚拟环境，在anaconda3下的envs目录下就能找到py27虚拟环境目录，在py27目录下即可看到python.exe

在pycharm中创建py2.7虚拟环境

B站有很多关于anconda虚拟环境的教程，可以去看看~

在kali中安装anconda的时候，遇到了两个问题

conda命令未显示的问题

在大佬aep的帮助下，得知环境变量添加错误，一般网上都把path添加在~/.bash.rc中，而我的shell是zsh环境，所以应该把path添加在 ~/.zshrc中

打开终端自动进入conda环境

1
vim .condarc

在文件中键入：

1
auto_activate_base: false

各种例题

来自《从0到1:CTFer的成长之路》

例题下载链接

defcamp_r100

首先查看一下保护，没有开PIE

用ida分析，记录一下判断成功的地址：0x400844

失败的地址： 0x400855

官方脚本：

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

def main():
    
    #  auto_load_libs=False,阻止angr自动载入并分析依赖的库函数
    p = angr.Project("r100", auto_load_libs=False)
    
    simgr = p.factory.simulation_manager(p.factory.full_init_state())
    
    # 需要寻找和需要规避的地址，传入的可以是数组
    simgr.explore(find=0x400844, avoid=0x400855)
	
    # fund是一个表，found表示其中一条通往目标地址的路径,若找到，其类型为SimState，代表程序此时的一个状态
    # POSIX(Portable Operating System Interface):各种输入数据，posix.dump(0)获取标准输入(标准输入的文件句柄号为0)
    return simgr.found[0].posix.dumps(0).strip(b'\0\n')

def test():
    assert main().startswith(b'Code_Talkers')

if __name__ == '__main__':
    print(main())

官方给出的脚本跑了3秒多

hook函数改进方法

以下是nullbook书中给出的改进算法

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
import angr
import time

# 继承angr.SimProcedure类，并重写其中的run方法
# 通过验证函数的循环次数可以确定flag的长度为12,所以只需要让fgets函数传入12个字节的输入即可
class my_fgets(angr.SimProcedure):

    # s是rdi寄存器指向的内存地址，用来存放输入数据
    def run(self,s,num,f):
        simfd = self.state.posix.get_fd(0)

        # read_data，存放12个输入字符即可
        data,real_size = simfd.read_data(12)
        self.state.memory.store(s,data)
        return 12

def main():

    # 阻止angr自动载入并分析依赖的库函数
    p = angr.Project("r100",auto_load_libs=False)

    # hook printf函数，replace = True表示已经代替了之前的hook
    p.hook_symbol('printf',angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](),replace=True)

    # hook fgets函数
    p.hook_symbol('fgets',my_fgets(),replace=True)

    # blank_state 手动指定程序开始地址 addr是main函数的地址
    state = p.factory.blank_state(addr = 0x4007e8)

    simgr = p.factory.simulation_manager(state)
    
    simgr.explore(find=0x400844,avoid=0x400855)
   
    return simgr.found[0].posix.dumps(0).strip(b'\0\n') 
                                                        
                                                        

if __name__ == '__main__':
    time_start = time.time()
    print(main())
    time_end = time.time()
    print(time_end - time_start)

改进后的方法只用了1秒多！！

baby-re（DEFCON 2016 quals）

用ida分析，题目中是调用了12次scanf函数，将其存入到一个整形数组中，最后进入CheckSolution函数，CheckSolution非常巨大……

我们先来使用上一题种使用到的hook改进方法

1
2
# 阻止angr自动载入并分析依赖的库函数
p = angr.Project("./baby-re",auto_load_libs=False)

hook scanf函数

1
2
3
4
5
6
7
8
9
10
11
class my_scanf(angr.SimProcedure):

    # s是rdi寄存器指向的内存地址，用来存放输入数据
    def run(self,fmt,des):
        simfd = self.state.posix.get_fd(0)

        # read_data，存放4个字节即可
        data,real_size = simfd.read_data(4)
        self.state.memory.store(des,data)
        return 1
p.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)

遇到fflush和printf函数，就直接return

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

确定起始地址为main函数地址

1
state = p.factory.blank_state(addr = 0x4025E7)

确定寻找地址：

规避地址：

1
simgr.explore(find=0x4028E9,avoid=0x402941)

完整代码：

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
import angr
import time

class my_scanf(angr.SimProcedure):

    # s是rdi寄存器指向的内存地址，用来存放输入数据
    def run(self,fmt,des):
        simfd = self.state.posix.get_fd(0)

        # read_data，存放4个字节即可
        data,real_size = simfd.read_data(4)
        self.state.memory.store(des,data)
        return 1

def main():
    # 阻止angr自动载入并分析依赖的库函数
    p = angr.Project("./baby-re",auto_load_libs=False)

    state = p.factory.blank_state(addr = 0x4025E7)

    # 遇到printf函数和fflush函数，就直接return
    p.hook_symbol('printf', angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](), replace=True)
    p.hook_symbol('fflush', angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](), replace=True)

    p.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)

    simgr = p.factory.simulation_manager(state)


    simgr.explore(find=0x4028E9,avoid=0x402941)

    return simgr.found[0].posix.dumps(0)                
                                                        

if __name__ == '__main__':
    time_start = time.time()
    print(main())
    time_end = time.time()
    print(time_end - time_start)

这种方法跑出来花了100多秒

如何改进？

不运行时检查方法

在代码中加入

1
simgr.one_active.options.add(angr.options.LAZY_SOLVES)

速度提升是质的飞跃，只花了12秒！！

能否再提升效率呢？

scanf函数无法简单推断输入长度，所以有时候需要用claripy函数手动构造收入

导入claripy包来求解

完全可以把claripy当作z3来用，Claripy.BVS()可以直接创建符号变量，参数一为变量名，参数二为数据宽度（位数），

我们可以查看官方的代码：

1
2
3
4
5
6
7
8
# let's provide the exact variables received through the scanf so we don't have to worry about parsing stdin into a bunch of ints.
flag_chars = [claripy.BVS('flag_%d' % i, 32) for i in range(13)]
class my_scanf(angr.SimProcedure):
    def run(self, fmt, ptr): # pylint: disable=arguments-differ,unused-argument
        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)

我们可以通过以上的方式来创建用户的输入

但是这样的方式，我们不能再通过Dump标准输入来获得正确的输入

看看官方文档是怎么处理的：

1
2
3
# evaluate each of the flag chars against the constraints on the found state to construct the flag
flag = ''.join(chr(sm.one_found.solver.eval(c)) for c in flag_chars)
return flag

这边贴上官方代码：

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
#!/usr/bin/env python2
from __future__ import print_function

# Authors: David Manouchehri <manouchehri@protonmail.com>
#          P1kachu <p1kachu@lse.epita.fr>
#          Audrey Dutcher <audrey@rhelmot.io>
# DEFCON CTF Qualifier 2016
# Challenge: baby-re
# Write-up: http://hack.carleton.team/2016/05/21/defcon-ctf-qualifier-2016-baby-re/
# Runtime: ~15 seconds (thanks lazy solves!)

import angr
import claripy

def main():
    proj = angr.Project('./baby-re', auto_load_libs=False)

    # let's provide the exact variables received through the scanf so we don't have to worry about parsing stdin into a bunch of ints.
    flag_chars = [claripy.BVS('flag_%d' % i, 32) for i in range(13)]
    class my_scanf(angr.SimProcedure):
        def run(self, fmt, ptr): # pylint: disable=arguments-differ,unused-argument
            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)

    sm = proj.factory.simulation_manager()
    sm.one_active.options.add(angr.options.LAZY_SOLVES)
    sm.one_active.globals['scanf_count'] = 0

    # search for just before the printf("%c%c...")
    # If we get to 0x402941, "Wrong" is going to be printed out, so definitely avoid that.
    sm.explore(find=0x4028E9, avoid=0x402941)

    # evaluate each of the flag chars against the constraints on the found state to construct the flag
    flag = ''.join(chr(sm.one_found.solver.eval(c)) for c in flag_chars)
    return flag

def test():
    assert main() == 'Math is hard!'

if __name__ == '__main__':
    print(main())

惊呆我一整年，只用了9秒……

正想如何开了pie保护会怎样，没想到这样的例题就来了

sakura(Hitcon 2017)

在这一题中，开了pie保护

这个sub_850函数要把我的ida干翻了……

放大sub_850函数流程图，下面有很多类似的结构，都是给rbp+var_1E49赋值0的操作，只要是这种操作，都需要去规避，那我们就需要在程序运行时，将这些地址都添加到一个列表中，所以需要用到idc对其进行提取。

sub_850函数开始地址：

sub_850函数结束地址：

shift+F2，开启idc，选择idapython，在其中键入：

nullbook中是这样尝试的，但是我没有在idc库中找到NextHead()这个API

查看官方文档：

也就是用二进制方式读取数据，和nullbook中描述的类似

需要注意的是找到汇编指令的硬编码，用b’\xc6\x85\xB7\xE1\xFF\xFF\x00’代替即可

1
simgr.explore(find = (0x110CA+0x400000),avoid = avoids)

以下是总结nullbook和官方文档的脚本：

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
#!/usr/bin/env python2
from __future__ import print_function
import time
import hashlib
import angr

def main():
    e = open("./sakura",'rb').read()

    avoids = []
    index = 0
    while True:
        index = e.find(b'\xc6\x85\xB7\xE1\xFF\xFF\x00',index+1)
        if index == -1:
            break
        addr = 0x400000 + index
        avoids.append(addr)

    avoids.append(0x110EC+0x400000)  # 没有成功输出flag的位置

    proj = angr.Project('./sakura')

    state = proj.factory.entry_state()

    simgr = proj.factory.simulation_manager(state)

    simgr.one_active.options.add(angr.options.LAZY_SOLVES)

    simgr.explore(find = (0x110CA+0x400000),avoid = avoids)

    found = simgr.one_found
    
    text = found.solver.eval(found.memory.load(0x612040,400), cast_to=bytes)

    h = hashlib.sha256(text)
    flag = 'hitcon{'+h.hexdigest()+'}'
    return flag


if __name__ == '__main__':
    time_start = time.time()
    print(main())
    time_end = time.time()
    print(time_end - time_start)

运行结果：

当然nullbook书中介绍了更好的hook方法，以及跳过读取flag的步骤，将输入直接存放在内存中

2020虎符 enc (pe文件/单个函数angr执行)

主要的函数就两个，sub_441050和sub_4412A0

可以通过特征码或者插件得知sub_441050这个函数是md5加密算法

（这边主要想学习一下angr的知识）

通过大佬的神之动调，我们得知传入的v11的值为794c87696d24d16e7b9e3dddad778c93

下面sub_4012A0很复杂，这边贴上大佬的代码(orz)，学一下从单个函数开始的angr执行

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
from angr import *
from claripy import *

flag=BVS('flag',8*16) #flag的长度16字节 BVS创造输入
result=BVV(b'\xae\xed\x13\x5c\xbd\xd2\xa1\x74\x9c\x4c\x5e\x02\xd3\x28\x9b\x60',8*16) #创建变量
disasm=BVV(b'794c87696d24d16e7b9e3dddad778c93',8*32) #创建变量
p=Project('task.exe',auto_load_libs=False) #是否自动载入依赖的库
p.hook(0x405128,SIM_PROCEDURES['libc']['malloc']()) #hook SIM_PROCEDURES['模块名']['库函数名']
p.hook(0x4035e4,SIM_PROCEDURES['libc']['calloc']())
st=p.factory.full_init_state(addr=0x40154d,add_options={
    options.SYMBOLTC_WRITE_ADDRESSES,
options.REGION_MAPPING,options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}) #设置引擎

st.memory.store(st.regs.ebp - 0x24, flag) #传入参数
st.memory.store(st.regs.ebp - 0x54, disasm) #传入参数
sim = p.factory.simgr(st)  #模拟执行
sim.explore(find=0x401558) #正确的位置
f = sim.one_found
f.solver.add(f.memory.load(f.regs.ebp - 0x24, 16) == result) #添加约束条件
print(f.solver.eval(flag, cast_to=bytes)) #打印输入

#只模拟执行4012a0加密函数
  1. 是构造参数，

函数加密之后的结果就写入flag.txt.enc中了，所以我们用010查看

用claripy.BVV()函数来构造位向量值。一参是值，二参是位数

1
result=BVV(b'\xae\xed\x13\x5c\xbd\xd2\xa1\x74\x9c\x4c\x5e\x02\xd3\x28\x9b\x60',8*16)
  1. 构造flag值，claripy.BVS()可以直接创建位向量符号，就像z3中的BitVec一样一参为变量名，二参为位数。由上面的步骤，可以知道flag是16个字节的长度
1
flag=BVS('flag',8*16)
  1. hook一些没有帮助的函数
1
2
p.hook(0x405128,SIM_PROCEDURES['libc']['malloc']()) #hook SIM_PROCEDURES['模块名']['库函数名']
p.hook(0x4035e4,SIM_PROCEDURES['libc']['calloc']())

  1. 创建工程

    1
    2
    3
    st=p.factory.full_init_state(addr=0x40154d,add_options={
        options.SYMBOLTC_WRITE_ADDRESSES,
    options.REGION_MAPPING,options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}) #设置引擎

  2. 函数的参数传递，看ida就很清晰了

1
2
st.memory.store(st.regs.ebp - 0x24, flag) #传入参数二
st.memory.store(st.regs.ebp - 0x54, disasm) #传入参数一
  1. 模拟执行
1
sim = p.factory.simgr(st)  #模拟执行
  1. 确定寻找的地方（即下一条语句的开始点）
1
sim.explore(find=0x401558) #正确的位置
  1. 为出路 f 添加约束条件，结果要与flag.txt.enc文件中的内容一致
1
2
f = sim.one_found
f.solver.add(f.memory.load(f.regs.ebp - 0x24, 16) == result)

​ v11经过函数运算之后，值传递给了Buffer

  1. 输出flag
1
print(f.solver.eval(flag, cast_to=bytes)) #打印输入

佩服，五体投地……(orz)

CSCI-4968-MBE

crackme0x00a

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
import angr
import time

def main():

    congras=0x08048533
    wrong=0x08048554

    p = angr.Project("crackme0x00a", auto_load_libs=False)

    p.hook_symbol('printf', angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](), replace=True)

    state = p.factory.full_init_state()
    simgr = p.factory.simulation_manager(state)

    simgr.one_active.options.add(angr.options.LAZY_SOLVES)
    simgr.explore(find=congras, avoid=wrong)

    return simgr.found[0].posix.dumps(0).strip(b'\0\n')

if __name__ == '__main__':
    time_start = time.time()
    print(main())
    time_end = time.time()
    print(time_end - time_start)

# b'g00dJ0B!
# 1.2658519744873047

crackme0x01, crackme0x02,crackme0x03和以上类似

crackme0x04

直接看crackme0x04，以下是流程图

两重判断，官方文档中使用的是控制流图CFG()函数，去寻找exit函数的地址，自动识别正确的地址

1
FIND_ADDR = cfg.kb.functions.function(name="exit").addr
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
import angr
import time

def main():

    AVOID_ADDR = 0x080484fb

    p = angr.Project("crackme0x04", auto_load_libs=False)

    p.hook_symbol('_printf', angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](), replace=True)

    cfg = p.analyses.CFG()

    FIND_ADDR = cfg.kb.functions.function(name="exit").addr

    simgr = p.factory.simulation_manager()

    simgr.explore(find = FIND_ADDR,avoid = AVOID_ADDR)

    return simgr.found[0].posix.dumps(0)

if __name__ == '__main__':
    time_start = time.time()
    print(main())
    time_end = time.time()
    print(time_end - time_start)

crackme0x05

函数的意思，相当于三重判断

mian函数

check()函数

parell()函数

三重判断？看官方文档：

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
#!/usr/bin/env python2
# -*- coding: utf-8 -*-

# Author: David Manouchehri <manouchehri@protonmail.com>
# Modern Binary Exploitation
# http://security.cs.rpi.edu/courses/binexp-spring2015/

import angr
import subprocess

def main():
    proj = angr.Project('crackme0x05', load_options={"auto_load_libs": False})

#!/usr/bin/env python2
# -*- coding: utf-8 -*-

# Author: David Manouchehri <manouchehri@protonmail.com>
# Modern Binary Exploitation
# http://security.cs.rpi.edu/courses/binexp-spring2015/

import angr
import subprocess

def main():
    proj = angr.Project('crackme0x05', load_options={"auto_load_libs": False})

    def correct(state):
        try:
            return b'Password OK' in state.posix.dumps(1)
        except:
            return False

    def wrong(state):
        try:
            return b'Password Incorrect' in state.posix.dumps(1)
        except:
            return False

    sm = proj.factory.simulation_manager()
    sm.explore(find=correct, avoid=wrong)

    #print(sm.found[0].posix.dumps(1))
    return sm.found[0].posix.dumps(0) # .lstrip('+0').rstrip('B')

def test():
	# it SHOULD just be two numbers but the way angr models scanf means that it could technically be any number of formats
	# so we gotta check against ground truth
	with open('input', 'wb') as fp:
		fp.write(main())

	assert subprocess.check_output('./crackme0x05 < input', shell=True) == b'IOLI Crackme Level 0x05\nPassword: Password OK!\n'

if __name__ == '__main__':
		print(repr(main()))

这次官方文档给出的意思就是explore()函数中，传入的不是地址，也不是地址数组，而是函数

大概意思就是这个程序的输入是否存在目标字符串，贴上大佬的解释