DDCTF2018 Reverse writeup

baby_mips

花了一天，终于写完了

这是一道mips指令集的逆向题。
关于mips架构 https://zh.wikipedia.org/wiki/MIPS%E6%9E%B6%E6%A7%8B

初步尝试

在ubuntu运行
./baby_mips

会让输入16个值,然后提示非法指令

在IDA中分析一下

IDA分析

进入IDA首先就是搜索字符串
显而易见

图形化分析这里

可以看出是一个简单的条件判断

如果你以为F5看算法写脚本就结束，那就too native了

使用qemu模拟器动态调试

baby_mips是MIPS指令集上的程序，IDA只能静态分析，不能debug。采取的方法是在linux机上安装qemu模拟器，利用qemu来运行MIPS指令程序。

因此，首先当然是在ubuntu上安装qemu模拟器了
sudo apt-get install qemu
就可以了

qemu可以模拟很多指令集

关于用法，最简单的
qemu-你需要的指令集文件名

如果要利用IDA调试(IDA远程调试)
qemu-你需要的指令集 -g 端口文件名
原理：qemu -g port指令开启一个gdbserver。port另一端可以由IDA或gdb连接调试。

运行以后在IDA

选GDB调试，点左边绿色的RUN

确定

确定

下面我们需要输入的是Hostname和Port，如果你是在运行qemu的系统里运行IDA，Hostname就填127.0.0.1，要是别的系统，比如你用的是虚拟机，就填运行qume的系统的IP,Port就填刚刚qemu里设置好的就行。(这些是常识了)

然后确认IDA就可以动态调试了

经过尝试，这里的baby_mips是mips小字端程序，所以我们运行指令
qemu-mipsel -g 6666 baby_mips
然后IDA点确定


成功了

我们运行程序，输入16个数，弹出一个错

程序停在了00400430，并且这里的指令是以EB02开头的

往下翻翻，发现非常多的EB02，然后下面的指令就不被识别了

IDA有一个强大的插件

keypatch —–http://www.keystone-engine.org/keypatch/

可以用这个插件把第一个EB02 NOP ，然后运行的话会发现又在下一个EB02报错，所以应该就是EB02的问题了

至于原理，参阅了很多篇wp，大概就是

查找lwc1指令的含义，发现是与协处理器相关的指令。通过对后面的代码块进行分析发现，后面并没有用到$f29和$t1寄存器的内容

指令的头两个字节为 \xEB\x02 ，且在x86指令集中 \xEB 为跳转指令。

把操作码反汇编成汇编代码后发现第一条指令是 jmp 0x4 ，刚好MIPS指令集每条指令大小为4字节。

猜测程序让我们遇到这个指令就跳转四字节

于是现在的思路就是将所有EB02开头的指令nop

由于MIPS指令是定长的，均为4个字节。因此，可以在选定的代码块中，将所有以EB 02开始的4字节数据全部替换成00 00 00 00，在MIPS指令中，nop对应的机器码为00 00 00 00

需要固定监测指令的头部，是因为可能会误清除掉正常指令

使用脚本去除EB02指令

下面是各位大佬写的IDC或IDPython脚本，功能都是去除EB02指令

来自‘奈沙夜影’

Code

#include <idc.idc>

static matchBytes(StartAddr, Match) 
{ 
    auto Len, i, PatSub, SrcSub; 
    Len = strlen(Match);

    while (i < Len) 
    { 
       PatSub = substr(Match, i, i+1); 
       SrcSub = form("%02X", Byte(StartAddr)); 
       SrcSub = substr(SrcSub, i % 2, (i % 2) + 1); 

       if (PatSub != "?" && PatSub != SrcSub) 
       { 
        return 0; 
       } 

       if (i % 2 == 1) 
       { 
        StartAddr++; 
       } 
       i++; 
    }
    return 1; 
}


static main() 
{ 
   auto StartVa, SavedStartVa, StopVa, Size, i, j;

    StartVa = 0x400420; 
    StopVa = 0x403233;

    Size = StopVa - StartVa; 
    SavedStartVa = StartVa;

    for (i = 0; i < Size/4; i++) 
    { 
       if (matchBytes(StartVa, "EB02????")) 
       { 
            Message("Find%x:%02x%02x%02x%02x\n", StartVa,Byte(StartVa),Byte(StartVa+1),Byte(StartVa+2),Byte(StartVa+3));
            for (j = 0; j < 4; j++) 
            { 

                 PatchByte(StartVa, 0x00); 
                 MakeCode(StartVa); 
                 StartVa++; 
            } 
       } 
        else
            StartVa=StartVa+4; 
    }

    AnalyzeArea(SavedStartVa, StopVa); 
    Message("Clear eb02 Opcode Ok "); 
}

来自‘逢魔安全实验室’

Code

import os
f = open("baby_mips", "rb")
content = f.read()
content = list(content)
for x in range(0, len(content)):
    if content[x] == "\xeb" and content[x+1] == "\x02" and (x%4==0):
        content[x] = "\x00"
        content[x+1] = "\x00"
        content[x+2] = "\x00"
        content[x+3] = "\x00"
content = "".join(content)
p = open("patch", "wb")
p.write(content)

来自‘cq674350529’

Code

import idautils
import idc
import idaapi

