逆向学习笔记3

第四周elf各wp

1.elf

这是一道例题，主要教我们如何使用Z3求解器进行解题

首先我们对题分析发现：

  v5 = -85;
  v4 = 0;
  for ( i = 0; i <= 39; ++i )
  {
    for ( j = 0; j <= 50; ++j )
    {
      *(_BYTE *)(i + a1) ^= *(_BYTE *)((i + 1) % 40 + a1);
      v5 ^= j ^ v4++ ^ 0x5F;
      result = v5 ^ *(_BYTE *)(i + a1);
      *(_BYTE *)(i + a1) = result;
    }
  }
  return result;
}

这个题只是对输入的字符串进行如上异或加密，继续分析发现这个加密的结果也给了我们：

date =[0x000000A1, 0x000000AD, 0x00000050, 0x00000043, 0x000000B2, 0x000000C1, 0x00000099, 0x000000A0, 0x000000AC, 0x0000003E, 0x00000022, 0x000000F3, 0x000000BA, 0x00000059, 0x000000C7, 0x0000003C, 0x00000085, 0x00000065, 0x000000E8, 0x00000006, 0x0000008D, 0x00000092, 0x00000049, 0x00000004, 0x000000DD, 0x000000E5, 0x000000F0, 0x00000089, 0x000000B8, 0x00000015, 0x0000006A, 0x00000080, 0x000000CE, 0x0000001C, 0x000000B6, 0x0000001D, 0x00000096, 0x00000075, 0x000000D6, 0x000000DF,0x000000FF]

所以我们可以开始写Z3的python脚本继续解题：

from z3 import *
date =[0x000000A1, 0x000000AD, 0x00000050, 0x00000043, 0x000000B2, 0x000000C1, 0x00000099, 0x000000A0, 0x000000AC, 0x0000003E, 0x00000022, 0x000000F3, 0x000000BA, 0x00000059, 0x000000C7, 0x0000003C, 0x00000085, 0x00000065, 0x000000E8, 0x00000006, 0x0000008D, 0x00000092, 0x00000049, 0x00000004, 0x000000DD, 0x000000E5, 0x000000F0, 0x00000089, 0x000000B8, 0x00000015, 0x0000006A, 0x00000080, 0x000000CE, 0x0000001C, 0x000000B6, 0x0000001D, 0x00000096, 0x00000075, 0x000000D6, 0x000000DF,0x000000FF]
flag = [BitVec('flag[%2d]' % i ,8) for i in range(40)]
out = [0] * 40
for i in range(40):
    out[i] = flag[i]
v1 = 0xAB
v2 = 0 
for i in range(40):
    for j in range(51):
        v1 = (v1 ^ j ^ v2 ^0x5F)%256
        out[i] ^= out[(i + 1)%40]
        out[i] ^= v1
        v2 += 1
f = Solver()
for i in range(40):
    f.add(out[i] == date[i])
while(f.check() == sat):
    condition =[]
    m = f.model() 
    p = ""
    for i in range(40):
        p += chr(int("%s" % (m[flag[i]])))
    condition.append(flag[i] != int("%s" % (m[flag[i]])))
    print(p)
    f.add(Or(condition))

由于学长们在文档中细致入微的注释，所以这里的脚本并没有太多的问题，但是要注意有一点，在写脚本时最好用out[i]来代替flag[i]进行运算，因为out在运行时是不断在改变的，而我们要求的flag是唯一不变的，所以我们需要一个中间量来代替flag进行运算，这个思想在后面几个题中也会用到。

flag：

1	flag{bW0342vrc6ohFsmdBtc4BOYwdMY2WKkItU}

2.elf

这个题比上一个题要难不少，难点有两个，一是：这里的main与不是我们要找的解题代码，我们首先要找的应该是入口函数，所以点击IDA上方中的Exports窗口找到入口函数_sub_930138，这个才是我们这道题最关键的代码。

