Solve baby_mips with angr

背景

baby_mips是DDCTF 2018 逆向的第1题,是MIPS指令架构的。MIPS指令架构是一种采用精简指令集的处理器架构,常用于路由器等嵌入式设备中。

静态分析

使用file命令查看文件格式,如下。可以看到程序为MIPS架构 小端格式,同时是通过静态链接生成的。

1
2
$ file baby_mips
baby_mips: ELF 32-bit LSB executable, MIPS, MIPS32 version 1 (SYSV), statically linked, stripped

使用IDA Pro加载程序后,查看程序的字符串列表,如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
.rodata:00412FC0 00000009 C Var[0]:                                               
.rodata:00412FD0 00000009 C Var[1]:
.rodata:00412FDC 00000009 C Var[2]:
.rodata:00412FE8 00000009 C Var[3]:
.rodata:00412FF4 00000009 C Var[4]:
.rodata:00413000 00000009 C Var[5]:
.rodata:0041300C 00000009 C Var[6]:
.rodata:00413018 00000009 C Var[7]:
.rodata:00413024 00000009 C Var[8]:
.rodata:00413030 00000009 C Var[9]:
.rodata:0041303C 0000000A C Var[10]:
.rodata:00413048 0000000A C Var[11]:
.rodata:00413054 0000000A C Var[12]:
.rodata:00413060 0000000A C Var[13]:
.rodata:0041306C 0000000A C Var[14]:
.rodata:00413078 0000000A C Var[15]:
.rodata:00413084 00000036 C The flag is: DDCTF{%c%c%c%c%c%c%c%c%c%c%c%c%c%c%c%c}\n
.rodata:004130BC 00000006 C Wrong
... ...

查找字符串The flag is: DDCTF ...的交叉引用,进入sub_403238函数。在函数开始处,调用了sub_4044d0、sub_4038a0等函数,根据字符串信息,猜测可能是读取输入。之后,在0x40365c处跳转到loc_400420处执行代码,之后根据v0的值进行判断,如下:

跳转到loc_400420处,代码比较乱,存在很多IDA无法识别的代码块,同时中间夹杂着很多数据,导致无法分析具体的处理流程。下面尝试进行动态调试分析。

动态分析

环境搭建

由于程序是MIPS指令架构的,而通常我们使用的电脑是x86架构的,无法直接运行该程序,这时可以借助Qemu模拟器来运行程序。QEMU是运行在用户层的开源全虚拟化解决方案,可以在Intel机器上虚拟出完整的操作系统 。QEMU主要有两种运作模式:

  • User Mode:即使用者模式,能单独运行那些为不同处理编译的Linux程序;
  • System Mode:即系统模式,能够模拟整个系统,包括中央处理器及其他周边设备。

由于baby_mips程序是通过静态链接生成的,为了方便,在User Mode下使用QEMU来运行该程序。以Ubuntu为例,首先安装qemu-static,如下:

1
$ sudo apt-get install qemu-static

安装完成后,运行该程序,如下。根据提示随便输入几个数字,提示Illegal instruction

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
$ qemu-mipsel-static ./baby_mips
Var[0]: 0
Var[1]: 1
Var[2]: 2
Var[3]: 3
Var[4]: 4
Var[5]: 5
Var[6]: 6
Var[7]: 7
Var[8]: 8
Var[9]: 9
Var[10]: 10
Var[11]: 11
Var[12]: 12
Var[13]: 13
Var[14]: 14
Var[15]: 15
qemu: uncaught target signal 4 (Illegal instruction) - core dumped
Illegal instruction (core dumped)

下面通过动态调试来定位错误。

动态调试

qemu系列命令提供了一个-g选项,用来等待外部的gdb调试器连接。下面指定1234端口来等待调试器连接,如下:

1
$ qemu-mipsel-static -g 1234 ./baby_mips

之后可以采用gdb调试器来进行调试,这里使用IDA Pro来进行调试。首先选择调试器为”Remote GDB debugger”

之后,在”Debugger”->”Process options”中设置对应的参数

然后,点击”Debugger”->”Attach to process”即可开始调试。通过跟踪程序的执行流程,发现当程序运行到0x400430时会提示错误Illegal instruction

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
.text:00400420 loc_400420:                              # CODE XREF: sub_403238+424p
.text:00400420 addiu $sp, -0x410
.text:00400424 sw $fp, 0x40C($sp)
.text:00400428 move $fp, $sp
.text:0040042C sw $a0, 0x410($fp)
.text:00400430 lwc1 $f29, 0x2EB($t1)
.text:00400434 li $v0, 0x1EF9
.text:00400438 sw $v0, 8($fp)
.text:0040043C lw $v0, 8($fp)
.text:00400440 sll $v0, 1
.text:00400444 sw $v0, 8($fp)
.text:00400448 lwu $s6, 0x2EB($s6)
.text:0040044C li $v0, 0xBD5A
.text:00400450 sw $v0, 0xC($fp)
.text:00400454 lw $v0, 0xC($fp)
.text:00400458 xori $v0, 8