start_addr = 0x400420
end_addr = 0x403234
while start_addr <= end_addr:
    if Byte(start_addr) == 0xeb and Byte(start_addr +1) == 0x2:
        PatchByte(start_addr,0x00)
        PatchByte(start_addr+1,0x00)
        PatchByte(start_addr+2,0x00)
        PatchByte(start_addr+3,0x00)
    start_addr += 4

选择上述其中一个脚本，在桌面保存成一个.py或.idc文件
选择File->Script file或Script command

然后import导入或直接写也可以，然后RUN

关闭这个窗口，会有一个提示是否保存修改，点击Yes，这时桌面会生成一个patch

IDA载入这个patch，可以发现在ubuntu下的IDA里指令都可以被识别，而且可以运行，我在win10运行的IDA会有几个小段不能识别，需要手动改为指令，将0x400420处的代码转换成函数

将数据转为代码和函数

首先往下看看，有几段没有识别的

把它们全部选中(00401A58-00401F28)，右键,选择Analyze selected area或按C，

选Analyze，然后Yes，然后就会变成代码

当然这还没完，函数头部00400420没有变量声明，识别出来的肯定是错误的函数，因此在00400420右键，选择Create function

就可以了
然后图形化分析就像下面那样

记得保存修改，路径Edit->Patch program->Apply patches input file

标准转换方式

1.函数和数据互换

在重新格式化之前，首先必须删除其当前的格式（代码或数据）。右击你希望取消定义的项目，在结果上下文菜单中选择Undefine（也可使用Edit▶Undefine命令或热键U），即可取消函数、代码或数据的定义

转换成code后，此时不能使用图形view
创建函数（Edit—>Functions—>Create Function….）就可以了

2.代码和数据转换

通过Edit▶Data和热键D来完成,之后使用Undefine
之后使用code指令

算法分析

1.反编译器分析

用图形化分析sub_400420这个函数

一共十六个条件，必须每条都得满足才行

IDA的F5不能用，我们需要能够分析MIPS的反编译器
· Retdec https://github.com/avast-tl/retdec
· JEB-MIPS https://www.pnfsoftware.com/jeb/demomips

下面是三种找出算法的方法

1.Retdec

RetDec 是一个可重定向的机器码反编译器，它基于 LLVM，支持各种体系结构、操作系统和文件格式：
支持的文件格式：ELF，PE，Mach-O，COFF，AR（存档），Intel HEX 和原始机器码。
支持的体系结构（仅限 32 位）：Intel x86，ARM，MIPS，PIC32 和 PowerPC。

安装和使用方法GitHub上都写了
或者这里有一个很好的简易介绍 https://firmianay.gitbooks.io/ctf-all-in-one/content/doc/5.11.1_retdec.html

我在win10安装之后，把patch放到了D盘根目录，Retdec文件夹也是，然后在cmd中执行
D:\retdec\bin\decompile.sh D:\patch
等待分析(因为我装了Git，就自动调用Git bash执行了，其他情况还没试过)
结束后D盘生成下面几个文件

打开patch.c，看sub_400420
我的不知道出了什么问题，分析不了，直接return 1。。。感觉应该是把函数分解了

借用一下‘niuwuwu’的图

是16个方程求解，解方程下面说，接下来用JEB反编译

2.JEB-MIPS

先到官网下载试用版的JEB，试用版功能是完整版的百分之九十，所以其实足够学习用了(国外友人客服也非常专业且友好)

解压后有三个运行脚本，分别是Windows，Linux和Mac OS的，我为了方便就装Ubuntu了

不管是哪个系统，我们都需要JAVA8的环境

Ubuntu安装JAVA8
sudo apt-get install openjdk-8-jdk
查看java版本，看看是否安装成功
java -version

成功后运行脚本，就打开主程序了，导入patch程序，找到00400420

右键，Decompile

很长很长的算式，就是16个方程了

2.手工分析清洗方程

(来自‘奈沙夜影’)

Code

