notsudoku
V&NCTF直接白给了，全程耗在了Crackme2上，辛辛苦苦找到密文和算法后发现需要动态调试？过程中not sudoku这题就扫了一眼，结果还没发现是python逆向，于是就爬爬了。
正文
好像是第一次做python exe的逆向
首先使用 exeinfo 差壳，发现有个 UPX
用 upx.exe -d 脱壳
比赛的时候没想到这个是python逆向，直接拖到ida里面了，于是直接gg
再使用 exeinfo 查一下，会发现是 pyinstaller 编译的文件，说明是python逆向
上网下载一下 pyinstxtractor.py 进行反编译
$ python3 pyinstxtractor.py notsudoku-noupx.exe
进入文件夹，找没有后缀的文件，发现有一个叫做 2 的，使用 010editor 从 struct 文件复制文件头（第一行），然后添加 .pyc 后缀，进行 pyc 反编译
$ uncompyle6 -o 2.py 2.pyc
即可得到 python 源码文件
发现文件里有一些日文，于是边阅读边修改就行
# uncompyle6 version 3.7.4
# Python bytecode 3.7 (3394)
# Decompiled from: Python 3.6.9 (default, Jan 26 2021, 15:33:00)
# [GCC 8.4.0]
# Embedded file name: 2.py
# Compiled at: 1995-09-28 00:18:56
# Size of source mod 2**32: 272 bytes
import time, sys, hashlib
class class_a:
def __init__(self):
self.dic = {}
self.list_a = []
self.inputflag = ''
self.list_b = []
self.int = 65
def え(self, other):
def の(f):
self.dic[other] = f
return f
return の
def お(self, other):
return self.dic.get(other)
def run(self):
i = 0
while True:
invoke = self.list_a[i][0]
value = self.list_a[i][1]
value_2 = self.list_a[i][2]
func = self.お(invoke)
func(value, value_2)
i += 1
object_a = class_a()
@object_a.え('add')
def f(a, b):
if a == 1:
object_a.list_b += b
@object_a.え('string')
def f(a, b):
if a == 1:
print(object_a.inputflag)
else:
if a == 2:
print(object_a.list_b)
else:
if a == 3:
print((object_a.flag), end='')
else:
print(a, end='')
@object_a.え('exit')
def f(a, b):
sys.exit()
@object_a.え('input')
def f(a, b):
object_a.inputflag = input()
@object_a.え('sleep')
def f(a, b):
time.sleep(a)
@object_a.え('crypt')
def f(a, b):
if len(object_a.inputflag) % 2 != 0:
sys.exit()
for i in object_a.inputflag:
if ord(i) > 52 or ord(i) < 48: # input > '0', input < '4'
sys.exit()
x = str(hashlib.new('md5', bytes((object_a.inputflag), encoding='utf8')).hexdigest())
if x[:6] != 'e3a912': # md5 start with 'e3a912'
sys.exit()
object_a.flag = x
@object_a.え('initlist')
def f(a, b):
j = 0
for i in range(0, len(object_a.inputflag), 2):
j += 1
a = int(object_a.inputflag[i])
b = int(object_a.inputflag[(i + 1)])
object_a.list_b[a][b] = j # 为list_b赋值
@object_a.え('basiccheck')
def f(a, b):
if object_a.list_b[0][1] != 24 or object_a.list_b[4][3] != 2:
sys.exit()
if object_a.list_b[0][2] != 1 or object_a.list_b[2][3] != 20:
sys.exit()
if object_a.list_b[1][0] != 23 or object_a.list_b[3][4] != 3:
sys.exit()
# 024334xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx23xxxx1001xx
@object_a.え('check')
def f(a, b):
int = 0
if b == -1:
for i in range(5):
int += object_a.list_b[a][i]
if int != object_a.int:
sys.exit()
else:
for i in range(5):
int += object_a.list_b[i][b]
if int != object_a.int:
sys.exit()
# list_b 每行每列和为65
# 02433420112112034430403122130414004132233324100142
object_a.list_a = [
[
'string', 'welcome baby~ ', 0],
[
'string', 'input your flag~:', 0],
[
'input', 0, 0],
[
'string', 'your input is:', 0],
[
'string', 1, 0],
[
'string', "let's check......", 0],
[
'sleep', 0.5, 0],
[
'add', 1, [[0 for i in range(5)]]],
[
'add', 1, [[0 for i in range(5)]]],
[
'add', 1, [[0 for i in range(5)]]],
[
'add', 1, [[0 for i in range(5)]]],
[
'add', 1, [[0 for i in range(5)]]], # list_b 包含5个五元list
[
'crypt', 0, 0],
[
'initlist', 0, 0],
[
'basiccheck', 0, 0],
[
'check', 0, -1],
[
'check', 1, -1],
[
'check', 2, -1],
[
'check', 3, -1],
[
'check', 4, -1],
[
'check', 0, 0],
[
'check', 0, 1],
[
'check', 0, 2],
[
'check', 0, 3],
[
'check', 0, 4],
[
'string', 'Goodjob!', 0],
[
'string', 'The flag is vnctf{', 0],
[
'string', 3, 0],
[
'string', '}', 0],
[
'exit', 0, 0]]
object_a.run()
不太懂python的注解，这里好像是通过给定的字符串调用相应的函数？
整体就是一个五阶幻方，最后使用hashlib里的md5算一下
>>> import hashlib
>>> hashlib.new('md5', bytes(('02433420112112034430403122130414004132233324100142'), encoding='utf8')).hexdigest()
'e3a912c1e911ad82544af0c3d753f44f'
套上 vnctf{} 即可
FilpGame
官方WP写的好玄学，其实用z3也可以解的
逆向分析
拖入ida，通过字符串定位到关键代码。
sub_401020("Input: ");
sub_401050("%s", inputstring, 512);
v0 = 0;
v13 = 0;
if ( inputstring[0] )
{
v1 = dword_403398;
v2 = dword_40339C;
v14 = dword_403398;
while ( v0 < 214 )
{
v3 = v0;
v4 = &inputstring[v0];
v5 = v3 & 1;
if ( v5 ) // 第奇数位
{
v6 = *v4;
if ( (unsigned __int8)(*v4 - '0') > 9u )
{
if ( (unsigned __int8)(v6 - 'A') > 0x19u )// 大于大写字母时
{
v2 = -1;
dword_40339C = -1;
}
else // 大写字母时
{
v2 = v6 - '7';
dword_40339C = v6 - '7';
}
}
else // 为数字时
{
v2 = v6 - '0';
dword_40339C = v6 - '0';
}
}
else // 偶数位
{
v7 = *v4;
if ( (unsigned __int8)(*v4 - '0') > 9u )
{
if ( (unsigned __int8)(v7 - 'A') > 0x19u )
{
dword_403398 = -1;
break;
}
v1 = v7 - '7';
}
else
{
v1 = v7 - '0';
}
dword_403398 = v1;
v14 = v1;
}
if ( v1 > 0xF || v2 > 0xF ) // 不能大于F
break;
if ( v5 ) // 奇数时，两位两位进行计算
{
if ( dword_403018 >= (signed int)(v1 + 16 * v2) )// 0FFFFFFFF
break;
dword_403018 = v1 + 16 * v2; // v1为列，v2为行
v8 = 0;
do
{
v9 = v1 + dword_40212C[v8]; // -1 0 0 0 1 先输入的数
v10 = v2 + dword_402140[v8]; // 0 0 -1 1 0 后输入的数
if ( v9 <= 0xF && v10 <= 0xF )
final_check[v10] ^= 1 << (15 - v9); // 将所选位置及周围一圈的数字都进行取反，位置用大写十六进制表示
v1 = v14;
++v8;
}
while ( v8 < 5 );
}
v0 = v13 + 1;
v13 = v0;
if ( !inputstring[v0] )
goto LABEL_25;
}
}
else
{
LABEL_25:
v11 = final_check; // 目标：均为-1
while ( *v11 == -1 )
{
++v11;
if ( (signed int)v11 >= (signed int)&unk_40303C )
{
sub_401020("right, vnctf{MD5(%s)}\n");
return 0;
}
}
}
sub_401020("wrong\n");
return 0;
脚本求解
简单的说就是已知一个 $16\times 16$ 的 $01$ 方阵，每次对一个格子取反，都会对相邻的四个格子同样进行取反，最终求解一个操作顺序使得所有的数字为 $1$。
一开始写了个回溯，然后直接炸了。
经过队友的提醒开始用z3求解（队友的z3还是从我这里学的。。。），但没想到踩到了好多坑，也学会了一些z3的新用法。
直接上最后的代码。
from z3 import *
init_check = [
[1, 0, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 0, 1],
[1, 0, 0, 0, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0, 0],
[1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 1, 0, 0, 1],
[0, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 0],
[1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0],
[1, 0, 1, 0, 0, 0, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1],
[1, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0],
[0, 1, 0, 0, 1, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0],
[0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 1, 1, 0, 0],
[0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0],
[0, 1, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1],
[1, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1],
[0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0],
[1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1],
[0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 1],
[0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0]
]
posx = [0, -1, 0, 1, 0]
posy = [0, 0, -1, 0, 1]
solver = Solver()
change = [ [BitVec('change%x%x' % (i, j), 2) for j in range(16)] for i in range(16) ]
for i in range(16):
for j in range(16):
for k in range(5):
if i + posx[k] >= 0 and i + posx[k] < 16 and j + posy[k] >= 0 and j + posy[k] < 16:
init_check[i][j] ^= (change[i + posx[k]][j + posy[k]])
for i in range(16):
for j in range(16):
solver.add(change[i][j] & 2 == 0)
for i in range(16):
for j in range(16):
solver.add(init_check[i][j] == 1)
while solver.check() == sat:
length = 0
model = solver.model()
for i in range(16):
for j in range(16):
if model[change[i][j]] == 1:
length += 2
if length < 220:
for i in range(16):
for j in range(16):
if model[change[i][j]] == 1:
print ('%X%X' % (j, i), end = '')
print ()
condition = []
for i in range(16):
for j in range(16):
condition.append(change[i][j] != int("%s" % (model[change[i][j]])))
solver.add(Or(condition))
print ('\nfinish')
运行结果
$ FilpGame python3 solve.py
2050608090A0B0C0D02131417191A1B1527282B2D2E2F213234363B3D36494C4D4E415456575C5D5E50626566686C6F6071787B7C72838587898C8D81949596999B9C9F95A8AAAEA0B1B3B4B7B1C2C3C4C6C9CBCEC0D4D7D9DBDCDED0E1E3E4E5E6E8E9ECEEEFE3F7F8FBF
finish
过程中踩到的坑：
- 这道题的行和列很绕，一定要看清楚；
- 不知道为什么，
BitVec大小不能设置成 $1$； - 这题的解有很多，所以最后需要用一个
condition和Or来找到所有的解； - 如果对数没有最基本的约束的话，可能会出现一堆
None的情况。
程序运行结果
$ FilpGame ./FilpGame.exe
Input: 2050608090A0B0C0D02131417191A1B1527282B2D2E2F213234363B3D36494C4D4E415456575C5D5E50626566686C6F6071787B7C72838587898C8D81949596999
B9C9F95A8AAAEA0B1B3B4B7B1C2C3C4C6C9CBCEC0D4D7D9DBDCDED0E1E3E4E5E6E8E9ECEEEFE3F7F8FBF
right, vnctf{MD5(2050608090A0B0C0D02131417191A1B1527282B2D2E2F213234363B3D36494C4D4E415456575C5D5E50626566686C6F6071787B7C72838587898C8D8
1949596999B9C9F95A8AAAEA0B1B3B4B7B1C2C3C4C6C9CBCEC0D4D7D9DBDCDED0E1E3E4E5E6E8E9ECEEEFE3F7F8FBF)}
最后算一下md5
>>> import hashlib
>>> hl = hashlib.md5()
>>> str = '2050608090A0B0C0D02131417191A1B1527282B2D2E2F213234363B3D36494C4D4E415456575C5D5E50626566686C6F6071787B7C72838587898C8D81949596999B9C9F95A8AAAEA0B1B3B4B7B1C2C3C4C6C9CBCEC0D4D7D9DBDCDED0E1E3E4E5E6E8E9ECEEEFE3F7F8FBF'
>>> hl.update(str.encode(encoding='utf-8'))
>>> hl.hexdigest()
'c51a6d6d3929cd2a0192572e604b371d'
拿到flag！
总结
又学到了一些z3的用法，真不戳。
这道题告诉我们，以后算法题无脑上z3就完事了。。。
鸣谢
感谢 SSGSS 师傅，在我纠结于官方WP的解法时提醒我还有Z3这个神奇的东西！