Ten wpis jest częścią cyklu “Od zera do bughuntera” – listę wszystkich postów znajdziesz tutaj.
Osobiście lubię “zwalać” pracę na mój procesor. Zwłaszcza nudne i powtarzalne czynności bo często w nich strzelam babole, które skutkują jeszcze większymi błędami na wyjściu. Fajnym dodatkiem do tego wszystkiego jest sensowna “klikalność” rozwiązania – sensowność rozumiem w ten sposób, że czynność mogę zautomatyzować za pomocą trzech kliklnięć a nie trzydziestu trzech.
Wszystkie wymienione wyżej warunki spełnia Ponce, czyli plugin do IDA’y pozwalający wyklikać sobie zadane zmienne symbolic execution / taint analysis i rozwiązać odpowiednio skonstruowane równanie. W moim mniemaniu jest to bardzo fajne narzędzie do wszelakich zadań CTF które dają się rozwiązać w prosty sposób a brakuje czasu aby to zrobić 🙂
W tym poście przedstawię rozwiązanie zadania rozgrzewkowego RE, z wrześniowego CTF Ekoparty za pomocą Ponce.
Od ogranizatorów otrzymujemy statycznie skompilowaną pod x64 binarkę ELF:
a@b:~/Desktop$ file warmup
warmup: ELF 64-bit LSB executable, x86-64, version 1 (GNU/Linux), statically linked, for GNU/Linux 2.6.32, BuildID[sha1]=b9e93849cf9889813b7f88f5b7a0609df69bbf48, stripped
Zadanie jest klasycznym problemem do rozwiązania za pomocą symbolic execution – poniżej długi listing zdekompilowanej funkcji:
signed __int64 sub_4009D8()
{
signed __int64 result; // rax@29
if ( unk_6CCD62 == aO[0] )
{
if ( unk_6CCD72 == a_[0] )
{
if ( unk_6CCD6D == aU[0] )
{
if ( unk_6CCD67 == aT[0] )
{
if ( unk_6CCD69 == a1[0] )
{
if ( unk_6CCD63 == asc_4A1725[0] )
{
if ( unk_6CCD6C == aJ[0] )
{
if ( unk_6CCD65 == aS_0[0] )
{
if ( unk_6CCD68 == asc_4A172B[0] )
{
if ( unk_6CCD64 == a1[0] )
{
if ( unk_6CCD6A == aS_0[0] )
{
if ( unk_6CCD6B == a_[0] )
{
if ( unk_6CCD66 == a_[0] )
{
if ( unk_6CCD7A == a_[0] )
{
if ( unk_6CCD6E == a5[0] )
{
if ( unk_6CCD6F == aT[0] )
{
if ( unk_6CCD70 == a_[0] )
{
if ( unk_6CCD71 == off_4A1731 )
{
if ( unk_6CCD61 == BYTE2(off_4A1731) )
{
if ( unk_6CCD73 == unk_4A1735 )
{
if ( unk_6CCD74 == off_4A1731 )
{
if ( unk_6CCD75 == unk_4A1737 )
{
if ( unk_6CCD76 == unk_4A1739 )
{
if ( unk_6CCD77 == a_[0] )
{
if ( unk_6CCD78 == aU[0] )
{
if ( unk_6CCD79 == off_4A173B )
{
if ( unk_6CCD60 == BYTE2(off_4A173B) )
{
if ( unk_6CCD7B == unk_4A173F )
{
sub_4101B0("valid!");
result = 1LL;
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
return result;
}
Naszym zadaniem jest zlokalizowanie bufora wejściowego i oznaczenie go jako symbolizowanej pamięci. Można to zrobić w prosty sposób, wpisując dowolną wartość i lokalizując ją w pamięci na początku wykonania funkcji sprawdzającej. W moim przypadku inputem będzie EKO{AAAAAAAAAAAAAAAAAAAAAAA}.
Znaleziony bufor rezyduje w pamięci pod adresem 0x06CCD60. Taki adres, wraz z rozmiarem bufora (26) wpisujemy w okienku dialogowym Ponce po wybraniu opcji “Symbolize Memory” (pomarańczowa strzałka, czerwona pokazuje log z Ponce):
Po wskazaniu Ponce co nas interesuje, przechodzimy do dalszego wykonania naszego zadania. Ponce zaznacza na grafie symbolizowane odwołania do pamięci na jasnozielono, wraz z komentarzem.
Ostatnim krokiem jest wyklikanie rozwiązania solvera SMT (i tak do ostatniego znaku flagi 😉 ). W moim wypadku klikam prawym przyciskiem myszy na warunek jaki musi być spełniony, aby przejść do interesującego mnie brancha (czerwona strzałka) i wybieram opcję: SMT -> Solve formula:
W okienku Output pojawią się rozwiązania zadanego równania (na screenie rozwiązanie dla literki “O” z flagi):
Klikając tak kilkanaście razy i składając literki do kupy, naszym oczom ukaże się rozwiązanie zadania: EKO{1s_th1s_ju5t_4_w4rm_up?}.