f = open("code.txt", "r")
flower = ["slti", "sdc1"]
a0 = 0x76ff270
v0 = 0xd0000
v1 = 8
fp = [0 for i in range(0x500)]
table = [0x0, 0x42d1f0, 0x0, 0x42d1f0,
0xa, 0xa, 0x0, 0x9,
0x4250bc, 0x9, 0x426630, 0x42d1f0,
0x40a3ec, 0x37343431, 0x363434, 0x0,
0x0, 0x42d1f0, 0x0, 0x4250bc,
0x0, 0x0, 0x425060, 0x42d1f0,
0x403ad0, 0x0, 0x0, 0x1000,
0x425088, 0x76fff184, 0x412fcd, 0x1,
0x410570, 0x425190, 0x40ca48, 0x0,
0x0, 0x42d1f0, 0x0, 0x42d1f0,
0x425088, 0xffffffff, 0x4106c4, 0xffffffff,
0x76fff184, 0x412fcd, 0x1, 0x42d1f0,
0x0, 0x425088, 0x40ccac, 0x0,
0x0, 0x0, 0x0, 0x42d1f0,
0x0, 0x425190, 0x76ffeef8, 0x425190,
0x10, 0x425088, 0x40baac, 0x42d1f0,
0x412fcd, 0x1, 0x425088, 0x40baac,
0x76fff184, 0x412fce, 0x40b684, 0x0,
0x0, 0x0, 0x0, 0x42d1f0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x42d1f0, 0x0, 0x42d1f0,
0x0, 0x4250bc, 0x413081, 0x9,
0x403f24, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x42d1f0,
0x0, 0x413078, 0x0, 0x0,
0x0, 0x0, 0xd0000, 0xf1f4,
0xcf8, 0xf5f1, 0x7883, 0xe2c6,
0x67, 0xeccc, 0xc630, 0xba2e,
0x6e41, 0x641d, 0x716d, 0x4505,
0x76fff224, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0xfffffffe, 0x0,
0x76fff2ac, 0x412fcd, 0x1, 0x0,
0x6, 0x7fffffff, 0x1, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x0,
0xa, 0xa, 0x425088, 0x8,
0x7ffffff8, 0x100, 0x413f38, 0x1,
0x413f38, 0x0, 0x2, 0x76fff0f8,
0x0, 0x0, 0x7fffffff, 0x76fff220,
0x405050, 0x550001, 0x0, 0x425000,
0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, 0x76fff220,
0x404d84, 0x42d1f0, 0x0, 0x500,
0x5, 0x42d1f0, 0xb3b, 0x76fff224,
0x115, 0x1a131100, 0x76fff220, 0x76fff270,
0x76fff2ac, 0xffbecf88, 0xa, 0x405880]
j = 0
functions = 0
for i in range(0xb4, 0x410, 4):
    fp[i] = table[j]
    j += 1
input = [int(str(i)*3, 16) for i in range(16)]
try:
    while(True):
        code = f.readline()
        if(code == ""):
            print("finish")
            break
        if(code[:3] == "loc"):
            # print("\n[s]:\t" + code[:-1])
            continue
        if(code.find("nop")!=-1):
            continue
        code = code.split("$")
        # print(code)

        c = code[0].strip()

        if(c=="sw"):
            n1 = code[1].split(",")[0]
            n2 = 0x410 - int("0x" + code[1].split("_")[1].split("(")[0], 16)
            code = ("fp[" + hex(n2) + "] = " + n1)
        elif(c=="li"):
            n1 = code[1].split(",")[0]
            n2 = code[1].split(",")[1].strip()
            code = (n1 + " = " + n2)
        elif(c=="lw"):
            n1 = code[1].split(",")[0]
            if("".join(code).find("fp")!=-1):
                n2 = 0x410 - int("0x" + code[1].split("_")[1].split("(")[0], 16)
                code = (n1 + " = fp[" + hex(n2) + "]")
                # print("# " + hex(fp[n2]))
                #输出方程
                print("0x%x*"%fp[n2],end='')
            else:
                # print("[c]:\t" + "".join(code)[:-1], "v0=%x"%v0)
                n2 = ((v0) + int(code[1].split(",")[1].replace("(", "")))//4
                code = (n1 + " = input[" + str(n2) + "]")
                print("a[%d]"%n2)


                # print(code)
                # print(hex(v0))
                # break
        elif(c=="sll"):
            n1 = code[1].split(",")[0]
            n2 = code[1].split(",")[1].strip()
            code = (n1 + " = " + n1 + "<<" + n2)
        elif(c=="sra"):
            n1 = code[1].split(",")[0]
            n2 = code[1].split(",")[1].strip()
            code = (n1 + " = " + n1 + ">>" + n2)
        elif(c=="xori"):
            n1 = code[1].split(",")[0]
            n2 = code[1].split(",")[1].strip()
            code = (n1 + " = " + n1 + "^" + n2)
        elif(c=="addiu"):
            n1 = code[1].split(",")[0]
            n2 = code[1].split(",")[1].strip()
            code = (n1 + " = " + n1 + "+" + n2)
            # print("+")
        elif(c=="mul"):
            n1 = code[1].split(",")[0]
            n2 = code[2].split(",")[0].strip()
            n3 = code[3].strip()
            code = (n1 + " = " + n2 + "*" + n3)
        elif(c=="addu"):
            n1 = code[1].split(",")[0]
            n2 = code[2].split(",")[0].strip()
            code = (n1 + " = " + n1 + "+" + n2)
            print("+")
        elif(c=="subu"):
            n1 = code[1].split(",")[0]
            n2 = code[2].split(",")[0].strip()
            code = (n1 + " = " + n1 + "-" + n2)
            print("-")
        elif(c=="beq"):
            print("=0x%x"%(v0))
            print("================================================one function=====================================")
            functions +=1
            continue
        elif(c=="negu"):
            n1 = code[1].split(",")[0]
            n2 = code[2].split(",")[0].strip()
            code = (n1 + " = " + "-" + n2)
            print("-")
        elif(c=="nop"):
            continue
        elif(c=="lui"):
            n1 = code[1].split(",")[0]
            n2 = code[1].split(",")[1].strip()
            code = (n1 + " = " + n2 + "<<32")
        elif(c=="move" or c=="and"):
            continue
        elif(c in flower):
            # print("[f]:\t" + "".join(code)[:-1])
            continue

        else:
            print("[x]:\tFind unknown code | " + "".join(code))
            break
        # print("[-]:\t" + code)
        exec(code)
except Exception as e:
    print(repr(e))
    print(code)
