学习一下angr符号执行…
符号执行
基本概念
符号执行 (Symbolic Execution)是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。
使用符号执行分析一个程序时,该程序会使用符号值作为输入,而非一般执行程序时使用的具体值。在达到目标代码时,分析器可以得到相应的路径约束,然后通过约束求解器来得到可以触发目标代码的具体值。
符号执行技术是一种白盒的静态分析技术。即,分析程序可能的输入需要能够获取到目标源代码的支持。同时,它是静态的,因为并没有实际的执行程序本身,而是分析程序的执行路径。
python虚拟环境
在windows和linux中我都装的是anaconda来配置python虚拟环境。建议搭配pycharm使用
常用命令:
1 | # 创建一个名为py38的python3.8版本的虚拟环境: |
用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 | import angr |
官方给出的脚本跑了3秒多
hook函数改进方法
以下是nullbook书中给出的改进算法
1 | import angr |
改进后的方法只用了1秒多!!
baby-re(DEFCON 2016 quals)
用ida分析,题目中是调用了12次scanf函数,将其存入到一个整形数组中,最后进入CheckSolution函数,CheckSolution非常巨大……
我们先来使用上一题种使用到的hook改进方法
1 | # 阻止angr自动载入并分析依赖的库函数 |
hook scanf函数
1 | class my_scanf(angr.SimProcedure): |
遇到fflush和printf函数,就直接return
1 | p.hook_symbol('printf', angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'](), replace=True) |
确定起始地址为main函数地址
1 | state = p.factory.blank_state(addr = 0x4025E7) |
确定寻找地址:
规避地址:
1 | simgr.explore(find=0x4028E9,avoid=0x402941) |
完整代码:
1 | import angr |
这种方法跑出来花了100多秒
如何改进?
不运行时检查方法
在代码中加入
1 | simgr.one_active.options.add(angr.options.LAZY_SOLVES) |
速度提升是质的飞跃,只花了12秒!!
能否再提升效率呢?
scanf函数无法简单推断输入长度,所以有时候需要用claripy函数手动构造收入
导入claripy包来求解
完全可以把claripy当作z3来用,Claripy.BVS()可以直接创建符号变量,参数一为变量名,参数二为数据宽度(位数),
我们可以查看官方的代码:
1 | # 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. |
我们可以通过以上的方式来创建用户的输入
但是这样的方式,我们不能再通过Dump标准输入来获得正确的输入
看看官方文档是怎么处理的:
1 | # evaluate each of the flag chars against the constraints on the found state to construct the flag |
这边贴上官方代码:
1 | #!/usr/bin/env python2 |
惊呆我一整年,只用了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 | #!/usr/bin/env python2 |
运行结果:
当然nullbook书中介绍了更好的hook方法,以及跳过读取flag的步骤,将输入直接存放在内存中
2020虎符 enc (pe文件/单个函数angr执行)
主要的函数就两个,sub_441050和sub_4412A0
可以通过特征码或者插件得知sub_441050这个函数是md5加密算法
(这边主要想学习一下angr的知识)
通过大佬的神之动调,我们得知传入的v11的值为794c87696d24d16e7b9e3dddad778c93
下面sub_4012A0很复杂,这边贴上大佬的代码(orz),学一下从单个函数开始的angr执行
1 | from angr import * |
- 是构造参数,
函数加密之后的结果就写入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) |
- 构造flag值,claripy.BVS()可以直接创建位向量符号,就像z3中的BitVec一样一参为变量名,二参为位数。由上面的步骤,可以知道flag是16个字节的长度
1 | flag=BVS('flag',8*16) |
- hook一些没有帮助的函数
1 | p.hook(0x405128,SIM_PROCEDURES['libc']['malloc']()) #hook SIM_PROCEDURES['模块名']['库函数名'] |
创建工程
1
2
3st=p.factory.full_init_state(addr=0x40154d,add_options={
options.SYMBOLTC_WRITE_ADDRESSES,
options.REGION_MAPPING,options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}) #设置引擎函数的参数传递,看ida就很清晰了
1 | st.memory.store(st.regs.ebp - 0x24, flag) #传入参数二 |
- 模拟执行
1 | sim = p.factory.simgr(st) #模拟执行 |
- 确定寻找的地方(即下一条语句的开始点)
1 | sim.explore(find=0x401558) #正确的位置 |
- 为出路 f 添加约束条件,结果要与flag.txt.enc文件中的内容一致
1 | f = sim.one_found |
v11经过函数运算之后,值传递给了Buffer
- 输出flag
1 | print(f.solver.eval(flag, cast_to=bytes)) #打印输入 |
佩服,五体投地……(orz)
CSCI-4968-MBE
crackme0x00a
1 | import angr |
crackme0x01, crackme0x02,crackme0x03和以上类似
crackme0x04
直接看crackme0x04,以下是流程图
两重判断,官方文档中使用的是控制流图CFG()函数,去寻找exit函数的地址,自动识别正确的地址
1 | FIND_ADDR = cfg.kb.functions.function(name="exit").addr |
1 | import angr |
crackme0x05
函数的意思,相当于三重判断
mian函数
check()函数
parell()函数
三重判断?看官方文档:
1 | #!/usr/bin/env python2 |
这次官方文档给出的意思就是explore()函数中,传入的不是地址,也不是地址数组,而是函数
大概意思就是这个程序的输入是否存在目标字符串,贴上大佬的解释