Ciscn 2020 Re 部分题解

这比赛我也是没话说，不知道是不是因为某“鼎尖赛事”中逆向出了问题让某秋被骂的很惨，这次国赛直接放两道签到题。题目数量最少，难度跨度极大，简单题是个人都会做，最后一个难题又偏的不得了（神他妈智能合约逆向），反正感觉这次国赛初赛体验极差

0x01 z3

main
这题直接Z3一把梭，唯一要注意的时候就是数据提取的时候要小端序整理一下,然后可以在输入这个地方创建以下数组，然后复制出来批量替换v46会比较方便
main
main

 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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57


c = "17 4F 00 00 F6 9C 00 00 DB 8D 00 00 A6 8E 00 00 29 69 00 00 11 99 00 00 A2 40 00 00 3E 2F 00 00 B6 62 00 00 82 4B 00 00 6C 48 00 00 02 40 00 00 D7 52 00 00 EF 2D 00 00 DC 28 00 00 0D 64 00 00 8F 52 00 00 3B 61 00 00 81 47 00 00 17 6B 00 00 37 32 00 00 93 2A 00 00 5F 61 00 00 BE 50 00 00 8E 59 00 00 56 46 00 00 31 5B 00 00 3A 31 00 00 10 30 00 00 FE 67 00 00 5F 4D 00 00 DB 58 00 00 99 37 00 00 A0 60 00 00 50 27 00 00 59 37 00 00 53 89 00 00 22 71 00 00 F9 81 00 00 24 55 00 00 71 89 00 00 1D 3A 00 00".split()
ciper = []
for i in range(168//4):
    ciper.append(c[i*4+3])
    ciper[i] += c[i*4+2]
    ciper[i] += c[i*4+1]
    ciper[i] += c[i*4]
ciper = [eval(i.replace("0000","0x")) for i in ciper]
print(ciper)

from z3 import *
flag = [Int("flag%d" % i) for i in range(42)]
solver = Solver()

solver.add(ciper[4 -4]==34 * flag[3]
     + 12 * flag[0]
     + 53 * flag[1]
     + 6 * flag[2]
     + 58 * flag[4]
     + 36 * flag[5]
     + flag[6])
solver.add(ciper[5 -4]==27 * flag[4]
     + 73 * flag[3]
     + 12 * flag[2]
     + 83 * flag[0]
     + 85 * flag[1]
     + 96 * flag[5]
     + 52 * flag[6])
solver.add(ciper[6 -4]==24 * flag[2]
     + 78 * flag[0]
     + 53 * flag[1]
     + 36 * flag[3]
     + 86 * flag[4]
     + 25 * flag[5]
     + 46 * flag[6])
solver.add(ciper[7 -4]==78 * flag[1]
     + 39 * flag[0]
     + 52 * flag[2]
     + 9 * flag[3]
     + 62 * flag[4]
     + 37 * flag[5]
     + 84 * flag[6])
solver.add(ciper[8 -4]==48 * flag[4]
     + 14 * flag[2]
     + 23 * flag[0]
     + 6 * flag[1]
     + 74 * flag[3]
     + 12 * flag[5]
     + 83 * flag[6])

......（以下省略n个方程）

print(solver.check())
if solver.check() == sat:
    model = solver.model()
    result = [ chr( model[flag[i]].as_long() ) for i in range(42) ]
    print("".join(result))

0x02 hyperthreading

多线程反调
main
在main函数中可以看到开了3个线程，其中只有第一个线程函数也就是 StartAddress 里面才是真正算法。第二个线程函数 sub_401200 会将输入的每一字节与当前TIB的BingDebugged位相加后保存。因为当程序被调试后，BeingDebugged位为1，与之相加，就会将输入改变掉。这个函数的处理方法有很多种，可以在main函数里直接把这次 CreateThread 整个过程nop掉，也可以将 sub_401200 空间全部nop掉，再不济，最笨的方法就是动调时在 sub_401200 函数开头处下断，然后修改这个线程的TIB.BingDebugged位。第三条线程 loc_401240 里面其实就是循环调用 IsDebuggerPresent API，如果检测掉调试器就exit。本质上 IsDebuggerPresent 函数也就是检测BingDebugged标志位，但这个有一个注意点，就是这个标志位是线程独立的，也就是说我们不能仅仅修改一处，要把每个线程都改过来。我这里嫌麻烦，直接将该函数 jnz short loc_401247 指令后又添了一条指令 jz short loc_401247，也就是说不管BingDebugged位是否为真都跳转，也就是在这里实现了一个真死循环，从而让反调无效。

然后看算法里面动调一下把花指令patch一下，可以看到算法是非常简单的，两次移位一次异或一次加法，同样会又BingDebugged位参与运算，这里直接上脚本了
main

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16


ciper = [
    0xDD, 0x5B, 0x9E, 0x1D, 0x20, 0x9E, 0x90, 0x91, 0x90, 0x90, 
    0x91, 0x92, 0xDE, 0x8B, 0x11, 0xD1, 0x1E, 0x9E, 0x8B, 0x51, 
    0x11, 0x50, 0x51, 0x8B, 0x9E, 0x5D, 0x5D, 0x11, 0x8B, 0x90, 
    0x12, 0x91, 0x50, 0x12, 0xD2, 0x91, 0x92, 0x1E, 0x9E, 0x90, 
    0xD2, 0x9F
]

for i in range(len(ciper)):
    ciper[i] -= 0x23
    if ciper[i] <0:
        ciper[i] += 0x100
    ciper[i] ^= 0x23
    ciper[i] = ((ciper[i] >> 6) ^ (ciper[i]<<2))&0xFF
print(ciper)
print("".join([chr(i) for i in ciper]))