print(functions)
# print(fp)

解方程

解方程的方法很多
比如Python的有

Numpy 求解线性方程组
SciPy 求解非线性方程组
SymPy

上面三个有个链接可以参照https://zhuanlan.zhihu.com/p/24893371

numpy求解

来自‘niuwuwu’

Code

import numpy as np
from scipy.linalg import solve
A=[
    [-56251,64497,-61787,29993,-16853,2147,-51990,-36278,-34108,-1148,1798,-43452,-16150,-56087,-17677,-41752],
    [-39354,63754,50513,2396,-37448,43585,19468,-4688,-62869,-20663,41173,61113,30862,38224,-601,53899],
    [26798,-58888,14929,-21751,-12385,55961,-20714,24897,40045,9805,25147,39173,-21952,-42840,37937,-8559],
    [-2789,53359,16747,54195,-30020,39916,-32582,60338,13971,27307,-30484,47826,37554,64914,-1745,27669],
    [40374,6523,13380,-53413,-1194,7796,-31815,-51866,-40252,-56883,57811,23278,-5785,61525,-6984,-7335],
    [-57052,-64573,-62351,2628,21493,12939,-60006,435,15009,-4091,22743,4901,48803,-43203,5263,-32994],
    [54760,41053,22537,-56473,46316,19787,-40180,2088,2044,26575,-5207,31098,-23838,21642,46750,13706],
    [-40176,-43382,48718,-25423,21452,-36714,-24119,-13231,-52192,49742,54709,-32636,20233,21460,48733,15155],
    [38446,-880,-2443,50487,-46973,-56178,-37138,-9079,-19096,-60988,-1823,-21538,43896,-4141,-19370,-47796],
    [5176,18400,-53852,36119,-32120,47724,17154,5390,-29717,14471,8755,1432,-45518,-8148,-56623,-48254],
    [30203,-50712,-27560,-16075,3618,590,44305,20581,33442,-7743,-43075,-16234,45723,-44899,42321,49264],
    [42705,-32299,-19156,5594,28870,8059,58103,-60723,-32112,-7128,45985,-24915,63910,18427,-51408,22619],
    [-57517,20738,-32286,55995,26666,37550,-51489,13733,32455,-2897,-39622,-54523,50733,-24649,-17849,-62326],
    [-15716,-38264,64476,-37524,-61551,13536,12920,1407,-63767,-55105,-46543,-36562,-20712,2063,-6668,9074],
    [47490,18611,52416,3107,32177,-41780,11008,7223,5652,881,26719,-28444,46077,-272,-32475,-9432],
    [-58938,-35689,35708,44689,45902,36614,38550,731,49990,6727,61526,-35587,-39199,-43886,-56409,-25519],
]
B=[-24232262,17175305,8705731,26962228,-6384428,-15459013,19554563,-188243,-19590071,-12754495,6442406,-2869966,-4805280,-18964176,8938201,3896470]

a = np.array(A)
b = np.array(B)
x =solve(a,b)
print(x)

来自‘ljt1000’

Code

import numpy as np

A  = "-15858,-48466,32599,38605,-44159,23939,45662,9287,47754,47937,41896,51986,-26968,22561,30701,63487;"
A += "60228,-3993,-16615,57134,-19246,-38581,40294,-44968,-28198,-58965,-39534,22458,-8828,48593,46135,23871;"
A += "59121,42162,-65140,-3847,-23842,-47173,-39252,37804,-20964,-19217,56467,5112,9324,61729,61599,3578;"
A += "-36731,-26147,1670,19245,26847,39911,8628,57946,-51207,63125,-21537,-9321,40745,-58129,30962,-27610;"
A += "-63560,-53320,-34289,61060,-14289,46922,53218,36638,-61969,-33727,-4681,32423,-17044,-46689,-35443,-24156;"
A += "-10571,-11103,51585,-24771,63730,57047,-63227,4227,-56470,-22654,-46325,62842,22480,59412,24937,62085;"
A += "52617,-54333,61495,33704,-41733,-44527,51882,-61765,-24691,-10103,31055,61454,-59349,9812,-48848,-47279;"
A += "-40696,-26470,54670,-23715,10008,7723,-62622,53112,31753,-5047,-48878,-58448,19875,-34944,-22161,35800;"
A += "-23196,-43354,-58947,3384,-2426,-60194,51907,-20177,-31882,61703,42398,-4627,45749,-29203,-11139,-41301;"
A += "-37819,-10066,-48579,-62613,-28961,40001,-37989,-27875,-20264,-33616,-5998,30740,-29594,21652,5165,51797;"
A += "52993,62328,4196,-55719,-1917,28075,-44831,-15799,13652,-52110,-38933,62219,40030,-23815,-19505,60128;"
A += "35796,-28033,-59250,46833,39767,-22909,5585,-42334,64787,6068,60536,-54554,22189,-49945,40846,64023;"
A += "-18536,-35823,4253,-63956,20175,43158,30523,28298,-29564,18809,50821,-38574,3005,33408,58281,-29452;"
A += "2848,39836,46250,24950,38512,31901,-21506,-36050,44162,41717,-36605,-26097,-38073,36024,7349,19105;"
A += "22525,15747,63301,42436,-26106,-22761,48830,6176,-55225,-45599,-30368,50701,5775,10902,12758,-19336;"
A += "-58450,-51156,-5460,32490,-26701,27355,34100,-14902,10736,54258,-9189,-25920,48339,-61339,61403,-30542"

