2017 Dimi CTF Prequal WhatIsTheEnd
메인을 보면 33글자를 입력받을 받는다. 그리고 어떠한 연산을 하고 맞는지 비교해준다.
int __cdecl main(int a1)
{
int v2; // [esp-Ah] [ebp-70h]
int v3; // [esp-6h] [ebp-6Ch]
int v4; // [esp-2h] [ebp-68h]
char v5; // [esp+1h] [ebp-65h]
signed int i; // [esp+2h] [ebp-64h]
signed int j; // [esp+2h] [ebp-64h]
char v8; // [esp+6h] [ebp-60h]
char v9; // [esp+7h] [ebp-5Fh]
char v10; // [esp+8h] [ebp-5Eh]
char v11; // [esp+9h] [ebp-5Dh]
char v12; // [esp+Ah] [ebp-5Ch]
char v13; // [esp+Bh] [ebp-5Bh]
char v14; // [esp+Ch] [ebp-5Ah]
char v15; // [esp+Dh] [ebp-59h]
char v16; // [esp+Eh] [ebp-58h]
char v17; // [esp+Fh] [ebp-57h]
char v18; // [esp+10h] [ebp-56h]
char v19; // [esp+11h] [ebp-55h]
char v20; // [esp+12h] [ebp-54h]
char v21; // [esp+13h] [ebp-53h]
char v22; // [esp+14h] [ebp-52h]
char v23; // [esp+15h] [ebp-51h]
char v24; // [esp+16h] [ebp-50h]
char v25; // [esp+17h] [ebp-4Fh]
char v26; // [esp+18h] [ebp-4Eh]
char v27; // [esp+19h] [ebp-4Dh]
char v28; // [esp+1Ah] [ebp-4Ch]
char v29; // [esp+1Bh] [ebp-4Bh]
char v30; // [esp+1Ch] [ebp-4Ah]
char v31; // [esp+1Dh] [ebp-49h]
char v32; // [esp+1Eh] [ebp-48h]
char v33; // [esp+1Fh] [ebp-47h]
char v34; // [esp+20h] [ebp-46h]
char v35; // [esp+21h] [ebp-45h]
char v36; // [esp+22h] [ebp-44h]
char v37; // [esp+23h] [ebp-43h]
char v38; // [esp+24h] [ebp-42h]
char v39; // [esp+25h] [ebp-41h]
__int16 v40; // [esp+26h] [ebp-40h]
int v41; // [esp+28h] [ebp-3Eh]
__int16 v42; // [esp+2Ch] [ebp-3Ah]
int v43; // [esp+2Eh] [ebp-38h]
int v44; // [esp+32h] [ebp-34h]
int v45; // [esp+36h] [ebp-30h]
int v46; // [esp+3Ah] [ebp-2Ch]
int v47; // [esp+3Eh] [ebp-28h]
int v48; // [esp+42h] [ebp-24h]
int v49; // [esp+46h] [ebp-20h]
unsigned int v50; // [esp+4Ah] [ebp-1Ch]
int v51; // [esp+4Eh] [ebp-18h]
int v52; // [esp+52h] [ebp-14h]
int v53; // [esp+56h] [ebp-10h]
int *v54; // [esp+5Ah] [ebp-Ch]
v54 = &a1;
v50 = __readgsdword(0x14u);
v40 = 0;
v8 = 172;
v9 = 171;
v10 = 30;
v11 = 44;
v12 = 166;
v13 = 161;
v14 = 156;
v15 = 232;
v16 = 255;
v17 = 97;
v18 = 9;
v19 = 83;
v20 = 37;
v21 = 20;
v22 = 130;
v23 = 60;
v24 = 165;
v25 = 145;
v26 = 165;
v27 = 219;
v28 = 233;
v29 = 4;
v30 = 96;
v31 = 224;
v32 = 26;
v33 = 110;
v34 = 97;
v35 = 65;
v36 = 183;
v37 = 79;
v38 = 83;
v39 = 205;
LOBYTE(v40) = 27;
v41 = 0;
v49 = 0;
memset((&v42 & 0xFFFFFFFC), 0, 4 * (((&v41 - (&v42 & 0xFFFFFFFC) + 34) & 0xFFFFFFFC) >> 2));
printf("INPUT: ");
__isoc99_scanf(
"%33s",
&v41,
v2,
v3,
v4,
0,
*&v8,
*&v12,
*&v16,
*&v20,
*&v24,
*&v28,
*&v32,
*&v36,
*&v40,
*(&v41 + 2),
v43,
v44,
v45,
v46,
v47,
v48,
v49);
v53 = 0;
v52 = 1;
v51 = 0;
v5 = ptrace(0, 0, 1, 0);
for ( i = 0; i <= 32; ++i )
*(&v41 + i) ^= v5 ^ rand();
for ( j = 0; j <= 32; ++j )
{
if ( (*(&v8 + j) ^ *(&v41 + j)) != *(&v41 + j + 1) )
{
puts("Nope!");
return -1;
}
}
puts("Correct!");
return 0;
}
여기서는 v8[i] ^ input[i] ^ rand[i] == input[i+1] ^ rand[i+1] 이러한 연산을 하고 있는데 우선 v8은 고정 값이고 rand()는 시드 값이 없으니까 그냥 긁어오면 된다.
ptrace는 디버깅중이 아니니까 0을 리턴하니까 xor연산해도 같은 값이 나오니까 무시해도 된다. 디버깅 중이면 -1을 리턴한다.
나는 라이브러리를 불러와서 rand값을 다 구하고 z3 이용해서 풀었다.
from ctypes import CDLL
from z3 import *
libc = CDLL('/lib/x86_64-linux-gnu/libc.so.6')
rand_table = []
table = [172,171,30,44,166,161,156,232,255,97,9,83,37,20,130,60,165,145,165,219,233,4,96,224,26,110,97,65,183,79,83,205,27]
for i in range(33):
rand_table.append(libc.rand()%256)
s = Solver()
a1 = [BitVec('a%i'%i,8)for i in range(33)]
s.add(a1[0] == ord('d'))
s.add(a1[1] == ord('i'))
s.add(a1[2] == ord('m'))
s.add(a1[3] == ord('i'))
for i in range(32):
s.add(table[i] ^ a1[i] ^ rand_table[i] == a1[i+1] ^ rand_table[i+1])
print s.check()
m = s.model()
print ''.join(chr(int(str((m.evaluate(a1[i]))))) for i in range(33))
FLAG : dimigo{Always_String_END_is_NULL}