逆向小工具


拿到binary时的步骤:

  • file
  • strings
  • ltrace/strace
  • gdb/OD
  • IDA

angr

符号执行

符号执行 (Symbolic Execution)是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时,该程序会使用符号值作为输入,而非一般执行程序时使用的具体值。在达到目标代码时,分析器可以得到相应的路径约束,然后通过约束求解器来得到可以触发目标代码的具体值。 符号模拟技术(symbolic simulation)则把类似的思想用于硬件分析。符号计算(Symbolic computation)则用于数学表达式分析。

angr简介

angr是一个多架构的二进制分析平台,具备对二进制文件的动态符号执行能力和多种静态分析能力。 angr的简要过程:

  • 将二进制程序载入angr分析系统
  • 将二进制程序转换成中间件语言(intermediate representation, IR)
  • 将IR语言转换成语义较强的表达形式,比如,这个程序做了什么,而不是它是什么。
  • 执行进一步的分析,比如,完整的或者部分的静态分析(依赖关系分析,程序分块)、程序空间的符号执行探索(挖掘溢出漏洞)、一些对于上面方式的结合。
    # 不需要命令行参数的情况

    import angr     # 导入angr库

    proj = angr.Project('./binary',auto_load_libs=False)        # 参数auto_load_libs设置是否载入动态连接库
    state = proj.factory.entry_state()        # 读取入口点的状态
    simgr = proj.factory.simgr(state)       # 载入状态

    simgr.explore(find=0xaaaa,avoid=0xbbbb)     # 查找路径,find参数表示要达到目的正确路径,avoid参数表示要避免的路径
    # example Out: <SimulationManager with 2 active, 1 found, 12 avoid>

    simgr.found[0].posix.dumps(0)   # 得到的结果是列表,只有一个结果时即第一个元素:found[0]


    # 需要命令行参数的情况

    import angr
    import claripy      # angr中的一个求解器引擎

    proj = angr.Project('./binary',auto_load_libs=False)
    argv1 = claripy.BVS('argv1',50*8)       # BVS为字节对象,其中第一个参数为参数名,第二个参数为字符个数(一般每8bit为一个英文字符,这里设置50个字符长度)整个语句用于生成程序的参数(符号集)

    state = proj.factory.entry_state(args=['./binary',arvg1])       # 读取程序入口点状态,并传入构造好的参数(符号集)

    simgr = proj.factory.simgr(state)

    simgr.explore(find=0xaaaa,avoid=0xbbbb)
    # example Out: <SimulationManager with 3 active, 1 found, 46 avoid>

    print simgr.found[0].solver.eval(argv1)     # 得到的结果为bit类型,利用sovler.eval转化为ascii码对应的十六进制数

    print simgr.found[0].solver.eval(argv1cast_to=str)    # 通过设置参数cast_to使结果变为字符串

z3

Z3 is a theorem prover from Microsoft Research Z3 is a Satisfaiability Modulo Thories(SMT) solver

z3 Types

  • BitVec:指特定大小的数据类型
    • BitVec(“x”,32)对应c语言中的int
    • BitVec(“x”,8)对应c语言中的char
  • Int(整型)
  • Real(实数)
  • Bool(布尔值)
  • Array
  • ……

Tips

  • z3中没有signed/unsigned类型
  • 使用<,<=,>=,/,/%,»操作signed类型变量
  • 使用ULT,ULE,UGT,UGE,UDIV,Uremand,LShR操作unsigned类型变量
  • 将BitVec的大小设成运算过程中最大的

模板

    from z3 import *
    inputs = [BitVec('inputs_%d'%i,8)for i in range(32)]    # char inputs[32]

    s = Solver()
    s.add(...)
    if s.check()!=sat:      # check检查是否有解,有解时返回结果sat
        print 'unsat'       # check检查无解时返回结果unsat
    else:
        m = s.modle()
        print m
        print repr("".join([chr(m[inputs[i]].as_long()) for i in range(32)]))
        # repr方法用于返回一个string格式

例子:

    // Soup Meat Tea (SMT) (TM)
    //
    // We welcome you to our delicious kitchen featuring many dishes from all
    // around the world. With so many choices we really don't know the perfect
    // combination. Fortunately our previous chef left the best set of dishes for
    // a table of 8 people. Can you reconstruct the set of dishes?
    //
    // The service provided by our last chef can be found at.. find the ip/port
    // as if it's a stego001 challenge :-)
    //
    // Compile with:    gcc -std=c99 soup_meat_tea.c -o soup_meat_tea
    // Test with:       echo -n $'... payload ...'|./soup_meat_tea

    #include <stdio.h>
    #include <stdint.h>
    #include <stdlib.h>
    #include <unistd.h>

    uint32_t state = 42;

    typedef enum {
        D_SOUP_CHICKEN,
        D_SOUP_MEAT,
        D_SOUP_NAZI,
        D_CHICKEN_RAW,
        D_CHICKEN_BLACK,
        D_MEAT_BLACKANGUS,
        D_MEAT_WAGYU,
        D_MEAT_HORSE,
        D_TIRAMISU,
        D_ICE_BANANA,
        D_ICE_STRAWBERRY,
        D_OVERFLOW,
    } dish_t;

    const char *dishes[] = {
        "soup-chicken", "soup-meat", "soup-nazi", "chicken-raw", "chicken-black",
        "meat-blackangus", "meat-wagyu", "meat-horse", "tiramisu", "ice-banana",
        "ice-strawberry",
    };

    void dish(uint8_t d)
    {
        state = ((state + d) * 3294782) ^ 3159238819;
    }

    int main()
    {
        uint8_t input[32];
        read(0, input, 32);

        for (uint32_t idx = 0; idx < 32; idx++) {
            dish(input[idx]);
        }

        printf("That's some delicious.. ");
        for (uint32_t idx = 0; idx < 32; idx++) {
            if(input[idx] < D_OVERFLOW) {
                printf("%s ", dishes[input[idx]]);
            }
            else {
                printf("%s ", "<YUEATTHIS>");
            }
        }

        if(state == 0xde11c105) {
            system("/bin/cat flag.txt");
        }
        return 0;
    }

z3求解:

    from z3 import *

    state = 42
    def dish(d):
        global state
        state = ((state + d) * 3294782) ^ 3159238819
    inputs = [BitVec('inputs_%d'%i,8) for i in range(32)]
    for idx in range(32):
        dish(inputs[idx])
    s = Solver()
    for i in range(32):
        s.add(inputs[i]>=0,inputs[i]<=0xff>)
    s.add(state == 0xde11c105)
    if s.check() == sat:
        m = s.model()
        print m
        print repr("".join([chr(m[inputs[i]].as_long()) for i in range(32)]))