如何求解fla
题目下载
1，直接内存获取
对于一些比较简单的题目，可以通过直接查看内存的方式获取flag。对于这种形式，只需要在比的地方下个断点，然后通过查看内存即刻得到flag。
参考例子：
远程动态调试
2.对算法进行逆变操作
如果一个判断过程的代码如下所示，那么要分析convert的算法，然后分析结果写出对应的逆算法，通过reverse_convert(stardard)方式求得flag
main函数：
这像base64，因为有=补齐，打开change：
可以确定是变表的base64，使用python进行逆运算（需要安装pybase64库）：
import base64
check = "ms4otszPhcr7tMmzGMkHyFn"
tmp = "ELF8n0BKxOCbj/WU9mwle4cG6hytqD+P3kZ7AzYsag2NufopRSIVQHMXJri51Tdv"
stdbase64 = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"
check2 = ""
for i in range(len(check)):
check2 += stdbase64[tmp.index(check[i])]
check2 += "="
print(check2)
flag = base64.b64decode(check2)
print(flag.decode())
3.线性变换求解（偏PWN，并且需要用到liunx，暂时略）
4.约束求解
使用OD打开，跟随GetWindowTextA：
f9运行，随便输入数据。栈区回溯：
回车
在IDA中找到这个函数：
发现是CWnd::GetWindowTextA，说明还要回溯一次：
IDA中找到这个函数，就是main函数了：
int __thiscall sub_4016F0(void *this)
{
void *v1; // edi
int v2; // eax
const char *v3; // eax
char *v4; // ebp
signed int v5; // esi
const char *v6; // esi
unsigned int len; // ecx
unsigned int v8; // edx
int v9; // eax
signed __int32 v10; // ecx
bool v11; // zf
bool v12; // sf
int v13; // ecx
BOOL v14; // eax
signed __int32 v15; // edx
const char *v17; // [esp+14h] [ebp-41Ch]
void *v18; // [esp+18h] [ebp-418h]
int v19; // [esp+1Ch] [ebp-414h]
char v20; // [esp+20h] [ebp-410h]
void **v21; // [esp+33Ch] [ebp-F4h]
BOOL v22; // [esp+3B0h] [ebp-80h]
int v23; // [esp+42Ch] [ebp-4h]
v1 = this;
v18 = this;
CDialog::CDialog((CDialog *)&v21, 0x81u, 0);
v21 = &CNotify::`vftable';
v23 = 0;
v2 = sub_410F13();
if ( v2 == 0 )
sub_401A00(-2147467259);
v17 = (const char *)((*(int (__thiscall **)(int))(*(_DWORD *)v2 + 12))(v2) + 16);
LOBYTE(v23) = 1;
v19 = 0;
memset(&v20, 0, 0x31Cu);
CWnd::GetWindowTextA((int)v1 + 120, (int)&v17);// 获取文本
v3 = v17;
if ( *((_DWORD *)v17 - 3) < 40 )
{
if ( *((_DWORD *)v17 - 1) > 1 )
{
sub_401960(*((_DWORD *)v17 - 3));
v3 = v17;
}
v6 = v3;
len = strlen(v3);
v8 = 3 * (len / 3);
if ( len != v8 )
len = v8 + 3; // 补齐
v4 = (char *)malloc(8 * len / 6 + 1);
if ( !v4 )
{
LOBYTE(v23) = 0;
v9 = (int)(v17 - 16);
v10 = _InterlockedDecrement((volatile signed __int32 *)v17 - 1);
v11 = v10 == 0;
v12 = v10 < 0;
goto LABEL_16;
}
base64(v4, (int)v6, strlen(v6));
sub_401000(v4, (int)&v19); // v19 = v4 - 3
v14 = sub_401040(v13, &v19);
v1 = v18;
v5 = v14;
if ( v14 )
v5 = 1;
}
else
{
v4 = (char *)v18;
v5 = 0;
}
if ( v4 )
free(v4);
v22 = v5 != 0;
CDialog::DoModal((CDialog *)&v21);
(*(void (__thiscall **)(void *))(*(_DWORD *)v1 + 344))(v1);
LOBYTE(v23) = 0;
v9 = (int)(v17 - 16);
v15 = _InterlockedDecrement((volatile signed __int32 *)v17 - 1);
v11 = v15 == 0;
v12 = v15 < 0;
LABEL_16: // 错误
if ( v12 || v11 )
(*(void (__stdcall **)(int))(**(_DWORD **)v9 + 4))(v9);
v23 = -1;
v21 = &CNotify::`vftable';
return sub_40557C();
}
分析流程发现是base64加密，然后值全部减3，再check
解密脚本
python3
from z3 import *
import base64
check = [0x97, 0x82, 0xAF, 0xBE, 0XA3, 0XBD, 0X95, 0X84, 0XC0, 0XBC, 0X9F, 0XA2, 0X83, 0X63, 0XA8, 0XC5, 0X97, 0X97, 0XA4, 0XA4, 0X98, 0XA6, 0XCD, 0XBC, 0XA3, 0XA2, 0X92, 0XA1, 0XA2, 0X87, 0X95, 0X9C, 0XB4, 0XDA, 0XE5, 0XC0, 0X9F, 0XB9, 0XCA, 0X16, 0, 0]
s = Solver()
B = [BitVec("x%s"%i,8) for i in range(41)] #?
for i in range(39):
s.add(B[i] + B[i+1] == check[i])
s.add(B[9] - B[20] == 22)
s.add(B[40] == 0)
print(s.check())
print(s.model())
t = s.model()
print("[", end = "")
for ii in range(40):
print(t[B[ii]],end = ",")
print(t[B[40]],end = "")
print("]")
re1 = [84,67,63,112,78,85,104,45,87,105,83,76,86,45,54,114,83,68,83,81,83,69,97,108,80,83,79,67,94,68,67,82,74,106,112,117,75,84,101,101,0]
re1_a = ""
for i in re1:
re1_a += chr(i+3)
re2 = base64.b64decode(re1_a).decode()
print(re2)
'''
while ( *v3 + v3[1] == *(_DWORD *)((char *)v3 + (char *)&v5 - (char *)a2) )
{
++v2;
++v3;
if ( v2 >= 39 )
{
if ( a2[9] - a2[20] == 22 )
return a2[40] == 0;
return 0;
}
}
'''
后续内容敬请期待，关于z3的使用主页其他文章也有涉及