Python的二进制分析框架angr

作为一个 Web 狗有时候简单的逆向或者苦力活还是可以做做的，但是本着能白嫖不自己干为主的精神，发现了 angr，记录一下一些简单的应用。

官方Github地址

安装(基于Kali 64)

安装 virtualenv

pip install virtualenv

创建目录

mkdir angr_enviroment && cd angr_enviroment/

创建独立运行的python运行环境

命名为 venv:(因为安装angr的时候总是会因为python环境问题出现各种错误）

virtualenv –no-site-packages venv

创建一个独立的python运行环境，我们还加上了一个参数--no-site-packages,这样已经安装到当前系统的所有第三方包都不会复制过来，我们就得到了一个不带任何第三方包的“干净”的python运行环境。新建的python环境被放到了当前目录下的venv目录，有了venv这个python环境，可以用source进入该环境

进入对应的环境

source venv/bin/activate

就可以正常安装各种第三方包，并运行python命令，在venv环境下，用pip安装的包都会被安装到venv这个环境下，系统python环境不受任何影响，也就是说,venv环境是专门针对anger_enviroment这个应用创建的。

安装angr

pip install angr

退出当前venv环境

使用deactive命令：deactive，这个时候会回到正常的环境。

对于简单的二进制程序验证的计算

环境：Kali Linux 2019.3，Python 2.7

以自己写的 elf 为例，代码如下：

#include <stdio.h>
#include <string.h>
// wust{i_l0ve_y0u}
int main()
{
	char buf[35];

	printf("input your flag\n");
	scanf("%s", buf);
	for (int i = 0; i < strlen(buf); ++i)
	{
		buf[i] ^= 0xe;
	}

	if (!strcmp(buf,"y{}zugQb>xkQw>{s"))
	{
		printf("Congratulations!\n");
	}else{
		printf("go out\n");
	}

	return 0;
}

我们首先用 IDA 分析一下程序，可以看到，对输入进行一顿计算后(异或0xe)，与字符串对比，如果正确的话即输出 Congratulations!。

于是我们可以用脚本进行自动化分析计算，看看怎样输入才能达到输出 Congratulations!的目的。

脚本：

import angr

proj = angr.Project("xor")
simgr = proj.factory.simgr()
simgr.explore(find=lambda s: b"Congratulations!" in s.posix.dumps(1))
print(simgr.found[0].posix.dumps(0))

运行结果:

解决 CTF 中的题目

CSAW CTF 2015 Quals - Reversing 500, “wyvern”

Binary File in Here

exp:

#!/usr/bin/env python
# coding: utf-8
import angr
import claripy
import time

def main():
    # Load the binary. This is a 64-bit C++ binary, pretty heavily obfuscated.
    # its correct emulation by angr depends heavily on the libraries it is loaded with,
    # so if this script fails, try copying to this dir the .so files from our binaries repo:
    # https://github.com/angr/binaries/tree/master/tests/x86_64
    p = angr.Project('wyvern')

    # It's reasonably easy to tell from looking at the program in IDA that the key will
    # be 29 bytes long, and the last byte is a newline. Let's construct a value of several
    # symbols that we can add constraints on once we have a state.

    flag_chars = [claripy.BVS('flag_%d' % i, 8) for i in range(28)]
    flag = claripy.Concat(*flag_chars + [claripy.BVV(b'\n')])

    # This block constructs the initial program state for analysis.
    # Because we're going to have to step deep into the C++ standard libraries
    # for this to work, we need to run everyone's initializers. The full_init_state
    # will do that. In order to do this peformantly, we will use the unicorn engine!
    st = p.factory.full_init_state(
            args=['./wyvern'],
            add_options=angr.options.unicorn,
            stdin=flag,
    )

    # Constrain the first 28 bytes to be non-null and non-newline:
    for k in flag_chars:
        st.solver.add(k != 0)
        st.solver.add(k != 10)

    # Construct a SimulationManager to perform symbolic execution.
    # Step until there is nothing left to be stepped.
    sm = p.factory.simulation_manager(st)
    sm.run()

    # Get the stdout of every path that reached an exit syscall. The flag should be in one of these!
    out = b''
    for pp in sm.deadended:
        out = pp.posix.dumps(1)
        if b'flag{' in out:
            return next(filter(lambda s: b'flag{' in s, out.split()))

    # Runs in about 15 minutes!

def test():
    assert main() == b'flag{dr4g0n_or_p4tric1an_it5_LLVM}'

if __name__ == "__main__":
    before = time.time()
    print(main())
    after = time.time()
    print("Time elapsed: {}".format(after - before))

如何使用 angr 解决 CTF 的题目，详细参考官方文档的例子：

Examples using angr to solve CTF challenges

挖坑 TO-DO

To be continue…