复盘SUCTF 2019 Writeup
Reverse
SignIn
exeinfope 载入查壳。一个64位的ELF程序，无壳。
NOT Win EXE - .o - ELF executable [ 64bit obj. Shared obj file - CPU : AMD x86-64 - OS: unspecified ]
先来静态分析一波，载入IDA。找到 main 函数地址，F5大法...
__int64 __fastcall main(__int64 a1, char **a2, char **a3)
{
char N; // [rsp+0h] [rbp-4A0h]
char e; // [rsp+10h] [rbp-490h]
char m; // [rsp+20h] [rbp-480h]
char c; // [rsp+30h] [rbp-470h]
char v8; // [rsp+40h] [rbp-460h]
char v9; // [rsp+B0h] [rbp-3F0h]
unsigned __int64 v10; // [rsp+498h] [rbp-8h]
v10 = __readfsqword(0x28u);
puts("[sign in]");
printf("[input your flag]: ", a2);
__isoc99_scanf("%99s", &v8);
sub_96A(&v8, (__int64)&v9);
__gmpz_init_set_str((__int64)&c, (__int64)"ad939ff59f6e70bcbfad406f2494993757eee98b91bc244184a377520d06fc35", 16LL);
__gmpz_init_set_str((__int64)&m, (__int64)&v9, 16LL);
__gmpz_init_set_str(
(__int64)&N,
(__int64)"103461035900816914121390101299049044413950405173712170434161686539878160984549",
10LL);
__gmpz_init_set_str((__int64)&e, (__int64)"65537", 10LL);
__gmpz_powm((__int64)&m, (__int64)&m, (__int64)&e, (__int64)&N);
if ( (unsigned int)__gmpz_cmp(&m, &c) )
puts("GG!");
else
puts("TTTTTTTTTTql!");
return 0LL;
}
可以看到程序先接收了输入到 v8 数组。然后经过sub_96A函数的处理。通过 gdb 动态调试可得该函数的作用即是将 HEX 转 ASCII。
继续往下看，程序调用了 __gmpz_init_set_str 函数，经过 Google 之后得知这其实是一个 GNU 高精度算法库(GNU Multiple Precision Arithmetic Library)。
官方文档入口
通过查阅官方文档，我知道了 __gmpz_init_set_str 其实就是 mpz_init_set_str
int mpz_init_set_str (mpz_t rop, const char *str, int base) [Function]
Initialize rop and set its value like mpz_set_str
int mpz_set_str (mpz_t rop, const char *str, int base) [Function]
Set the value of rop from str, a null-terminated C string in base base. White space is allowed
in the string, and is simply ignored.
很显然这个函数的作用就是将 str 字符数组以 base 指定的进制解读成数值并写入 rop 所指向的内存。该程序通过调用这个函数来实现数据的初始化赋值。
之后调用的一个函数 __gmpz_powm 在文档中的定义是这样的:
void mpz_powm (mpz_t rop, const mpz_t base, const mpz_t exp, const mpz_t mod) [Function]
Set rop to base^exp mod mod.
该函数将计算 base 的 exp 次方，并对 mod 取模，最后将结果写入 rop 中。
这种计算与RSA中的加密过程如出一辙。
再往下就是关键比较函数 __gmpz_cmp
int mpz_cmp (const mpz t op1, const mpz t op2) [Function]
Compare op1 and op2. Return a positive value if op1 > op2, zero if op1 = op2, or a negative
value if op1 < op2.
程序中比较之前 mpz_powm 运算的结果与程序中硬编码的值是否相等，如果相等则输出 tql。看到这里应该可以基本确定这是一道已知密文求解RSA明文的题目。
根据RSA的实现过程，首先来计算密钥。第一步是获得大整数 N ，根据程序可得
N = 103461035900816914121390101299049044413950405173712170434161686539878160984549
值得注意的是，这里的 N 是十进制的。
接下来对它进行大整数的因数分解，这里借助 yafu 工具。
>yafu-x64.exe
factor(103461035900816914121390101299049044413950405173712170434161686539878160984549)
fac: factoring 103461035900816914121390101299049044413950405173712170434161686539878160984549
fac: using pretesting plan: normal
fac: no tune info: using qs/gnfs crossover of 95 digits
starting SIQS on c78: 103461035900816914121390101299049044413950405173712170434161686539878160984549
==== sieving in progress (1 thread): 36224 relations needed ====
==== Press ctrl-c to abort and save state ====
SIQS elapsed time = 1.8809 seconds.
Total factoring time = 1.9647 seconds
***factors found***
P39 = 366669102002966856876605669837014229419
P39 = 282164587459512124844245113950593348271
ans = 1
至此我们得到了 p 和 q
p = 366669102002966856876605669837014229419
q = 282164587459512124844245113950593348271
再从程序中得知 e 的值为
e = 65537
接下来就可以求出私钥 d，并通过私钥 d，求出明文 m，再将其转化成 ASCII 即可得到 flag
import gmpy2
p = 366669102002966856876605669837014229419
q = 282164587459512124844245113950593348271
N = 103461035900816914121390101299049044413950405173712170434161686539878160984549
c = 0xad939ff59f6e70bcbfad406f2494993757eee98b91bc244184a377520d06fc35
e = 65537
d = gmpy2.invert(e,(p-1)*(q-1))
m = gmpy2.powmod(c,d,p*q)
print hex(m)[2:].decode('hex')
Rev
一个 64 位的没有加壳的程序
先看字符串
.rdata:0000000140005428 0000000E C You lost sth.
.rdata:0000000140005438 00000006 C pause
.rdata:0000000140005448 00000009 C You win!
.rdata:00000001400054C8 00000010 C string too long
看到 You win ! 和 You lost sth，执行一下程序，输入 inputflagtest 猜测应该返回 You lost sth
D:\CTF\SUCTF2019\Rev>cpp.exe
inputflagtest
D:\CTF\SUCTF2019\Rev>
实际上什么也没有返回，说明程序在输出 You lost sth 之前就停止了，动态调试一下找到是在哪里停下的
调试之后发现
if ( v4 != 3 )
_exit(v4);
.text:00000001400016A0 cmp esi, 3
.text:00000001400016A3 jz short loc_1400016AE
.text:00000001400016A5 mov ecx, esi ; Code
.text:00000001400016A7 call cs:__imp__exit
我们首先得知道这个 v4 是干什么用的，才有可能阻止程序停止。于是往前看，找到一个循环
while ( 1 )
{ // while start
v129 = v83;
sub_140002120(v83, &v113);
sub_140002120(&v84, &v115);
v85 = v117;
v86 = BYTE2(v117);
v8 = *(&v112 + 1);
v129 = v87;
sub_140002120(v87, v83);
sub_140002120(&v88, &v84);
v89 = v85;
v90 = v86;
v91 = v8;
v92 = v8;
v95 = 0i64;
v96 = 15i64;
LOBYTE(v94) = 0;
v93 = 0;
sub_140001FC0(v83);
v7 |= 4u;
if ( v93 && BYTE8(v107) ) // 不进
v9 = v91 != *(&v106 + 1) || v92 != v107;
else
v9 = v93 != BYTE8(v107); // v9 = 1
if ( v96 >= 0x10 ) // 不进
{
v10 = v94;
if ( v96 + 1 >= 0x1000 )
{
v10 = *(v94 - 1);
if ( (v94 - v10 - 8) > 0x1F )
invalid_parameter_noinfo_noreturn();
}
j_j_free(v10);
}
v95 = 0i64;
v96 = 0xFi64;
LOBYTE(v94) = 0;
sub_140001FC0(v87);
if ( !v9 )
break;
if ( !BYTE8(v107) )
wassert(L"valid_", L"E:\\boost_1_69_0\\boost\\token_iterator.hpp", 0x3Bu);
v11 = &Src[32 * v4];
if ( v11 != Memory )
{
v12 = Memory;
if ( v109[1] >= 0x10 )
v12 = Memory[0];
sub_140002240(v11, v12, v109[0]);
}
++v4; // 在这里发现可以增加 v4
if ( !BYTE8(v107) )
wassert(L"valid_", L"E:\\boost_1_69_0\\boost\\token_iterator.hpp", 0x36u);
BYTE8(v107) = sub_140002B80(&Buf, &v106 + 1, v107, Memory);
} // while end
在这个循环之前程序将 v4 初始化为 0，也就是说我们需要通过 ++v4 这条语句让 v4 = 3 才能让程序不退出。很自然的想到去找这个循环的出口。于是找到一个
if ( !v9 )
break;
再往前看与 v9 相关的代码
v93 = 0;
...
if ( v93 && BYTE8(v107) )
v9 = v91 != *(&v106 + 1) || v92 != v107;
else
v9 = v93 != BYTE8(v107);
v93 已经确定是 0 了。这里涉及到一个 v107 的值，它的值直接决定了 v9 会怎么变化，于是往前找到
BYTE8(v107) = sub_140002B80(&Buf, &v106 + 1, v5, Memory);
发现 v107 的值是由函数 sub_140002B80 决定的。于是现在的问题就变成了研究这个函数的作用
这个函数的逻辑跳转比较复杂，但是经过动态调试之后，可以总结出来的是
strEnd = a3;
strI = a2;
v35 = *strI + 1; // 取下一个字符
*strI = v35;
if ( v35 == strEnd )
return 1;
该函数的第二个参数是我们输入的字符串指针，它会移动该指针，去取字符串中的每一位字符，取到空白符或者标点符就会返回 1 并且指针的位置也会保存下来，换言之它起到了一个分割字符串的作用，只不过分割的字符可以是任意的标点符或空白符。主要借助的是以下两个函数来实现
isspace()
ispunct()
知道了这个函数的作用我们就能弄清楚刚刚的循环的作用了，很显然是在分割字符串，而 v3 = 3 也就意味着有三个部分
我们把输入重新改成 input_flag_test，再动态调试一遍，发现程序在此处停止了
if ( v122 != 10 ) // 第一部分的长度要等于10才行
{
v14 = sub_140002090(Src);
_exit(v14);
}
v122 变量存储的是第一部分字符串的长度，于是我们更改输入为 input2nput_flag_test 继续调试
发现了以下循环
do
{
v20 = &Dst;
if ( v18 >= 0x10 )
v20 = v19;
if ( (*(v20 + v17) ^ 0xAB) != *(&v129 + v17) )
{
Sleep(0xD4A51000);
_exit(0);
}
v21 = &Dst;
if ( v18 >= 0x10 )
v21 = v19;
sub_140001020("%c", *(v21 + v17));
++v15;
++v17;
}
while ( v15 < v16 );
此时 v16 的值是 10 v15与v17 保存了当前的字符下标，我们发现 Dst 的每一位必须要与 0xAB 异或，且得到的值要与 v129 表中的值要相等。往前看到
sub_140002690(&Dst, Src, &v76); // 在一个字符串中搜索另一个字符串，并去掉另一个字符串
LODWORD(v129) = 0xDFC8DED8; // 异或之后 是 suctf
WORD2(v129) = 0xCD;
分析一下 sub_140002690，首先从看它传入的参数 v76 被固定成了 0x31，即 '1'
动态调试后，发现它的作用很简单 sub_140002690(d,s,a) ，在 s 中去除 a 字符串并拷贝给 d
写个脚本跑一下
v129 = "CD DF C8 DE D8".split(" ")
r = ""
for i in v129 :
r += chr(int(i,16)^0xAB)
print(r)
# suctf
由于只有 5 个字符，但前面得到的信息是第一部分要有 10 个字符，这说明有 5 个字符是 '1'，在 sub_140002690 中被去除了。于是第一部分就可以确定下来是 11111suctf
输入 11111suctf_flag_test ，继续调试遇到了
if ( Size != 4 ) // 第二段的长度得 = 4 否则就 you lost
goto LABEL_149;
这里的 Size 刚好保存了第二部分的数据长度，我们这里刚刚好是 4 个
if ( v25 != v24 ) // 判断字符是否取到尾了
{
while ( (*v25 - 97) <= 6u || (*v25 - 65) <= 6u )// [a-gA-G]
{
if ( ++v25 == v24 )
goto LABEL_55;
}
goto LABEL_149; // You lost
}
...
LABEL_149:
v71 = sub_140002810(std::cout, "You lost sth.");
这里的循环主要限定了第二部分的字符范围为 [a-gA-G]
于是我们转换一下输入为 11111suctf_abcd_test 继续调试
do
{
v37 = *v33; // 取一个字符给 v37
v38 = sub_1400023D0(&v78);
*v33 = std::ctype<char>::toupper(v38, v37);// 替换 v38~v37 范围内的小写字母为大写字母
v33 = (v33 + 1);
}
while ( (v33 - v35) != v36 ); // 是否处理完字符
这里将刚才输入的字符串第二部分的字母从小写转到大写
if ( Size == v100 && !memcmp(v41, v40, Size) ) // 原来就得是大写
这里 memcmp 将刚才转化成大写之后的字符串与原先转化之前的字符串进行了比较，换句话说，我原先输入的第二部分字符串就必须是大写否则这里就无法进入分支
于是改变输入 11111suctf_ABCD_test 继续调试
v44 = 0i64;
do
{
v45 = Buf2;
if ( v30 >= 0x10 )
v45 = v29;
v46 = Buf2;
if ( v30 >= 0x10 )
v46 = v29;
if ( *(v45 + v44) + 2 != *(v46 + v44 + 1) )// 后一个字符要和前一个字符相差2
v22 = 1;
++v43;
++v44;
}
while ( v43 < (v42 - 1) );
这一段的主要作用是告诉我们第二段的字符串内容，每两个字符之间后一个字符要和前一个字符相差 2
结合 [a-gA-G] 的范围得出结果 11111suctf_ACEG_test 继续调试
while ( 1 )
{
v53 = *v52; // 取了一个字符 v52 = "test" v53=0x74
v54 = Buf2[0]; // 字符串长度 Buf[0] = 4 v54 = 4
if ( !(v54 & *(*(sub_1400023D0(&Buf2[1]) + 24) + 2 * v53)) )// *(sub_1400023D0(&Buf2[1]) + 24) = 000000000043EA00
// *(000000000043EA00) = 0x20
// 判断是否是纯数字
break;
v52 = (v52 + 1);
if ( v52 == v73 )
goto LABEL_104;
}
这里用了一种很奇妙的方法来判断第三部分的字符是否是纯数字的
我们去内存中 dump 出 0x0000000000500210 这个位置往下某一块区域的表
debug013:0000000000500210 db 84h
debug013:0000000000500211 db 0
debug013:0000000000500212 db 84h
debug013:0000000000500213 db 0
debug013:0000000000500214 db 84h
debug013:0000000000500215 db 0
debug013:0000000000500216 db 84h
debug013:0000000000500217 db 0
debug013:0000000000500218 db 84h
debug013:0000000000500219 db 0
debug013:000000000050021A db 84h
debug013:000000000050021B db 0
debug013:000000000050021C db 84h
debug013:000000000050021D db 0
debug013:000000000050021E db 84h
debug013:000000000050021F db 0
debug013:0000000000500220 db 84h
debug013:0000000000500221 db 0
debug013:0000000000500222 db 84h
debug013:0000000000500223 db 0
正好 10 个 0x84 代表着 0-9 ，经过运算只有落在这部分区域里才有可能让 v54(=4) 与 0x84 与运算，才有可能不触发 break，所以这里的作用就是要求第三部分的所有字符都是数字字符
最后关键的一部分
v62 = v61 + v127 - v59; // 取第三部分长度
if ( v59 > (v61 + v127) )
v62 = 0i64;
if ( v62 )
{
do
{
v3 = *v60 + 2 * (5 * v3 - 24); // 把字符串型的数字转为数值型的数字 例如 '3'=>3
v60 = (v60 + 1); // 取下一个字符
}
while ( v60 - v59 != v62 );
}
if ( !(v3 & 1)
&& ((1234 * v3 + 5678) / 4396 ^ 0xABCDDCBA) == 0xABCDB8B9
&& ((2334 * v3 + 9875) / 7777 ^ 0x12336790) == 0x1233FC70 )
{
v63 = std::basic_ostream<char,std::char_traits<char>>::operator<<(std::cout, v3, v60);
v64 = sub_140002810(v63, "}");
std::basic_ostream<char,std::char_traits<char>>::operator<<(v64, sub_1400029E0);
}
v65 = sub_140002810(std::cout, "You win!");
std::basic_ostream<char,std::char_traits<char>>::operator<<(v65, sub_1400029E0);
直接分析可能很难理解，但是通过动态调试观察可以发现是先将数字字符转化为数值型数据，然后满足一个表达式才能输出 '}'，这里我们用 z3 来计算 v3 的确定值
from z3 import *
x = BitVec('x',32)
s = Solver()
s.add(x&1==0)
s.add((1234 * x + 5678) / 4396 ^ 0xABCDDCBA == 0xABCDB8B9)
s.add((2334 * x + 9875) / 7777 ^ 0x12336790 == 0x1233FC70)
if s.check() == sat :
print(s.model())
# [x = 31415926]
至此，我们就得到了最终的答案 11111suctf_ACEG_31415926
hardCPP
这题用了OLLVM混淆(控制流平坦化)，我在分析前选择了基于angr框架的符号执行来实现去除控制流平坦化。
$ python deflat.py ~/Desktop/hardCpp 0x4007E0
*******************relevant blocks************************
prologue: 0x4007e0
main_dispatcher: 0x400876
pre_dispatcher: 0x4012e3
retn: 0x40114a
relevant_blocks: ['0x400caa', '0x400dd3', '0x400d71', '0x400ba6', '0x400d15', '0x4010ea', '0x40107d', '0x400c30', '0x4012c4', '0x400d8d', '0x401172', '0x400bea', '0x400f40', '0x400ccf', '0x401155', '0x401037', '0x400ff1', '0x4010a4', '0x400bb0', '0x40108c', '0x400d62', '0x400f5e', '0x401188', '0x4012b5']
*******************symbolic execution*********************
-------------------dse 0x400caa---------------------
-------------------dse 0x400dd3---------------------
CRITICAL | 2019-10-08 06:28:05,385 | angr.sim_state | The name state.se is deprecated; please use state.solver.
-------------------dse 0x400d71---------------------
-------------------dse 0x400ba6---------------------
-------------------dse 0x400d15---------------------
-------------------dse 0x4010ea---------------------
-------------------dse 0x40107d---------------------
-------------------dse 0x400c30---------------------
-------------------dse 0x4012c4---------------------
-------------------dse 0x400d8d---------------------
-------------------dse 0x401172---------------------
-------------------dse 0x400bea---------------------
-------------------dse 0x400f40---------------------
-------------------dse 0x400ccf---------------------
-------------------dse 0x401155---------------------
-------------------dse 0x401037---------------------
-------------------dse 0x400ff1---------------------
-------------------dse 0x4010a4---------------------
-------------------dse 0x400bb0---------------------
-------------------dse 0x40108c---------------------
-------------------dse 0x400d62---------------------
-------------------dse 0x400f5e---------------------
-------------------dse 0x401188---------------------
-------------------dse 0x4012b5---------------------
-------------------dse 0x4007e0---------------------
************************flow******************************
0x400caa: ['0x400ccf']
0x4010ea: ['0x40114a', '0x4012c4']
0x400d71: ['0x400d8d', '0x4010a4']
0x4010a4: ['0x4010ea', '0x4012c4']
0x400ba6: ['0x400dd3']
0x400bb0: ['0x400bea']
0x40108c: ['0x400d71']
0x4007e0: ['0x400bb0']
0x401155: ['0x400c30']
0x400d62: ['0x400d71']
0x400d15: ['0x400d62', '0x401172']
0x401188: ['0x400dd3']
0x400ff1: ['0x401037', '0x4012b5']
0x40107d: ['0x40108c']
0x400c30: ['0x400caa', '0x401155']
0x4012c4: ['0x4010ea']
0x401172: ['0x400d15']
0x400dd3: ['0x400f40', '0x400f40']
0x400bea: ['0x400c30', '0x401155']
0x400d8d: ['0x400dd3', '0x401188']
0x400f40: ['0x400f5e', '0x400ff1']
0x400ccf: ['0x400d15', '0x401172']
0x4012b5: ['0x401037']
0x401037: ['0x40107d', '0x4012b5']
0x40114a: []
************************patch*****************************
Successful! The recovered file: /home/puret/Desktop/hardCpp_recovered
相关资料可以看:
bird 大佬最早发布的脚本 https://github.com/SnowGirls/deflat
后来有大佬改成 python3版本的 https://github.com/cq674350529/deflat
我直接拿来用的时候发现有一些小bug，fork了之后修正了小bug 对这道题的处理上不会再出现问题了 https://github.com/Pure-T/deflat
不过这题不用去除控制流平坦化也是可以做的，问题不大。
这是我去控制流平坦化之后的结果
int __cdecl main(int argc, const char **argv, const char **envp)
{
char v3; // al
char v4; // al
char v5; // al
char v6; // al
char v8; // al
char v9; // al
char v10; // al
char v11; // al
char v12; // [rsp+A0h] [rbp-90h]
char v13; // [rsp+A8h] [rbp-88h]
char v14; // [rsp+B0h] [rbp-80h]
char v15; // [rsp+B8h] [rbp-78h]
char v16; // [rsp+C0h] [rbp-70h]
char v17; // [rsp+C8h] [rbp-68h]
char v18; // [rsp+CFh] [rbp-61h]
int v19; // [rsp+D0h] [rbp-60h]
int v20; // [rsp+D4h] [rbp-5Ch]
int v21; // [rsp+D8h] [rbp-58h]
int v22; // [rsp+DCh] [rbp-54h]
char s[24]; // [rsp+E0h] [rbp-50h]
char v24; // [rsp+F8h] [rbp-38h]
char v25; // [rsp+100h] [rbp-30h]
char v26; // [rsp+108h] [rbp-28h]
char v27; // [rsp+110h] [rbp-20h]
int v28; // [rsp+114h] [rbp-1Ch]
const char **v29; // [rsp+118h] [rbp-18h]
int v30; // [rsp+120h] [rbp-10h]
int v31; // [rsp+124h] [rbp-Ch]
int v32; // [rsp+128h] [rbp-8h]
bool v33; // [rsp+12Eh] [rbp-2h]
bool v34; // [rsp+12Fh] [rbp-1h]
v31 = 0;
v30 = argc;
v29 = argv;
v28 = time(0LL);
puts("func(?)=\"01abfc750a0c942167651c40d088531d\"?");// #
s[0] = getchar();
fgets(&s[1], 21, stdin);
v22 = time(0LL);
v21 = v22 - v28;
v32 = v22 - v28;
if ( y >= 10 && (((_BYTE)x - 1) * (_BYTE)x & 1) != 0 )
goto LABEL_14;
while ( 1 )
{
v20 = strlen(s);
v33 = v20 != 21;
if ( y < 10 || (((_BYTE)x - 1) * (_BYTE)x & 1) == 0 )
break;
LABEL_14:
v20 = strlen(s);
}
if ( y >= 10 && (((_BYTE)x - 1) * (_BYTE)x & 1) != 0 )
goto LABEL_15;
while ( 1 )
{
v19 = 1;
if ( y < 10 || (((_BYTE)x - 1) * (_BYTE)x & 1) == 0 )
break;
LABEL_15:
v19 = 1;
}
while ( v19 < 21 ) // v19 [1,20]
{
if ( y >= 10 && (((_BYTE)x - 1) * (_BYTE)x & 1) != 0 )
{
v18 = v21 ^ s[v19];
v17 = main::$_0::operator() const((__int64)&v26, v18);
v16 = main::$_1::operator() const((__int64)&v24, s[v21 - 1 + v19]);
v8 = main::$_1::operator() const(char)::{lambda(int)#1}::operator() const(&v16, 7);
v18 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v17, v8);
v15 = main::$_2::operator() const(&v27, (unsigned int)v18);
v14 = main::$_2::operator() const(&v27, (unsigned int)s[v21 - 1 + v19]);
v9 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v14, 18LL);
v13 = main::$_3::operator() const((__int64)&v25, v9);
v10 = main::$_3::operator() const(char)::{lambda(char)#1}::operator() const(&v13, 3LL);
v12 = main::$_0::operator() const((__int64)&v26, v10);
v11 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v12, 2);
v18 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v15, (unsigned int)v11);
}
do
{
v18 = v21 ^ s[v19];
v17 = main::$_0::operator() const((__int64)&v26, v18);
v16 = main::$_1::operator() const((__int64)&v24, s[v21 - 1 + v19]);
v3 = main::$_1::operator() const(char)::{lambda(int)#1}::operator() const(&v16, 7);
v18 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v17, v3);
v15 = main::$_2::operator() const(&v27, (unsigned int)v18);
v14 = main::$_2::operator() const(&v27, (unsigned int)s[v21 - 1 + v19]);
v4 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v14, 18LL);
v13 = main::$_3::operator() const((__int64)&v25, v4);
v5 = main::$_3::operator() const(char)::{lambda(char)#1}::operator() const(&v13, 3LL);
v12 = main::$_0::operator() const((__int64)&v26, v5);
v6 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v12, 2);
v18 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v15, (unsigned int)v6);
v34 = enc[v19 - 1] != v18;
}
while ( v34 );
while ( y >= 10 && (((_BYTE)x - 1) * (_BYTE)x & 1) != 0 )
;
++v19;
}
if ( y >= 10 && (((_BYTE)x - 1) * (_BYTE)x & 1) != 0 )
goto LABEL_17;
while ( 1 )
{
puts("You win");
if ( y < 10 || (((_BYTE)x - 1) * (_BYTE)x & 1) == 0 )
break;
LABEL_17:
puts("You win");
}
return 0;
}
去除的并不是很完美，还是有很多地方没有处理好，后来对比原程序有丢失一些信息，问题主要发生在去除控制流平坦化时，识别返回块的处理上，这里不展开。
先给了一个 md5 值
puts("func(?)=\"01abfc750a0c942167651c40d088531d\"?");
反查 md5 知道是 '#' 字符
s[0] = getchar();
fgets(&s[1], 21, stdin);
这种写法应该是在暗示我第一个字符是 '#'，之后还要输入20个字符，一共21个字符
在往后他记录了一个时间差
v28 = time(0LL);
puts("func(?)=\"01abfc750a0c942167651c40d088531d\"?");// #
s[0] = getchar();
fgets(&s[1], 21, stdin);
v22 = time(0LL);
v21 = v22 - v28;
v32 = v22 - v28;
将开始输入前的时间和开始输入之后的时间差记录成了一个变量，后来我注意到在原程序中判断了这个时间差，若大于0就退出程序，在我这里被去除控制流平坦化的脚本给删去了。当时我选择先不管这个变量，往后看看，也许不影响解题。
再往后看，有一些多余的流程，忽略就好了。
v20 = strlen(s);
v33 = v20 != 21;
这里获取了输入字符串的长度，并记录下长度是否等于 21
v19 = 1;
初始化 v19 = 1，紧接着一个大循环
while ( v19 < 21 ) // v19 [1,20]
{
if ( y >= 10 && (((_BYTE)x - 1) * (_BYTE)x & 1) != 0 )
{
v18 = v21 ^ s[v19];
v17 = main::$_0::operator() const((__int64)&v26, v18);
v16 = main::$_1::operator() const((__int64)&v24, s[v21 - 1 + v19]);
v8 = main::$_1::operator() const(char)::{lambda(int)#1}::operator() const(&v16, 7);
v18 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v17, v8);
v15 = main::$_2::operator() const(&v27, (unsigned int)v18);
v14 = main::$_2::operator() const(&v27, (unsigned int)s[v21 - 1 + v19]);
v9 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v14, 18LL);
v13 = main::$_3::operator() const((__int64)&v25, v9);
v10 = main::$_3::operator() const(char)::{lambda(char)#1}::operator() const(&v13, 3LL);
v12 = main::$_0::operator() const((__int64)&v26, v10);
v11 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v12, 2);
v18 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v15, (unsigned int)v11);
}
do
{
v18 = v21 ^ s[v19];
v17 = main::$_0::operator() const((__int64)&v26, v18);
v16 = main::$_1::operator() const((__int64)&v24, s[v21 - 1 + v19]);
v3 = main::$_1::operator() const(char)::{lambda(int)#1}::operator() const(&v16, 7);
v18 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v17, v3);
v15 = main::$_2::operator() const(&v27, (unsigned int)v18);
v14 = main::$_2::operator() const(&v27, (unsigned int)s[v21 - 1 + v19]);
v4 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v14, 18LL);
v13 = main::$_3::operator() const((__int64)&v25, v4);
v5 = main::$_3::operator() const(char)::{lambda(char)#1}::operator() const(&v13, 3LL);
v12 = main::$_0::operator() const((__int64)&v26, v5);
v6 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v12, 2);
v18 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v15, (unsigned int)v6);
v34 = enc[v19 - 1] != v18;
}
while ( v34 );
while ( y >= 10 && (((_BYTE)x - 1) * (_BYTE)x & 1) != 0 )
;
++v19;
}
注意到循环的条件是 v19 < 21，猜测这里 v19 代表的是当前处理的字符串中字符的下标，也就是说它是从字符串的第二个字符开始处理的，这与之前猜测的以 '#' 开头呼应了
这个循环里还是有冗余的代码，我们把它处理一下去除不会执行的地方
while ( v19 < 21 ) // v19 [1,20]
{
do
{
v18 = v21 ^ s[v19];
v17 = main::$_0::operator() const((__int64)&v26, v18);
v16 = main::$_1::operator() const((__int64)&v24, s[v21 - 1 + v19]);
v3 = main::$_1::operator() const(char)::{lambda(int)#1}::operator() const(&v16, 7);
v18 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v17, v3);
v15 = main::$_2::operator() const(&v27, (unsigned int)v18);
v14 = main::$_2::operator() const(&v27, (unsigned int)s[v21 - 1 + v19]);
v4 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v14, 18LL);
v13 = main::$_3::operator() const((__int64)&v25, v4);
v5 = main::$_3::operator() const(char)::{lambda(char)#1}::operator() const(&v13, 3LL);
v12 = main::$_0::operator() const((__int64)&v26, v5);
v6 = main::$_0::operator() const(char)::{lambda(char)#1}::operator() const((__int64)&v12, 2);
v18 = main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(&v15, (unsigned int)v6);
v34 = enc[v19 - 1] != v18;
} while ( v34 );
++v19;
}
逻辑更加清晰了，在 do While 循环的最后，判断前面经过处理之后的结果 v18 是否等于 enc 表中的值，如果不等于就继续处理变化。换句话说，我们要控制我们的输入使得经过它规定的算法变化之后，等于 enc 表中的值，即可得到 flag
一个一个函数分析，我们随便输入 #input_flag_test_6789 调试看看
char __fastcall main::$_0::operator() const(__int64 a1, char a2)
{
return a2;
}
.text:00000000004012F0 push rbp
.text:00000000004012F1 mov rbp, rsp
.text:00000000004012F4 mov al, sil
.text:00000000004012F7 mov [rbp+var_10], rdi
.text:00000000004012FB mov [rbp+var_11], al
.text:00000000004012FE mov al, [rbp+var_11]
.text:0000000000401301 mov [rbp+var_8], al
.text:0000000000401304 mov al, [rbp+var_8]
.text:0000000000401307 pop rbp
.text:0000000000401308 retn
main::$_0 很显然就做了一件事情返回参数 a2，怕伪代码出错，我还特意看了一眼汇编
char __fastcall main::$_1::operator() const(__int64 a1, char a2)
{
return a2;
}
main::$_1 与 \$_0 一样
__int64 __fastcall main::$_1::operator() const(char)::{lambda(int)#1}::operator() const(char *a1, int a2)
{
return (unsigned int)(char)(*a1 % a2);
}
该函数取 a1 数组的第一个字符值与 a2 进行取模运算
__int64 __fastcall main::$_0::operator() const(char)::{lambda(char)#1}::operator() const(__int64 a1, char a2)
{
signed int v2; // eax
signed int v3; // eax
__int64 v5; // [rsp+0h] [rbp-40h]
int v6; // [rsp+4h] [rbp-3Ch]
int v7; // [rsp+8h] [rbp-38h]
int v8; // [rsp+Ch] [rbp-34h]
int v9; // [rsp+10h] [rbp-30h]
int v10; // [rsp+14h] [rbp-2Ch]
__int64 v11; // [rsp+18h] [rbp-28h]
char v12; // [rsp+23h] [rbp-1Dh]
int v13; // [rsp+24h] [rbp-1Ch]
bool v14; // [rsp+2Ah] [rbp-16h]
bool v15; // [rsp+2Bh] [rbp-15h]
unsigned int v16; // [rsp+2Ch] [rbp-14h]
v14 = (((_BYTE)x_5 - 1) * (_BYTE)x_5 & 1) == 0;// v14 = 1
v15 = y_6 < 10; // v15 = 1
v13 = 1023500310;
v12 = a2;
v11 = a1;
do
{
while ( 1 )
{
while ( 1 )
{
while ( 1 )
{
v10 = v13;
v9 = v13 + 0x796B2E2C;
if ( v13 != 0x8694D1D4 )
break;
*(&v5 - 2) = v11;
*((_BYTE *)&v5 - 16) = v12;
v13 = 0xAB705FC8;
}
v8 = v10 + 0x548FA038;
if ( v10 != 0xAB705FC8 )
break;
v3 = 0x8694D1D4;
*(&v5 - 2) = v11;
*((_BYTE *)&v5 - 16) = v12;
v16 = *((char *)&v5 - 16) + *(char *)*(&v5 - 2);// v16 = v11 + v12
if ( y_6 < 10 || (((_BYTE)x_5 - 1) * (_BYTE)x_5 & 1) == 0 )
v3 = 0x56CAF6B1;
v13 = v3;
}
v7 = v10 - 0x3D016016;
if ( v10 != 0x3D016016 )
break;
v2 = 0x8694D1D4;
if ( v15 || v14 )
v2 = 0xAB705FC8;
v13 = v2;
}
v6 = v10 - 0x56CAF6B1;
}
while ( v10 != 0x56CAF6B1 );
return v16;
}
这个函数看上去代码那么多。。其实都是混淆，真正执行的就一句话
v16 = v11 + v12
这里的 v11 v12 就是传入的参数 a1 a2
下一个函数也是一样...
char __fastcall main::$_2::operator() const(__int64 a1, char a2)
{
signed int v2; // eax
signed int v3; // eax
char v5; // [rsp+0h] [rbp-50h]
int v6; // [rsp+Ch] [rbp-44h]
int v7; // [rsp+10h] [rbp-40h]
int v8; // [rsp+14h] [rbp-3Ch]
int v9; // [rsp+18h] [rbp-38h]
int v10; // [rsp+1Ch] [rbp-34h]
__int64 v11; // [rsp+20h] [rbp-30h]
char v12; // [rsp+2Fh] [rbp-21h]
int v13; // [rsp+30h] [rbp-20h]
bool v14; // [rsp+35h] [rbp-1Bh]
bool v15; // [rsp+36h] [rbp-1Ah]
char v16; // [rsp+37h] [rbp-19h]
v14 = (((_BYTE)x_11 - 1) * (_BYTE)x_11 & 1) == 0;
v15 = y_12 < 10;
v13 = -1990873412;
v12 = a2;
v11 = a1;
while ( 1 )
{
while ( 1 )
{
while ( 1 )
{
v10 = v13;
v9 = v13 + 1990873412;
if ( v13 != -1990873412 )
break;
v2 = -1373097315;
if ( v15 || v14 )
v2 = 1457028246;
v13 = v2;
}
v8 = v10 + 1373097315;
if ( v10 != -1373097315 )
break;
*((_QWORD *)&v5 - 2) = v11;
*(&v5 - 16) = v12;
v5 = *(&v5 - 16);
v13 = 1457028246;
}
v7 = v10 + 961146335;
if ( v10 == -961146335 )
break;
v6 = v10 - 1457028246;
if ( v10 == 1457028246 )
{
v3 = -1373097315;
*((_QWORD *)&v5 - 2) = v11;
*(&v5 - 16) = v12;
v5 = *(&v5 - 16);
v16 = v5;
if ( y_12 < 10 || (((_BYTE)x_11 - 1) * (_BYTE)x_11 & 1) == 0 )
v3 = -961146335;
v13 = v3;
}
}
return v16;
}
也是一样虚胖...看上去很复杂，实际上执行的就三句话
*((_QWORD *)&v5 - 2) = v11;
*(&v5 - 16) = v12;
v5 = *(&v5 - 16);
v16 = v5;
其实就是把第二个参数 a2 返回
__int64 __fastcall main::$_2::operator() const(char)::{lambda(char)#1}::operator() const(_BYTE *a1, char a2)
{
return (unsigned int)(char)(a2 ^ *a1);
}
这个函数也比较友好...异或一下
char __fastcall main::$_3::operator() const(__int64 a1, char a2)
{
signed int v2; // eax
signed int v3; // eax
char v5; // [rsp+0h] [rbp-50h]
int v6; // [rsp+Ch] [rbp-44h]
int v7; // [rsp+10h] [rbp-40h]
int v8; // [rsp+14h] [rbp-3Ch]
int v9; // [rsp+18h] [rbp-38h]
int v10; // [rsp+1Ch] [rbp-34h]
__int64 v11; // [rsp+20h] [rbp-30h]
char v12; // [rsp+2Fh] [rbp-21h]
int v13; // [rsp+30h] [rbp-20h]
bool v14; // [rsp+35h] [rbp-1Bh]
bool v15; // [rsp+36h] [rbp-1Ah]
char v16; // [rsp+37h] [rbp-19h]
v14 = (((_BYTE)x_15 - 1) * (_BYTE)x_15 & 1) == 0;
v15 = y_16 < 10;
v13 = -538471561;
v12 = a2;
v11 = a1;
while ( 1 )
{
while ( 1 )
{
v10 = v13;
v9 = v13 + 2065325572;
if ( v13 != -2065325572 )
break;
*((_QWORD *)&v5 - 2) = v11;
*(&v5 - 16) = v12;
v5 = *(&v5 - 16);
v13 = 975002192;
}
v8 = v10 + 983538015;
if ( v10 == -983538015 )
break;
v7 = v10 + 538471561;
if ( v10 == -538471561 )
{
v2 = -2065325572;
if ( v15 || v14 )
v2 = 975002192;
v13 = v2;
}
else
{
v6 = v10 - 975002192;
if ( v10 == 975002192 )
{
v3 = -2065325572;
*((_QWORD *)&v5 - 2) = v11;
*(&v5 - 16) = v12;
v5 = *(&v5 - 16);
v16 = v5;
if ( y_16 < 10 || (((_BYTE)x_15 - 1) * (_BYTE)x_15 & 1) == 0 )
v3 = -983538015;
v13 = v3;
}
}
}
return v16;
}
返回第二个参数 a2
__int64 __fastcall main::$_3::operator() const(char)::{lambda(char)#1}::operator() const(char *a1, char a2)
{
return (unsigned int)(a2 * *a1);
}
第二个参数跟第一个参数的第一个字符相乘
最后给出一个 enc 数组
.data:0000000000602060 public enc
.data:0000000000602060 ; char enc[20]
.data:0000000000602060 enc db 0F3h ; DATA XREF: main+70A↑r
.data:0000000000602061 db 2Eh ; .
.data:0000000000602062 db 18h
.data:0000000000602063 db 36h ; 6
.data:0000000000602064 db 0E1h
.data:0000000000602065 db 4Ch ; L
.data:0000000000602066 db 22h ; "
.data:0000000000602067 db 0D1h
.data:0000000000602068 db 0F9h
.data:0000000000602069 db 8Ch
.data:000000000060206A db 40h ; @
.data:000000000060206B db 76h ; v
.data:000000000060206C db 0F4h
.data:000000000060206D db 0Eh
.data:000000000060206E db 0
.data:000000000060206F db 5
.data:0000000000602070 db 0A3h
.data:0000000000602071 db 90h
.data:0000000000602072 db 0Eh
.data:0000000000602073 db 0A5h
.data:0000000000602073 _data ends
刚好 20 个值
将上面的函数逻辑整理一下，大概就是下面的代码，可能语法会有点问题不影响理解
v18 = v21 ^ s[v19];
v17 = v18
v16 = s[v21 - 1 + v19]
v3 = v16[0] % 7
v18 = v17 + v3
v15 = v18
v14 = s[v21 - 1 + v19]
v4 = 18 ^ v14[0]
v13 = v4
v5 = v13[0] * 3
v12 = v5
v6 = v12[0] + 2
v18 = v15[0] ^ v6
// 最后整理成
v18 = ((v21 ^ s[v19]) + (s[v21 - 1 + v19] % 7)) ^ ((18 ^ s[v21 - 1 + v19]) * 3 + 2)
c = ((time ^ input[i]) + (input[time - 1 + i] % 7)) ^ ((18 ^ input[time - 1 + i]) * 3 + 2)
由于这里 time 预期为 0 所以
c = ((0 ^ input[i]) + (input[i-1] % 7)) ^ ((18 ^ input[i-1]) * 3 + 2)
已知 c 和 i 的情况下，很显然这个算法是可逆的
flag = [0 for i in range(21)]
flag[0] = 0x23
enc = 'F3 2E 18 36 E1 4C 22 D1 F9 8C 40 76 F4 0E 00 05 A3 90 0E A5'.split(' ')
c = [int(i,16) for i in enc]
for i in range(1,len(c)+1) :
flag[i] = (((c[i-1] ^ ((flag[i-1] ^ 18) * 3 + 2)) - (flag[i-1]%7)) ^ 0) & 0xff
print(''.join(map(chr,flag)))
最后得到答案 #flag{mY-CurR1ed_Fns}
babyunic
考察的是 unicorn CPU 模拟器
func 文件里放的是机器指令，babyunic 会借助 un.so.1 模拟执行 func 里的指令
__int64 __fastcall main(int a1, char **a2, char **a3)
{
const void *s1; // ST10_8
const char *v4; // ST18_8
__int64 v5; // ST00_8
if ( a1 == 2 )
{
puts("SUCTF 2019");
printf("input your flag:", a2);
s1 = malloc(0x200uLL);
v4 = (const char *)malloc(0x200uLL);
__isoc99_scanf("%50s", v4);
sub_CBA(v4, (__int64)s1, *(const char **)(v5 + 8));
if ( !memcmp(s1, &unk_202020, 168uLL) )
puts("congratuation!");
else
puts("fail!");
}
else
{
puts("no input files");
}
return 0LL;
}
给了一张常量表 unk_202020，与 s1 比较相等就说明输入的 flag 是正确的
将输入的内容传入 sub_CBA 处理
uc_open(3LL, 0x40000004LL, &uc_engine);
借助 uc_open 函数我们可以确定 func 的指令架构和位数
在 unicorn/include/unicorn/unicorn.h 位置处，我们可以找到
UNICORN_EXPORT
uc_err uc_open(uc_arch arch, uc_mode mode, uc_engine **uc);
/*
Close a Unicorn engine instance.
NOTE: this must be called only when there is no longer any
usage of @uc. This API releases some of @uc's cached memory, thus
any use of the Unicorn API with @uc after it has been closed may
crash your application. After this, @uc is invalid, and is no
longer usable.
@uc: pointer to a handle returned by uc_open()
@return UC_ERR_OK on success, or other value on failure (refer to uc_err enum
for detailed error).
*/
知道了三个参数的作用，我们再去找 arch 和 mode 的值定义
// Architecture type
typedef enum uc_arch {
UC_ARCH_ARM = 1, // ARM architecture (including Thumb, Thumb-2)
UC_ARCH_ARM64, // ARM-64, also called AArch64
UC_ARCH_MIPS, // Mips architecture
UC_ARCH_X86, // X86 architecture (including x86 & x86-64)
UC_ARCH_PPC, // PowerPC architecture (currently unsupported)
UC_ARCH_SPARC, // Sparc architecture
UC_ARCH_M68K, // M68K architecture
UC_ARCH_MAX,
} uc_arch;
// Mode type
typedef enum uc_mode {
UC_MODE_LITTLE_ENDIAN = 0, // little-endian mode (default mode)
UC_MODE_BIG_ENDIAN = 1 << 30, // big-endian mode
// arm / arm64
UC_MODE_ARM = 0, // ARM mode
UC_MODE_THUMB = 1 << 4, // THUMB mode (including Thumb-2)
UC_MODE_MCLASS = 1 << 5, // ARM's Cortex-M series (currently unsupported)
UC_MODE_V8 = 1 << 6, // ARMv8 A32 encodings for ARM (currently unsupported)
// mips
UC_MODE_MICRO = 1 << 4, // MicroMips mode (currently unsupported)
UC_MODE_MIPS3 = 1 << 5, // Mips III ISA (currently unsupported)
UC_MODE_MIPS32R6 = 1 << 6, // Mips32r6 ISA (currently unsupported)
UC_MODE_MIPS32 = 1 << 2, // Mips32 ISA
UC_MODE_MIPS64 = 1 << 3, // Mips64 ISA
// x86 / x64
UC_MODE_16 = 1 << 1, // 16-bit mode
UC_MODE_32 = 1 << 2, // 32-bit mode
UC_MODE_64 = 1 << 3, // 64-bit mode
// ppc
UC_MODE_PPC32 = 1 << 2, // 32-bit mode (currently unsupported)
UC_MODE_PPC64 = 1 << 3, // 64-bit mode (currently unsupported)
UC_MODE_QPX = 1 << 4, // Quad Processing eXtensions mode (currently unsupported)
// sparc
UC_MODE_SPARC32 = 1 << 2, // 32-bit mode
UC_MODE_SPARC64 = 1 << 3, // 64-bit mode
UC_MODE_V9 = 1 << 4, // SparcV9 mode (currently unsupported)
// m68k
} uc_mode;
因此 uc_open 中的 3 对应的是 UC_ARCH_MIPS ，0x40000004 其实等于 0x40000000 + 0x4 对应 UC_MODE_MIPS32 + UC_MODE_BIG_ENDIAN
知道了架构和位数我们就可以反汇编它了，这里我借助一个神器 ghidra 直接反编译
由于代码量有点大就不全部贴出来了
void UndefinedFunction_00000000(byte *param_1,int *param_2)
{
int iStack16;
int iStack12;
iStack12 = 0;
while (param_1[iStack12] != 0) {
iStack12 = iStack12 + 1;
}
iStack16 = 0;
while (iStack16 < iStack12) {
param_1[iStack16] = (param_1[iStack16] << 3 | param_1[iStack16] >> 5) ^ (byte)iStack16;
iStack16 = iStack16 + 1;
}
*param_2 = ((((((((((((((((((((((((((((((((uint)*param_1 + (uint)param_1[1] + (uint)param_1[2]) -
(uint)param_1[3]) + (uint)param_1[4]) - (uint)param_1[5])
- (uint)param_1[6]) - (uint)param_1[7]) - (uint)param_1[8])+
(uint)param_1[9] + (uint)param_1[10]) - (uint)param_1[0xb]) +
(uint)param_1[0xc]) - (uint)param_1[0xd]) - (uint)param_1[0xe])+
(uint)param_1[0xf]) - (uint)param_1[0x10]) - (uint)param_1[0x11]) +
(uint)param_1[0x12] + (uint)param_1[0x13]) - (uint)param_1[0x14]) +
(uint)param_1[0x15] + (uint)param_1[0x16] + (uint)param_1[0x17] +
(uint)param_1[0x18]) - (uint)param_1[0x19]) + (uint)param_1[0x1a]) -
(uint)param_1[0x1b]) + (uint)param_1[0x1c] + (uint)param_1[0x1d]) -
(uint)param_1[0x1e]) - (uint)param_1[0x1f]) + (uint)param_1[0x20]) -
(uint)param_1[0x21]) + (uint)param_1[0x22] + (uint)param_1[0x23]) -
(uint)param_1[0x24]) - (uint)param_1[0x25]) + (uint)param_1[0x26]) -
(uint)param_1[0x27]) + (uint)param_1[0x28] + (uint)param_1[0x29];
param_2[1] = (((((((((((((((((((((((((((((((((((uint)*param_1 - (uint)param_1[1]) +
(uint)param_1[2]) - (uint)param_1[3]) -
(uint)param_1[4]) + (uint)param_1[5]) -
(uint)param_1[6]) - (uint)param_1[7]) -(uint)param_1[8])
- (uint)param_1[9]) + (uint)param_1[10]) -
(uint)param_1[0xb]) + (uint)param_1[0xc]) -(uint)param_1[0xd]
) - (uint)param_1[0xe]) + (uint)param_1[0xf]) -
(uint)param_1[0x10]) - (uint)param_1[0x11]) +(uint)param_1[0x12])
- (uint)param_1[0x13]) + (uint)param_1[0x14] + (uint)param_1[0x15])-
(uint)param_1[0x16]) - (uint)param_1[0x17]) - (uint)param_1[0x18]) +
(uint)param_1[0x19]) - (uint)param_1[0x1a]) + (uint)param_1[0x1b]) -
(uint)param_1[0x1c]) - (uint)param_1[0x1d]) + (uint)param_1[0x1e] +
(uint)param_1[0x1f] + (uint)param_1[0x20] + (uint)param_1[0x21] +
(uint)param_1[0x22] + (uint)param_1[0x23]) - (uint)param_1[0x24]) -
(uint)param_1[0x25]) - (uint)param_1[0x26]) - (uint)param_1[0x27]) -
(uint)param_1[0x28]) + (uint)param_1[0x29];
param_2[2] = ((((((((((((((((((((((((((((((uint)*param_1 - (uint)param_1[1]) + (uint)param_1[2] +
(uint)param_1[3]) - (uint)param_1[4]) + (uint)param_1[5])
- (uint)param_1[6]) - (uint)param_1[7]) + (uint)param_1[8])-
(uint)param_1[9]) - (uint)param_1[10]) - (uint)param_1[0xb]) -
(uint)param_1[0xc]) - (uint)param_1[0xd]) + (uint)param_1[0xe]) -
(uint)param_1[0xf]) - (uint)param_1[0x10]) + (uint)param_1[0x11] +
(uint)param_1[0x12] + (uint)param_1[0x13] + (uint)param_1[0x14] +
(uint)param_1[0x15]) - (uint)param_1[0x16]) + (uint)param_1[0x17] +
(uint)param_1[0x18] + (uint)param_1[0x19] + (uint)param_1[0x1a]) -
(uint)param_1[0x1b]) + (uint)param_1[0x1c]) - (uint)param_1[0x1d]) +
(uint)param_1[0x1e]) - (uint)param_1[0x1f]) + (uint)param_1[0x20] +
(uint)param_1[0x21]) - (uint)param_1[0x22]) - (uint)param_1[0x23]) +
(uint)param_1[0x24] + (uint)param_1[0x25] + (uint)param_1[0x26]) -
(uint)param_1[0x27]) + (uint)param_1[0x28]) - (uint)param_1[0x29];
param_2[3] = ...
......
这里第一个参数 param_1 是我们输入的字符串, param_2 最后得到的值要等于那个常量表
这里借助 z3 一把梭，不过要注意的是 enc 那个常量是以补码形式表示的
from z3 import *
import ctypes
e = [0xFFFFFF94,0xFFFFFF38,0x00000126,0xFFFFFF28,0xFFFFFC10,0x00000294,0xFFFFFC9E,0x000006EA,0x000000DC,0x00000006,0xFFFFFF0C,0xFFFFFDF6,0xFFFFFA82,0xFFFFFCD0,0x00000182,0x000003DE,0x0000014E,0x000002B2,0xFFFFF8D8,0x00000174,0xFFFFFAA6,0xFFFFF9D4,0x000001C2,0xFFFFF97C,0x0000035A,0x00000146,0xFFFFFF3C,0xFFFFFA14,0x000001CE,0x000007DC,0xFFFFFD48,0x00000098,0x0000085E,0xFFFFFDB0,0xFFFFFFBC,0x0000036E,0xFFFFFF4E,0xFFFFF836,0x000005C0,0x000006AE,0x00000694,0x00000022]
en = map(lambda x: ctypes.c_int32(x).value,e)
enc = [IntVal(i) for i in en]
# enc = map(lambda x: ctypes.c_int32(x).value, enc)
c = [Int('c%d' % i) for i in range(42)]
flag = []
solver = Solver()
for v in c :
solver.add(v >= 0x0)
solver.add(v <= 0xff)
solver.add(enc[0]==(((((((((((((((((((((((((((((((c[0]+c[1]+c[2])-c[3])+c[4])-c[5])-c[6])-c[7])-c[8])+c[9]+c[10])-c[0xb])+c[0xc])-c[0xd])-c[0xe])+c[0xf])-c[0x10])-c[0x11])+c[0x12]+c[0x13])-c[0x14])+c[0x15]+c[0x16]+c[0x17]+c[0x18])-c[0x19])+c[0x1a])-c[0x1b])+c[0x1c]+c[0x1d])-c[0x1e])-c[0x1f])+c[0x20])-c[0x21])+c[0x22]+c[0x23])-c[0x24])-c[0x25])+c[0x26])-c[0x27])+c[0x28]+c[0x29])
solver.add(enc[1]==((((((((((((((((((((((((((((((((((c[0]-c[1])+c[2])-c[3])-c[4])+c[5])-c[6])-c[7])-c[8])-c[9])+c[10])-c[0xb])+c[0xc])-c[0xd])-c[0xe])+c[0xf])-c[0x10])-c[0x11])+c[0x12])-c[0x13])+c[0x14]+c[0x15])-c[0x16])-c[0x17])-c[0x18])+c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])-c[0x1d])+c[0x1e]+c[0x1f]+c[0x20]+c[0x21]+c[0x22]+c[0x23])-c[0x24])-c[0x25])-c[0x26])-c[0x27])-c[0x28])+c[0x29])
solver.add(enc[2]==(((((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3])-c[4])+c[5])-c[6])-c[7])+c[8])-c[9])-c[10])-c[0xb])-c[0xc])-c[0xd])+c[0xe])-c[0xf])-c[0x10])+c[0x11]+c[0x12]+c[0x13]+c[0x14]+c[0x15])-c[0x16])+c[0x17]+c[0x18]+c[0x19]+c[0x1a])-c[0x1b])+c[0x1c])-c[0x1d])+c[0x1e])-c[0x1f])+c[0x20]+c[0x21])-c[0x22])-c[0x23])+c[0x24]+c[0x25]+c[0x26])-c[0x27])+c[0x28])-c[0x29])
solver.add(enc[3]==(((((((((((((((((((((((((((((((c[0]-c[1])-c[2])-c[3])-c[4])-c[5])+c[6]+c[7])-c[8])-c[9])-c[10])-c[0xb])+c[0xc])-c[0xd])+c[0xe])-c[0xf])+c[0x10])-c[0x11])+c[0x12]+c[0x13]+c[0x14])-c[0x15])+c[0x16]+c[0x17]+c[0x18])-c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e])-c[0x1f])-c[0x20])-c[0x21])+c[0x22])-c[0x23])+c[0x24]+c[0x25]+c[0x26])-c[0x27])+c[0x28]+c[0x29])
solver.add(enc[4]==(((((((((((((((((((((((((((((((((c[0]-c[1])-c[2])+c[3])-c[4])-c[5])+c[6]+c[7]+c[8]+c[9])-c[10])+c[0xb]+c[0xc])-c[0xd])+c[0xe])-c[0xf])+c[0x10]+c[0x11])-c[0x12])+c[0x13])-c[0x14])+c[0x15])-c[0x16])-c[0x17])-c[0x18])+c[0x19])-c[0x1a])-c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e]+c[0x1f])-c[0x20])+c[0x21])-c[0x22])-c[0x23])+c[0x24])-c[0x25])+c[0x26])-c[0x27])-c[0x28])-c[0x29])
solver.add(enc[5]==((((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3]+c[4]+c[5]+c[6]+c[7]+c[8])-c[9])-c[10])-c[0xb])-c[0xc])-c[0xd])-c[0xe])+c[0xf])-c[0x10])+c[0x11])-c[0x12])+c[0x13]+c[0x14])-c[0x15])+c[0x16])-c[0x17])+c[0x18])-c[0x19])+c[0x1a]+c[0x1b])-c[0x1c])+c[0x1d])-c[0x1e])+c[0x1f]+c[0x20]+c[0x21])-c[0x22])-c[0x23])-c[0x24])+c[0x25])-c[0x26])-c[0x27])+c[0x28]+c[0x29])
solver.add(enc[6]==(((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3]+c[4])-c[5])+c[6]+c[7]+c[8]+c[9])-c[10])+c[0xb]+c[0xc])-c[0xd])+c[0xe]+c[0xf]+c[0x10]+c[0x11])-c[0x12])-c[0x13])-c[0x14])-c[0x15])-c[0x16])-c[0x17])+c[0x18]+c[0x19])-c[0x1a])+c[0x1b]+c[0x1c]+c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])-c[0x23])+c[0x24]+c[0x25])-c[0x26])-c[0x27])+c[0x28])-c[0x29])
solver.add(enc[7]==((((((((((((((((((((((((((((((c[0]+c[1])-c[2])-c[3])-c[4])+c[5]+c[6])-c[7])+c[8]+c[9])-c[10])+c[0xb])-c[0xc])+c[0xd])-c[0xe])+c[0xf])-c[0x10])+c[0x11])-c[0x12])-c[0x13])+c[0x14])-c[0x15])+c[0x16])-c[0x17])-c[0x18])+c[0x19])-c[0x1a])+c[0x1b]+c[0x1c]+c[0x1d]+c[0x1e]+c[0x1f]+c[0x20])-c[0x21])+c[0x22])-c[0x23])+c[0x24]+c[0x25]+c[0x26]+c[0x27])-c[0x28])-c[0x29])
solver.add(enc[8]==(((((((((((((((((((((((((((((c[0]-c[1])-c[2])+c[3]+c[4])-c[5])+c[6]+c[7]+c[8]+c[9]+c[10])-c[0xb])-c[0xc])+c[0xd])-c[0xe])+c[0xf]+c[0x10]+c[0x11]+c[0x12])-c[0x13])+c[0x14]+c[0x15])-c[0x16])-c[0x17])+c[0x18]+c[0x19]+c[0x1a])-c[0x1b])+c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])+c[0x22])-c[0x23])-c[0x24])+c[0x25])-c[0x26])-c[0x27])+c[0x28])-c[0x29])
solver.add(enc[9]==(((((((((((((((((((((((((((((c[0]+c[1]+c[2])-c[3])+c[4]+c[5]+c[6])-c[7])-c[8])-c[9])-c[10])+c[0xb]+c[0xc]+c[0xd])-c[0xe])+c[0xf]+c[0x10])-c[0x11])-c[0x12])+c[0x13]+c[0x14])-c[0x15])-c[0x16])-c[0x17])+c[0x18])-c[0x19])-c[0x1a])-c[0x1b])+c[0x1c]+c[0x1d]+c[0x1e])-c[0x1f])+c[0x20]+c[0x21])-c[0x22])-c[0x23])-c[0x24])-c[0x25])+c[0x26])-c[0x27])+c[0x28]+c[0x29])
solver.add(enc[10]==((((((((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3])-c[4])-c[5])+c[6]+c[7])-c[8])-c[9])-c[10])-c[0xb])+c[0xc]+c[0xd]+c[0xe])-c[0xf])+c[0x10])-c[0x11])+c[0x12]+c[0x13]+c[0x14])-c[0x15])+c[0x16])-c[0x17])-c[0x18])-c[0x19])+c[0x1a])-c[0x1b])-c[0x1c])+c[0x1d])-c[0x1e])+c[0x1f]+c[0x20])-c[0x21])-c[0x22])+c[0x23])-c[0x24])-c[0x25])+c[0x26])-c[0x27])+c[0x28]+c[0x29])
solver.add(enc[0xb]==((((((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3]+c[4])-c[5])+c[6]+c[7])-c[8])+c[9]+c[10])-c[0xb])-c[0xc])-c[0xd])-c[0xe])+c[0xf])-c[0x10])-c[0x11])-c[0x12])+c[0x13]+c[0x14])-c[0x15])+c[0x16])-c[0x17])+c[0x18]+c[0x19]+c[0x1a]+c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])-c[0x23])+c[0x24]+c[0x25])-c[0x26])-c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0xc]==(((((((((((((((((((((((((((((((((((((c[0]-c[1])-c[2])-c[3])+c[4])-c[5])-c[6])+c[7]+c[8])-c[9])+c[10])-c[0xb])-c[0xc])-c[0xd])+c[0xe])-c[0xf])+c[0x10])-c[0x11])+c[0x12])-c[0x13])-c[0x14])-c[0x15])-c[0x16])+c[0x17])-c[0x18])+c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])+c[0x1d])-c[0x1e])-c[0x1f])+c[0x20]+c[0x21]+c[0x22])-c[0x23])-c[0x24])-c[0x25])-c[0x26])+c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0xd]==(((((((((((((((((((((((((((((((((c[0]-c[1])+c[2])-c[3])+c[4])-c[5])+c[6])-c[7])+c[8])-c[9])+c[10])-c[0xb])+c[0xc]+c[0xd]+c[0xe]+c[0xf])-c[0x10])-c[0x11])-c[0x12])+c[0x13]+c[0x14]+c[0x15])-c[0x16])-c[0x17])+c[0x18]+c[0x19])-c[0x1a])-c[0x1b])+c[0x1c]+c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])+c[0x21])-c[0x22])-c[0x23])+c[0x24])-c[0x25])-c[0x26])-c[0x27])+c[0x28])-c[0x29])
solver.add(enc[0xe]==(((((((((((((((((((((((((c[0]+c[1]+c[2])-c[3])-c[4])-c[5])+c[6])-c[7])+c[8]+c[9]+c[10])-c[0xb])+c[0xc])-c[0xd])-c[0xe])+c[0xf]+c[0x10]+c[0x11])-c[0x12])-c[0x13])-c[0x14])-c[0x15])+c[0x16]+c[0x17]+c[0x18])-c[0x19])+c[0x1a]+c[0x1b]+c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])+c[0x20]+c[0x21]+c[0x22]+c[0x23]+c[0x24]+c[0x25]+c[0x26])-c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0xf]==((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3]+c[4]+c[5])-c[6])+c[7])-c[8])-c[9])-c[10])+c[0xb]+c[0xc]+c[0xd])-c[0xe])-c[0xf])-c[0x10])+c[0x11])-c[0x12])-c[0x13])-c[0x14])-c[0x15])+c[0x16]+c[0x17]+c[0x18]+c[0x19]+c[0x1a]+c[0x1b])-c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])+c[0x20])-c[0x21])+c[0x22]+c[0x23]+c[0x24]+c[0x25])-c[0x26])+c[0x27]+c[0x28])-c[0x29])
solver.add(enc[0x10]==((((((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3])-c[4])-c[5])+c[6]+c[7]+c[8]+c[9]+c[10])-c[0xb])+c[0xc])-c[0xd])+c[0xe]+c[0xf]+c[0x10])-c[0x11])+c[0x12])-c[0x13])+c[0x14])-c[0x15])-c[0x16])-c[0x17])-c[0x18])-c[0x19])+c[0x1a]+c[0x1b]+c[0x1c]+c[0x1d])-c[0x1e])-c[0x1f])+c[0x20])-c[0x21])-c[0x22])+c[0x23])-c[0x24])+c[0x25])-c[0x26])+c[0x27])-c[0x28])+c[0x29])
solver.add(enc[0x11]==((((((((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3]+c[4])-c[5])+c[6]+c[7]+c[8])-c[9])-c[10])+c[0xb])-c[0xc])+c[0xd]+c[0xe]+c[0xf])-c[0x10])+c[0x11])-c[0x12])-c[0x13])+c[0x14])-c[0x15])+c[0x16])-c[0x17])-c[0x18])+c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])+c[0x1d])-c[0x1e])-c[0x1f])+c[0x20])-c[0x21])-c[0x22])+c[0x23])-c[0x24])+c[0x25])-c[0x26])+c[0x27]+c[0x28])-c[0x29])
solver.add(enc[0x12]==((((((((((((((((((((((((((((((((((c[0]-c[1])-c[2])-c[3])+c[4]+c[5])-c[6])+c[7])-c[8])+c[9]+c[10])-c[0xb])-c[0xc])-c[0xd])+c[0xe])-c[0xf])-c[0x10])+c[0x11]+c[0x12]+c[0x13])-c[0x14])-c[0x15])-c[0x16])-c[0x17])-c[0x18])-c[0x19])-c[0x1a])-c[0x1b])+c[0x1c]+c[0x1d]+c[0x1e])-c[0x1f])-c[0x20])-c[0x21])+c[0x22])-c[0x23])-c[0x24])-c[0x25])-c[0x26])-c[0x27])-c[0x28])+c[0x29])
solver.add(enc[0x13]==((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3])-c[4])-c[5])+c[6])-c[7])-c[8])-c[9])-c[10])-c[0xb])-c[0xc])-c[0xd])+c[0xe]+c[0xf]+c[0x10])-c[0x11])+c[0x12]+c[0x13]+c[0x14]+c[0x15])-c[0x16])+c[0x17]+c[0x18])-c[0x19])+c[0x1a]+c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e]+c[0x1f]+c[0x20]+c[0x21])-c[0x22])+c[0x23])-c[0x24])-c[0x25])-c[0x26])+c[0x27]+c[0x28])-c[0x29])
solver.add(enc[0x14]==((((((((((((((((((((((((((((((((((((c[0]+c[1])-c[2])-c[3])-c[4])+c[5])-c[6])+c[7])-c[8])-c[9])+c[10]+c[0xb])-c[0xc])-c[0xd])+c[0xe])-c[0xf])-c[0x10])+c[0x11])-c[0x12])-c[0x13])+c[0x14]+c[0x15])-c[0x16])+c[0x17]+c[0x18])-c[0x19])-c[0x1a])-c[0x1b])-c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])+c[0x21])-c[0x22])+c[0x23]+c[0x24])-c[0x25])+c[0x26])-c[0x27])+c[0x28])-c[0x29])
solver.add(enc[0x15]==(((((((((((((((((((((((((((((((((((c[0]-c[1])-c[2])-c[3])+c[4]+c[5]+c[6]+c[7])-c[8])-c[9])-c[10])-c[0xb])-c[0xc])-c[0xd])-c[0xe])-c[0xf])-c[0x10])+c[0x11])-c[0x12])-c[0x13])+c[0x14])-c[0x15])+c[0x16]+c[0x17]+c[0x18])-c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])-c[0x23])-c[0x24])+c[0x25])-c[0x26])-c[0x27])-c[0x28])+c[0x29])
solver.add(enc[0x16]==(((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3]+c[4]+c[5]+c[6]+c[7])-c[8])+c[9])-c[10])+c[0xb])-c[0xc])+c[0xd]+c[0xe]+c[0xf])-c[0x10])+c[0x11]+c[0x12])-c[0x13])-c[0x14])+c[0x15]+c[0x16])-c[0x17])+c[0x18])-c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e]+c[0x1f])-c[0x20])+c[0x21])-c[0x22])-c[0x23])-c[0x24])-c[0x25])+c[0x26])-c[0x27])+c[0x28]+c[0x29])
solver.add(enc[0x17]==(((((((((((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3])-c[4])-c[5])-c[6])-c[7])+c[8])-c[9])-c[10])+c[0xb]+c[0xc])-c[0xd])-c[0xe])+c[0xf])-c[0x10])-c[0x11])+c[0x12]+c[0x13])-c[0x14])-c[0x15])+c[0x16])-c[0x17])+c[0x18]+c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])-c[0x23])-c[0x24])-c[0x25])+c[0x26])-c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0x18]==(((((((((((((((((((((((((c[0]+c[1])-c[2])+c[3]+c[4])-c[5])+c[6]+c[7])-c[8])+c[9]+c[10])-c[0xb])-c[0xc])-c[0xd])-c[0xe])+c[0xf]+c[0x10]+c[0x11])-c[0x12])+c[0x13]+c[0x14]+c[0x15]+c[0x16]+c[0x17]+c[0x18]+c[0x19])-c[0x1a])-c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e])-c[0x1f])+c[0x20]+c[0x21]+c[0x22])-c[0x23])-c[0x24])-c[0x25])-c[0x26])+c[0x27]+c[0x28])-c[0x29])
solver.add(enc[0x19]==((((((((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3])-c[4])+c[5]+c[6])-c[7])+c[8]+c[9]+c[10])-c[0xb])-c[0xc])+c[0xd])-c[0xe])+c[0xf])-c[0x10])+c[0x11]+c[0x12]+c[0x13])-c[0x14])-c[0x15])+c[0x16]+c[0x17])-c[0x18])-c[0x19])+c[0x1a])-c[0x1b])+c[0x1c])-c[0x1d])+c[0x1e])-c[0x1f])-c[0x20])+c[0x21])-c[0x22])-c[0x23])-c[0x24])-c[0x25])+c[0x26])-c[0x27])+c[0x28]+c[0x29])
solver.add(enc[0x1a]==(((((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3]+c[4])-c[5])-c[6])+c[7])-c[8])-c[9])-c[10])-c[0xb])+c[0xc])-c[0xd])+c[0xe])-c[0xf])+c[0x10])-c[0x11])+c[0x12])-c[0x13])-c[0x14])+c[0x15]+c[0x16]+c[0x17]+c[0x18]+c[0x19])-c[0x1a])-c[0x1b])-c[0x1c])-c[0x1d])+c[0x1e]+c[0x1f])-c[0x20])-c[0x21])-c[0x22])+c[0x23]+c[0x24])-c[0x25])-c[0x26])+c[0x27]+c[0x28]+c[0x29])
solver.add(enc[0x1b]==(((((((((((((((((((((((((((((((c[0]-c[1])+c[2])-c[3])+c[4])-c[5])-c[6])-c[7])-c[8])-c[9])-c[10])-c[0xb])+c[0xc]+c[0xd])-c[0xe])+c[0xf]+c[0x10]+c[0x11]+c[0x12]+c[0x13])-c[0x14])-c[0x15])-c[0x16])-c[0x17])+c[0x18]+c[0x19]+c[0x1a])-c[0x1b])+c[0x1c]+c[0x1d]+c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])+c[0x23])-c[0x24])-c[0x25])-c[0x26])-c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0x1c]==((((((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3]+c[4])-c[5])+c[6]+c[7])-c[8])-c[9])+c[10]+c[0xb])-c[0xc])+c[0xd])-c[0xe])+c[0xf])-c[0x10])+c[0x11]+c[0x12]+c[0x13])-c[0x14])-c[0x15])+c[0x16])-c[0x17])-c[0x18])-c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])-c[0x1d])-c[0x1e])+c[0x1f])-c[0x20])-c[0x21])+c[0x22]+c[0x23]+c[0x24])-c[0x25])-c[0x26])+c[0x27]+c[0x28]+c[0x29])
solver.add(enc[0x1d]==((((((((((((((((((((((((((c[0]+c[1])-c[2])-c[3])-c[4])+c[5]+c[6]+c[7])-c[8])+c[9])-c[10])-c[0xb])+c[0xc])-c[0xd])+c[0xe]+c[0xf])-c[0x10])+c[0x11]+c[0x12])-c[0x13])+c[0x14]+c[0x15]+c[0x16]+c[0x17])-c[0x18])+c[0x19]+c[0x1a])-c[0x1b])+c[0x1c]+c[0x1d]+c[0x1e]+c[0x1f]+c[0x20])-c[0x21])-c[0x22])+c[0x23]+c[0x24])-c[0x25])+c[0x26]+c[0x27])-c[0x28])+c[0x29])
solver.add(enc[0x1e]==((((((((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3])-c[4])-c[5])-c[6])-c[7])+c[8]+c[9])-c[10])-c[0xb])-c[0xc])+c[0xd])-c[0xe])-c[0xf])+c[0x10])-c[0x11])-c[0x12])-c[0x13])+c[0x14])-c[0x15])-c[0x16])+c[0x17]+c[0x18])-c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])+c[0x23]+c[0x24]+c[0x25])-c[0x26])+c[0x27]+c[0x28]+c[0x29])
solver.add(enc[0x1f]==((((((((((((((((((((((((((((((c[0]+c[1])-c[2])+c[3]+c[4])-c[5])-c[6])+c[7]+c[8]+c[9]+c[10]+c[0xb]+c[0xc])-c[0xd])-c[0xe])-c[0xf])+c[0x10]+c[0x11]+c[0x12]+c[0x13])-c[0x14])+c[0x15])-c[0x16])+c[0x17])-c[0x18])-c[0x19])+c[0x1a]+c[0x1b])-c[0x1c])+c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])+c[0x21])-c[0x22])+c[0x23])-c[0x24])+c[0x25])-c[0x26])+c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0x20]==(((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3])-c[4])+c[5]+c[6]+c[7]+c[8])-c[9])+c[10]+c[0xb])-c[0xc])+c[0xd]+c[0xe])-c[0xf])+c[0x10])-c[0x11])+c[0x12]+c[0x13]+c[0x14])-c[0x15])-c[0x16])+c[0x17])-c[0x18])+c[0x19]+c[0x1a]+c[0x1b])-c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])+c[0x22]+c[0x23]+c[0x24]+c[0x25])-c[0x26])+c[0x27])-c[0x28])+c[0x29])
solver.add(enc[0x21]==(((((((((((((((((((((((((((((((c[0]-c[1])-c[2])+c[3]+c[4]+c[5]+c[6])-c[7])-c[8])+c[9]+c[10]+c[0xb])-c[0xc])-c[0xd])+c[0xe]+c[0xf])-c[0x10])+c[0x11])-c[0x12])+c[0x13])-c[0x14])+c[0x15]+c[0x16]+c[0x17])-c[0x18])-c[0x19])+c[0x1a]+c[0x1b])-c[0x1c])+c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])-c[0x23])+c[0x24])-c[0x25])+c[0x26])-c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0x22]==((((((((((((((((((((((((((((((c[0]+c[1])-c[2])+c[3])-c[4])-c[5])-c[6])+c[7]+c[8]+c[9]+c[10]+c[0xb])-c[0xc])-c[0xd])-c[0xe])+c[0xf])-c[0x10])+c[0x11])-c[0x12])+c[0x13])-c[0x14])-c[0x15])+c[0x16]+c[0x17])-c[0x18])-c[0x19])+c[0x1a]+c[0x1b]+c[0x1c]+c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])-c[0x23])-c[0x24])+c[0x25]+c[0x26]+c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0x23]==((((((((((((((((((((((((((c[0]-c[1])+c[2]+c[3]+c[4])-c[5])-c[6])+c[7]+c[8])-c[9])-c[10])+c[0xb]+c[0xc]+c[0xd])-c[0xe])-c[0xf])+c[0x10])-c[0x11])+c[0x12]+c[0x13])-c[0x14])-c[0x15])-c[0x16])+c[0x17]+c[0x18])-c[0x19])-c[0x1a])+c[0x1b]+c[0x1c])-c[0x1d])-c[0x1e])+c[0x1f]+c[0x20])-c[0x21])+c[0x22]+c[0x23]+c[0x24]+c[0x25]+c[0x26]+c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0x24]==(((((((((((((((((((((((((c[0]+c[1]+c[2])-c[3])-c[4])-c[5])-c[6])+c[7]+c[8]+c[9])-c[10])+c[0xb]+c[0xc])-c[0xd])+c[0xe]+c[0xf]+c[0x10]+c[0x11]+c[0x12]+c[0x13]+c[0x14]+c[0x15])-c[0x16])-c[0x17])+c[0x18])-c[0x19])-c[0x1a])-c[0x1b])-c[0x1c])+c[0x1d]+c[0x1e]+c[0x1f]+c[0x20])-c[0x21])-c[0x22])-c[0x23])-c[0x24])+c[0x25])-c[0x26])+c[0x27]+c[0x28])-c[0x29])
solver.add(enc[0x25]==((((((((((((((((((((((((((((((((((((((c[0]-c[1])-c[2])+c[3])-c[4])+c[5])-c[6])-c[7])-c[8])-c[9])+c[10])-c[0xb])-c[0xc])-c[0xd])-c[0xe])-c[0xf])-c[0x10])+c[0x11]+c[0x12])-c[0x13])-c[0x14])-c[0x15])+c[0x16])-c[0x17])+c[0x18])-c[0x19])-c[0x1a])+c[0x1b])-c[0x1c])-c[0x1d])+c[0x1e]+c[0x1f])-c[0x20])+c[0x21])-c[0x22])+c[0x23])-c[0x24])-c[0x25])+c[0x26])-c[0x27])-c[0x28])-c[0x29])
solver.add(enc[0x26]==((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3])-c[4])+c[5]+c[6]+c[7])-c[8])-c[9])-c[10])+c[0xb]+c[0xc]+c[0xd])-c[0xe])-c[0xf])-c[0x10])-c[0x11])-c[0x12])-c[0x13])+c[0x14]+c[0x15])-c[0x16])+c[0x17]+c[0x18]+c[0x19]+c[0x1a]+c[0x1b])-c[0x1c])-c[0x1d])+c[0x1e]+c[0x1f])-c[0x20])-c[0x21])+c[0x22])-c[0x23])-c[0x24])-c[0x25])+c[0x26]+c[0x27]+c[0x28])-c[0x29])
solver.add(enc[0x27]==(((((((((((((((((((((((((c[0]-c[1])-c[2])-c[3])-c[4])+c[5])-c[6])-c[7])-c[8])+c[9])-c[10])+c[0xb])-c[0xc])+c[0xd]+c[0xe])-c[0xf])-c[0x10])-c[0x11])+c[0x12]+c[0x13]+c[0x14]+c[0x15]+c[0x16])-c[0x17])+c[0x18]+c[0x19]+c[0x1a]+c[0x1b]+c[0x1c])-c[0x1d])+c[0x1e]+c[0x1f]+c[0x20]+c[0x21]+c[0x22])-c[0x23])-c[0x24])+c[0x25]+c[0x26]+c[0x27])-c[0x28])+c[0x29])
solver.add(enc[0x28]==((((((((((((((((((((((c[0]-c[1])-c[2])-c[3])+c[4]+c[5]+c[6])-c[7])+c[8]+c[9])-c[10])+c[0xb])-c[0xc])-c[0xd])-c[0xe])+c[0xf]+c[0x10]+c[0x11]+c[0x12]+c[0x13]+c[0x14]+c[0x15]+c[0x16])-c[0x17])+c[0x18]+c[0x19])-c[0x1a])+c[0x1b]+c[0x1c])-c[0x1d])+c[0x1e]+c[0x1f]+c[0x20])-c[0x21])-c[0x22])+c[0x23]+c[0x24])-c[0x25])+c[0x26]+c[0x27]+c[0x28]+c[0x29])
solver.add(enc[0x29]==(((((((((((((((((((((((((((((((c[0]+c[1]+c[2]+c[3]+c[4]+c[5]+c[6])-c[7])-c[8])-c[9])+c[10]+c[0xb])-c[0xc])+c[0xd])-c[0xe])-c[0xf])-c[0x10])-c[0x11])-c[0x12])-c[0x13])+c[0x14])-c[0x15])+c[0x16])-c[0x17])-c[0x18])+c[0x19]+c[0x1a]+c[0x1b]+c[0x1c])-c[0x1d])-c[0x1e])-c[0x1f])-c[0x20])-c[0x21])-c[0x22])-c[0x23])-c[0x24])-c[0x25])-c[0x26])-c[0x27])-c[0x28])+c[0x29])
if solver.check() == sat :
r = solver.model()
for i in range(42) :
flag.append(r[c[i]].as_long()^i)
flag = ''.join(map(lambda x : chr(((x >> 3) | (x << 5)) & 0xff),flag))
print(flag)
# SUCTF{Un1c0rn_Engin3_Is_@_P0wer7ul_TO0ls!}
Akira Homework
程序有反调试，nop 掉 call cs:IsDebuggerPresent，还开了 ASLR，用 010editor 关闭 ASLR
v1 = 0;
memset(&v4, 0, 0x13ui64);
memset(&Dst, 0, 0x6Dui64);
memcpy(&Dst, aJLJLJL1pzxcp6b, 0x6Cui64);
for ( i = 0; (unsigned __int64)i < 0x6C; ++i )
aJLJLJL1pzxcp6b[i] ^= byte_140015F20[0];
puts(aJLJLJL1pzxcp6b);
sub_140009FF0((__int64)"%18s", &v4, 19i64);
调试到这，发现程序很多的字符串应该都是加密了，而 key 就是 byte_140015F20
sub_140009FF0 应该是一个输入函数，但是每次调试到那程序都自动退出，不知道是反调试还是本身有 bug
只好 nop 掉它，手工修改内存
v13 = a1;
memset(Dst, 0, 0x13ui64);
memcpy(Dst, &unk_140015E38, 0x12ui64);
for ( i = 0; (unsigned __int64)i < 19; ++i )
Dst[i] ^= byte_140015F20[1];
memset(v12, 0, 0x13ui64);
for ( j = 0; (unsigned __int64)j < 18; ++j )
v12[j] = j ^ *(_BYTE *)(v13 + j);
v5 = 1;
v6 = 5;
v7 = 4;
v8 = 2;
v9 = 3;
v10 = 0;
for ( k = 0; (unsigned __int64)k < 0x12; ++k )
{
if ( Dst[k] != v12[6 * (k / 6) + *(&v5 + k % 6)] )
return 0;
}
return 1;
第一段算法很好懂，逆向一下
s = [0 for i in range(18)]
v5 = [1,5,4,2,3,0]
dst =[int(i,16) for i in '6A 5A 65 6B 71 41 72 68 55 7C 39 67 3E 30 4F 7D 7C 64 45'.split(" ")]
for k in range(0x12) :
s[6 * (int(k / 6)) + v5[k % 6] ] = dst[k]
for j in range(18) :
s[j] = s[j] ^ j
print(''.join(map(chr,s)))
# Akira_aut0_ch3ss_!
得到一段字符串
继续调试然后程序执行到了
sub_140008300((__int64)&v9, 3i64, 1048578);
return sub_140006C10(qword_140016178, v9, 0i64);
跟进 sub_140006C10 函数看看
发现这里对大量的数据进行解密操作
char __fastcall sub_140008910(__int64 a1, const char *a2)
{
int i; // [rsp+20h] [rbp-28h]
int v4; // [rsp+24h] [rbp-24h]
char *Str; // [rsp+28h] [rbp-20h]
Str = (char *)a2;
v4 = strlen(a2);
for ( i = 0; i < dword_140011194; ++i )
{
if ( !(i % 3) )
byte_1400111A0[i] ^= Str[i / 3 % v4]; // .data:00000001400111A0
}
SetEvent(Handles[0]); // 设置事件 Handles[0] 为激发状态
return 1;
}
密钥就是我们刚才传入的字符串，这说明 sub_140006C10 是一个解密函数，交叉引用看下有三处调用，结合前面有一段创建三个空事件的代码，猜测可能是要进行三次解密之后将这块数据 dump 出来
调试到 sub_1400093B0 获取了当前进程的路径
hFile = CreateFileW(&Filename, 0x80000000, 1u, 0i64, 3u, 0, 0i64);
并且读取了 filePath:signature 交换数据流
sub_140007DD0(&Buffer, v2, (__int64)v26); // md5
v10 = 0xFCu;
v11 = 0xAEu;
v12 = 0xEBu;
v13 = 0x6E;
v14 = 0x34;
v15 = 0xB4u;
v16 = 0x30;
v17 = 0x3E;
v18 = 0x99u;
v19 = 0xB9u;
v20 = 0x12;
v21 = 6;
v22 = 0xBDu;
v23 = 0x32;
v24 = 0x5F;
v25 = 0x2B;
并且经过 md5 运算然后比较
反查 FCAEEB6E34B4303E99B91206BD325F2B 得到 Overwatch
添加交换数据流信息
echo Overwatch > WinRev.exe:signature
还要注意在内存中把截断符加上，不然 md5 值不一样
Stack[00002EE4]:000000000014FC2B db 4Fh ; O
Stack[00002EE4]:000000000014FC2C db 76h ; v
Stack[00002EE4]:000000000014FC2D db 65h ; e
Stack[00002EE4]:000000000014FC2E db 72h ; r
Stack[00002EE4]:000000000014FC2F db 77h ; w
Stack[00002EE4]:000000000014FC30 db 61h ; a
Stack[00002EE4]:000000000014FC31 db 74h ; t
Stack[00002EE4]:000000000014FC32 db 63h ; c
Stack[00002EE4]:000000000014FC33 db 68h ; h
Stack[00002EE4]:000000000014FC34 db 0
最后一样也是会执行到解密函数 sub_140006C10
if ( (unsigned __int64)k >= 0x10 )
{
sub_140008300((__int64)&v9, 3i64, 1048578);
return sub_140006C10(qword_140016178, v9, 0i64);
}
之后程序就开启 sleep 了，应该还遗漏了什么，回头去检查发现
v6 = beginthreadex(0i64, 0, (unsigned int (__stdcall *)(void *))StartAddress, &ArgList, 0, 0i64);
这个函数启动了一个子线程，调试一下子线程看看它做了什么
在调试的过程中，要注意这里有个 TLS 回调函数
__int64 TlsCallback_0()
{
__int64 result; // rax
int i; // [rsp+20h] [rbp-18h]
int j; // [rsp+24h] [rbp-14h]
int k; // [rsp+28h] [rbp-10h]
int l; // [rsp+2Ch] [rbp-Ch]
for ( i = 0; (unsigned __int64)i < 0x1A; ++i )
ProcName[i] ^= byte_140015F20[6]; // NtQueryInformationProcess
for ( j = 0; (unsigned __int64)j < 0x19; ++j )
asc_140015EA8[j] ^= byte_140015F20[7]; // ZwQueryInformationThread
for ( k = 0; (unsigned __int64)k < 0x11; ++k )
asc_140015EC8[k] ^= byte_140015F20[8]; // NtQueueApcThread
for ( l = 0; ; ++l )
{
result = l;
if ( (unsigned __int64)l >= 0xA )
break;
byte_140015E78[l] ^= byte_140015F20[5]; // ntdll.dll
}
return result;
}
主要用来解密出三个函数的名字，由于这题开了多线程，TLS 回调函数会被多次执行。。我们在这里下个断点，让它只解密一次。。之后断到这里都直接修改 RIP 跳过
接着继续分析我们的子线程
v4 = Process32FirstW(hSnapshot, &pe);
if ( !v4 )
return 0i64;
while ( v4 )
{
memset(v9, 0, 0x21ui64);
memset(Str1, 0, 0x42ui64);
v1 = wcslen(pe.szExeFile);
sub_140007DD0(pe.szExeFile, v1, (__int64)v9);
for ( i = 0; i < 16; ++i )
sub_140008DF0((__int64)&Str1[2 * i], 3i64, (__int64)L"%02x", (unsigned __int8)v9[i]);
for ( j = 0; (unsigned __int64)j < 0x31; ++j )
{
if ( !wcscmp((const wchar_t *)Str1, &a438078d884693c[33 * j]) )
exit(-1);
}
v4 = Process32NextW(hSnapshot, &pe); // 列进程 判断进程 md5 是否有跟常量表中相同的 相同就退出
}
这里建了一个循环获取所有进程名的 md5 跟常量表的 md5 比较，相同就退出程序，猜测是反调试。F9 一运行程序果然停止了，应该是检测到了 IDA 的进程 (我用 IDA 调试的)
看到后面又运行了
if ( !byte_140016158 )
{
sub_140006C10(qword_140016178, v7, (__int64)&v5);
byte_140016158 = 1;
}
这里我直接修改 RIP 到 sub_140006C10，执行解密函数，到这里应该要开始考虑解密函数的调用顺序问题，应该是子线程先执行，接着是 Akira_aut0_ch3ss_! 密钥解密，最后是数据流密码的解密。
由于子线程还没执行完，我们继续跟踪下去
sub_140008500(qword_140016188);
这个函数传了一个全局变量，该全局变量指向 TLS 回调函数中解密出来的三个函数地址
NtQueryInformationProcess ZwQueryInformationThread NtQueueApcThread
单步进去发现各种反调试函数...
sub_140008D20(qword_140016188, *v1, (__int64)sub_140009850);
这里通过调用 NtQueueApcThread 将 sub_140009850 函数加入 APC 队列 (此处涉及 windows 内核理解不是很深，不到位的地方烦请大佬补充)
接下来进入了 sub_140009850
WaitForMultipleObjects(3u, Handles, 1, 5000u);
这里等待 5 秒，需要三个事件都处于激活状态才能往下执行。
到这里我选择重新调试，先暂停主线程，将子线程运行到 WaitForMultipleObjects 处，并暂停子线程，恢复主线程，再按照前面说的顺序把主线程的解密函数执行完，然后暂停主线程，恢复子线程，此时三个事件已经都激活了
往下调发现在校验文件头
if ( *v11 == 'M' && *((_BYTE *)v5 + 1) == 'Z' )
{
sub_140007D80((__int64)v5, v4, 0, (__int64)v8);
v10 = v0;
if ( v0 )
v2 = 0;
}
接着就可以单步进入 sub_140007D80 了
这个函数粗略看下做了一些拷贝的工作和释放内存的操作，我们把解密出来的 DLL 导出，然后再拖入 IDA 分析
if ( Src )
{
CloseHandle(hFileMappingObject);
Dst = malloc(0x8000ui64);
memset(Dst, 0, 0x8000ui64);
memcpy(Dst, Src, 0x8000ui64);
strcpy(&v7, "Ak1i3aS3cre7K3y");
memset(&Str1, 0, 0x11ui64);
sub_7FFFDA782800(&v7, &Str1, Dst);
if ( !strcmp(&Str1, &Str2) )
sub_7FFFDA7826F0("Get finally answer!\n");
else
sub_7FFFDA7826F0("wow... game start!\n");
result = 1;
}
sub_7FFFDA782800 函数往里走会发现 AES S盒代换表，因此猜测是 AES 加密，并且密钥是 Ak1i3aS3cre7K3y 按这个密钥来看应该是 128 bit 的长度
密文在子线程中
Src = 0x94u;
v16 = 0xBFu;
v17 = 0x7A;
v18 = 0xC;
v19 = 0xA4u;
v20 = 0x35;
v21 = 0x50;
v22 = 0xD1u;
v23 = 0xC2u;
v24 = 0x15;
v25 = 0xECu;
v26 = 0xEFu;
v27 = 0x9Du;
v28 = 0x9Au;
v29 = 0xAAu;
v30 = 0x56;
最后得到 flag{Ak1rAWin!}
[复制链接]
发表于 2019-10-18 00:01
发表于 2019-10-18 08:15
|
发表于 2019-10-18 00:04
厉害厉害
用在哪里的呢 
