前言

让我们一起拨开云雾,玩转angr吧!
此篇将会讲解如何使用angr进行输入、输出以及条件约束

获取命令行输入

我以ais3_crackme为例,来说明如何进行命令行输入。

运行程序,提示如下:

载入IDA,逻辑同样的简单。

再上一篇也提到过,在angr==8.18.10.25版本中,需要通过claripy模块,来构造输入。claripy是一个符号求解引擎和z3类似,我们完全可以将其当成是z3进行使用。

claripy关于变量的定义在claripy.ast.bv.BV当中

通常使用claripy.BVS()创建位向量符号

使用claripy.BVV()创建位向量值

argv1 = claripy.BVS("argv1",100*8)

argv1是符号名称,100*8是长度以bit为单位,这里是输入了100个字节。

在设置初始SimgrState时可以进行如下设置
initial_state = p.factory.entry_state(args=["./ais3_crackme",argv1])

通常来说在做题时,flag的长度还是很好判断的。

之后初始化simulation_manager,设置find以及avoid

那么此时我们不能像之前那样通过posix.dump(0)来打印出结果,因为我们是通过命令行传参,输入的数据,那么此时使路径正确的数据保存在哪里呢?

我们需要继续查看SimState都由哪些属性。

之前也提到过claripy是类似于z3的符号执行引擎,所以可以看到solver属性

:ivar solver: The symbolic solver and variable manager for this state

同样的我们查看found.solver都有哪些属性和方法。

为了能正确的将found中保存的符号执行的结果打印出来,我们可以使用eval方法。

并且可以使用cast_to参数对需要打印的值进行类型转换

通常来说只要找到了找到了正确的路径,那么打印结果并不是太大的问题。

完整的脚本如下:

#!/usr/bin/env python


'''
ais3_crackme has been developed by Tyler Nighswander (tylerni7) for ais3.

It is an easy crackme challenge. It checks the command line argument.
'''

import angr
import claripy


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

    #create an initial state with a symbolic bit vector as argv1
    argv1 = claripy.BVS("argv1",100*8) #since we do not the length now, we just put 100 bytes
    initial_state = project.factory.entry_state(args=["./crackme1",argv1])

    #create a path group using the created initial state 
    sm = project.factory.simulation_manager(initial_state)

    #symbolically execute the program until we reach the wanted value of the instruction pointer
    sm.explore(find=0x400602) #at this instruction the binary will print(the "correct" message)

    found = sm.found[0]
    #ask to the symbolic solver to get the value of argv1 in the reached state as a string
    solution = found.solver.eval(argv1, cast_to=bytes)

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

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


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

正常输入并设置约束条件

这里我用上一篇刚开始用到的csaw_wyvern作为例题

IDA载入

首先映入眼帘的是C++程序,由于angr是只实现了C库,为了深入C++标准库中,我们需要在设置state时需要使用full_init_state方法,并且设置unicorn引擎。

通过IDA的分析以及猜测,基本上可以确定flag长度为28,因此我们构造长度为28的BVS变量,并在结尾加上\n

我们通过claripy构造输入变量

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

claripy.Concat方法用于bitVector的连接

而后在初始化state时设置stdin参数

st = p.factory.full_init_state(
            args=['./wyvern'],
            add_options=angr.options.unicorn,
            stdin=flag,
    )

add_options=angr.options.unicorn,是为了设置unicorn引擎

其实我们现在已经设置好了stateangr已经可以正常工作了,但是为了提高angr的执行效率,我们有必要进行条件约束。

设置起来并不麻烦。

for k in flag_chars:
        st.solver.add(k != 0)
        st.solver.add(k != 10)

而后便可以执行了。这里我先不设置find,直接通过run()方法运行,这样可以得到29个deadended分支。

这里有必要再说一下SimulationManager的三种运行方式:

step()每次向前运行一个基本块,并返回进行分类

run()运行完所有的基本块,然后会出现deadended的状态,此时我们通常访问最后一个状态来获取我们所需要的信息。

explore()根据findavoid进行基本块的执行,最后会返回foundavoid状态

一般来说我们使用explore()方法即可。

此时的flag应该就在这29个deadended分支中某个分支的stdout中,我们得想办法将其取出,通常来说是在最后一个分支当中。

当然我们还是通过代码将其取出。

out = b''
    for pp in sm.deadended:
        out = pp.posix.dumps(1)
        if b'flag{' in out:
            return out[out.find(b"flag{"):]

如果不用run()方法,而是通过explore()运行,也是可以的。
在IDA中找到最终正确的分支0x0x4037FD

如下设置:

最后在found[0].posix.dumps(0)打印出flag值,但在执行过程中,我明显感觉到CPU在飞速的旋转。(可能是电脑太渣,哈哈!)

ps:这道题我记得还可以用pintools解决,而且pizza大佬还写过一个去混淆的脚本,总之方法有很多,不过angr算是比较快速的一种。

对结果进行条件约束

对于angr来说,执行到正确的路径并不难,但对于我们来说,要想正确的打印出flag,恐怕还得飞一番功夫。

这里以asisctffinals2015_fake为例。

载入IDA

从题目来看,其大概逻辑是通过输入正确的值,经过计算,最后会输出由v5 v6 v7 v8 v9所组成的字符串,也就是flag。

就此题而言,仅仅设置BVS和find是远远不够的,我们需要对found状态下的memory,进行条件约束,从而打印出正确的flag。

我们跳过前面的命令行输入部分,直接从0x4004AC开始,因为strtol用于将字符串转化为整数,而我们通过claripy.BVS构造的符号变量是一个bit向量,无法使用strtol转换。当然如果你不闲麻烦,可以将strtolnop掉,然后使用之前所说的命令行传参的方法。

初始化状态如下设置:

state = p.factory.blank_state(addr=0x4004AC)
    inp = state.solver.BVS('inp', 8*8)
    state.regs.rax = inp

    simgr= p.factory.simulation_manager(state)
    simgr.explore(find=0x400684)
    found = simgr.found[0]

此时的状态是0x400684时,put将要打印edi寄存器的值.

为了对结果设置条件约束,我们需要如下设置:

flag_addr = found.regs.rdi
    found.add_constraints(found.memory.load(flag_addr, 5) == int(binascii.hexlify(b"ASIS{"), 16))

首先根据题目条件可以知道flag的长度应该为38(5+32+1)字节,并且的前5个字节是ASIS{,最后一个字节是}其余也都应该是可打印字符

这时可以进行如下约束:

flag = found.memory.load(flag_addr, 40)
    for i in range(5, 5+32):
        cond_0 = flag.get_byte(i) >= ord('0')
        cond_1 = flag.get_byte(i) <= ord('9')
        cond_2 = flag.get_byte(i) >= ord('a')
        cond_3 = flag.get_byte(i) <= ord('f')
        cond_4 = found.solver.And(cond_0, cond_1)
        cond_5 = found.solver.And(cond_2, cond_3)
        found.add_constraints(found.solver.Or(cond_4, cond_5))

    found.add_constraints(flag.get_byte(32+5) == ord('}'))

最后将结果通过eval输出即可.
flag_str = found.solver.eval(flag, cast_to=bytes)

总结

以上我们已经了解了如何使用angr进行输入输出以及条件约束,这就掌握angr的基本用法,接下来我们要继续深入,学会如何对内存以及寄存器进行直接的存取。

源链接

Hacking more

...