z3介绍
Z3 内置了多种变量类型，基本能覆盖常见计算机数据结构。包括整数、浮点数、BitVector、数组等。
先来一个简单的例子看一下 Z3 能做什么：
from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
上面的例子中，定义了两个变量：x 和 y。类型为 Int（注意这里的 Int 可不是 C/C++ 里面包含上下界的 int，Z3 中的 Int 对应的就是数学中的整数，Z3 中的 BitVector 才对应到 C/C++ 中的 int）。
然后就调用了 solve 函数求解三个条件下的满足模型，这三个条件分别是 x 大于 2，y 小于 10，并且 x 加 2 个 y 等于 7。
运行一下结果：
(z3env) $ python example.py
[y = 0, x = 7]
可以看出，Z3 找到了 y=0，x=7 这组解。细心的小伙伴会发现，x=5,y=1 也符合条件，为什么没有体现？原因在于 Z3 在默认情况下，只寻找满足所有条件的一组解，而不是找出所有解。
z3安装
Z3的安装我在windows上没有成功不知道为什么，所以在linux上安装了。
这是unbuntu安装的教程：https://blog.csdn.net/sky_xyc/article/details/79878211（需要翻墙，装老版本的）
这是window安装的教程：https://blog.csdn.net/weixin_41529962/article/details/80274125
例题
Generate
链接：https://pan.baidu.com/s/1HoXLRgQnFd4GbVR9kp7Gvg 提取码：1r26
查壳，发现是无壳的，ida打开
int __cdecl main(int argc, const char **argv, const char **envp)
{
__int64 v3; // rdx
__int64 v4; // rcx
__int64 v5; // r8
__int64 v6; // r9
int result; // eax
char v8; // [rsp+46h] [rbp-Ah]
char v9; // [rsp+47h] [rbp-9h]
signed int i; // [rsp+48h] [rbp-8h]
signed int j; // [rsp+48h] [rbp-8h]
unsigned int v12; // [rsp+4Ch] [rbp-4h]
_fentry__(*(_QWORD *)&argc, argv, envp);
monstartup();
_main();
v12 = Getinput(v4, v3, v5, v6, 0i64, 0i64);
v9 = 0;
for ( i = 0; i <= 31; ++i )
{
v8 = v9 ^ v12 ^ byte_404020[i];
if ( ((unsigned __int8)v8 <= 0x40u || (unsigned __int8)v8 0x5Au) &&
v8 != 95 && v8 != 123 && v8 != 125 )
{
puts("Errorn");
exit(1);
}
byte_408040[i] = v8;
v9 ^= byte_404020[i];
v12 = 1;
}
result = is_begin_with(byte_408040, start);
if ( result )
{
result = (unsigned __int8)byte_40805F;
if ( byte_40805F == 125 )
{
result = puts("Congratulations!nflag is:");
for ( j = 0; j <= 31; ++j )
result = putchar(byte_408040[j]);
}
}
return result;
}
分析一下主函数，可以看到让我们输入一个数，然后给了一些限定条件。第一个函数输入一个纯数字的大数。
int __fastcall Getinput(__int64 a1, __int64 a2, __int64 a3)
{
_QWORD *v3; // rdi
__int64 v5; // [rsp+0h] [rbp-80h]
char DstBuf; // [rsp+20h] [rbp-60h]
_fentry__(a1, a2, a3);
memset(&v5 + 4, 0, 0x30ui64);
v3 = &v5 + 10;
*(_DWORD *)v3 = 0;
*((_WORD *)v3 + 2) = 0;
puts("try to enter a number to generate the flag");
read(0, &DstBuf, 0x10u);
return atoi(&DstBuf);
}
最主要的就是这一段函数
for ( i = 0; i <= 31; ++i )
{
v7 = v8 ^ v11 ^ byte_404020[i];
if ( ((unsigned __int8)v7 <= 0x40u || (unsigned __int8)v7 0x5Au) &&
v7 != 95 && v7 != 123 && v7 != 125 )
{
puts("Errorn");
exit(1);
}
byte_408040[i] = v7;
v8 ^= byte_404020[i];
v11 >>= 1;
}
Byte_404020里面的数可以直接dump出来，需要判断的就是这几个限定条件经过异或计算的数需要大于0x40小于0x5A或者为95,123,125，通过转换我们其实可以看到这三个数就是’_’,’{‘,’}’。
下面的这一句判断的是经过上面循环得到的字符串的开头5个字母是否为“FLAG{”
result = is_begin_with((__int64)byte_408040, (__int64)start, v6);
start db 'FLAG{',0
最后的这个应该是ida的分析错误
if ( result )
{
result = (unsigned __int8)byte_40805F;
if ( byte_40805F == 125 )
{
result = puts("Congratulations!nflag is:");
for ( j = 0; j <= 31; ++j )
result = putchar(byte_408040[j]);
字符串40805F和408040应该是同一个字符串，就是判断了最后一位是不是’}’。
然后再输出正确。
现在最主要的就是处理限定条件那一段。
脚本：
from z3 import *
l1=[164, 25, 4, 130, 126, 133, 80, 168, 209, 234, 227, 249,232, 225, 96, 58,
26, 10, 135, 221, 225, 97, 160, 192,96, 164, 72, 40, 22, 11, 5, 32]
l2='FLAG{'
s=Solver()
num=BitVec('x',64)
s.add(num=2**31) #移位31次所以一定比2^31要大
v7=0
v8=0
for i in range(0,32):
v7=(v8^(num&0xff)^l1[i])&0xff
if i<5:
s.add(v7==ord("FLAG{"[i]))
else:
s.add(Or(And(v764,v7<=90),v7==95,v7==123,v7==125)) #注意这里或和与的写法
v8^=l1[i]&0xff
num>>=1
s.check()
print(s.model())
结果：
root@LAPTOP-0KFHJK29:/mnt/c/Users/123/Desktop# python Generate.py
[x = 3658134498]
再运行程序输出的就是flag了
另一种做法，数据应该不大，可以直接爆破，大概花费了80s左右。
结果：
99999999,199999999,299999999,399999999,499999999,599999999,699999999,799999999,899999999,999999999,1099999999,1199999999,1299999999,1399999999,1499999999,1599999999,1699999999,1799999999,1899999999,1999999999,2099999999,2199999999,2299999999,2399999999,2499999999,2599999999,2699999999,2799999999,2899999999,2999999999,3099999999,3199999999,3299999999,3399999999,3499999999,3599999999,
3658134498
FLAG{**ZZLOZEZ_ZAAPHTZIZ**_}
80.928000s
脚本：
#include <stdio.h>
#include <string.h>
#include <time.h>
int main()
{
int s[] = { 164, 25, 4, 130, 126, 133, 80, 168, 209, 234, 227, 249,232, 225,
96, 58, 26, 10, 135, 221, 225, 97, 160, 192,96, 164, 72, 40, 22, 11, 5, 32
};
char m[] = "FLAG{" ;
char flag[100];
unsigned long long int i;
double start, finish;
start = clock();
long long int count = 0;
for (i = 0;i < 10000000000000000;i++)//从2^31开始
{
count++;
if (count == 100000000)
{
printf("%lld,", i);
count = 0;
}
memset(flag, 0, sizeof(flag));
unsigned long long int v8 = 0;
unsigned long long int v7;
int f = 1;
unsigned long long int num = i;
for (int j = 0;j <= 31;j++)
{
if (!f)
break;
v7 = (v8 ^ num^s[j])&0xff;
if ((v7 <= 64 || v7 90) && v7 != 95 && v7 != 123 && v7 != 125)
f = 0;
flag[j] = v7;
v8^=s[j];
num = num >> 1;
if (j == 5)
{
for (int w = 0;w < 5;w++)
{
if (flag[w] != m[w])
{
f = 0;
break;
}
}
}
}
if (f)
{
printf("n");
printf("%lldn", i);
puts(flag);
finish = clock();
printf("%lfs", (finish - start) / CLOCKS_PER_SEC);
while (1);
}
}
REconvolution
链接：https://pan.baidu.com/s/15QULmF7c8FyHgsFev7W8Sg 提取码：q4mt
32位，无壳，直接用ida打开
int __cdecl main(int argc, const char **argv, const char **envp)
{
unsigned int v3; // esi
unsigned int v4; // kr00_4
char v5; // bl
unsigned int v6; // eax
char *v7; // edx
char v8; // cl
int v9; // eax
char v11[80]; // [esp+8h] [ebp-A4h]
char v12[80]; // [esp+58h] [ebp-54h]
sub_401020("Please input your flag: ");
sub_401050("%40s", v12);
memset(v11, 0, 0x50u);
v3 = 0;
v4 = strlen(v12);
if ( v4 )
{
do
{
v5 = v12[v3];
v6 = 0;
do
{
v7 = &v11[v6 + v3];
v8 = v5 ^ byte_41C658[v6++];
*v7 += v8;
}
while ( v6 \< 0x20 );
++v3;
}
while ( v3 < v4 );
}
v9 = strcmp(v11, (const char *)&unk_41E8B0);
if ( v9 )
v9 = -(v9 < 0) | 1;
if ( v9 )
puts("No, it isn't.");
else
puts("Yes, it is.");
return 0;
}
主函数就是输入一个字符串，然后在一个两重循环里进行累加的异或运算。把最后得到的新的字符串和另一个字符串比较。
if ( v4 )
{
do
{
v5 = v12[v3];
v6 = 0;
do
{
v7 = &v11[v6 + v3];
v8 = v5 ^ byte_41C658[v6++];
*v7 += v8;
}
while ( v6 < 0x20 );
++v3;
}
while ( v3 < v4 );
}
主要来看下这个运算的地方。V4是输入的字符串的长度，v12是输入的字符串。byte_41C658是一个只有0x32个字节的字符串数组。V5为当前循环到的flag的字符，V7获得了v11字符串的地址，v8为当前flag里面的字符和另一个字符串异或，然后再给v7。要注意这个v11的初始开始的值是随着v3的增加而改变的，也就是说flag字符串里面的第一个字符只会经历一次运算。而且这个循环只会进行进行0x20次，因为我们不知道输入的flag要求的长度为多少所以我们无法判断是不是每一次的循环都会对所有的flag里面的数都循环一遍，如果flag的长度超过0x20那就代表着前面有一段循环是无法对后面的几个数进行计算的。
下面列了张大概的计算图，我们假设有和最后需要比较的字符串一样的长度。l2是需要比较的字符串，l1是异或的字符串
l2[0]=flag[0]^l1[0]
l2[1]=flag[0]^l1[1]+flag[1]^l1[0]
l2[2]=flag[0]^l1[2]+flag[1]^l1[1]+flag[2]^l1[0]
.
.
.
l2[32]=flag[1]^l1[31]+......+flag[32]^l1[0]
l2[33]=flag[2]^l1[31]+......+flag[33]^l1[0]
l2[34]=flag[3]^l1[31]+......+flag[34]^l1[0]
.
.
.
l2[64]=flag[33]^l1[31]+......+flag[64]^l1[0]
所以我们全部都要考虑进去，先算前0x20个
for i in range(1,32):
count=0
num=l2[i]
while count<i:
num=num-((flag[count]^l1[i-count])&0xff)
count+=1
flag[i]=(num^l1[0])&0xff
主要还是要异或0xff把数字控制在0-255里。接下来再算后面的
for i in range(32,len(l2)):
count=i-31
num=l2[i]
while count<i:
num=num-((flag[count]^l1[i-count])&0xff)
count+=1
flag[i]=(num^l1[0])&0xff
注意这个count的初始值，最多只有0-31次循环所以第32次就要改变了。
完整的脚本:
l1=[0x21,0x22,0x23,0x24,0x25,0x26,0x27,0x28,0x29,0x2A,0x2B,0x2C,0x2D,0x2E,0x2F,0x3A,
0x3B,0x3C,0x3D,0x3E,0x3F,0x40,0x5B,0x5C,0x5D,0x5E,0x5F,0x60,0x7B,0x7C,0x7D,0x7E]
l2=[0x72,0xE9,0x4D,0xAC,0xC1,0xD0,0x24,0x6B,0xB2,0xF5,0xFD,0x45,0x49,0x94,0xDC,0x10,
0x10,0x6B,0xA3,0xFB,0x5C,0x13,0x17,0xE4,0x67,0xFE,0x72,0xA1,0xC7,0x04,0x2B,0xC2,
0x9D,0x3F,0xA7,0x6C,0xE7,0xD0,0x90,0x71,0x36,0xB3,0xAB,0x67,0xBF,0x60,0x30,0x3E,
0x78,0xCD,0x6D,0x35,0xC8,0x55,0xFF,0xC0,0x95,0x62,0xE6,0xBB,0x57,0x34,0x29,0x0E,3]
#print(len(l2))
flag=[0]*len(l2)
flag[0]=l2[0]^l1[0]
for i in range(1,32):
count=0
num=l2[i]
while count<i:
num=num-((flag[count]^l1[i-count])&0xff)
count+=1
flag[i]=(num^l1[0])&0xff
for i in range(32,len(l2)):
count=i-31
num=l2[i]
while count<i:
num=num-((flag[count]^l1[i-count])&0xff)
count+=1
flag[i]=(num^l1[0])&0xff
for i in range(len(l2)):
print(chr(flag[i]),end='')
运行结果:
SYC{4+mile+b3gin+with+sing1e+step}!Ü!Ø)Ô!Ð1Ì1Ø)Ä!ööþ;¶mè]øÓöC
猜也能猜到应该是到’}’结束，也就是flag就为
SYC{4+mile+b3gin+with+sing1e+step}
下面在用一种z3约束器的解法
from z3 import *
l1=[0x21,0x22,0x23,0x24,0x25,0x26,0x27,0x28,0x29,0x2A,0x2B,0x2C,0x2D,0x2E,0x2F,0x3A,
0x3B,0x3C,0x3D,0x3E,0x3F,0x40,0x5B,0x5C,0x5D,0x5E,0x5F,0x60,0x7B,0x7C,0x7D,0x7E]
l2=[0x72,0xE9,0x4D,0xAC,0xC1,0xD0,0x24,0x6B,0xB2,0xF5,0xFD,0x45,0x49,0x94,0xDC,0x10,
0x10,0x6B,0xA3,0xFB,0x5C,0x13,0x17,0xE4,0x67,0xFE,0x72,0xA1,0xC7,0x04,0x2B,0xC2,
0x9D,0x3F,0xA7,0x6C,0xE7,0xD0,0x90,0x71,0x36,0xB3,0xAB,0x67,0xBF,0x60,0x30,0x3E,
0x78,0xCD,0x6D,0x35,0xC8,0x55,0xFF,0xC0,0x95,0x62,0xE6,0xBB,0x57,0x34,0x29,0x0E,3]
s=Solver()
ans=[0]*100
flag=[BitVec(('x%s' % i),8) for i in range(len(l2)) ]
#先随机len(l2)长度的字符串
for i in range(len(l2)):
for j in range(0x20):
ans[i+j]+=l1[j]^flag[i] #模拟计算过程
for i in range(len(l2)):
s.add(ans[i]==l2[i]) #添加条件
print s.check()
m = s.model()
#print(m)
for i in range(0,len(l2)):
print chr(int("%s" % (m[flag[i]]))),
运行结果:
sat
S Y C { 4 + m i l e + b 3 g i n + w i t h + s i n g 1 e + s t e p } ! ! ) ! 1 1
) ! ; m ] C
只用了4s左右还是很快了
Z3约束器会用的话还是能加快解题过程，就不需要再对代码进行逆向。
Position
链接：https://pan.baidu.com/s/1tsZufdvfyMY5yA_aH8Ehxw 提取码：1f80
先查壳，无壳。打开文件，是输入Name和Serial。从题目另外给的txt文件中可以得到Serial为76876-77776，Name的最后一位为p 用ida打开，没找到关键函数，字符串也是一堆乱七八糟的.
换od打开，在GetWindowTextW处下断点，堆栈回溯两次到达关键函数，回溯三次到达主函数。在根据在od里面的位置，找到在ida的位置。 主函数
void __thiscall sub_401CD0(char *this)
{
char *v1; // esi
signed int v2; // eax
CWnd *v3; // ecx
v1 = this;
v2 = sub_401740((int)this);
v3 = (CWnd *)(v1 + 188);
if ( v2 )
CWnd::SetWindowTextW(v3, L"Correct!");
else
CWnd::SetWindowTextW(v3, L"Wrong");
}
需要v2为1 关键函数sub_401740
signed int __stdcall sub_401740(int a1)
{
int v1; // edi
int v3; // esi
int v4; // esi
__int16 v5; // bx
unsigned __int8 v6; // al
unsigned __int8 v7; // ST2C_1
unsigned __int8 v8; // al
unsigned __int8 v9; // bl
wchar_t *v10; // eax
__int16 v11; // di
wchar_t *v12; // eax
__int16 v13; // di
wchar_t *v14; // eax
__int16 v15; // di
wchar_t *v16; // eax
__int16 v17; // di
wchar_t *v18; // eax
__int16 v19; // di
unsigned __int8 v20; // al
unsigned __int8 v21; // ST2C_1
unsigned __int8 v22; // al
unsigned __int8 v23; // bl
wchar_t *v24; // eax
__int16 v25; // di
wchar_t *v26; // eax
__int16 v27; // di
wchar_t *v28; // eax
__int16 v29; // di
wchar_t *v30; // eax
__int16 v31; // di
wchar_t *v32; // eax
__int16 v33; // si
unsigned __int8 v34; // [esp+10h] [ebp-28h]
unsigned __int8 v35; // [esp+10h] [ebp-28h]
unsigned __int8 v36; // [esp+11h] [ebp-27h]
unsigned __int8 v37; // [esp+11h] [ebp-27h]
unsigned __int8 v38; // [esp+13h] [ebp-25h]
unsigned __int8 v39; // [esp+13h] [ebp-25h]
unsigned __int8 v40; // [esp+14h] [ebp-24h]
unsigned __int8 v41; // [esp+14h] [ebp-24h]
unsigned __int8 v42; // [esp+19h] [ebp-1Fh]
unsigned __int8 v43; // [esp+19h] [ebp-1Fh]
unsigned __int8 v44; // [esp+1Ah] [ebp-1Eh]
unsigned __int8 v45; // [esp+1Ah] [ebp-1Eh]
unsigned __int8 v46; // [esp+1Bh] [ebp-1Dh]
unsigned __int8 v47; // [esp+1Bh] [ebp-1Dh]
unsigned __int8 v48; // [esp+1Ch] [ebp-1Ch]
unsigned __int8 v49; // [esp+1Ch] [ebp-1Ch]
int v50; // [esp+20h] [ebp-18h]
int v51; // [esp+24h] [ebp-14h]
char v52; // [esp+28h] [ebp-10h]
int v53; // [esp+34h] [ebp-4h]
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v50);
v1 = 0;
v53 = 0;
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v51);
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v52);
LOBYTE(v53) = 2;
CWnd::GetWindowTextW(a1 + 304, &v50);//输入Name
if ( *(_DWORD *)(v50 - 12) == 4 ) //输入长度为4个字节
{
v3 = 0;
while ( (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v3) >= 97u
&& (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v3) <= 122u )
{ //判断4个字节为a-z
if ( ++v3 >= 4 )
{
LABEL_7:
v4 = 0;
while ( 1 )
{
if ( v1 != v4 )
{
v5 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v4);
if ( (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v1) == v5 )//4个字母均不相同
goto LABEL_2;
}
if ( ++v4 >= 4 )
{
if ( ++v1 < 4 )
goto LABEL_7;
CWnd::GetWindowTextW(a1 + 420, &v51);输入Serial
if ( *(_DWORD *)(v51 - 12) == 11 && (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 5) == '-' )// Serial长度为11且第6个字符为‘-’
{
v6 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 0);//取出v50[0]，进行下列变换。
v7 = (v6 & 1) + 5;
v48 = ((v6 >> 4) & 1) + 5;
v42 = ((v6 >> 1) & 1) + 5;
v44 = ((v6 >> 2) & 1) + 5;
v46 = ((v6 >> 3) & 1) + 5;
v8 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 1);//同理
v34 = (v8 & 1) + 1;
v40 = ((v8 >> 4) & 1) + 1;
v36 = ((v8 >> 1) & 1) + 1;
v9 = ((v8 >> 2) & 1) + 1;
v38 = ((v8 >> 3) & 1) + 1;
v10 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v7 + v9, v10, 0xAu, 10);//将v7+v9存入v10中，以下同理
v11 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0);
if ( (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 0) == v11 )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v12 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v46 + v38, v12, 0xAu, 10);
v13 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 1);
if ( v13 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v14 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v42 + v40, v14, 0xAu, 10);
v15 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 2);
if ( v15 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v16 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v44 + v34, v16, 0xAu, 10);
v17 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 3);
if ( v17 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v18 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v48 + v36, v18, 0xAu, 10);
v19 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 4);
if ( v19 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v20 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 2);
v21 = (v20 & 1) + 5;
v49 = ((v20 >> 4) & 1) + 5;
v43 = ((v20 >> 1) & 1) + 5;
v45 = ((v20 >> 2) & 1) + 5;
v47 = ((v20 >> 3) & 1) + 5;
v22 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, 3);
v35 = (v22 & 1) + 1;
v41 = ((v22 >> 4) & 1) + 1;
v37 = ((v22 >> 1) & 1) + 1;
v23 = ((v22 >> 2) & 1) + 1;
v39 = ((v22 >> 3) & 1) + 1;
v24 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v21 + v23, v24, 0xAu, 10);
v25 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 6);
if ( v25 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v26 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v47 + v39, v26, 0xAu, 10);
v27 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 7);
if ( v27 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v28 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v43 + v41, v28, 0xAu, 10);
v29 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 8);
if ( v29 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v30 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v45 + v35, v30, 0xAu, 10);
v31 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 9);
if ( v31 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
v32 = (wchar_t *)ATL::CSimpleStringT<wchar_t,1>::GetBuffer(&v52);
itow_s(v49 + v37, v32, 0xAu, 10);
v33 = ATL::CSimpleStringT<wchar_t,1>::GetAt(&v51, 10);
if ( v33 == (unsigned __int16)ATL::CSimpleStringT<wchar_t,1>::GetAt(&v52, 0) )
{
ATL::CSimpleStringT<wchar_t,1>::ReleaseBuffer(&v52, -1);
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v52);
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v51);
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v50);
return 1;
}
}
}
}
}
}
}
}
}
}
}
goto LABEL_2;
}
}
}
}
}
LABEL_2:
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v52);
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v51);
ATL::CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>::~CStringT<wchar_t,StrTraitMFC_DLL<wchar_t,ATL::ChTraitsCRT<wchar_t>>>(&v50);
return 0;
}
这里面
ATL::CSimpleStringT<wchar_t,1>::GetAt(&v50, v3)等价于v50[v3]
itow_s(v42 + v40, v14, 0xAu, 10);等价于将v42+v40放到v14中
itow_s函数
errno_t _itow_s(
int value,
wchar_t *buffer,
size_t sizeInCharacters,
int radix
);
将int类型转换为radix进制，然后以宽字符串的形式以sizeInCharacters长度存放在buffer中
代码量虽然看着比较多，但仔细读下，大部分都是一样的。几个关键的部分上面代码已经给出注释。 根据代码可以拿到10个算式
((Password[0]&1)+5+(((Password[1]>>2) & 1 )+1))==ord('7')-48
((((Password[0]>>3) & 1)+5)+(((Password[1]>>3)&1)+1))==ord('6')-48
(((Password[0]>>1) & 1)+5+(((Password[1]>>4) & 1 )+1))==ord('8')-48
(((Password[0]>>2) & 1)+5+(((Password[1]) & 1 )+1))==ord('7')-48
(((Password[0]>>4) & 1)+5+(((Password[1]>>1) & 1 )+1))==ord('6')-48
(((Password[2]) & 1)+5+(((Password[3]>>2) & 1 )+1))==ord('7')-48
(((Password[2]>>3) & 1)+5+(((Password[3]>>3) & 1 )+1))==ord('7')-48
(((Password[2]>>1) & 1)+5+(((Password[3]>>4) & 1 )+1))==ord('7')-48
(((Password[2]>>2) & 1)+5+(((Password[3]) & 1 )+1))==ord('7')-48
(((Password[2]>>4) & 1)+5+(((Password[3]>>1) & 1 )+1))==ord('6')-48
原程序用itow_s将运算值转为文本，然后取文本的最高位和输入的ASCII进行比较，但是运算结果只有一位数，就直接减48
因为只有4个字节，而且还告诉了我们最后一位，实际只需要求3位，所以用爆破或者z3均可以。题目也告诉了我们不止一个答案
爆破：
l1='76876-77776'
flag1=''
flag2=''
for i in range(97,123):
v7=(i&1)+5
v48=((i>>4)&1)+5
v42=((i>>1)&1)+5
v44=((i>>2)&1)+5
v46=((i>>3)&1)+5
for j in range(97,123):
v34=(j&1)+1
v40=((j>>4)&1)+1
v36=((j>>1)&1)+1
v9=((j>>2)&1)+1
v38=((j>>3)&1)+1
if v7+v9==ord(l1[0])-48 and v46+v38==ord(l1[1])-48 and v42+v40==ord(l1[2])-48 and v44+v34==ord(l1[3])-48 and v48+v36==ord(l1[4])-48:
flag1+=chr(i)
flag1+=chr(j)
flag1+=' '
for i in range(97,123):
v21=(i&1)+5
v49=((i>>4)&1)+5
v43=((i>>1)&1)+5
v45=((i>>2)&1)+5
v47=((i>>3)&1)+5
j=ord('p')
v35=(j&1)+1
v41=((j>>4)&1)+1
v37=((j>>1)&1)+1
v23=((j>>2)&1)+1
v39=((j>>3)&1)+1
if v21+v23==ord(l1[6])-48 and v47+v39==ord(l1[7])-48 and v43+v41==ord(l1[8])-48 and v45+v35==ord(l1[9])-48 and v49+v37==ord(l1[10])-48:
flag2+=chr(i)
flag2+=chr(j)
flag2+=' '
print(flag1)
print(flag2)
结果
bu cq ft gp
mp
gp里面p重复了，去除，第一排剩下的3个和第二排组合一下都是答案
z3：
from z3 import *
s=Solver()
Password=[BitVec('u%d'%i,8) for i in range(0,4)]
for i in range(4):
s.add(Password[i]>=ord('a'))
s.add(Password[i]<=ord('z'))
s.add(Password[3]==ord('p'))
s.add(((Password[0]&1)+5+(((Password[1]>>2) & 1 )+1))==ord('7')-48)
s.add(((((Password[0]>>3) & 1)+5)+(((Password[1]>>3)&1)+1))==ord('6')-48)
s.add((((Password[0]>>1) & 1)+5+(((Password[1]>>4) & 1 )+1))==ord('8')-48)
s.add((((Password[0]>>2) & 1)+5+(((Password[1]) & 1 )+1))==ord('7')-48)
s.add((((Password[0]>>4) & 1)+5+(((Password[1]>>1) & 1 )+1))==ord('6')-48)
s.add((((Password[2]) & 1)+5+(((Password[3]>>2) & 1 )+1))==ord('7')-48)
s.add((((Password[2]>>3) & 1)+5+(((Password[3]>>3) & 1 )+1))==ord('7')-48)
s.add((((Password[2]>>1) & 1)+5+(((Password[3]>>4) & 1 )+1))==ord('7')-48)
s.add((((Password[2]>>2) & 1)+5+(((Password[3]) & 1 )+1))==ord('7')-48)
s.add((((Password[2]>>4) & 1)+5+(((Password[3]>>1) & 1 )+1))==ord('6')-48)
s.check()
print(s.model())
结果：
$ python position.py
[u2 = 109, u0 = 98, u1 = 117, u3 = 112]
Z3只会解出一个解，就是bump