angr-CTF符号执行
本帖最后由 Thunder_J 于 2019-5-10 20:18 编辑# 0x00：简介
符号执行简单来说就是用符号来模拟程序执行，在我看来就相当于暴力破解，比如一个程序要求你进行一个复杂的运算，每次动态调试只能输入一次，然而符合执行可以尽可能的遍历每一条路径，这样就方便了许多。
# 0x01：安装
这里不建议实体机安装，坑太多，直接上docker，[安装教程](https://blog.csdn.net/Sanky0u/article/details/81155964)
# 0x02：例题
## r100(defcamp)
[题目链接](http://whalectf.xin/challenges)
将程序载入IDA静态分析，主函数如下
```c
signed __int64 __fastcall main(__int64 a1, char **a2, char **a3)
{
signed __int64 result; // rax
char s; //
unsigned __int64 v5; //
v5 = __readfsqword(0x28u);
printf("Enter the password: ", a2, a3);
if ( !fgets(&s, 255, stdin) )
return 0LL;
if ( (unsigned int)sub_4006FD((__int64)&s) )
{
puts("Incorrect password!");
result = 1LL;
}
else
{
puts("Nice!");
result = 0LL;
}
return result;
}
```
加密函数如下，因为我们这里用符号执行来做，所以不进行算法分析
```c
signed __int64 __fastcall sub_4006FD(__int64 a1)
{
signed int i; //
const char *v3; //
const char *v4; //
const char *v5; //
v3 = "Dufhbmf";
v4 = "pG`imos";
v5 = "ewUglpt";
for ( i = 0; i <= 11; ++i )
{
if ( (&v3) - *(char *)(i + a1) != 1 )
return 1LL;
}
return 0LL;
}
```
我们需要知道的是，程序有两个分支，输入密码后会进行判断，正确输出nice，错误输入wrong，我们希望的是输出nice，那么这里就可以进行用符号执行来做，我们将题目文件拷贝到docker中后，直接写脚本如下，先直观感受一下脚本，我们希望执行0x400844中的内容，不希望执行0x400855的内容，脚本如下：
```python
import angr # 导入angr库
p=angr.Project('./r100',auto_load_libs=False) # 加载程序
state=p.factory.entry_state() # 创建一个状态,默认为程序的入口地址
simgr=p.factory.simgr(state) # 创建一个模拟器用来模拟程序执行,遍历所有路径
res=simgr.explore(find=0x400844,avoid=0x400855) # 约束执行的流程，0x400844为打印nice附近的地址，0x400855附近即为打印错误的地址
print (res.found.posix.dumps(0)) # 打印found的第一个结果
```
运行结果如下，可以爆破得到密码 'Code_Talkers' ：
```bash
(angr) angr@e223cdab7ce9:~$ python exp.py
WARNING | 2019-04-24 12:58:26,540 | angr.state_plugins.symbolic_memory | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | 2019-04-24 12:58:26,544 | angr.state_plugins.symbolic_memory | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | 2019-04-24 12:58:26,544 | angr.state_plugins.symbolic_memory | 1) setting a value to the initial state
WARNING | 2019-04-24 12:58:26,544 | angr.state_plugins.symbolic_memory | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | 2019-04-24 12:58:26,544 | angr.state_plugins.symbolic_memory | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY_REGISTERS}, to suppress these messages.
WARNING | 2019-04-24 12:58:26,546 | angr.state_plugins.symbolic_memory | Filling register r15 with 8 unconstrained bytes referenced from 0x400890 (PLT.ptrace+0x290 in r100 (0x400890))
WARNING | 2019-04-24 12:58:26,549 | angr.state_plugins.symbolic_memory | Filling register r14 with 8 unconstrained bytes referenced from 0x400895 (PLT.ptrace+0x295 in r100 (0x400895))
WARNING | 2019-04-24 12:58:26,552 | angr.state_plugins.symbolic_memory | Filling register r13 with 8 unconstrained bytes referenced from 0x40089a (PLT.ptrace+0x29a in r100 (0x40089a))
WARNING | 2019-04-24 12:58:26,555 | angr.state_plugins.symbolic_memory | Filling register r12 with 8 unconstrained bytes referenced from 0x40089f (PLT.ptrace+0x29f in r100 (0x40089f))
WARNING | 2019-04-24 12:58:26,563 | angr.state_plugins.symbolic_memory | Filling register rbx with 8 unconstrained bytes referenced from 0x4008b0 (PLT.ptrace+0x2b0 in r100 (0x4008b0))
WARNING | 2019-04-24 12:58:26,657 | angr.state_plugins.symbolic_memory | Filling register cc_ndep with 8 unconstrained bytes referenced from 0x400690 (PLT.ptrace+0x90 in r100 (0x400690))
'Code_Talkers\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\xf5\x00'
```
## crackme(ais3)
[题目链接](http://whalectf.xin/challenges)
同样载入IDA看主函数：
```c
int __cdecl main(int argc, const char **argv, const char **envp)
{
int result; // eax
if ( argc == 2 )
{
if ( (unsigned int)verify((__int64)argv) )
puts("Correct! that is the secret key!");
else
puts("I'm sorry, that's the wrong secret key!");
result = 0;
}
else
{
puts("You need to enter the secret key!");
result = -1;
}
return result;
}
```
程序流程还是和上一题很相似，只是需要我们输入正确的参数从而得到flag，加密函数如下，我们同样不需要分析它
```c
_BOOL8 __fastcall verify(__int64 a1)
{
int i; //
for ( i = 0; *(_BYTE *)(i + a1); ++i )
{
if ( encrypted != ((unsigned __int8)((unsigned __int8)(*(_BYTE *)(i + a1) ^ i) << ((i ^ 9) & 3)) | (unsigned __int8)((signed int)(unsigned __int8)(*(_BYTE *)(i + a1) ^ i) >> (8 - ((i ^ 9) & 3))))
+ 8 )
return 0LL;
}
return i == 23;
}
```
符号执行脚本如下：
```python
import angr
import claripy # 处理用户输入
proj = angr.Project('./ais3_crackme')
argv1 = claripy.BVS('argv1', 50*8) # 猜测flag长度小于50,乘8是转换为字节
state = proj.factory.entry_state(args=['./ais3_crackme',argv1]) # 传递状态
simgr = proj.factory.simgr(state)
res=simgr.explore(find = 0x400602, avoid=0x40060e)
print(hex（res.found.solver.eval(argv1)))
```
运行结果，我们只需要将答案转一次base16即可得到flag：
```bash
(angr) angr@e223cdab7ce9:~$ python exp2.py
WARNING | 2019-04-24 13:44:41,180 | angr.state_plugins.symbolic_memory | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | 2019-04-24 13:44:41,181 | angr.state_plugins.symbolic_memory | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | 2019-04-24 13:44:41,181 | angr.state_plugins.symbolic_memory | 1) setting a value to the initial state
WARNING | 2019-04-24 13:44:41,182 | angr.state_plugins.symbolic_memory | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | 2019-04-24 13:44:41,182 | angr.state_plugins.symbolic_memory | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY_REGISTERS}, to suppress these messages.
WARNING | 2019-04-24 13:44:41,183 | angr.state_plugins.symbolic_memory | Filling register r12 with 8 unconstrained bytes referenced from 0x400625 (__libc_csu_init+0x5 in ais3_crackme (0x400625))
WARNING | 2019-04-24 13:44:41,187 | angr.state_plugins.symbolic_memory | Filling register r13 with 8 unconstrained bytes referenced from 0x400638 (__libc_csu_init+0x18 in ais3_crackme (0x400638))
WARNING | 2019-04-24 13:44:41,196 | angr.state_plugins.symbolic_memory | Filling register r14 with 8 unconstrained bytes referenced from 0x40063d (__libc_csu_init+0x1d in ais3_crackme (0x40063d))
WARNING | 2019-04-24 13:44:41,203 | angr.state_plugins.symbolic_memory | Filling register r15 with 8 unconstrained bytes referenced from 0x400642 (__libc_csu_init+0x22 in ais3_crackme (0x400642))
WARNING | 2019-04-24 13:44:41,209 | angr.state_plugins.symbolic_memory | Filling register rbx with 8 unconstrained bytes referenced from 0x400647 (__libc_csu_init+0x27 in ais3_crackme (0x400647))
WARNING | 2019-04-24 13:44:41,364 | angr.state_plugins.symbolic_memory | Filling register cc_ndep with 8 unconstrained bytes referenced from 0x4004b0 (register_tm_clones+0x20 in ais3_crackme (0x4004b0))
0x616973337b495f74616b335f673030645f6e307433737d000000000000000000000000000000000000000000000000000000
```
转码后得到flag: ais3{I_tak3_g00d_n0t3s}
# 0x03：总结
符号执行相当于是往一个框架里填东西，想要执行什么，不想执行什么自己要很清楚，以后有这种题目直接套模板就行了。
页:
[1]