z3约束器的使用用例

8023zil 发表于 2023-11-13 08:48

本帖最后由 8023zil 于 2023-11-15 11:03 编辑

[]
[]
[]

```c
__int64 __fastcall check(__int64 a1, __int64 a2)
{
__int64 result; // rax
int i; //
int breakflag; //
int j; //

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"

```c
_BYTE *__fastcall checkposition(const char *flag, const char *table, __int64 pos)
{
_BYTE *result; // rax
int i; //
int j; //
int table_len; //
int flag_len; //

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 == table )
   {
   *(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存放的是位置坐标！

```c
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 - 48;    // 将 position_copy 中的字符转换为整数
*(number_ptr + i) = *(4LL * v10 + number_copy);// 修改 number_ptr 指向的内存位置的值
}

for ( j = 0; j < position_len; ++j )
position_copy = *(number_ptr + j);// 修改 position_copy 中的字符

position_copy = 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
};
```
![]

```c
__int64 __fastcall a2o(const char *a1, __int64 last)
{
__int64 result; // rax
unsigned int i; //
int len_position; //

len_position = strlen(a1);
for ( i = 0; ; ++i )
{
result = i;
if ( i >= len_position )
   break;
*(4LL * i + last) = a1;
}
return result;
}
```
这里可以将position的值赋值给last！！！

分析完这些小函数后就可以开始整体分析了！
```c
int __cdecl main(int argc, const char **argv, const char **envp)
{
int i; //
int j; //
int k; //
int finish_key; //
unsigned __int64 v8; //

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 = 0;
   for ( k = 0; k <= 4; ++k )
   finish_key = (finish_key + last * matrix) & 0x1F;
   if ( i == j && finish_key != 1 )
   exit(0);
   if ( i != j && finish_key )
   exit(0);
}
}
puts("congratulation");
return 0;
}
```
首先将输入的flag转化为-》position -》加密position -》放入last中
所以最后我们只要知道last，就可以逆向出flag！

由代码可知：
```c
for ( i = 0; i <= 4; ++i )
{
for ( j = 0; j <= 4; ++j )
{
   finish_key = 0;
   for ( k = 0; k <= 4; ++k )
   finish_key = (finish_key + last * matrix) & 0x1F;
   if ( i == j && finish_key != 1 )
   exit(0);
   if ( i != j && finish_key )
   exit(0);
}
}
```
只需要满足这个程序就可以推算出last的值！

由
```c
   if ( i == j && finish_key != 1 )
   exit(0);
   if ( i != j && finish_key )
   exit(0);
```
可知：
```
finish={





}
```

接下来只需要逆向：
```c
for ( i = 0; i <= 4; ++i )
{
for ( j = 0; j <= 4; ++j )
{
   finish_key = 0;
   for ( k = 0; k <= 4; ++k )
   finish_key = (finish_key + last * matrix) & 0x1F;
}
}
```
其中matrix已知,而且finish也已知，只有last未知！！
```c
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,};
```
所以相当于可以解方程：
已知x，y求z
这可以使用python的z3库来求解！
```python
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 = # 创建25个整数变量

s = Solver()

# 添加已知的限制条件
# s.add(last == 19)
# s.add(last == 22)
# s.add(last == 22)

for i in range(5):
for j in range(5):
   equation = 0
   for k in range(5):
         equation = (equation + last * matrix) & 0x1F
   s.add(finish_key == equation)

if s.check() == sat:
model = s.model()
solution = ].as_long() for i in range(25)]
print(solution)
else:
print("No solution found.")

```
跑出来的结果：``
毫无疑问这就是last的正确值了！

由 flag转化为-》position -》加密position -》放入last
可知：
只需要知道每个输入的字符被改成序号，再被加密后对应的结果就可以获得一个字典：
输入flag："01234_asdzxcpoityumnbAOZWXGMY"
再去动态调试获取被加密后的position，就可以获得：
```c
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了！
```python
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] = b_values

flag =
for idx in range(len(flag)):
print(mapping],end="")

```
结果是：xtd4co_ymiunbbx3Aypsmbzii
flag是：SYC{xtd4co_ymiunbbx3Aypsmbzii}

xixicoco 发表于 2023-11-13 15:11

虽然看不懂，但是觉得很有用

Yancy-Lan 发表于 2023-11-13 22:51

大佬要是开发个某4*90的脱壳软件就好了:lol

Hmily 发表于 2023-11-17 17:06

@8023zil 看https://www.52pojie.cn/misc.php?mod=faq&action=faq&id=29&messageid=36 这个方法把图片插入到markdown的文章中吧。

页: [1]

吾爱破解 - 52pojie.cn's Archiver

z3约束器的使用用例