(天堂之门技术, 自解密, 不可逆算法, Z3求解问题)
查壳
无壳, 为Win32程序
运行
错误了会弹出神曲, 很搞笑
分析
使用ida进行分析
一开始下断点下在了sub_9B1940()这里, 然后调半天还是跳不动, 然后发现断点下在后面就没事了, 后来搜索搜到了相关的信息
https://bbs.pediy.com/thread-270153.htm 详细的信息在这个网站中
可以知道的是天堂之门的作用是在一个32位进程中执行64位的代码以及调用64位的API
主要分析算法
// 传入的参数为8个字符, 也就是长度为64为的明文
char __cdecl encode(int input, int o)
{
char result; // al
char right[32]; // [esp+0h] [ebp-D0h]
char big[128]; // [esp+20h] [ebp-B0h] BYREF
char left[32]; // [esp+A0h] [ebp-30h] BYREF
BOOL v6; // [esp+C0h] [ebp-10h]
BOOL v7; // [esp+C4h] [ebp-Ch]
int j; // [esp+C8h] [ebp-8h]
int i; // [esp+CCh] [ebp-4h]
for ( i = 0; i < 64; ++i )
{
big[i + 32] = *(input + dword_214820[i] - 1);// v4 的下标: 32 ~ 95 为input
result = i + 1;
}
for ( i = 0; i < 32; ++i )
{
big[i + 96] = big[i + 32]; // 96 ~ 127 为前四个字符
result = i + 1;
}
for ( i = 0; i < 32; ++i )
{
result = i;
left[i] = big[i + 64];
}
for ( j = 0; j < 16; ++j )
{
for ( i = 0; i < 32; ++i )
right[i] = left[i];
result = sub_211000(left, &outdata1[48 * j], big);// 后四个字符的字符经过加密后放在了前面四个字符的位置, 而input前面的四个字符在8~11的位置
for ( i = 0; i < 32; ++i ) // 注意此时v4的状况是: 0 ~ 31 为加密后的后四个字符, 32 ~ 63是未加密的前四个字符, 64 ~ 95是未加密的后四个字符, 96 ~ 127是未加密的前四个字符
{
v7 = big[i + 96] != big[i];
v6 = v7;
result = i;
left[i] = v6; // left[i] = 加密后的后四个字符[i] ^ 未加密的前四个字符[i]
}
for ( i = 0; i < 32; ++i )
{
result = i;
big[i + 96] = right[i]; // 第一次v3还是未加密的后四个字符, 到后面就变成了异或又的数据了
}
}
for ( i = 0; i < 32; ++i )
{
big[i + 32] = left[i];
result = i + 1;
}
for ( i = 0; i < 32; ++i )
{
result = i;
big[i + 64] = big[i + 96];
}
for ( i = 0; i < 64; ++i )
{
result = big[outdata3[i] + 31]; // 顺序的v5 后v3
*(i + o) = result;
}
return result;
}
跟进gub_211000()
int __cdecl sub_211000(int left, int y, int big)
{
int result; // eax
char v4[80]; // [esp+0h] [ebp-74h]
int env5; // [esp+50h] [ebp-24h]
int env6; // [esp+54h] [ebp-20h]
BOOL env7; // [esp+58h] [ebp-1Ch]
BOOL env8; // [esp+5Ch] [ebp-18h]
BOOL env9; // [esp+60h] [ebp-14h]
int env10; // [esp+64h] [ebp-10h]
int j; // [esp+68h] [ebp-Ch]
int env12; // [esp+6Ch] [ebp-8h]
int i; // [esp+70h] [ebp-4h]
for ( i = 0; i < 48; ++i )
{
v4[i] = *(left + table1[i] - 1); // table中有些数是重复的
result = i + 1;
}
for ( i = 0; i < 48; ++i ) // xor
{
env9 = v4[i] != *(i + y); // 这个就相当于一个位级的异或运算, 异或的a2数据可以dump下来
env8 = env9;
v4[i] = env8;
result = i + 1;
}
for ( i = 0; i < 8; ++i )
{
env12 = 6 * i;
env6 = v4[6 * i + 5] + 2 * v4[6 * i]; // 取首尾
env5 = v4[6 * i + 4] + 4 * v4[6 * i + 2] + 8 * v4[6 * i + 1] + 2 * v4[6 * i + 3];// 取中间
result = env5;
env10 = table2[64 * i + 16 * env6 + env5]; // 这里的变换有点像是拼图, 首位变成开头的两个位,中间四个位移到了后面, 然后再充当下标从table2中取值放在v10中
env12 = 4 * i;
for ( j = 3; j >= 0; --j ) // 注意j是从3开始的, 总共进行4次
{
env7 = env10 % 2 != 0; // 这个其实就看最后一位就可以判断了, 偶数则v7 = 0, 奇数则v7 = 1
v4[j + 48 + env12] = env7; // 这个是在v4后面补上的
env10 /= 2; // 这时的v10已经是取到了table的值了
result = j - 1;
}
}
for ( i = 0; i < 32; ++i )
{
result = table3[i];
*(i + big) = v4[result + 47]; // 最终给a3通过table3的顺序附上加密后的数据
}
return result;
}
首先尝试了z3求解
from z3 import *
inpuu = [Int('inpuu%d' % i) for i in range(64)]
s = Solver()
big = [0] * 128
left = [0] * 32
right = [0] * 32
v4 = [0] * 48
o = [0] * 64
ip = [0] * 64
output0 = [0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 1, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 0, 1, 0, 1, 0, 1, 1, 0]
index2 = [58, 50, 42, 34, 26, 18, 10, 2, 60, 52,
44, 36, 28, 20, 12, 4, 62, 54, 46, 38,
30, 22, 14, 6, 64, 56, 48, 40, 32, 24,
16, 8, 57, 49, 41, 33, 25, 17, 9, 1, 59,
51, 43, 35, 27, 19, 11, 3, 61, 53, 45, 37,
29, 21, 13, 5, 63, 55, 47, 39, 31, 23, 15,
7]
outdata1 = [0x01, 0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x00, 0x00,
0x00, 0x01, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x01,
0x00, 0x01, 0x01, 0x00, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00,
0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00,
0x00, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x00, 0x00, 0x01,
0x00, 0x00, 0x00, 0x00, 0x00, 0x01, 0x00, 0x01, 0x00, 0x00,
0x01, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x00, 0x00, 0x00,
0x01, 0x01, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x00, 0x01,
0x00, 0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x00, 0x00,
0x01, 0x01, 0x01, 0x01, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00,
0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x01, 0x01, 0x00, 0x00,
0x00, 0x01, 0x01, 0x00, 0x01, 0x01, 0x00, 0x00, 0x00, 0x01,
0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01,
0x01, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x00, 0x01, 0x01,
0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01,
0x00, 0x01, 0x01, 0x00, 0x00, 0x00, 0x00, 0x01, 0x01, 0x01,
0x01, 0x01, 0x00, 0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00,
0x01, 0x01, 0x00, 0x00, 0x00, 0x01, 0x00, 0x01, 0x01, 0x00,
0x01, 0x00, 0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01,
0x00, 0x01, 0x00, 0x01, 0x01, 0x01, 0x00, 0x00, 0x01, 0x01,
0x00, 0x01, 0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x00,
0x00, 0x01, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01,
0x00, 0x00, 0x01, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x00,
0x01, 0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x01, 0x01,
0x00, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x00,
0x00, 0x01, 0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00, 0x00,
0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01,
0x01, 0x01, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x01, 0x01,
0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x01, 0x01, 0x00, 0x00,
0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x00,
0x00, 0x00, 0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01,
0x01, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01,
0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x01,
0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00, 0x00, 0x01, 0x01,
0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00,
0x00, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x00, 0x00,
0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01, 0x00,
0x01, 0x00, 0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00, 0x00,
0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x00, 0x01,
0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x01, 0x00, 0x01,
0x00, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00, 0x01,
0x01, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x00,
0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00, 0x00, 0x01, 0x01,
0x01, 0x01, 0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x00,
0x01, 0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x01, 0x01,
0x00, 0x00, 0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x01, 0x00,
0x00, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01,
0x00, 0x01, 0x01, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x01,
0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x00, 0x01, 0x01, 0x01,
0x00, 0x00, 0x01, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0x01, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01, 0x01,
0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01,
0x00, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01,
0x01, 0x00, 0x00, 0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x00,
0x00, 0x00, 0x00, 0x01, 0x01, 0x00, 0x00, 0x00, 0x01, 0x00,
0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01, 0x00,
0x01, 0x01, 0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01,
0x01, 0x00, 0x01, 0x00, 0x01, 0x00, 0x00, 0x00, 0x01, 0x01,
0x00, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x01, 0x01,
0x00, 0x00, 0x01, 0x00, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01,
0x00, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x00, 0x01, 0x01,
0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x01,
0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x01,
0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x00, 0x00, 0x00,
0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x01, 0x00, 0x01, 0x01,
0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01, 0x00, 0x01,
0x01, 0x01, 0x00, 0x00, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00,
0x00, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00,
0x01, 0x00, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x01, 0x00,
0x01, 0x01, 0x00, 0x01, 0x00, 0x00, 0x01, 0x01, 0x00, 0x00,
0x01, 0x00, 0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01,
0x01, 0x00, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00, 0x00, 0x00,
0x01, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x01, 0x01,
0x01, 0x01, 0x00, 0x01, 0x00, 0x01, 0x00, 0x01, 0x00, 0x00,
0x00, 0x01, 0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x00,
0x00, 0x01, 0x01, 0x01, 0x00, 0x01, 0x01, 0x01, 0x01, 0x00,
0x00, 0x00, 0x01, 0x01, 0x01, 0x00, 0x00, 0x00]
table1 = [32, 1, 2, 3, 4, 5, 4, 5, 6, 7, 8, 9, 8, 9,
10, 11, 12, 13, 12, 13, 14, 15, 16, 17, 16,
17, 18, 19, 20, 21, 20, 21, 22, 23, 24, 25,
24, 25, 26, 27, 28, 29, 28, 29, 30, 31, 32,
1]
table2 = [0xe, 0x4, 0xd, 0x1, 0x2, 0xf, 0xb, 0x8, 0x3, 0xa, 0x6, 0xc, 0x5, 0x9, 0x0, 0x7,
0x0, 0xf, 0x7, 0x4, 0xe, 0x2, 0xd, 0x1, 0xa, 0x6, 0xc, 0xb, 0x9, 0x5, 0x3, 0x8,
0x4, 0x1, 0xe, 0x8, 0xd, 0x6, 0x2, 0xb, 0xf, 0xc, 0x9, 0x7, 0x3, 0xa, 0x5, 0x0,
0xf, 0xc, 0x8, 0x2, 0x4, 0x9, 0x1, 0x7, 0x5, 0xb, 0x3, 0xe, 0xa, 0x0, 0x6, 0xd,
0xf, 0x1, 0x8, 0xe, 0x6, 0xb, 0x3, 0x4, 0x9, 0x7, 0x2, 0xd, 0xc, 0x0, 0x5, 0xa,
0x3, 0xd, 0x4, 0x7, 0xf, 0x2, 0x8, 0xe, 0xc, 0x0, 0x1, 0xa, 0x6, 0x9, 0xb, 0x5,
0x0, 0xe, 0x7, 0xb, 0xa, 0x4, 0xd, 0x1, 0x5, 0x8, 0xc, 0x6, 0x9, 0x3, 0x2, 0xf,
0xd, 0x8, 0xa, 0x1, 0x3, 0xf, 0x4, 0x2, 0xb, 0x6, 0x7, 0xc, 0x0, 0x5, 0xe, 0x9,
0xa, 0x0, 0x9, 0xe, 0x6, 0x3, 0xf, 0x5, 0x1, 0xd, 0xc, 0x7, 0xb, 0x4, 0x2, 0x8,
0xd, 0x7, 0x0, 0x9, 0x3, 0x4, 0x6, 0xa, 0x2, 0x8, 0x5, 0xe, 0xc, 0xb, 0xf, 0x1,
0xd, 0x6, 0x4, 0x9, 0x8, 0xf, 0x3, 0x0, 0xb, 0x1, 0x2, 0xc, 0x5, 0xa, 0xe, 0x7,
0x1, 0xa, 0xd, 0x0, 0x6, 0x9, 0x8, 0x7, 0x4, 0xf, 0xe, 0x3, 0xb, 0x5, 0x2, 0xc,
0x7, 0xd, 0xe, 0x3, 0x0, 0x6, 0x9, 0xa, 0x1, 0x2, 0x8, 0x5, 0xb, 0xc, 0x4, 0xf,
0xd, 0x8, 0xb, 0x5, 0x6, 0xf, 0x0, 0x3, 0x4, 0x7, 0x2, 0xc, 0x1, 0xa, 0xe, 0x9,
0xa, 0x6, 0x9, 0x0, 0xc, 0xb, 0x7, 0xd, 0xf, 0x1, 0x3, 0xe, 0x5, 0x2, 0x8, 0x4,
0x3, 0xf, 0x0, 0x6, 0xa, 0x1, 0xd, 0x8, 0x9, 0x4, 0x5, 0xb, 0xc, 0x7, 0x2, 0xe,
0x2, 0xc, 0x4, 0x1, 0x7, 0xa, 0xb, 0x6, 0x8, 0x5, 0x3, 0xf, 0xd, 0x0, 0xe, 0x9,
0xe, 0xb, 0x2, 0xc, 0x4, 0x7, 0xd, 0x1, 0x5, 0x0, 0xf, 0xa, 0x3, 0x9, 0x8, 0x6,
0x4, 0x2, 0x1, 0xb, 0xa, 0xd, 0x7, 0x8, 0xf, 0x9, 0xc, 0x5, 0x6, 0x3, 0x0, 0xe,
0xb, 0x8, 0xc, 0x7, 0x1, 0xe, 0x2, 0xd, 0x6, 0xf, 0x0, 0x9, 0xa, 0x4, 0x5, 0x3,
0xc, 0x1, 0xa, 0xf, 0x9, 0x2, 0x6, 0x8, 0x0, 0xd, 0x3, 0x4, 0xe, 0x7, 0x5, 0xb,
0xa, 0xf, 0x4, 0x2, 0x7, 0xc, 0x9, 0x5, 0x6, 0x1, 0xd, 0xe, 0x0, 0xb, 0x3, 0x8,
0x9, 0xe, 0xf, 0x5, 0x2, 0x8, 0xc, 0x3, 0x7, 0x0, 0x4, 0xa, 0x1, 0xd, 0xb, 0x6,
0x4, 0x3, 0x2, 0xc, 0x9, 0x5, 0xf, 0xa, 0xb, 0xe, 0x1, 0x7, 0x6, 0x0, 0x8, 0xd,
0x4, 0xb, 0x2, 0xe, 0xf, 0x0, 0x8, 0xd, 0x3, 0xc, 0x9, 0x7, 0x5, 0xa, 0x6, 0x1,
0xd, 0x0, 0xb, 0x7, 0x4, 0x9, 0x1, 0xa, 0xe, 0x3, 0x5, 0xc, 0x2, 0xf, 0x8, 0x6,
0x1, 0x4, 0xb, 0xd, 0xc, 0x3, 0x7, 0xe, 0xa, 0xf, 0x6, 0x8, 0x0, 0x5, 0x9, 0x2,
0x6, 0xb, 0xd, 0x8, 0x1, 0x4, 0xa, 0x7, 0x9, 0x5, 0x0, 0xf, 0xe, 0x2, 0x3, 0xc,
0xd, 0x2, 0x8, 0x4, 0x6, 0xf, 0xb, 0x1, 0xa, 0x9, 0x3, 0xe, 0x5, 0x0, 0xc, 0x7,
0x1, 0xf, 0xd, 0x8, 0xa, 0x3, 0x7, 0x4, 0xc, 0x5, 0x6, 0xb, 0x0, 0xe, 0x9, 0x2,
0x7, 0xb, 0x4, 0x1, 0x9, 0xc, 0xe, 0x2, 0x0, 0x6, 0xa, 0xd, 0xf, 0x3, 0x5, 0x8,
0x2, 0x1, 0xe, 0x7, 0x4, 0xa, 0x8, 0xd, 0xf, 0xc, 0x9, 0x0, 0x3, 0x5, 0x6, 0xb]
table3 = [0x10, 0x7, 0x14, 0x15, 0x1d, 0xc, 0x1c, 0x11, 0x1, 0xf, 0x17, 0x1a,
0x5, 0x12, 0x1f, 0xa, 0x2, 0x8, 0x18, 0xe, 0x20, 0x1b, 0x3, 0x9, 0x13,
0xd, 0x1e, 0x6, 0x16, 0xb, 0x4, 0x19]
outdata3 = [0x28, 0x8, 0x30, 0x10, 0x38, 0x18, 0x40, 0x20, 0x27, 0x7,
0x2f, 0xf, 0x37, 0x17, 0x3f, 0x1f, 0x26, 0x6, 0x2e, 0xe,
0x36, 0x16, 0x3e, 0x1e, 0x25, 0x5, 0x2d, 0xd, 0x35, 0x15,
0x3d, 0x1d, 0x24, 0x4, 0x2c, 0xc, 0x34, 0x14, 0x3c, 0x1c,
0x23, 0x3, 0x2b, 0xb, 0x33, 0x13, 0x3b, 0x1b, 0x22, 0x2,
0x2a, 0xa, 0x32, 0x12, 0x3a, 0x1a, 0x21, 0x1, 0x29, 0x9,
0x31, 0x11, 0x39, 0x19]
for i in range(64):
ip[i] = inpuu[i]
for i in range(64):
big[i + 32] = ip[index2[i] - 1]
result = i + 1
for i in range(32):
big[i + 96] = big[i + 32]
result = i + 1
for i in range(32):
result = i
left[i] = big[i + 64]
for y in range(16):
for x in range(32):
right[x] = left[x]
#从这里开始就是encode函数
for i in range(48):
v4[i] = left[table1[i] - 1]
enresult = i + 1
for i in range(48):
env9 = (v4[i] != outdata1[48 * y + i])
v4[i] = env9
result += 1
for i in range(8):
env12 = i * 6
env6 = v4[6 * i + 5] + 2 * v4[6 * i]
env5 = v4[6 * i + 4] + 4 * v4[6 * i + 2] + 8 * v4[6 * i + 1] + 2 * v4[6 * i + 3]
result = env5
t = (64 * i) + (16 * env6) + env5
env10 = table2[t]
env12 = 4 * i
for j in range(3, -1, -1):
env7 = ((env10 % 2) != 0)
v4[j + 48 + env12] = env7
env10 //= 2#!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
result = j - 1
for i in range(32):
result = table3[i]
big[i] = v4[result + 47]
#到这里encode结束
for i in range(32):
v7 = (big[i + 96] != big[i])
result = i
left[i] = v7
for i in range(32):
result = i
big[i + 96] = right
for i in range(32):
big[i + 32] = left[i]
result = i + 1
for i in range(32):
result = i
big[i + 64] = big[i + 96]
for i in range(64):
result = big[outdata3[i] + 31]
o[i] = result
for i in range(64):
s.add(o[i] == output0[i])
if s.check() == sat:
m = s.model()
for i in range(64):
print(int("%d" % (m[inpuu[i]])), end='')
else:
print("failed to solve")
由于所设的未知数inpuu是不能作为数组的下标的, 所以无法使用z3来求解
逆向算法
也行不通, 因为这个步骤
这一步是通过对table2中的一个元素取值, 然后用其正负来决定一个位是0还是1, 但是table2中有大量的重复元素, 这道值算法逆向的时候有多种不同的结果, 所以算法是很难逆的
最
最后发现了题目本身带有自解密, 之前也遇到过, 所以还是审题不仔细, 浪费了大量的时间
解密过程进行之前修改Buf2的内存, 改为参考密文即可实现解密得出正确的flag
汇编语言更清晰
修改后记得右键apply change
步过到return 0
得到明文
flag
hgame{WOWOW_h @ ppy_n3w_ye4r_2022}