Diberikan sebuah binary 64 bit not stripped. Pseudocode dari fungsi main adalah sebagai berikut:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 |
int __cdecl main(int argc, const char **argv, const char **envp) { char v4; // [rsp+0h] [rbp-30h] _BYTE v5[3]; // [rsp+5h] [rbp-2Bh] _BYTE v6[6]; // [rsp+Ah] [rbp-26h] int v7; // [rsp+14h] [rbp-1Ch] char v8; // [rsp+19h] [rbp-17h] unsigned __int64 v9; // [rsp+28h] [rbp-8h] v9 = __readfsqword(0x28u); __isoc99_scanf("%5c-%5c-%5c-%5c-%5c", &v4, v5, v6, &v6[5], &v7); v8 = 0; if ( checker(&v4) ) unlock(); else printf("Invalid serial key"); return 0; } |
Dilihat program meminta input sepanjang 25 karakter dan kemudian input akan diproses oleh fungsi checker() dan bila hasil dari checker() adalah true maka fungsi unlock() akan dipanggil. Berikut pseudocode dari fungsi unlock():
|
1 2 3 4 5 6 7 8 9 10 |
int unlock() { char i; // al FILE *stream; // [rsp+8h] [rbp-8h] stream = fopen("flag.txt", "r"); for ( i = fgetc(stream); i != -1; i = fgetc(stream) ) putchar(i); return fclose(stream); } |
Fungsi tersebut akan membuka file flag.txt pada server nc.
Berikut pseudocode dari fungsi checker():
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 |
_BOOL8 __fastcall checker(char *a1) { if ( a1[20] - *a1 != 24 ) return 0LL; if ( a1[8] + a1[5] != 126 ) return 0LL; if ( a1[14] * a1[5] != 3696 ) return 0LL; if ( a1[21] - a1[1] != 33 ) return 0LL; if ( a1[10] - *a1 != 2 ) return 0LL; if ( a1[17] - *a1 != 19 ) return 0LL; if ( a1[17] * a1[1] != 3848 ) return 0LL; if ( a1[4] + a1[6] != 123 ) return 0LL; if ( a1[13] * a1[16] != 4488 ) return 0LL; if ( a1[1] * a1[6] != 2600 ) return 0LL; if ( a1[13] * a1[23] != 3536 ) return 0LL; if ( a1[8] - a1[5] != 14 ) return 0LL; if ( a1[15] + a1[5] != 123 ) return 0LL; if ( a1[20] - a1[17] != 5 ) return 0LL; if ( a1[17] + a1[16] != 140 ) return 0LL; if ( a1[16] + a1[14] != 132 ) return 0LL; if ( a1[3] * a1[6] != 4250 ) return 0LL; if ( a1[18] + a1[14] != 145 ) return 0LL; if ( 2 * a1[13] != 136 ) return 0LL; if ( a1[17] - a1[10] != 17 ) return 0LL; if ( a1[11] + a1[8] != 145 ) return 0LL; if ( a1[9] + a1[1] != 135 ) return 0LL; if ( a1[11] + a1[24] != 146 ) return 0LL; if ( a1[3] - a1[7] != 11 ) return 0LL; if ( *a1 - a1[2] != 2 ) return 0LL; if ( a1[11] - a1[13] != 7 ) return 0LL; if ( a1[3] + a1[4] != 158 ) return 0LL; if ( a1[3] - a1[16] != 19 ) return 0LL; if ( a1[4] - a1[14] != 7 ) return 0LL; if ( a1[12] * a1[1] != 4056 ) return 0LL; if ( a1[20] + a1[8] != 149 ) return 0LL; if ( a1[9] - a1[4] != 10 ) return 0LL; if ( a1[9] - a1[6] != 33 ) return 0LL; if ( a1[9] * a1[13] != 5644 ) return 0LL; if ( a1[16] + a1[5] != 122 ) return 0LL; if ( a1[16] - a1[10] != 9 ) return 0LL; if ( a1[17] + a1[24] != 145 ) return 0LL; if ( a1[20] - a1[13] != 11 ) return 0LL; if ( a1[18] * a1[11] != 5925 ) return 0LL; if ( a1[21] * a1[23] != 4420 ) return 0LL; if ( a1[22] * a1[7] != 5698 ) return 0LL; if ( a1[15] - a1[19] != 12 ) return 0LL; if ( a1[16] - a1[1] != 14 ) return 0LL; if ( a1[3] - a1[13] != 17 ) return 0LL; if ( a1[12] * a1[8] != 5460 ) return 0LL; if ( a1[21] * a1[13] != 5780 ) return 0LL; if ( a1[7] * a1[1] != 3848 ) return 0LL; if ( a1[22] + a1[6] != 127 ) return 0LL; if ( a1[13] + a1[5] == 124 ) return a1[24] + a1[1] == 123; return 0LL; } |
Dari pseudocode diatas, dilihat terdapat banyak hitungan untuk validasi huruf atau angka mana yang memenuhi syarat agar bisa dapat flag. Untuk menyelesaikan hitungan-hitungan ini, kita dapat menggunakan z3 solver. Dari sana, z3 akan mencari karakter apa saja yang memenuhi kriteria tersebut. Berikut script yang digunakan:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 |
from z3 import * # Validasi untuk karakter yang valid def is_valid(x): return Or( (x == ord('A')), (x == ord('B')), (x == ord('C')), (x == ord('D')), (x == ord('E')), (x == ord('F')), (x == ord('G')), (x == ord('H')), (x == ord('I')), (x == ord('J')), (x == ord('K')), (x == ord('L')), (x == ord('M')), (x == ord('N')), (x == ord('O')), (x == ord('P')), (x == ord('Q')), (x == ord('R')), (x == ord('S')), (x == ord('T')), (x == ord('U')), (x == ord('V')), (x == ord('W')), (x == ord('X')), (x == ord('Y')), (x == ord('Z')), (x == ord('0')), (x == ord('1')), (x == ord('2')), (x == ord('3')), (x == ord('4')), (x == ord('5')), (x == ord('6')), (x == ord('7')), (x == ord('8')), (x == ord('9')) ) s = Solver() vec = "" for i in range(25): vec += "k[{}] ".format(i) k = BitVecs(vec, 32) # Memasukkan semua constraint ke dalam z3 s.add(k[20] - k[0] == 24) s.add(k[8] + k[5] == 126) s.add(k[14] * k[5] == 3696) s.add(k[21] - k[1] == 33) s.add(k[10] - k[0] == 2) s.add(k[17] - k[0] == 19) s.add(k[17] * k[1] == 3848) s.add(k[4] + k[6] == 123) s.add(k[13] * k[16] == 4488) s.add(k[1] * k[6] == 2600) s.add(k[13] * k[23] == 3536) s.add(k[8] - k[5] == 14) s.add(k[15] + k[5] == 123) s.add(k[20] - k[17] == 5) s.add(k[17] + k[16] == 140) s.add(k[16] + k[14] == 132) s.add(k[3] * k[6] == 4250) s.add(k[18] + k[14] == 145) s.add(2 * k[13] == 136) s.add(k[17] - k[10] == 17) s.add(k[11] + k[8] == 145) s.add(k[9] + k[1] == 135) s.add(k[11] + k[24] == 146) s.add(k[3] - k[7] == 11) s.add(k[0] - k[2] == 2) s.add(k[11] - k[13] == 7) s.add(k[3] + k[4] == 158) s.add(k[3] - k[16] == 19) s.add(k[4] - k[14] == 7) s.add(k[12] * k[1] == 4056) s.add(k[20] + k[8] == 149) s.add(k[9] - k[4] == 10) s.add(k[9] - k[6] == 33) s.add(k[9] * k[13] == 5644) s.add(k[16] + k[5] == 122) s.add(k[16] - k[10] == 9) s.add(k[17] + k[24] == 145) s.add(k[20] - k[13] == 11) s.add(k[18] * k[11] == 5925) s.add(k[21] * k[23] == 4420) s.add(k[22] * k[7] == 5698) s.add(k[15] - k[19] == 12) s.add(k[16] - k[1] == 14) s.add(k[3] - k[13] == 17) s.add(k[12] * k[8] == 5460) s.add(k[21] * k[13] == 5780) s.add(k[7] * k[1] == 3848) s.add(k[22] + k[6] == 127) s.add(k[13] + k[5] == 124) s.add(k[24] + k[1] == 123) for i in range(25): s.add(is_valid(k[i])) while s.check() == sat: model = s.model() serial = "" nope = [] for i in k: if str(i) and model[i] is not None: serial += chr(int(str(model[i]))) nope.append(i != model[i]) s.add((nope[:-1])) print(serial) |
Berikut hasil dari eksekusi script:
Dari hasil yang didapat tinggal memisahkan per 5 karakter.
745UI-82JFS-9KNDB-CBJO7-OUM4G
Masukkan karakter ke nc server dan mendapatkan flag.