flag loader

TCPサーバの接続情報と、ELFファイル flag_loader が与えられた。

flag_loaderGhidraで逆コンパイルすると、以下の処理をしていることが読み取れた。

  1. 以下の3個の関数check1, check2, check3を順に実行する。
  2. この3個の関数の戻り値を32bitで乗算した結果を引数として sleep 関数を呼び出す。
  3. flag.txt の内容を出力する。

Information to connect to a TCP server and a ELF file flag_loader were given.

Decompiling flag_loader via Ghidra, I found it doing these processes:

  1. Execute following three functions check1, check2, check3 in this order.
  2. Call the function sleep with the 32-bit product of the return values of the three functions.
  3. Output the contents of the file flag.txt.

check_functions.c

以下のプログラムを用い、 各関数で die(); が呼ばれず、かつsleep関数に渡す積が小さくなるような入力をZ3で求め、 それをサーバに入力することで、flagが得られた。
ビットベクトルはそのまま比較すると符号付き整数とみなされるので、z3.BV2Int を用い、符号なし整数として比較するようにした。

I created this progran to obtain the input not to have the functions execute die(); and make the product to pass to the function sleep small via Z3.
Bit vectors are considered as signed when directly compared, so I used z3.BV2Int to have it compare them as unsigned integers.
I obtained the flag by entering the obtained data to the server.

solver.py

このプログラムは、以下のように用いる。

  1. 引数なしで実行し、check1関数に入力する文字列を求める。
  2. check1関数に渡した文字列と、check2関数で出力された数値を引数として実行し、check2関数に入力する数値を求める。
  3. check1関数に渡した文字列と、check2関数に入力した数値と、check3関数で出力された数値を引数として実行し、check3関数に入力する数値を求める。

The usage of this program is:

  1. Run with no arguments to obtain a string to enter to the function check1.
  2. Run with the string entered to the function check1 and the integer printed from the function check2 to obtain integers to enter to the function check2.
  3. Run with the string entered to the function check1, the integers entered to the function check2, and the integer printed from the function check3 to obtain integers to enter to the function check3.
実行例 An example of execution YUKI.N>solver.py sat ~+3<6 1866035072 2428932224 140795439 176647168 756433920 1610415176 1610675593 YUKI.N>solver.py "~+3<6" 42841 sat ~+3<6 3387238233 907771904 2485319530 2509601282 2539509760 2674387530 2676083786 YUKI.N>solver.py "~+3<6" 3387238233 907771904 37438 sat ~+3<6 3387238233 907771904 1327179816 3756883515 3855539323 3997909600 4242394368 YUKI.N>
DUCTF{y0u_sur3_kn0w_y0ur_int3gr4l_d4t4_typ3s!}

DownUnderCTF 2021