第四题英雄救美 solved by Syclover-CTF对抗-看雪-安全社区|安全招聘|kanxue.com

第四题英雄救美 solved by Syclover

2021-5-14 15:51 5808

第四题英雄救美 solved by Syclover

无名侠

2021-5-14 15:51

5808

第四题英雄救美

为啥叫英雄救美？？？？全程没看到美女

sub_391240 对输入数据进行转换
这个函数有点小坑.....

table1 = [0x24, 0x42, 0x50, 0x56, 0x3A, 0x75, 0x62, 0x66, 0x59, 0x70, 0x7D, 0x5D, 0x44, 0x74, 0x4E, 0x3E, 0x61, 0x54, 0x5E, 0x4D, 0x47, 0x6D, 0x4A, 0x51, 0x23, 0x2A, 0x48, 0x72, 0x60, 0x4F, 0x27, 0x77, 0x6A, 0x69, 0x63, 0x30, 0x21, 0x68, 0x64, 0x79, 0x7B, 0x6F, 0x5A, 0x7A, 0x2D, 0x40, 0x6E, 0x2B, 0x3F, 0x26, 0x25, 0x73, 0x5F, 0x2F, 0x67, 0x3C, 0x65, 0x5B, 0x57, 0x29, 0x58, 0x55, 0x78, 0x52, 0x46, 0x53, 0x4C, 0x52, 0x41, 0x3B, 0x2E, 0x6C, 0x3D, 0x43, 0x45, 0x6B, 0x76, 0x4B, 0x2D, 0x28, 0x71]

$B$BP => 12123

sub_391000 9x9 数独 check

map1 = [0x00000000, 0x00000004, 0x00000000, 0x00000007, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000009, 0x00000002, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000006, 0x00000000, 0x00000007, 0x00000008, 0x00000003, 0x00000000, 0x00000000, 0x00000000, 0x00000005, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000001, 0x00000000, 0x00000000, 0x00000000, 0x00000003, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000002, 0x00000000, 0x00000001, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000005, 0x00000000, 0x00000000, 0x00000000, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000004, 0x00000009, 0x00000000, 0x00000000, 0x00000000, 0x00000007, 0x00000001, 0x00000003, 0x00000000, 0x00000005, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000009, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000008, 0x00000000, 0x00000006, 0x00000000]
 
mat = []
for y in range(9):
    line = list()
    for x in range(9):
        line.append(map1[y * 9 + x])
    mat.append(line)

数独输出如下

4 0 7 0 0 0 0 0
2 0 0 0 0 6 0 7
3 0 0 0 5 4 0 0
1 0 0 0 3 0 0 0
0 0 2 0 1 0 0 0
0 0 5 0 0 0 4 0
0 4 9 0 0 0 7 1
0 5 0 0 0 0 9 4
0 0 0 0 8 0 6 0

用 z3 脚本解一下数独

X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ] 
      for i in range(9) ]
 
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9) 
             for i in range(9) for j in range(9) ]
 
rows_c   = [ Distinct(X[i]) for i in range(9) ]
 
cols_c   = [ Distinct([ X[i][j] for i in range(9) ]) 
             for j in range(9) ]
 
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j] 
                        for i in range(3) for j in range(3) ]) 
             for i0 in range(3) for j0 in range(3) ]
 
sudoku_c = cells_c + rows_c + cols_c + sq_c
 
instance = [[0, 4, 0, 7, 0, 0, 0, 0, 0],
 [9, 2, 0, 0, 0, 0, 6, 0, 7],
 [8, 3, 0, 0, 0, 5, 4, 0, 0],
 [0, 1, 0, 0, 0, 3, 0, 0, 0],
 [0, 0, 0, 2, 0, 1, 0, 0, 0],
 [0, 0, 0, 5, 0, 0, 0, 4, 0],
 [0, 0, 4, 9, 0, 0, 0, 7, 1],
 [3, 0, 5, 0, 0, 0, 0, 9, 4],
 [0, 0, 0, 0, 0, 8, 0, 6, 0]]
 
instance_c = [ If(instance[i][j] == 0, 
                  True, 
                  X[i][j] == instance[i][j]) 
               for i in range(9) for j in range(9) ]
 
s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ] 
          for i in range(9) ]
    print_matrix(r)
else:
    print ("failed to solve")

得到结果

result = [[5, 4, 6, 7, 1, 9, 2, 3, 8],
 [9, 2, 1, 8, 3, 4, 6, 5, 7],
 [8, 3, 7, 6, 2, 5, 4, 1, 9],
 [7, 1, 8, 4, 6, 3, 9, 2, 5],
 [4, 5, 3, 2, 9, 1, 7, 8, 6],
 [6, 9, 2, 5, 8, 7, 1, 4, 3],
 [2, 8, 4, 9, 5, 6, 3, 7, 1],
 [3, 6, 5, 1, 7, 2, 8, 9, 4],
 [1, 7, 9, 3, 4, 8, 5, 6, 2]]

反推输入

dict_map = {}
for k in range(len(table1)):
    kk = k % 9 + 1
    if kk not in dict_map:
        dict_map[kk] = []
    dict_map[kk].append(table1[k])
 
for kk in dict_map:
    print(kk, dict_map[kk])
 
flag = ''
for y in range(9):
    cnt = 0
    for x in range(9):
        if instance[y][x] == 0:
            flag = flag + chr(dict_map[result[y][x]][y])
            cnt = cnt + 1
    flag = flag + chr(ord('9') - cnt)
print(flag)