n00bzCTF 2023 に 0nePadding で参加して 79 位 / 855 チームでした。
今回は軽めの参加でしたが、学びのあった問題をメモしておきます。
もくじ
MyPin(Rev)
I made a safe with a pin of only two digits.
問題バイナリとして与えられた jar ファイルを実行してみると、以下のようなアプリケーションが起動しました。
クラスの構成は以下の通りでした。
jar -tf My-pin.jar
>
META-INF/
META-INF/MANIFEST.MF
Mypin.class
PinButton.class
ResetButton.class
Secret.classjar ファイルをデコンパイルした結果を確認してみたところ、以下の処理を行っているアプリケーションであることがわかりました。
- ボタンを 1 回押す事に変数 cnt が 1 加算されて、最大で 9 回ボタンの操作ができる。
- ボタンが押されると “0” か “1” が Secret クラスの process 関数に与えられ、事前定義された mydata の配列の一部が更新される。
- Secret クラスの getData 関数は、 mydata 配列の情報を元に何らかの文字列を生成するロジックを持つ。
- 入力値として取りうるパターンは 2**9(=512) 個なので、その中のいずれかの入力で getData 関数の出力結果が Flag になる。
ここまで特定できたので、あとは Java プログラムを Python で書き起こしてブルートフォースすれば楽勝や！と思っていたのですが、残念ながらあらゆるデコンパイル方式を試して確認したものの、書き起こした Python スクリプトが元の Java プログラムと完全に同一の動作をすることはありませんでした。
参考：GitHub - skylot/jadx: Dex to Java decompiler
結局のところ、jar ファイル(もしくは class ファイル)は、ライブラリとして自作の Java プログラムから呼び出せることを利用して解くのが正攻法だったようです。
まず、以下のコマンドで jar ファイルを class ファイルに展開します。
jar xf My-pin.jarこれで Secret.class というファイルを入手できるので、問題バイナリの Secret クラスを再利用してブルートフォースで Flag を特定するために以下の Java プログラムを作成しました。
public class Solve {
public static void main(String[] args) {
// 2**9 = 512
for (int i = 0; i < 512; i++) {
String pin = String.format("%9s", Integer.toBinaryString(i)).replace(' ', '0');
Secret secret = Secret.getInstance();
secret.resetInstance();
for (char c : pin.toCharArray()) {
secret.process(c);
}
String data = secret.getData();
if(data.contains("n00bz")) {
System.out.println("PIN: " + pin + ", Flag: " + data);
}
}
}
}参考：n00bzCTF 2023 - MyPin :: Chocapikk’s blog
これを、Secret.class と同じディレクトリに Solve.java として配置し、以下のコマンドを実行することで Flag を特定できます。
javac Solve.java ; java Solve参考：Java import giving error - Stack Overflow
EZrev(Rev)
Rev is EZ! Author: NoobHacker
与えられた Class ファイルをデコンパイルすると以下のようなコードを取得できます。
/*
* Decompiled with CFR 0.150.
*/
import java.util.Arrays;
public class EZrev {
public static void main(String[] arrstring) {
int n;
if (arrstring.length != 1) {
System.out.println("L");
return;
}
String string = arrstring[0];
if (string.length() != 31) {
System.out.println("L");
return;
}
int[] arrn = string.chars().toArray();
for (n = 0; n < arrn.length; ++n) {
arrn[n] = n % 2 == 0 ? (int)((char)(arrn[n] ^ 0x13)) : (int)((char)(arrn[n] ^ 0x37));
}
for (n = 0; n < arrn.length / 2; ++n) {
if (n % 2 == 0) {
int n2 = arrn[n] - 10;
arrn[n] = (char)(arrn[arrn.length - 1 - n] + 20);
arrn[arrn.length - 1 - n] = (char)n2;
continue;
}
arrn[n] = (char)(arrn[n] + 30);
}
int[] arrn2 = new int[]{130, 37, 70, 115, 64, 106, 143, 34, 54, 134, 96, 98, 125, 98, 138, 104, 25, 3, 66, 78, 24, 69, 91, 80, 87, 67, 95, 8, 25, 22, 115};
if (Arrays.equals(arrn, arrn2)) {
System.out.println("W");
} else {
System.out.println("L");
}
}
}あとは、単純に逆算するコードを書けば Flag を特定できます。
arr2 = [130, 37, 70, 115, 64, 106, 143, 34, 54, 134, 96, 98, 125, 98, 138, 104, 25, 3, 66, 78, 24, 69, 91, 80, 87, 67, 95, 8, 25, 22, 115]
arr = arr2.copy()
for i in range(len(arr)//2):
if i % 2 == 0:
n2 = arr[i]
arr[i] = arr[len(arr)-1-i]
arr[len(arr)-1-i] = n2
print(arr)
for i in range(len(arr)//2):
if i % 2 != 0:
arr[i] = arr2[i] - 30
else:
arr[i] = arr2[len(arr)-1-i] + 10
arr[len(arr)-1-i] = arr2[i] - 20
for i in range(len(arr2)):
if i % 2 == 0:
arr[i] = arr[i] ^ 0x13
else:
arr[i] = arr[i] ^ 0x37
for a in arr:
print(chr(a), end="")zzz(Rev)
問題バイナリとして与えられた ELF ファイルを Ghidra でデコンパイルすると以下のような結果が得られました。
read 関数で fd=0 から 0x1e を読み取っているようですので、標準入力からデータを受け取って check 関数に流していることがわかります。
check 関数は以下のようなデコンパイル結果でした。
ぱっと見で angr 案件っぽいことがわかるので、以下のテンプレを試してみました。
(問題名が zzz なので、もしかしたら z3 で条件式を解くのが想定解かも？)
import angr
proj = angr.Project("chall", auto_load_libs=False)
init_state = proj.factory.entry_state(args = ['chall'])
simgr = proj.factory.simgr(init_state)
simgr.explore(find=(0x401654), avoid=([0x4016ca,0x4011a9]))
# 出力
simgr.found[0].posix.dumps(0)ただ、上記のテンプレだと上手く Flag を取得することができませんでした。
恐らく angr で制約の指定をしていないのが原因だと思います。
ちょっと細かい制約を入れて angr を回すやり方がよくわからなかったので、恐らく想定解通りの Z3Pyを使用することにしました。
Ghidra のデコンパイル結果を元に以下のような制約を追加した Solver を作成し、Flag を取得できました。
from z3 import *
flag = [BitVec(f"flag[{i}]", 8) for i in range(0x1e)]
s = Solver()
# 独自の制約を追加
s.add(flag[0] == ord("n"))
s.add(flag[1] == ord("0"))
s.add(flag[2] == ord("0"))
s.add(flag[3] == ord("b"))
s.add(flag[4] == ord("z"))
s.add(flag[5] == ord("{"))
s.add(flag[0x1e-1] == ord("}"))
for i in range(0x1e):
s.add(And(
(flag[i] >= 0x21),
(flag[i] <= 0x7e)
))
# 問題の制約
s.add(flag[0] >> 4 == 0x6)
s.add(flag[1] == flag[2])
s.add(And(
((flag[6] | flag[3]) == 0x7a),
((flag[6] & flag[3]) == 0x42)
))
s.add(flag[0x1c] == flag[4])
s.add(And(
(flag[0x1d] * flag[5] == 0x3c0f),
And(
(flag[8] + flag[6] + flag[7] == 0x12e),
(flag[7] * flag[6] - flag[8] == 0x2a8a)
)
))
s.add(And(
And(
(flag[9] - flag[8] == 5),
(flag[10] - flag[9] == 0x1b),
(flag[10] ^ flag[0xb] == 0x20)
),
And(
(flag[0xc] == flag[0xf]),
(flag[0xb] + flag[0xc] == 0xb4),
(flag[0xc] + flag[0xd] == 0xb9)
)
))
s.add(And(
(flag[0xd] + flag[0xe] - flag[0x10] == flag[0xd]),
And(
(flag[0x11] + flag[0x10] == 0xd9),
(flag[0x11] == flag[0xd])
),
And(flag[0xe] + flag[0x10] == flag[0xe] * 2)
))
s.add(And(
And(
(flag[0x12] == ord('Z')),
(flag[0x12] == flag[0x13]),
((flag[0x15] ^ flag[0x13] ^ flag[0x14]) == 0x7f)
),
((flag[0x14] ^ flag[0x15] ^ flag[0x16]) == flag[0x15]),
(flag[0x15] == ord('_')),
(flag[6] + flag[0x18] == 0xb4)
))
s.add(flag[0x18] + ~flag[0x17] == -0x21)
s.add(flag[0x19] == flag[9])
s.add(And(
(flag[0x1b] + flag[0x1a] == 0xd4),
(flag[0x1b] == flag[0x1c])
))
while s.check() == sat:
m = s.model()
for c in flag:
print(chr(m[c].as_long()),end="")
print("")
breakまとめ
今回はライト目の参加でした。
引き続き精進。