使用 Angr-Part I

Use angr - 1

安装 angr

在 Ubuntu 上，首先我们应该安装所有的编译所需要的依赖环境：

sudo apt install python-dev libffi-dev build-essential virtualenvwrapper

强烈建议在虚拟环境中安装 angr，因为有几个 angr 的依赖（比如 z3）是从他们的原始库中 fork 而来，如果你已经安装了 z3,那么你肯定不希望 angr 的依赖覆盖掉官方的共享库。

对于大多数*unix 系统，只需要 mkvirtualenv angr && pip install angr 安装 angr 就好了。

如果这样安装失败的话，那么可以按照这样的顺序：

1. claripy
2. archinfo
3. pyvex
4. cle
5. angr

从 angr 的官方仓库安装。

附安装方法：

git clone https://github.com/angr/claripy
cd claripy
sudo pip install -r requirements.txt
sudo python setup.py build
sudo python setup.py install

其他几个 angr 官方库的安装也是如此。

一些问题

如果在安装完成 angr 后，在 ipython 环境中有这样的报错：

Python 2.7.12 (default, Nov 19 2016, 06:48:10) 
Type "copyright", "credits" or "license" for more information.

IPython 2.4.1 -- An enhanced Interactive Python.
?         -> Introduction and overview of IPython's features.
%quickref -> Quick reference.
help      -> Python's own help system.
object?   -> Details about 'object', use 'object??' for extra details.

In [1]: import angr
---------------------------------------------------------------------------
ImportError                               Traceback (most recent call last)
<ipython-input-1-bcea9b74a356> in <module>()
----> 1 import angr

/root/angr/angr/__init__.pyc in <module>()
     23 from .state_plugins.inspect import BP
     24 
---> 25 from .project import *
     26 from .errors import *
     27 #from . import surveyors

/root/angr/angr/project.py in <module>()
    590 from .factory import AngrObjectFactory
    591 from .simos import SimOS, os_mapping
--> 592 from .analyses.analysis import Analyses
    593 from .surveyors import Surveyors
    594 from .knowledge_base import KnowledgeBase

/root/angr/angr/analyses/__init__.py in <module>()
     20 from .congruency_check import CongruencyCheck
     21 from .static_hooker import StaticHooker
---> 22 from .reassembler import Reassembler
     23 from .binary_optimizer import BinaryOptimizer
     24 from .disassembly import Disassembly

/root/angr/angr/analyses/reassembler.py in <module>()
      7 from itertools import count
      8 
----> 9 import capstone
     10 import cffi
     11 import cle

/usr/local/lib/python2.7/dist-packages/capstone/__init__.py in <module>()
      4 if _python2:
      5     range = xrange
