[D^3CTF 2024] Re
RandomVM
ptrace反调试，第一个绕，第二个绕
把算法抄出来，暴力
载入linux，通过ida64远程调试，这个程序开始srand了一下，确定了随机数，然后后面vmhandler全部都是用rand来决定控制流的，我还试了下，好像win下同seed产生的rand还不一样。。
第二个函数是vm了，进去后每个函数都有一个功能块和一个跳转块
只看功能块，跳转快不看，很快就能看到有syscall，通过查表，0x65是ptrace，刚开始没发现这个可能和反调试有关系，导致第三块数据一直都是0xff，搞了3个小时都不知道哪里错了，在暴力的时候甚至无解。。最后重新细心F8了一遍VM才发现这茬，整个过程好像有3次ptrace，经过测试，第一次把返回值从0xff改成0x0，过反调试，第二三次不要管，如果改会导致程序崩溃（好像是检测？）然后再把((val >> bits) | (val << (8 - bits) )) & 0xff这个函数抄出来，慢慢还原代码即可。
通过逆向工程把生成加密文本的过程用python模拟出来，然后暴力破解
Exp
ans = [0x9D,0x6B,0xA1,0x02,0xD7,0xED,0x40,0xF6,0x0E,0xAE,0x84,0x19]
import string
def fun(val, bits):
if bits >= 8:
return 0
return ((val >> bits) | (val << (8 - bits) )) & 0xff
def getAns(input):
context = [0 for i in range(13)]
MAGIC = [3, 5, 6, 7, 4, 4, 7, 7, 2, 4, 4, 7]
for i in range(12):
context[i] ^= input[i]
context[i+1] = input[i]
#print(i,[hex(j) for j in context ])
context[i+1] = fun(context[i+1], MAGIC[i])
if i != 1 and i != 2 and i != 5 and i != 7 and i != 8 and i != 9 and i != 10:
context[i+1] ^= MAGIC[i]
#print(i,[hex(j) for j in context ])
for i in range(1, 12):
context[i+1] ^= context[i]
return context[1:]
a = getAns(("m3owJumpVm1111111111111").encode())
print([hex(j) for j in a])
ab = 'abcdefghijklmnopqrstuvwxyz0123456789'
for i in range(0,256):
a = getAns(("m3owJumpVmvm"+chr(i)+ "11111111111111").encode())
if a[9]==ans[9]:
print([hex(eee) for eee in a])
print(i)
for i in ab:
for j in ab:
for k in ab:
for w in ab:
a = getAns(("m3ow"+i+j+k+w+ "111111111111").encode())
if a[0]==ans[0] and a[1]==ans[1] and a[2] == ans[2] and a[3]==ans[3]:
print([hex(eee) for eee in a])
print(i+j+k+w)注意，最底下的是开始手动爆破的，因为发现前三个字符会影响结果list的前几个，而不会扩散到后面，所以直接这么写了，然后找到m3ow后，看倒数第二个，从ascii 0-256手动遍历，然后就出来了。
补一下z3的exp
from z3 import *
ans = [0x9D,0x6B,0xA1,0x02,0xD7,0xED,0x40,0xF6,0x0E,0xAE,0x84,0x19]
sol = Solver()
def fun(v, b):
r = ((v >> b) | v << (8 - b)) & 0xff
print(r)
return r
v = [BitVec(f"v{i}", 8) for i in range(12)]
MAGIC = [3,5,6,7,4,4,7,7,2,4,4,7]
for i in range(12):
v[i] = fun(v[i], MAGIC[i])
if not i in [1,2,5,7,8,9,10]:
v[i] ^= MAGIC[i]
if i != 11:
v[i] ^= v[i+1]
for i in range(11):
v[i+1] ^= v[i]
for i in range(12):
sol.add(v[i] == ans[i])
print(sol.check())
m = sol.model()
result = [0] * 12
for p in m.decls():
# print(chr(m[v[i]].as_long()),end='')
result[int((p.name()[1:]))] = m[p].as_long()
print(list(map(chr, result)))
print("".join(map(chr, result)))
# m3owJumpVmvMezJunk
如下是Exp,table是过了反调试的Table，如果没有反调试，程序会在TLS中修改为错误的表，从而无法正确解密。
sub_401917是魔改TEA的加密函数，sub_401917_d是魔改TEA的解密函数。
hashxx是在fakeflag之后的验证
0000000000401786 | C745 A0 A9B3DDB6 | mov dword ptr ss:[rbp-60],B6DDB3A9 | !
000000000040178D | C745 A4 232C1636 | mov dword ptr ss:[rbp-5C],36162C23 |
0000000000401794 | C745 A8 BFFA8918 | mov dword ptr ss:[rbp-58],1889FABF |
000000000040179B | C745 AC 3BE7E46C | mov dword ptr ss:[rbp-54],6CE4E73B |
00000000004017A2 | C745 B0 FCF85A0A | mov dword ptr ss:[rbp-50],A5AF8FC |
00000000004017A9 | C745 B4 1584FF21 | mov dword ptr ss:[rbp-4C],21FF8415 |
00000000004017B0 | C745 B8 57958544 | mov dword ptr ss:[rbp-48],44859557 |
00000000004017B7 | C745 BC B727C22D | mov dword ptr ss:[rbp-44],2DC227B7 |
00000000004017BE | C745 EC 00000000 | mov dword ptr ss:[rbp-14],0 |
如上，是hash后的对应表，如下程序通过暴力破解了hash。#include <iostream>
#include <vector>
#include <Windows.h>
using namespace std;
unsigned int table[] = { 21588,17922,17527,24158,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70,68,94,51,67,84,70 };
//unsigned int table[] = {21520, 17990, 17476, 24173, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70, 68, 94, 51, 67, 84, 70};
void __fastcall sub_401917(unsigned int* src, unsigned int sum, int offset)
{
unsigned int v6;
unsigned int v7;
v7 = *src;
v6 = src[1];
for (int i = 0; i <= 31; ++i)
{
v7 += (v6 + ((16 * v6) ^ (v6 >> 5))) ^ (table[sum & 3] + sum) ^ 0x44;
v6 += (v7 + ((32 * v7) ^ (v7 >> 6))) ^ (table[(sum >> 11) & 3] + sum) ^ 0x33;
sum -= offset;
}
src[0] = v7;
src[1] = v6;
}
void __fastcall sub_401917_d(unsigned int* src, unsigned int sum, int offset)
{
unsigned int v6;
unsigned int v7;
v7 = *src;
v6 = src[1];
sum -= 32 * offset;
for (int i = 0; i <= 31; ++i)
{
sum += offset;
v6 -= (v7 + ((32 * v7) ^ (v7 >> 6))) ^ (table[(sum >> 11) & 3] + sum) ^ 0x33;
v7 -= (v6 + ((16 * v6) ^ (v6 >> 5))) ^ (table[sum & 3] + sum) ^ 0x44;
}
src[0] = v7;
src[1] = v6;
}
int hashxx(int src)
{
for (int i = 0; i < 32; i++)
{
if (src < 0)
{
src *= 2;
src ^= 0x84A6972F;
}
else
{
src *= 2;
}
}
return src;
}
int main()
{
// 0xDD243DAB 0x898587D8
//cout << hashxx() << endl;
DWORD flag[] = {
0xB6DDB3A9, 0x36162C23, 0x1889FABF, 0x6CE4E73B, 0x0A5AF8FC, 0x21FF8415, 0x44859557, 0x2DC227B7
};
/*
for (size_t i = 0; i <= 0xffffffff; i++)
{
if (hashxx((int)i) == 0x0A5AF8FC)
{
cout << 3 << "|" << hex << i << endl;
break;
}
}
for (size_t i = 0; i <= 0xffffffff; i++)
{
if (hashxx((int)i) == 0x21FF8415)
{
cout << 4<< "|" << hex << i << endl;
break;
}
}
for (size_t i = 0; i <= 0xffffffff; i++)
{
if (hashxx((int)i) == 0x44859557)
{
cout <<5 << "|" << hex << i << endl;
break;
}
}
for (size_t i = 0; i <= 0xffffffff; i++)
{
if (hashxx((int)i) == 0x2DC227B7)
{
cout << 6 << "|" << hex << i << endl;
break;
}
}
*/
DWORD ffff[] =
{
0xDD243DAB,0x898587D8, 0x2fdf1d,0xbc4aca2, 0x4d68a16a, 0x616c5d29, 0x5b911af5, 0x4c7710dc
};
//char flag[] = { 0xB1,0xCB,0x06,0x54,0xA2,0x1E,0xA4,0xA4,0xC5,0x9A,0x48,0x34,0x97,0x87,0xD6,0x53,0x6F,0xC0,0xE0,0xB8,0xDB,0xF2,0x59,0x02,0x82,0x8D,0xE3,0x52,0x1D,0x5E,0x5D,0x59 };
char* v = (char*)malloc(114);
hashxx(0x0F9FC445);
strcpy_s(v, 114,"11111111111111111111111111111111111111111111111111111111111111111");
sub_401917((unsigned int*)v, 0xE8017300, 0xFF58F981);
sub_401917((unsigned int*)v + 2, 0xE8017300, 0xFF58F981);
sub_401917((unsigned int*)v + 4, 0xE8017300, 0xFF58F981);
sub_401917((unsigned int*)v + 6, 0xE8017300, 0xFF58F981);
sub_401917_d((unsigned int*)ffff, 0xE8017300, 0xFF58F981);
sub_401917_d((unsigned int*)ffff +2, 0xE8017300, 0xFF58F981);
sub_401917_d((unsigned int*)ffff +4, 0xE8017300, 0xFF58F981);
sub_401917_d((unsigned int*)ffff +6, 0xE8017300, 0xFF58F981);
}补一下z3 exp
from z3 import *
keys = [0xB6DDB3A9, 0x36162C23, 0x1889FABF, 0x6CE4E73B, 0x0A5AF8FC, 0x21FF8415, 0x44859557, 0x2dc227B7]
x = [BitVec(f"x{i}", 32) for i in range(len(keys))]
def hash(v):
for i in range(32):
v = If(v < 0 , (v << 1) ^ 0x84A6972F, v << 1)
return v
s = Solver()
for i in range(len(keys)):
s.add(hash(x[i]) == keys[i])
s.check()
m = s.model()
result = [0] * len(keys)
for p in m.decls():
result[int(p.name()[1:])] = m[p].as_long()
print([hex(i) for i in result])