b = "23261386,-1298872,13877344,9172342,-11622989,10343966,-9721165,-8286458,-7515929,-12609498,2179053,11137244,12446496,10255605,854242,1542147"

A = np.mat(A)
b = np.mat(b).T
r = np.linalg.solve(A,b)
print r

Z3约束器求解方程

Z3可以说很出名了
这里有个教程http://ericpony.github.io/z3py-tutorial/guide-examples.htm

来自‘奈沙夜影’

Code

from z3 import *

a = [BitVec("a%d"%i, 32) for i in range(16)]
s = Solver()
s.add(0xca6a*a[0] -0xd9ee*a[1] +0xc5a7*a[2] +0x19ee*a[3] +0xb223*a[4] +0x42e4*a[5] +0xc112*a[6] -0xcf45*a[7] +0x260d*a[8] +0xd78d*a[9] +0x99cb*a[10] -0x3e58*a[11] -0x97cb*a[12] +0xfba9*a[13] -0xdc28*a[14] +0x859b*a[15]  == 0xaa2ed7)
s.add(0xf47d*a[0] +0x12d3*a[1] -0x4102*a[2] +0xcedf*a[3] -0xafcf*a[4] -0xeb20*a[5] -0x2065*a[6] +0x36d2*a[7] -0x30fc*a[8] -0x7e5c*a[9] +0xeea8*a[10] +0xd8dd*a[11] -0xae2*a[12] +0xc053*a[13] +0x5158*a[14] -0x8d42*a[15]  == 0x69d32e)
s.add(0xffff52cf*a[0] -0x4fea*a[1] +0x2075*a[2] +0x9941*a[3] -0xbd78*a[4] +0x9e58*a[5] +0x40ad*a[6] -0x8637*a[7] -0x2e08*a[8] +0x4414*a[9] +0x2748*a[10] +0x1773*a[11] +0xe414*a[12] -0x7b19*a[13] +0x6b71*a[14] -0x3dcf*a[15]  == 0x3b89d9)
s.add(0xffffedd7*a[0] -0x1df0*a[1] +0x8115*a[2] +0x54bd*a[3] -0xf2ba*a[4] +0xdbd*a[5] +0x1dcf*a[6] +0x272*a[7] -0x2fcc*a[8] -0x93d8*a[9] -0x6f6c*a[10] -0x98ff*a[11] +0x2148*a[12] -0x6be2*a[13] +0x2e56*a[14] -0x7bdf*a[15]  == 0xff6a5aea)
s.add(0xffffa8c1*a[0] +0xdc78*a[1] -0x380f*a[2] +0x33c0*a[3] -0x7252*a[4] -0xe5a9*a[5] +0x7a53*a[6] -0x4082*a[7] -0x584a*a[8] +0xc8db*a[9] +0xd941*a[10] +0x6806*a[11] -0x8b97*a[12] +0x23d4*a[13] +0xac2a*a[14] +0x20ad*a[15]  == 0x953584)
s.add(0x5bb7*a[0] -0xfdb2*a[1] +0xaaa5*a[2] -0x50a2*a[3] -0xa318*a[4] +0xbcba*a[5] -0x5e5a*a[6] +0xf650*a[7] +0x4ab6*a[8] -0x7e3a*a[9] -0x660c*a[10] +0xaed9*a[11] -0xa60f*a[12] +0xf924*a[13] -0xff1d*a[14] +0xc888*a[15]  == 0xffd31341)
s.add(0x812d*a[0] -0x402c*a[1] +0xaa99*a[2] -0x33b*a[3] +0x311b*a[4] -0xc0d1*a[5] -0xfad*a[6] -0xc1bf*a[7] -0x1560*a[8] -0x445b*a[9] -0x9b78*a[10] +0x3b94*a[11] +0x2531*a[12] -0xfb03*a[13] +0x8*a[14] +0x8721*a[15]  == 0xff9a6b57)
s.add(0x15c5*a[0] +0xb128*a[1] -0x957d*a[2] +0xdf80*a[3] +0xee68*a[4] -0x3483*a[5] -0x4b39*a[6] -0x3807*a[7] -0x4f77*a[8] +0x652f*a[9] -0x686f*a[10] -0x7fc1*a[11] -0x5d2b*a[12] -0xb326*a[13] -0xacde*a[14] +0x1f11*a[15]  == 0xffd6b3d3)
s.add(0xaf37*a[0] +0x709*a[1] +0x4a95*a[2] -0xa445*a[3] -0x4c32*a[4] -0x6e5c*a[5] -0x45a6*a[6] +0xb989*a[7] +0xf5b7*a[8] +0x3980*a[9] -0x151d*a[10] +0xaf13*a[11] +0xa134*a[12] +0x67ff*a[13] +0xce*a[14] +0x79cf*a[15]  == 0xc6ea77)
s.add(0xffff262a*a[0] +0xdf05*a[1] -0x148e*a[2] -0x4758*a[3] -0xc6b2*a[4] -0x4f94*a[5] -0xf1f4*a[6] +0xcf8*a[7] +0xf5f1*a[8] -0x7883*a[9] -0xe2c6*a[10] -0x67*a[11] +0xeccc*a[12] -0xc630*a[13] -0xba2e*a[14] -0x6e41*a[15]  == 0xff1daae5)
s.add(0xffff9be3*a[0] -0x716d*a[1] +0x4505*a[2] -0xb99d*a[3] +0x1f00*a[4] +0x72bc*a[5] -0x7ff*a[6] +0x8945*a[7] -0xcc33*a[8] -0xab8f*a[9] +0xde9e*a[10] -0x6b69*a[11] -0x6380*a[12] +0x8cee*a[13] -0x7a60*a[14] +0xbd39*a[15]  == 0xff5be0b4)
s.add(0x245e*a[0] +0xf2c4*a[1] -0xeb20*a[2] -0x31d8*a[3] -0xe329*a[4] +0xa35a*a[5] +0xaacb*a[6] +0xe24d*a[7] +0xeb33*a[8] +0xcb45*a[9] -0xdf3a*a[10] +0x27a1*a[11] +0xb775*a[12] +0x713e*a[13] +0x5946*a[14] +0xac8e*a[15]  == 0x144313b)
s.add(0x157*a[0] -0x5f9c*a[1] -0xf1e6*a[2] +0x550*a[3] -0x441b*a[4] +0x9648*a[5] +0x8a8f*a[6] +0x7d23*a[7] -0xe1b2*a[8] -0x5a46*a[9] -0x5461*a[10] +0xee5f*a[11] -0x47e6*a[12] +0xa1bf*a[13] +0x6cf0*a[14] -0x746b*a[15]  == 0xffd18bd2)
s.add(0xf81b*a[0] -0x76cb*a[1] +0x543d*a[2] -0x4a85*a[3] +0x1468*a[4] +0xd95a*a[5] +0xfbb1*a[6] +0x6275*a[7] +0x30c4*a[8] -0x9595*a[9] -0xdbff*a[10] +0x1d1d*a[11] +0xb1cf*a[12] -0xa261*a[13] +0xf38e*a[14] +0x895c*a[15]  == 0xb5cb52)
s.add(0xffff6b97*a[0] +0xd61d*a[1] +0xe843*a[2] -0x8c64*a[3] +0xda06*a[4] +0xc5ad*a[5] +0xd02a*a[6] -0x2168*a[7] +0xa89*a[8] +0x2dd*a[9] -0x80cc*a[10] -0x9340*a[11] -0x3f07*a[12] +0x4f74*a[13] +0xb834*a[14] +0x1819*a[15]  == 0xa6014d)
s.add(0x48ed*a[0] +0x2141*a[1] +0x33ff*a[2] +0x85a9*a[3] -0x1c88*a[4] +0xa7e6*a[5] -0xde06*a[6] +0xbaf6*a[7] +0xc30f*a[8] -0xada6*a[9] -0xa114*a[10] -0x86e9*a[11] +0x70f9*a[12] +0x7580*a[13] -0x51f8*a[14] -0x492f*a[15]  == 0x2fde7c)


