[安洵杯 2019]Game复现

[安洵杯 2019]Game

IDA64打开

开了混淆，控制流平坦化，可以使用deflat.py进行去除。

要去除的有多个函数，再进行多次重复去除后可以得到

代码不多，慢慢分析，前面是一些生成数独以及检查。

直接看check部分，check没有做什么；

check1：

做了一些置换，以及简单运算。

有俩处，v9那里其实就是减去了48；后面用我们的输入去填D0g3这个数独，最后跟sudoku比较。

逆向，先将数独需要填入的拿出来，check1可以根据z3解。

EXP：

from z3 import *
sudoku = [1, 4, 5, 3, 2, 7, 6, 9, 8, 8, 3, 9, 6, 5, 4, 1, 2, 7, 6, 7, 2, 8, 1, 9, 5, 4, 3, 4, 9, 6, 1, 8, 5, 3, 7, 2,
           2, 1, 8, 4, 7, 3, 9, 5, 6, 7, 5, 3, 2, 9, 6, 4, 8, 1, 3, 6, 7, 5, 4, 2, 8, 1, 9, 9, 8, 4, 7, 6, 1, 2, 3, 5,
           5, 2, 1, 9, 3, 8, 7, 6, 4]
Dog3 = [1, 0, 5, 3, 2, 7, 0, 0, 8, 8, 0, 9, 0, 5, 0, 0, 2, 0, 0, 7, 0, 0, 1, 0, 5, 0, 3, 4, 9, 0, 1, 0, 0, 3, 0, 0, 0,
         1, 0, 0, 7, 0, 9, 0, 6, 7, 0, 3, 2, 9, 0, 4, 8, 0, 0, 6, 0, 5, 4, 0, 8, 0, 9, 0, 0, 4, 0, 0, 1, 0, 3, 0, 0, 2,
         1, 0, 3, 0, 7, 0, 4]
key = []
for i in range(81):
    if Dog3[i] == 0:
        key.append(sudoku[i]+48)
# key = [52, 54, 57, 51, 54, 52, 49, 55, 54, 50, 56, 57, 52, 54, 56, 53, 55, 50, 50, 56, 52, 51, 53, 53, 54, 49, 51, 55, 50, 49, 57, 56, 55, 54, 50, 53, 53, 57, 56, 54]
s = Solver()
x = [BitVec(f'x{i}', 8) for i in range(40)]
len1 = 40 >> 1
len2 = 40
for i in range(len1):
    x[i], x[len1] = x[len1], x[i]
    len1 += 1
for i in range(0, len2, 2):
    x[i], x[i + 1] = x[i + 1], x[i]
for i in range(len2):
    x[i] = (x[i] & 0xF3 | ~x[i] & 0xC) - 20
for i in range(len2):
    s.add(x[i] == key[i])

if s.check() == sat:
    model = s.model()
    sorted_model = sorted([(d.name(), model[d]) for d in model], key=lambda x: int(x[0][1:]))
    model_array = [value for name, value in sorted_model]

    print(model_array)

flag = [75, 68, 69, 69, 73, 70, 71, 75, 73, 74, 64, 65, 70, 71, 69, 74, 65, 69, 70, 64, 70, 68, 75, 65, 68, 70, 71, 73, 74, 70, 65, 64, 70, 68, 69, 64, 74, 71, 64, 74]
for i in range(40):
    print(chr(flag[i]),end='')
    
# KDEEIFGKIJ@AFGEJAEF@FDKADFGIJFA@FDE@JG@J