angr-CTF符号执行

Thunder_J

0x00：简介

符号执行简单来说就是用符号来模拟程序执行，在我看来就相当于暴力破解，比如一个程序要求你进行一个复杂的运算，每次动态调试只能输入一次，然而符合执行可以尽可能的遍历每一条路径，这样就方便了许多。

0x01：安装

这里不建议实体机安装，坑太多，直接上docker，安装教程

0x02：例题

r100(defcamp)

题目链接

将程序载入IDA静态分析，主函数如下

 signed __int64 __fastcall main(__int64 a1, char **a2, char **a3)
{
  signed __int64 result; // rax
  char s; // [rsp+0h] [rbp-110h]
  unsigned __int64 v5; // [rsp+108h] [rbp-8h]

  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;
}

加密函数如下，因为我们这里用符号执行来做，所以不进行算法分析

signed __int64 __fastcall sub_4006FD(__int64 a1)
{
  signed int i; // [rsp+14h] [rbp-24h]
  const char *v3; // [rsp+18h] [rbp-20h]
  const char *v4; // [rsp+20h] [rbp-18h]
  const char *v5; // [rsp+28h] [rbp-10h]

  v3 = "Dufhbmf";
  v4 = "pG`imos";
  v5 = "ewUglpt";
  for ( i = 0; i <= 11; ++i )
  {
    if ( (&v3)[i % 3][2 * (i / 3)] - *(char *)(i + a1) != 1 )
      return 1LL;
  }
  return 0LL;
}

我们需要知道的是，程序有两个分支，输入密码后会进行判断，正确输出nice，错误输入wrong，我们希望的是输出nice，那么这里就可以进行用符号执行来做，我们将题目文件拷贝到docker中后，直接写脚本如下，先直观感受一下脚本，我们希望执行0x400844中的内容，不希望执行0x400855的内容，脚本如下：

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[0].posix.dumps(0)) # 打印found的第一个结果

运行结果如下，可以爆破得到密码 'Code_Talkers' ：

(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)

题目链接

同样载入IDA看主函数：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  int result; // eax

  if ( argc == 2 )
  {
    if ( (unsigned int)verify((__int64)argv[1]) )
      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，加密函数如下，我们同样不需要分析它

_BOOL8 __fastcall verify(__int64 a1)
{
  int i; // [rsp+14h] [rbp-4h]

  for ( i = 0; *(_BYTE *)(i + a1); ++i )
  {
    if ( encrypted[i] != ((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;
}

符号执行脚本如下：

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[0].solver.eval(argv1)))

运行结果，我们只需要将答案转一次base16即可得到flag：

(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：总结

符号执行相当于是往一个框架里填东西，想要执行什么，不想执行什么自己要很清楚，以后有这种题目直接套模板就行了。