if(s.check()==sat):
    c = b''
    m = s.model()
    for i in range(16):
        print("a[%d]=%d"%(i, m[a[i]].as_long()))
    for i in range(16):
        print(chr(m[a[i]].as_long()&0xff), end='')

来自‘cq674350529’

Code

#!/usr/bin/env python

from z3 import *

a = [BitVec('a%d' %i, 32) for i in xrange(16)]

s = Solver()
s.add(0xffffc20e*a[0]-0xbd52*a[1]+0x7f57*a[2]+0x96cd*a[3]-0xac7f*a[4] +0x5d80*a[5]+0xb25e*a[6]+0x2447*a[7]+0xba8a*a[8]+0xbb41*a[9]+0xa3a8*a[10]+0xcb12*a[11]-0x6958*a[12]+0x5821*a[13]+0x77ed*a[14]+0xf7ff*a[15] == 0x162f0ca )
s.add(0xeb44*a[0]-0x0f99*a[1] - 0x40e7*a[2] +0xdf2e*a[3] -0x4b2e*a[4] -0x96b5*a[5] +0x9d66*a[6] -0xafa8*a[7] -0x6e26*a[8] -0xe655*a[9]- 0x9a6e*a[10] +0x57ba*a[11] -0x227c*a[12] +0xbdd1*a[13] +0xb437*a[14] +0x5d3f*a[15]== 0xffec2e48)
s.add(0xe6f1*a[0] +0xa4b2*a[1] -0xfe74*a[2] -0x0f07*a[3] -0x5d22*a[4] -0xb845*a[5] -0x9954*a[6] +0x93ac*a[7] -0x51e4*a[8] -0x4b11*a[9] +0xdc93*a[10] +0x13f8*a[11] +0x246c*a[12] +0xf121*a[13] +0xf09f*a[14] +0x0dfa*a[15] == 0xd3c060)
s.add(0xffff7085*a[0] -0x6623*a[1] +0x0686*a[2] +0x4b2d*a[3] +0x68df*a[4] +0x9be7*a[5] +0x21b4*a[6] +0xe25a*a[7] -0xc807*a[8] +0xf695*a[9] -0x5421*a[10] -0x2469*a[11] +0x9f29*a[12] -0xe311*a[13] +0x78f2*a[14] -0x6bda*a[15] == 0x8bf576)
s.add(0xffff07b8*a[0] -0xd048*a[1] -0x85f1*a[2] +0xee84*a[3] -0x37d1*a[4] +0xb74a*a[5] +0xcfe2*a[6]+ 0x8f1e*a[7] -0xf211*a[8] -0x83bf*a[9] -0x1249*a[10] +0x7ea7*a[11] -0x4294*a[12] -0xb661*a[13] -0x8a73*a[14] -0x5e5c*a[15] == 0xff4ea5b3)
s.add(0xffffd6b5*a[0] -0x2b5f*a[1]+ 0xc981*a[2] -0x60c3*a[3] +0xf8f2*a[4]+ 0xded7*a[5]- 0xf6fb*a[6] +0x1083*a[7]- 0xdc96*a[8]- 0x587e*a[9] -0xb4f5*a[10] +0xf57a*a[11] +0x57d0*a[12] +0xe814*a[13] +0x6169*a[14] +0xf285*a[15] == 0x9dd61e)
s.add(0xcd89*a[0] -0xd43d*a[1] +0xf037*a[2] +0x83a8*a[3] -0xa305*a[4] -0xadef*a[5] +0xcaaa*a[6] -0xf145*a[7]- 0x6073*a[8]- 0x2777*a[9] +0x794f*a[10] +0xf00e*a[11] -0xe7d5*a[12] +0x2654*a[13] -0xbed0*a[14] -0xb8af*a[15] == 0xff6baab3)
s.add(0xffff6108*a[0] -0x6766*a[1] +0xd58e*a[2] -0x5ca3*a[3] +0x2718*a[4] +0x1e2b*a[5] -0xf49e*a[6] +0xcf78*a[7] +0x7c09*a[8] -0x13b7*a[9] -0xbeee*a[10]- 0xe450*a[11] +0x4da3*a[12] -0x8880*a[13] -0x5691*a[14] +0x8bd8*a[15] == 0xff818f06)
s.add(0xffffa564*a[0] -0xa95a*a[1] -0xe643*a[2] +0x0d38*a[3] -0x097a*a[4] -0xeb22*a[5] +0xcac3*a[6] -0x4ed1*a[7] -0x7c8a*a[8] +0xf107*a[9] +0xa59e*a[10]- 0x1213*a[11] +0xb2b5*a[12] -0x7213*a[13] -0x2b83*a[14] -0xa155*a[15] == 0xff8d50e7)
s.add(0xffff6c45*a[0] -0x2752*a[1] -0xbdc3*a[2] -0xf495*a[3] -0x7121*a[4] +0x9c41*a[5] -0x9465*a[6]- 0x6ce3*a[7] -0x4f28*a[8] -0x8350*a[9] -0x176e*a[10] +0x7814*a[11] -0x739a*a[12] +0x5494*a[13] +0x142d*a[14] +0xca55*a[15] == 0xff3f9826)
s.add(0xcf01*a[0] +0xf378*a[1] +0x1064*a[2] -0xd9a7*a[3] -0x077d*a[4]+ 0x6dab*a[5] -0xaf1f*a[6]- 0x3db7*a[7] +0x3554*a[8] -0xcb8e*a[9] -0x9815*a[10]+ 0xf30b*a[11] +0x9c5e*a[12] -0x5d07*a[13] -0x4c31*a[14] +0xeae0*a[15] == 0x213fed)
s.add(0x8bd4*a[0] -0x6d81*a[1] -0xe772*a[2] +0xb6f1*a[3] +0x9b57*a[4] -0x597d*a[5] +0x15d1*a[6]- 0xa55e*a[7]+ 0xfd13*a[8]+ 0x17b4*a[9] +0xec78*a[10] -0xd51a*a[11] +0x56ad*a[12] -0xc319*a[13] +0x9f8e*a[14] +0xfa17*a[15] == 0xa9f0dc)
s.add(0xffffb798*a[0] -0x8bef*a[1] +0x109d*a[2]- 0xf9d4*a[3] +0x4ecf*a[4] +0xa896*a[5] +0x773b*a[6] +0x6e8a*a[7] -0x737c*a[8]+ 0x4979*a[9] +0xc685*a[10] -0x96ae*a[11] +0x0bbd*a[12] +0x8280*a[13] +0xe3a9*a[14] -0x730c*a[15] == 0xbdeb20)
s.add(0x0b20*a[0] +0x9b9c*a[1] +0xb4aa*a[2]+ 0x6176*a[3] +0x9670*a[4] +0x7c9d*a[5] -0x5402*a[6] -0x8cd2*a[7] +0xac82*a[8] +0xa2f5*a[9] -0x8efd*a[10] -0x65f1*a[11] -0x94b9*a[12] +0x8cb8*a[13] +0x1cb5*a[14] +0x4aa1*a[15] == 0x9c7cf5)
s.add(0x57fd*a[0] +0x3d83*a[1] +0xf745*a[2] +0xa5c4*a[3] -0x65fa*a[4] -0x58e9*a[5] +0xbebe*a[6] +0x1820*a[7] -0xd7b9*a[8] -0xb21f*a[9] -0x76a0*a[10] +0xc60d*a[11] +0x168f*a[12] +0x2a96*a[13] +0x31d6*a[14] -0x4b88*a[15] == 0xd08e2)
s.add(0xffff1bae*a[0] -0xc7d4*a[1] -0x1554*a[2] +0x7eea*a[3] -0x684d*a[4] +0x6adb*a[5] +0x8534*a[6] -0x3a36*a[7] +0x29f0*a[8] +0xd3f2*a[9] -0x23e5*a[10] -0x6540*a[11] +0xbcd3*a[12] -0xef9b*a[13] +0xefdb*a[14] -0x774e*a[15] == 0x178803)

