[日本語] [English]

flag loader

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

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

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

check_functions.c

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

solver.py

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

  1. 引数なしで実行し、check1関数に入力する文字列を求める。
  2. check1関数に渡した文字列と、check2関数で出力された数値を引数として実行し、check2関数に入力する数値を求める。
  3. check1関数に渡した文字列と、check2関数に入力した数値と、check3関数で出力された数値を引数として実行し、check3関数に入力する数値を求める。
実行例
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!}

writeup by MikeCAT

DownUnderCTF 2021