找到代码后开始对代码分析，发现有几个数据单独成列：

又继续分析发现，我们只有和v4进行比较就行了，也就只用v4=0x6D17531463814604LL，可这真的正确吗？如果仔细一点我们会发现v4其实只有8个字节的数据，但是最后比较时却要比较15个字节，所以v4肯定不只是这点字节，这里就涉及到IDA中一个知识点：IDA有时会把几个字节的数据分开给不同的数，也就时把v4的数据分开了，所以v4的真正数据我们应该进入调试模式直接拿到v4的完整数据（15byte）：

1	date =[0x04, 0x46, 0x81, 0x63, 0x14, 0x53, 0x17, 0x6D, 0x6A, 0x67, 0x76, 0x16, 0x34, 0x14, 0x34]

找到数据后我们就可以写脚本进行解题了，脚本模板直接按照1.elf来就可以了：

from z3 import *
date =[0x04, 0x46, 0x81, 0x63, 0x14, 0x53, 0x17, 0x6D, 0x6A, 0x67, 0x76, 0x16, 0x34, 0x14, 0x34]
flag = [BitVec('flag[%2d]' % i ,8) for i in range(15)]
out = [0] * 15
for i in range(0,15):
    out[i] = flag[i]
v2 = 0
for i in range(0,15):
    for j in range(0,3):
        out[i] ^= ((i ^ j ^ 0x32) % 256)
        out[i] += v2
        v2 += 1

f = Solver()
for i in range(0,15):
    f.add(out[i] == date[i])

while f.check() == sat:
    condition = []
    m = f.model() 
    p = ""
    for i in range(0,15):
        p += chr(m[flag[i]].as_long())
        condition.append(flag[i] != m[flag[i]].as_long())
    print(p)
    f.add(Or(condition))

flag：

1	0h_y0u1_finD0V0

3.elf

这个题其实和前两个题解题思路大相径庭，即调试拿到最后比较的字节，分析运算过程，写出脚本

所以先进入调试找最后要比较的v6

date = [0x66, 0x4E, 0xA9, 0xFD, 0x3C, 0x55, 0x90, 0x24, 0x57, 0xF6, 0x5D, 0xB1, 0x01, 0x20, 0x81, 0xFD, 0x36, 0xA9, 0x1F, 0xA1, 0x0E, 0x0D, 0x80, 0x8F, 0xCE, 0x77, 0xE8, 0x23, 0x9E, 0x27, 0x60, 0x2F, 0xA5, 0xCF, 0x1B, 0xBD, 0x32, 0xDB, 0xFF, 0x28, 0xA4, 0x5D]

那么开始写脚本：

from z3 import *

date = [0x66, 0x4E, 0xA9, 0xFD, 0x3C, 0x55, 0x90, 0x24, 0x57, 0xF6, 0x5D, 0xB1, 0x01, 0x20, 0x81, 0xFD, 0x36, 0xA9, 0x1F, 0xA1, 0x0E, 0x0D, 0x80, 0x8F, 0xCE, 0x77, 0xE8, 0x23, 0x9E, 0x27, 0x60, 0x2F, 0xA5, 0xCF, 0x1B, 0xBD, 0x32, 0xDB, 0xFF, 0x28, 0xA4, 0x5D]
flag = [BitVec('flag[%2d]' % i , 8) for i in range(42)]
out = [0] * 42 

for i in range(42):
    out[i] = flag[i]

solver = Solver()

for i in range(0, 7):
    for j in range(0, 6):
        v9 = 6 * i + j
        v11 = flag[v9]
        v10 = flag[v9]
        v11 = ~v11
        v11 = v11 & (i * (j + 2))
        v10 = v10 & ~(i * (j + 2)) | v11
        v9 = 7 * j + i
        out[v9] = v10
        
for i in range(1, 42):
    if i % 2 == 1:
        out[i] *= 107
    else:
        out[i] += out[i - 1]

for i in range(42):
    solver.add(out[i] == date[i])