for item in a:
    s.add(item > 0, item < 127)

if s.check() == sat:
    m = s.model()
    flag = []
    for i in xrange(16):
        flag.append(m[a[i]].as_long())
    print ''.join(map(chr, flag))

angr二进制自动化分析及符号执行

angr是一个基于python的二进制漏洞分析框架，集成了多种主流的分析技术，能够进行动态的符号执行分析和多种静态分析。

如果我们使用angr的话，就不再需要考虑算法内部的详细原理，利用符号执行可以大大减少分析时间

Code

.text:00403620                 lw      $gp, 0x98+var_50($fp)
.text:00403624                 addiu   $v0, $fp, 0x98+var_48
.text:00403628                 move    $a0, $v0
.text:0040362C                 jal     sub_400420
.text:00403630                 nop
.text:00403634                 lw      $gp, 0x98+var_50($fp)
.text:00403638                 beqz    $v0, loc_4036E4
.text:0040363C                 nop

通过静态分析可知，程序在0x40362c处调用sub_400420函数，其参数通过寄存器a0传递，然后返回值保存在v0寄存器中。之后对v0的内容进行判断，如果为1则输出flag(flag与用户输入的内容相关)，为0则输出”Wrong”。因此，只需要求解输入，保证sub_400420的返回值为1即可。