查找lwc1指令的含义,发现是与协处理器相关的指令。通过对后面的代码块进行分析发现,后面并没有用到$f29$t1寄存器的内容,于是尝试利用Keypatch插件直接将0x400430处的指令lwc1 $f29, 0x2EB($t1)nop掉。之后,再次运行程序并进行调试,程序运行到0x400448时又报错。同样采用nop指令的方式patch后,程序运行到0x400468时再次报错。通过分析发现,这些报错的指令的机器码均以EB 02开始,因此尝试编写脚本将所有类似的指令nop掉。

程序“修复”

由于MIPS指令是定长的,均为4个字节。因此,可以在选定的代码块中,将所有以EB 02开始的4字节数据全部替换成00 00 00 00,脚本如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
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

在MIPS指令中,nop对应的机器码为00 00 00 00

运行脚本后,选择”Edit”->”Patch program”->”Apply patch into input file…”,将更改保存到程序中。

之后,手动将从0x400420开始的代码块中夹杂的数据转换成代码,然后将0x400420处的代码转换成函数。之后就可以很清楚地看到函数0x400420内部的处理流程了。

求解

angr求解

通过对sub_0x400420函数内部的流程进行分析,其主要是对输入进行一系列运算,然后对运算结果进行校验,如果都满足则返回1,不满足则返回0。

虽然函数sub_0x400420内部的逻辑并不复杂,但是计算过程较多,比较繁琐,这时可以利用angr框架进行符号执行求解,而不用去理解具体的运算过程。angr是一个基于python的二进制漏洞分析框架,里面集成了多种主流的分析技术,能够进行动态的符号执行分析,也能够进行多种静态分析。近几年,其在CTF中的运用也很火。

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

1
2
3
4
5
6
7
8
.text:00403650                 lw      $gp, 0x98+var_50($fp)
.text:00403654 addiu $v0, $fp, 0x98+var_48
.text:00403658 move $a0, $v0
.text:0040365C jal sub_400420
.text:00403660 nop
.text:00403664 lw $gp, 0x98+var_50($fp)
.text:00403668 beqz $v0, loc_403714
.text:0040366C nop

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
#!/usr/bin/env python

import angr

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

start_address = 0x400420
memory_address = 0x10000000

find_address = 0x403220
avoid_address = (0x401a08, 0x401ba0,0x401d38, 0x401ed4, 0x402070, 0x40220c, 0x4023a4, 0x402540, 0x4026dc, 0x402878, 0x402a10, 0x402ba8, 0x402d44, 0x402edc, 0x403074, 0x403210)

state = project.factory.blank_state(addr=start_address, add_options={angr.options.LAZY_SOLVES})

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)

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))

Z3求解

这里也给出使用Z3进行求解的过程。Z3是由微软开发的一个约束求解器,可以简单的理解它是解方程的神器。

函数sub_400420内部对参数的处理过程其实就是一个16元1次方程组,将输入看作是16个未知数,需要记录每个未知数前面的系数以及具体的运算过程。最直观的方式是单步跟踪程序的执行流程,一个一个地进行记录,但这个过程有点繁琐。通过分析,发现真正的计算是从0x40187c处开始,而且系数在内存空间是连续存放的。

1
2
3
4
5
6
7
8
9
10
11
12
13
.text:0040187C                 lw      $v0, 0x410+var_408($fp)
.text:00401880 negu $v1, $v0
.text:00401884 lw $v0, 0x410+arg_0($fp)
.text:00401888 lw $v0, 0($v0)
.text:0040188C mul $v1, $v0
.text:00401890 lw $a0, 0x410+var_404($fp)
.text:00401894 lw $v0, 0x410+arg_0($fp)
.text:00401898 addiu $v0, 4
.text:0040189C lw $v0, 0($v0)
.text:004018A0 mul $v0, $a0, $v0
.text:004018A4 subu $v1, $v0
.text:004018A8 lw $a0, 0x410+var_400($fp)
.text:004018AC lw $v0, 0x410+arg_0(

因此可以直接在0x40187c处下断点,然后将0x410+var_408($fp)0x410+var_C($fp)这段内存空间的内容在动态调试的过程中dump下来,如下:

然后再通过查看具体的运算操作指令即可

得到系数和具体的运算操作后,就可以使用Z3进行求解了,如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
#!/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))

其他

IDA Pro暂时不支持将MISP汇编代码转换成类C代码,即所谓的F5功能。目前,可以反编译MIPS汇编代码的工具主要有两个:

  • Retargetable Decompiler
  • JEB Decompiler for MIPS

相关链接

  • QEMU, the FAST! processor emulator
  • Keypatch
  • angr
  • Z3 API in Python

附件下载

baby_mips