if solver.check() == sat:     
    condition = []                                        
    model = solver.model()
    result = ""
    for i in range(42):
        result += chr(model[flag[i]].as_long())
        condition.append(flag[i] != model[flag[i]].as_long())
    print("The original string is:", result)
else:
    print("No solution found.")

这里的脚本要注意一步在转化这个条件时v11 = s[v9];v10 = s[v9];要将s转化成flag[i]，而不是中间量out[i]，因为这里是初始赋值，此时out[]内都是0，所以无法赋值，只有将flag[]值向里面赋值才能行。

flag：

1	flag{wh03v3r_d1g5_1n70_17_f1nd5_7h3_7ru7h}

4.elf

这个题还是先三步走，即调试找字节，分析运算过程，写出脚本。

1	date = [0x22, 0x3F, 0x34, 0x32, 0x72, 0x33, 0x18, 0xA7, 0x31, 0xF1, 0x28, 0x84, 0xC1, 0x1E, 0x7A]

第一步很轻松，但是第二步发现有点不简单，

这里：

这个加密和之前的加密相比，需要我们一点一点仔细分析，首先这是一个循环的嵌套，先看内层，v10 = *((char *)&v7[-1] + v11 + j);v7数组的[-1]项被取地址后强行转化成了char型，所以我们要先搞懂v7[-1]是什么，网络上有人说这是指v7的最后一项，但在这里是不对的，这里算是IDA的一种特殊的数组调用，因为v7定义的是_int64 v7[3]，所以它的含义是访问v7前面的int64，那就是将v7里的值减8，然后获取那个v7指向的地方的8个字节的数据（因为是int64的指针），可以大概理解为移位了8位（在地址上），所以我们可以找到&v7[-1]：

当我理解&v7[-1]后这个题最难的地方就解决了，v10 = *((char *)&v7[-1] + v11 + j);后面的+v11+j其实就是将地址一个一个加一，即&v7 + n，所以就是一个一个地址的，那么我们就可以直接将v10全部找出来（先找地址对应的字节（十六进制），再将字节（十六进制）化为v10（十进制数据））：

1
2

地址对应的字节 = [0x01, 0x04, 0x07, 0x0A, 0x0D, 0x10, 0x12, 0x14, 0x17, 0x1A, 0x1D, 0x1F, 0x21, 0x24, 0x27, 0x2A, 0x2D, 0x2F, 0x31, 0x34, 0x37, 0x3A, 0x3D, 0x40, 0x43, 0x46, 0x49, 0x4C, 0x4F, 0x52]
v10 = [1, 4, 7, 10, 13, 16, 18, 20, 23, 26, 29, 31, 33, 36, 39, 42, 45, 47, 49, 52, 55, 58, 61, 64, 67, 70, 73, 76, 79, 82]

最后调试找到v5[]：

v5 = [0x0000000A, 0x00000004, 0x00000010, 0x00000008, 0x00000003, 0x00000005, 0x00000001, 0x00000004, 0x00000020, 0x00000008, 0x00000005, 0x00000003, 0x00000001, 0x00000003, 0x00000002, 0x00000008, 0x0000000B, 0x00000001, 0x0000000C, 0x00000008, 0x00000004, 0x00000004, 0x00000001, 0x00000005, 0x00000003, 0x00000008, 0x00000003, 0x00000021, 0x00000001, 0x0000000B, 0x00000008, 0x0000000B, 0x00000001, 0x00000004, 0x00000009, 0x00000008, 0x00000003, 0x00000020, 0x00000001, 0x00000002, 0x00000051, 0x00000008, 0x00000004, 0x00000024, 0x00000001, 0x0000000C, 0x00000008, 0x0000000B, 0x00000001, 0x00000005, 0x00000002, 0x00000008, 0x00000002, 0x00000025, 0x00000001, 0x00000002, 0x00000036, 0x00000008, 0x00000004, 0x00000041, 0x00000001, 0x00000002, 0x00000020, 0x00000008, 0x00000005, 0x00000001, 0x00000001, 0x00000005, 0x00000003, 0x00000008, 0x00000002, 0x00000025, 0x00000001, 0x00000004, 0x00000009, 0x00000008, 0x00000003, 0x00000020, 0x00000001, 0x00000002, 0x00000041, 0x00000008, 0x0000000C, 0x00000001]