angr脚本

Code

#!/usr/bin/env python

import angr

project = angr.Project('./patch', load_options={'auto_load_libs':False})

start_address = 0x400420
memory_address = 0x10000000

find_address = 0x4031F0
avoid_address = (0x4019E4, 0x401b7c,0x401D18, 0x401EB0, 0x40204C, 0x4021E4, 0x40237C, 0x402518, 0x4026B4, 0x40284C, 0x4029E4, 0x402B7C, 0x402D14, 0x402EB0, 0x403048, 0x4031E0)

state = project.factory.blank_state(addr=start_address)

for i in xrange(16):
    state.memory.store(memory_address+i*4, state.solver.BVS('a%d' % i, 32), endness=state.arch.memory_endness)

state.regs.a0 = memory_address

# add LAZY_SOLVES to speed up
simgr = project.factory.simulation_manager(state, add_options={angr.options.LAZY_SOLVES})

simgr.explore(find=find_address, avoid=avoid_address)

if simgr.found:
    find_state = simgr.found[0]

    # add constraints to reduce the keyspace
    for i in xrange(16):
        value = find_state.memory.load(memory_address+i*4,4, endness=find_state.arch.memory_endness)
        find_state.add_constraints(value > 0, value < 127)

    flag = [find_state.se.eval(find_state.memory.load(memory_address+i*4, 4, endness=find_state.arch.memory_endness)) for i in xrange(16)]
    print ''.join(map(chr,flag))

返回1的地址

find_address是使得函数sub_400420返回值为1的地址，而avoid_address是使得函数sub_400420返回值为0的地址。同时，将输入的16个数字保存在内存地址0x10000000处，然后将其赋值给a0寄存器，实现参数的传递。之后，直接从函数sub_400420的开始处开始分析。

第二种

Code

# -*- coding:utf-8 -*-
from angr import *
import logging
import IPython
logging.getLogger('angr.manager').setLevel(logging.DEBUG)
p = Project('baby_mips')
state = p.factory.blank_state(addr=0x400420)
DATA_ADDR = 0xA0000
state.regs.a0 = DATA_ADDR
for i in range(16*4):
    vec = state.solver.BVS("c{}".format(i),8,explicit_name=True)
    cond = state.solver.And(vec>=32,vec<=126) # low byte
    state.memory.store(DATA_ADDR+i,vec)
    if i % 4 == 0:
        pass
    #state.add_constraints(cond)
sm = p.factory.simulation_manager(state)
res = sm.explore(find=0x4031F0,avoid=[0x4019E4, 0x401b7c,0x401D18, 0x401EB0, 0x40204C, 0x4021E4, 0x40237C, 0x402518, 0x4026B4, 0x40284C, 0x4029E4, 0x402B7C, 0x402D14, 0x402EB0, 0x403048, 0x4031E0])

found = res.found[0]
mem = found.memory.load(DATA_ADDR,16*4)
print found.solver.eval(mem)
print '##########################################'
flag = ''
for i in range(16):
    v = found.memory.load(DATA_ADDR + 4*i,1)
    flag = flag + found.solver.eval(v,cast_to=str)
print flag  #7fe2c58fc9a7eb90

flag每个人都是不一样的，我的用angr解的话，最后得到的是7fe2c58fc9a7eb90

Flag

于是flag: DDCTF{7fe2c58fc9a7eb90}

z3解的话还可以得出具体每个变量的值，这里就不放图了