Z3约束器
IDA动态调试
Linux逆向(Linux Reverse)
__int64 __fastcall check(__int64 a1, __int64 a2)
{
__int64 result; // rax
int i; // [rsp+14h] [rbp-Ch]
int breakflag; // [rsp+18h] [rbp-8h]
int j; // [rsp+1Ch] [rbp-4h]
for ( i = 0; ; ++i )
{
result = *(i + a1);
if ( !result )
break;
breakflag = 0;
for ( j = 0; *(j + a2); ++j )
{
if ( *(i + a1) == *(j + a2) )
{
breakflag = 1;
break;
}
}
if ( !breakflag )
{
puts("Error: invalid input");
exit(0);
}
}
return result;
}
这段代码会限制你输入的字符必须属于其中："01234_asdzxcpoityumnbAOZWXGMY"
_BYTE *__fastcall checkposition(const char *flag, const char *table, __int64 pos)
{
_BYTE *result; // rax
int i; // [rsp+20h] [rbp-10h]
int j; // [rsp+24h] [rbp-Ch]
int table_len; // [rsp+28h] [rbp-8h]
int flag_len; // [rsp+2Ch] [rbp-4h]
table_len = strlen(table);
flag_len = strlen(flag);
for ( i = 0; i < flag_len; ++i )
{
*(i + pos) = '-';
for ( j = 0; j < table_len; ++j )
{
if ( flag[i] == table[j] )
{
*(i + pos) = j + 48;
break;
}
}
}
result = (flag_len + pos);
*result = 0;
return result;
}
这段代码会将你输入的字符在”01234_asdzxcpoityumnbAOZWXGMY“中寻找序号
比如你的字符为”0“-》位置就为序号0
将位置信息存放在：position中，首先将数字0转化为字符‘0’
其中：
ord('0') = 0 + 48
ord('1') = 1 + 48
.....
所以position存放的是位置坐标！
unsigned __int64 __fastcall exchange(char *position, __int64 number)
{
unsigned __int64 size; // 存储变量的大小
void *ptr; // 存储指针
__int64 number_copy; // 存储 number 的副本
char *position_copy; // 存储 position 的副本
int i; // 循环变量
int j; // 循环变量
int position_len; // 存储 position 的长度
int v10; // 临时变量
__int64 position_len_1; // 存储 position 的长度减一
__int64 *number_ptr; // 存储 number 的指针
unsigned __int64 v13; // 存储返回值
position_copy = position; // 将 position 的地址赋值给 position_copy
number_copy = number; // 将 number 的值赋值给 number_copy
v13 = __readfsqword(0x28u); // 读取 FS 寄存器中的值
position_len = strlen(position); // 计算 position 的长度
position_len_1 = position_len - 1LL; // position 的长度减一
size = 16 * ((4LL * position_len + 15) / 0x10uLL); // 计算变量的大小
while ( &number_copy != (&number_copy - (size & 0xFFFFFFFFFFFFF000LL)) )
; // 一个空循环，用于等待 number_copy 与指定的地址对齐
ptr = alloca(size & 0xFFF); // 在栈上分配内存空间
if ( (size & 0xFFF) != 0 )
*(&number_copy + (size & 0xFFF) - 8) = *(&number_copy + (size & 0xFFF) - 8); // 对齐内存访问
number_ptr = &number_copy; // 将 number_copy 的地址赋值给 number_ptr
for ( i = 0; i < position_len; ++i )
{
v10 = position_copy[i] - 48; // 将 position_copy 中的字符转换为整数
*(number_ptr + i) = *(4LL * v10 + number_copy); // 修改 number_ptr 指向的内存位置的值
}
for ( j = 0; j < position_len; ++j )
position_copy[j] = *(number_ptr + j); // 修改 position_copy 中的字符
position_copy[position_len] = 0; // 在 position_copy 的末尾添加一个空字符
return v13 - __readfsqword(0x28u); // 返回值计算
}
通过IDA动态调试可以发现！
这个函数会根据你的position的位置信息进行加密：
输入的flag为：”01234_asdzxcpoityumnbAOZWXGMY“
经过转换后：position为：
unsigned char position[] =
{
48, 49, 50, 51, 52, 53, 54, 55, 56, 57,
58, 59, 60, 61, 62, 63, 64, 65, 66, 67,
68, 69, 70, 71, 72, 73, 74, 75, 76,
};
经过exchange函数后position的结果：
unsigned char position[] =
{
1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 16, 19, 22, 26, 27, 28,
29, 31, 32, 50, 51, 52, 53, 54, 55
};
!Pasted image 20231030175701.png
__int64 __fastcall a2o(const char *a1, __int64 last)
{
__int64 result; // rax
unsigned int i; // [rsp+18h] [rbp-8h]
int len_position; // [rsp+1Ch] [rbp-4h]
len_position = strlen(a1);
for ( i = 0; ; ++i )
{
result = i;
if ( i >= len_position )
break;
*(4LL * i + last) = a1[i];
}
return result;
}
这里可以将position的值赋值给last！！！
分析完这些小函数后就可以开始整体分析了！
int __cdecl main(int argc, const char **argv, const char **envp)
{
int i; // [rsp+4h] [rbp-7Ch]
int j; // [rsp+8h] [rbp-78h]
int k; // [rsp+Ch] [rbp-74h]
int finish_key[26]; // [rsp+10h] [rbp-70h]
unsigned __int64 v8; // [rsp+78h] [rbp-8h]
v8 = __readfsqword(0x28u);
puts("welcome_to_math");
__isoc99_scanf("%s", &flag);
check(&flag, table); // 输入的内容必须是01234_asdzxcpoityumnbAOZWXGMY中的字符
checkposition(&flag, table, &position); // 将输入的字符转化为序号，存放在position中
exchange(&position, &number); // 将序号加密后存放在position中
a2o(&position, last);//将position的值放入last中！
for ( i = 0; i <= 4; ++i )
{
for ( j = 0; j <= 4; ++j )
{
finish_key[5 * i + j] = 0;
for ( k = 0; k <= 4; ++k )
finish_key[5 * i + j] = (finish_key[5 * i + j] + last[5 * i + k] * matrix[5 * k + j]) & 0x1F;
if ( i == j && finish_key[5 * i + j] != 1 )
exit(0);
if ( i != j && finish_key[5 * i + j] )
exit(0);
}
}
puts("congratulation");
return 0;
}
首先将输入的flag转化为-》position -》加密position -》放入last中
所以最后我们只要知道last，就可以逆向出flag！
由代码可知：
for ( i = 0; i <= 4; ++i )
{
for ( j = 0; j <= 4; ++j )
{
finish_key[5 * i + j] = 0;
for ( k = 0; k <= 4; ++k )
finish_key[5 * i + j] = (finish_key[5 * i + j] + last[5 * i + k] * matrix[5 * k + j]) & 0x1F;
if ( i == j && finish_key[5 * i + j] != 1 )
exit(0);
if ( i != j && finish_key[5 * i + j] )
exit(0);
}
}
只需要满足这个程序就可以推算出last的值！
由
if ( i == j && finish_key[5 * i + j] != 1 )
exit(0);
if ( i != j && finish_key[5 * i + j] )
exit(0);
可知：
finish={
[1, 0, 0, 0, 0]
[0, 1, 0, 0, 0]
[0, 0, 1, 0, 0]
[0, 0, 0, 1, 0]
[0, 0, 0, 0, 1]
}
接下来只需要逆向：
for ( i = 0; i <= 4; ++i )
{
for ( j = 0; j <= 4; ++j )
{
finish_key[5 * i + j] = 0;
for ( k = 0; k <= 4; ++k )
finish_key[5 * i + j] = (finish_key[5 * i + j] + last[5 * i + k] * matrix[5 * k + j]) & 0x1F;
}
}
其中matrix已知,而且finish也已知，只有last未知！！
matrix[25] ={18,29,16,19,27,8,31,8,23,30,29,3,28,10,21,18,29,8,16,28,11,30,7,20,7,};
所以相当于可以解方程：
已知x，y求z
这可以使用python的z3库来求解！
from z3 import *
finish_key = [1, 0, 0, 0, 0,
0, 1, 0, 0, 0,
0, 0, 1, 0, 0,
0, 0, 0, 1, 0,
0, 0, 0, 0, 1]
matrix = [18, 29, 16, 19, 27,
8, 31, 8, 23, 30,
29, 3, 28, 10, 21,
18, 29, 8, 16, 28,
11, 30, 7, 20, 7]
last = [BitVec(f"last_{i}", 8) for i in range(25)] # 创建25个整数变量
s = Solver()
# 添加已知的限制条件
# s.add(last[1] == 19)
# s.add(last[7] == 22)
# s.add(last[17] == 22)
for i in range(5):
for j in range(5):
equation = 0
for k in range(5):
equation = (equation + last[5 * i + k] * matrix[5 * k + j]) & 0x1F
s.add(finish_key[5 * i + j] == equation)
if s.check() == sat:
model = s.model()
solution = [model[last[i]].as_long() for i in range(25)]
print(solution)
else:
print("No solution found.")
跑出来的结果：[11, 19, 9, 5, 12, 14, 6, 22, 27, 16, 26, 28, 29, 29, 11, 4, 31, 22, 13, 8, 27, 29, 10, 16, 16]
毫无疑问这就是last的正确值了！
由 flag转化为-》position -》加密position -》放入last
可知：
只需要知道每个输入的字符被改成序号，再被加密后对应的结果就可以获得一个字典：
输入flag："01234_asdzxcpoityumnbAOZWXGMY"
再去动态调试获取被加密后的position，就可以获得：
a_values = [
1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 16, 19, 22, 26, 27, 28,
29, 31, 32, 50, 51, 52, 53, 54, 55
]
b_values = [
'0', '1', '2', '3', '4', '_', 'a', 's', 'd', 'z',
'x', 'c', 'p', 'o', 'i', 't', 'y', 'u', 'm', 'n',
'b', 'A', 'O', 'Z', 'W', 'X', 'G', 'M', 'Y'
]
这两组数据！
让后将刚刚跑出来的last数组按下面的字典输出出来，就可以获得flag了！
a_values = [
1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 16, 19, 22, 26, 27, 28,
29, 31, 32, 50, 51, 52, 53, 54, 55
]
b_values = [
'0', '1', '2', '3', '4', '_', 'a', 's', 'd', 'z',
'x', 'c', 'p', 'o', 'i', 't', 'y', 'u', 'm', 'n',
'b', 'A', 'O', 'Z', 'W', 'X', 'G', 'M', 'Y'
]
# 创建一个空字典
mapping = {}
# 将a_values和b_values对应起来，形成字典映射关系
for i in range(len(a_values)):
mapping[a_values[i]] = b_values[i]
flag = [11, 19, 9, 5, 12, 14, 6, 22, 27, 16, 26, 28, 29, 29, 11, 4, 31, 22, 13, 8, 27, 29, 10, 16, 16]
for idx in range(len(flag)):
print(mapping[flag[idx]],end="")
结果是：xtd4co_ymiunbbx3Aypsmbzii
flag是：SYC{xtd4co_ymiunbbx3Aypsmbzii}
发表于 2023-11-13 08:48
发表于 2023-11-17 17:06
