angr符号执行

简介

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

安装

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

例题

r100(defcamp)

题目和脚本docker里面都有,将程序载入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，那么这里就可以进行用符号执行来做。先直观感受一下脚本，我们希望执行0x400844中的内容，不希望执行0x400855的内容，脚本如下：

import angr

def main():
    p = angr.Project("r100", load_options={'auto_load_libs': False}) # 加载程序
	#约束执行的流程，0x400844为打印nice附近的地址，0x400855附近即为打印错误的地址
    ex = p.surveyors.Explorer(find=(0x400844, ), avoid=(0x400855,)) 
    ex.run() 

    return ex.found[0].posix.dumps(0).strip('\0\n') # 打印found的第一个结果

def test():
    assert main() == 'Code_Talkers'

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

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  #处理用户输入


def main():
    project = angr.Project("./ais3_crackme")

    argv1 = claripy.BVS("argv1",100*8) #猜测flag长度小于100,乘8是转换为字节
    initial_state = project.factory.entry_state(args=["./crackme1",argv1]) # 传递参数

    sm = project.factory.simulation_manager(initial_state)

    #象征性地执行程序，直到达到指令指针的要求值
    sm.explore(find=0x400602) #在这个指令程序将打印“正确的”消息

    found = sm.found[0]
    #请求符号解算程序以字符串的形式获取处于到达状态的argv1的值
    solution = found.solver.eval(argv1, cast_to=str)

    print repr(solution)
    solution = solution[:solution.find("\x00")]
    print solution
    return solution

def test():
    res = main()
    assert res == "ais3{I_tak3_g00d_n0t3s}"


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