----> 6 from . import arm, arm64, mips, ppc, sparc, systemz, x86, xcore
      7 
      8 __all__ = [

ImportError: cannot import name arm

可以看到，是 capstone 出现了问题。

解决这个问题的方法是重新安装 angr：

sudo pip install -I --no-use-wheel capstone

这样就能解决问题。

若是问题依然存在，那么请先卸载所有的 capstone：

   sudo pip3 uninstall capstone
    sudo pip uninstall capstone

然后从 pypi 源中获取最新版本安装：

wget https://pypi.python.org/packages/fd/33/d1fc2d01b85572b88c9b4c359f36f88f8c32f2f0b9ffb2d21cd41bad2257/capstone-3.0.5rc2-py2-none-manylinux1_x86_64.whl#md5=ecd7e1e39ea6dacf027c0cfe7eb1bf94
sudo pip2 install capstone-3.0.5rc2-py2-none-manylinux1_x86_64.whl

(如果 wget 这个安装包失败的话，你可以在 https://pypi.python.org/pypi/capstone/找到 capstone 最新的版本)

一点知识

首先，我们要知道 angr 这个二进制文件的分析框架是基于符号执行的一些理论。

这里有一份 PPT https://github.com/skyel1u/2017-summer-todos/blob/master/program-analysis/Program%20Analysis%20-%20Barrene%20Cheamario.pdf 比较了现有方法的优劣，值得一看。

这篇博客 http://ysc21.github.io/blog/2016-01-27-angr-script.html 里已经替我们整理好一些 angr 常用的方法(果断不要脸的引用过来)：

• Surveyors
• Path group
• Symbolic args
• Symbolic input
• Breakpoint
• Hook

Surveyors 和 Path Group 是做符号执行分析时候使用的方法，后四种则是一些辅助的方法。这几种方法我会慢慢补充用法。

Surveyors

实现符号执行的代码在第三行，个人感觉 surveyors.explorer 像是在遍历所有的程序运行的内存空间，可以使用 find=() 来找到某个内存地址，或是使用 avoid=() 来避免程序找到某个地址，或者进入死循环。使用 find 时候要注意，find 的地址必须是 basic block 的起始地址，否则 angr 并找不到该地址。

In [1]: import angr

In [2]: p=angr.Project('./angrybird')

In [3]: ex=p.surveyors.Ex
p.surveyors.Executor  p.surveyors.Explorer  

In [3]: ex=p.surveyors.Explorer(find=(0x404FBC,))

In [4]: ex.run
Out[4]: <bound method Explorer.run of <Explorer with paths: 1 active, 0 spilled, 0 deadended, 0 errored, 0 unconstrained, 0 found, 0 avoided, 0 deviating, 0 looping, 0 lost>>

In [5]: print ex.found[0].state.se._solver.result.model

line[5]是打印该地址的路径，也就是求出什么样子的输入会导致程序执行到那个地址上。

Path Group

这个方法和 surveyors 类似。这个方法的示例稍后补充。

一个例子

官方文档包含了大量的使用 angr 的例子，这里用一个最简单的一道 RE 题来检验 angr 的威力。

这里是一个简单的使用符号执行去获取一道 CTF 赛题的 flag：

• 使用 angr：

我们只需要知道程序输出 correct 的内存地址即可：

#!/usr/bin/env python
import angr
import claripy

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

    #通过BVS建立符号执行的初始状态，将它设置成 argv1
    argv1 = claripy.BVS("argv1",100*8) #由于我们不知道命令行参数的长度，先设置成 100bytes
    initial_state = project.factory.entry_state(args=["./ais3_crackme",argv1])

    #通过已经建立的初始状态来创建 path group 
    sm = project.factory.simgr(initial_state)

    #对这个程序进行符号执行的分析我们将会得到我们想要字符串的指令指针（即内存地址）
    sm.explore(find=0x400602) #这条指令将使二进制文件打印出“correct”的信息，注意上图

    found = sm.found[0]
    #查询 symbolic solver 已达到的状态来获取argv1的值作为字符串
    solution = found.se.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}" # flag

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

执行脚本，可以得到执行结果：

root@ubuntu ~# python solve.py 
'ais3{I_tak3_g00d_n0t3s}\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
ais3{I_tak3_g00d_n0t3s}
Total used 14.6215708256s.
'ais3{I_tak3_g00d_n0t3s}'

大约 15s 左右便可以得到结果。

如果比较熟悉 angr，这道简单的 RE 题目我们可以在 5 分钟之内做出来，由此可见 angr 的威力。

• 常规 RE:

把这题目拖到 IDA 里瞅瞅。

$ file ais3_crackme
ais3_crackme: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.24, BuildID[sha1]=248bcf6d61edeea95745e24b7e4c413c953db1e5, not stripped, with debug_info

64 位 ELF 文件，动态链接，没有去除符号表和 debug 信息。

程序流程不算太难，main 函数 F5 之后如下，运行需要获取一个命令行参数，双击跟进 verify 函数：

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

  if ( argc == 2 )
  {
    if ( verify(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;
}

下面这个是 verify 函数，输入是我们的命令行参数即 a1，encrypted[24]是加密后的字符串，这个算法就是检验我们的输入经过解密后和程序中储存的字符串是否相等：

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

  for ( i = 0; *(i + a1); ++i )
  {
    if ( encrypted[i] != (((*(i + a1) ^ i) << ((i ^ 9) & 3)) | ((*(i + a1) ^ i) >> (8 - ((i ^ 9) & 3)))) + 8 )
      return 0LL;
  }
  return i == 23;
}

encrypted[24]字符串：

.data:0000000000601020 ; char encrypted[24]
.data:0000000000601020 encrypted       db 0CAh                 ; DATA XREF: verify+6A↑r
.data:0000000000601021                 db  70h ; p
.data:0000000000601022                 db  93h
.data:0000000000601023                 db 0C8h
.data:0000000000601024                 db    6
.data:0000000000601025                 db  54h ; T
.data:0000000000601026                 db 0D2h
.data:0000000000601027                 db 0D5h
.data:0000000000601028                 db 0DAh
.data:0000000000601029                 db  6Ah ; j
.data:000000000060102A                 db 0D1h
.data:000000000060102B                 db  59h ; Y
.data:000000000060102C                 db 0DEh
.data:000000000060102D                 db  45h ; E
.data:000000000060102E                 db 0F9h
.data:000000000060102F                 db 0B5h
.data:0000000000601030                 db 0A6h
.data:0000000000601031                 db  87h
.data:0000000000601032                 db  19h
.data:0000000000601033                 db 0A5h
.data:0000000000601034                 db  56h ; V
.data:0000000000601035                 db  6Eh ; n
.data:0000000000601036                 db  63h ; c
.data:0000000000601037                 db    0
.data:0000000000601037 _data           ends

经过以上分析，我们可以用 Python 写出来一个 keygen：

#!/usr/bin/env python3
from z3 import *

b = [ BitVec('b%d' % i, 32) for i in range(24)]
s = Solver()

cmparr = [ 0xca,0x70,0x93,0xc8,0x06,0x54,0xd2,0xd5,0xda,0x6a,0xd1,0x59,0xde,0x45,0xf9,0xb5,0xa6,0x87,0x19,0xa5,0x56,0x6e,0x63,00]
print(len(cmparr))
for i in range(24):
    tempChr = ((b[i] ^ i) << ((i ^ 9) & 3)) &0xff | ((b[i] ^ i)  >> (8 - ((i ^ 9) & 3)))
    s.add((cmparr[i] & 0xff) == tempChr +8)

print(s.check())
 
m = s.model()

res = ""
for i in range(24):
        g = m[b[i]]
        inta = int(str(g))
        res += chr(inta & 0xff)
 
print("Key is %s" % res)

总体来看，学习使用 z3 库的时间大约半个小时，逆向分析并写出脚本&调试用时半个小时左右，主要时间并不是花费在分析程序逻辑上，当然也和我自己的编程能力太菜有关。

我把这个题目发给 @notwolf 去做，他使用传统分析方法去逆向这个程序，并且使用 C 语言写了 keygen:

unsigned char ida[] =
{
  202, 112, 147, 200,   6,  84, 210, 213, 218, 106, 
  209,  89, 222,  69, 249, 181, 166, 135,  25, 165, 
   86, 110,  99
};
int main(void)
{

int i;
for(i=0;i<23;++i)
{
switch(i%4)
{
case(0):
{
printf("%c",(((ida[i]-8)<<7)|(ida[i]-8)>>1)^i);
break;
		}

case (1):
{
	printf("%c",((ida[i]-8)<<8|((ida[i]-8)>>0))^i);

	break;
	}
case (2):
{
	printf("%c",((ida[i]-8)<<5)|(((ida[i]-8)>>3)^i));
	break;
}
case(3):
{
	printf("%c",((ida[i]-8)<<6)|((ida[i]-8)>>2)^i);
	break;
}
}
}

return 0;
}

他花费的时间大约一个小时左右。

这只是一个最基础的逆向题目，通常会出现在入门级 CTF 的 RE 类的第一道题目或者第二道题目中。如果程序流程更加复杂的话，传统 RE 的分析方法只能去人工花费大量时间去理顺程序流程，接着再去花费时间写 keygen，就一般情况来看，和自动化分析所费时间相比起来，一般的逆向分析方法花费的时间只会更多。

以上就是我在刚刚学习 angr 使用的一些思考，欢迎指正。