然后开始写脚本：

from z3 import *

date = [0x22, 0x3F, 0x34, 0x32, 0x72, 0x33, 0x18, 0xA7, 0x31, 0xF1, 0x28, 0x84, 0xC1, 0x1E, 0x7A]
flag = [BitVec('flag[%2d]' % i , 8) for i in range(15)]
out = [0] * 15
v5 = [0x0000000A, 0x00000004, 0x00000010, 0x00000008, 0x00000003, 0x00000005, 0x00000001, 0x00000004, 0x00000020, 0x00000008, 0x00000005, 0x00000003, 0x00000001, 0x00000003, 0x00000002, 0x00000008, 0x0000000B, 0x00000001, 0x0000000C, 0x00000008, 0x00000004, 0x00000004, 0x00000001, 0x00000005, 0x00000003, 0x00000008, 0x00000003, 0x00000021, 0x00000001, 0x0000000B, 0x00000008, 0x0000000B, 0x00000001, 0x00000004, 0x00000009, 0x00000008, 0x00000003, 0x00000020, 0x00000001, 0x00000002, 0x00000051, 0x00000008, 0x00000004, 0x00000024, 0x00000001, 0x0000000C, 0x00000008, 0x0000000B, 0x00000001, 0x00000005, 0x00000002, 0x00000008, 0x00000002, 0x00000025, 0x00000001, 0x00000002, 0x00000036, 0x00000008, 0x00000004, 0x00000041, 0x00000001, 0x00000002, 0x00000020, 0x00000008, 0x00000005, 0x00000001, 0x00000001, 0x00000005, 0x00000003, 0x00000008, 0x00000002, 0x00000025, 0x00000001, 0x00000004, 0x00000009, 0x00000008, 0x00000003, 0x00000020, 0x00000001, 0x00000002, 0x00000041, 0x00000008, 0x0000000C, 0x00000001]
v7 = [0x2A2724211F1D1A17, 0x403D3A3734312F2D, 0x0000524F4C494643]   
v10 = [1, 4, 7, 10, 13, 16, 18, 20, 23, 26, 29, 31, 33, 36, 39, 42, 45, 47, 49, 52, 55, 58, 61, 64, 67, 70, 73, 76, 79, 82]
v11 = 0
for i in range(15):
    out[i] = flag[i]
solver = Solver()

for i in range(15):
    for j in range(2):
        opcode = v5[v10[v11 + j]]
        if opcode == 2:
            out[i] += v5[v10[v11 + j] + 1]
        elif opcode == 3:
            out[i] -= v5[v10[v11 + j] + 1]
        elif opcode == 4:
            out[i] ^= v5[v10[v11 + j] + 1]
        elif opcode == 5:
            out[i] *= v5[v10[v11 + j] + 1]
        elif opcode == 11:
            out[i] -= 1
        elif opcode == 12:
            out[i] += 1
    v11 += 2

for i in range(15):
    solver.add(out[i] == date[i])

if solver.check() == sat:
    condition = []
    model = solver.model()
    result = ""
    for i in range(15):
        result += chr(model[flag[i]].as_long())
        condition.append(flag[i] != model[flag[i]].as_long())
    print("Flag:" , result)
else:
    print("Failed to solve")

flag：

1	757515121f3d478

第四周总结：

这周的几个题还是有一定的难度，尤其是分析题目和写脚本部分，但是经过这几个题的练手，大概可以解一些简单的题了，尤其是在写Z3上有点心得了，不过还是需要进行做题去巩固学的知识。