WaniCTF 2024 : gates - Githubissues

https://github.com/wani-hackase/wanictf2024-writeup/tree/main/rev/gates

本番で解けた問題だが、めちゃくちゃな方法で解いたので復習する

フラグ入力型の問題

$ ./gates
testtesttesttesttesttesttesttest
Wrong!

めちゃくちゃな方法も一応残しておく

IDAとGhidraでどういう処理がされているかはなんとなく読み取った 32文字の入力を受け取り、何かしらの変換をした後に、1文字ずつ検証していそうだと思ったしかし、肝心の変換処理が読めなかったので、gdbスクリプトで、各位置毎にどの文字にしたら求めることにした検証処理の手前にbreakpointを設定するために、ベースアドレスが知りたいシンボル情報がstripされていて、b mainと出来ないので、一度実行した後に、__libc_start_main関数にbreakpointを設定し、rdiレジスタを確認することで、main関数のアドレスを取得し、ベースアドレスを求めている

以下のプログラムをsolve.pyとして保存し、gdb gates -x solve.pyを実行する

import gdb

characters = '0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_-.$@!?\{\}'
flag = [''] * 32

for c in characters:
    with open('input.txt', 'w') as f:
        tmp_flag = flag[:]

        for i in range(32):
            if tmp_flag[i] == '':
                tmp_flag[i] = c

        f.write(''.join(tmp_flag))

    gdb.execute('r < input.txt')
    gdb.execute('b __libc_start_main')
    gdb.execute('r')
    main_addr = gdb.parse_and_eval('$rdi')
    base = main_addr - 0x1080
    gdb.execute('b *' + hex(base + 0x10FD))
    gdb.execute('c')

    rax = gdb.parse_and_eval('$rax')
    rdx = gdb.parse_and_eval('$rdx')

    for i in range(32):
        if flag[i] == '':
            x = gdb.execute('x/1bx ' + hex(rax + 0x10 * i), to_string=True).split(':')[1]
            y = gdb.execute('x/1bx ' + hex(rdx + i), to_string=True).split(':')[1]

            if x == y:
                flag[i] = c
                break

print(flag)

変換処理が位置毎に独立なら、これで良いのだが、独立でない場合は上手くいかない実際に出力は、['F', 'L', 'A', 'G', '{', 'I', 'N', 'T', 'r', '0', 'd', 'U', 'c', 't', 'i', 'o', 'n', '_', '7', '', '', 'R', '3', 'v', '', '', '$', '1', '', '', '', '}']となり、''となっている箇所が一部存在する

しかし、プログラム中のflagを更新して、再度実行すると、全ての位置で文字が求まった

import gdb

characters = '0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_-.$@!?\{\}'
flag = ['F', 'L', 'A', 'G', '{', 'I', 'N', 'T', 'r', '0', 'd', 'U', 'c', 't', 'i', 'o', 'n', '_', '7', '', '', 'R', '3', 'v', '', '', '$', '1', '', '', '', '}']

for c in characters:
    with open('input.txt', 'w') as f:
        tmp_flag = flag[:]

        for i in range(32):
            if tmp_flag[i] == '':
                tmp_flag[i] = c

        f.write(''.join(tmp_flag))

    gdb.execute('r < input.txt')
    gdb.execute('b __libc_start_main')
    gdb.execute('r')
    main_addr = gdb.parse_and_eval('$rdi')
    base = main_addr - 0x1080
    gdb.execute('b *' + hex(base + 0x10FD))
    gdb.execute('c')

    rax = gdb.parse_and_eval('$rax')
    rdx = gdb.parse_and_eval('$rdx')

    for i in range(32):
        if flag[i] == '':
            x = gdb.execute('x/1bx ' + hex(rax + 0x10 * i), to_string=True).split(':')[1]
            y = gdb.execute('x/1bx ' + hex(rdx + i), to_string=True).split(':')[1]

            if x == y:
                flag[i] = c
                break

print(flag)

出力は、['F', 'L', 'A', 'G', '{', 'I', 'N', 'T', 'r', '0', 'd', 'U', 'c', 't', 'i', 'o', 'n', '_', '7', '0', '_', 'R', '3', 'v', '3', 'R', '$', '1', 'N', 'G', '1', '}']となったよくこの方法で解けたなと思う

解説には

解いた人はたぶんみんな angr 使ってる気がするが、ここでは詳しく説明しない。（ただし今回みたいにポンコツ出題者がちゃんと angr で解けるかどうかを確認しないとき解けたりするので、使い方がわからない人は勉強したほうがいい。）

とあるので、まずはangrを使ったやり方から試す

angrの使い方から勉強

「詳解セキュリティコンテスト」によると、 angrでは、シンボリック実行というものを行うシンボリック実行というのは、メモリやレジスタの一部分を具体的な値として持つのではなく、シンボルという状態として扱い、プログラムが特定の箇所に到達するための条件を導出する導出にはSATソルバを使う

簡単なプログラムで試す

#include <stdio.h>

int check(int x) {
    return x*x*x - 30*x*x + 275*x - 750 == 0;
}

int main() {
    int x;
    scanf("%d", &x);
    if (check(x)) {
        puts("Correct!");
    } else {
        puts("Wrong...");
    }
}

angrを使って、Correct!が表示されるような入力を求める x^3-30x^2+275x-750 = (x-5)(x-10)(x-15) なので、5, 10, 15が出てきてほしい

以下のようなプログラムを書いた

import angr
import claripy

p = angr.Project('./main', load_options={'auto_load_libs': False})
x = claripy.BVS('x', 8 * 2)
state = p.factory.entry_state(stdin=x)
simgr = p.factory.simulation_manager(state)
simgr.explore(find=0x4011c3, avoid=0x4011d4)

try:
    e = simgr.found[0].solver.eval(x, cast_to=bytes)
    print(e)
except IndexError:
    print('Not found')

x = claripy.BVS('x', 8 * 2)
- BVSはBit Vector Symbolの略
- 第一引数の使われ方は不明(適当な文字列でも動く)
- 第二引数はシンボルのビット数を表す
- 今回シンボルとしているのは標準入力で、例えば標準入力が 1なら8ビット、12なら16ビット、12aなら24ビットである
- 標準入力で5, 10, 15を与える場合にCorrect!が表示されるが、5は05でも良いし、5aでも良い
- なので、今回のビット数は16ビットとした
- もし、方程式の解に3桁の数が含まれる場合、16ビットだと解を見つけることが出来ない

simgr.explore(find=0x4011c3, avoid=0x4011d4)

findに到達したいアドレス、avoidに到達してはいけないアドレスを指定する
findさえ指定すれば、avoidは無くても良いのでは？という気になるが、avoidを指定すると実行が速くなったりするんだろうか

アドレスはobjdumpなどで調べる

0000000000001188 <main>:
1188: 55                      push   rbp
1189: 48 89 e5                mov    rbp,rsp
118c: 48 83 ec 10             sub    rsp,0x10
1190: 48 8d 45 fc             lea    rax,[rbp-0x4]
1194: 48 89 c6                mov    rsi,rax
1197: 48 8d 05 66 0e 00 00    lea    rax,[rip+0xe66]        # 2004 <_IO_stdin_used+0x4>
119e: 48 89 c7                mov    rdi,rax
11a1: b8 00 00 00 00          mov    eax,0x0
11a6: e8 95 fe ff ff          call   1040 <__isoc99_scanf@plt>
11ab: 8b 45 fc                mov    eax,DWORD PTR [rbp-0x4]
11ae: 89 c7                   mov    edi,eax
11b0: e8 94 ff ff ff          call   1149 <check>
11b5: 85 c0                   test   eax,eax
11b7: 74 11                   je     11ca <main+0x42>
11b9: 48 8d 05 47 0e 00 00    lea    rax,[rip+0xe47]        # 2007 <_IO_stdin_used+0x7>
11c0: 48 89 c7                mov    rdi,rax
11c3: e8 68 fe ff ff          call   1030 <puts@plt>
11c8: eb 0f                   jmp    11d9 <main+0x51>
11ca: 48 8d 05 3f 0e 00 00    lea    rax,[rip+0xe3f]        # 2010 <_IO_stdin_used+0x10>
11d1: 48 89 c7                mov    rdi,rax
11d4: e8 57 fe ff ff          call   1030 <puts@plt>
11d9: b8 00 00 00 00          mov    eax,0x0
11de: c9                      leave
11df: c3                      ret

Correct!を出力するためのputs関数の呼び出しが0x11c3で、Wrong...を出力するためのputs関数の呼び出しが0x11d4である
https://ptr-yudai.hatenablog.com/entry/2019/08/17/223044

PIEが有効なとき、angrは標準で0x400000をベースアドレスとします。
なので、0x11c3, 0x11d4に0x400000を足して、find, avoidを指定する
objdumpで得られるアドレスをそのまま使いたいのであれば、ベースアドレスが0になるようにする
```
import angr
import claripy
```

p = angr.Project('./main', load_options={'auto_load_libs': False}, main_opts={'base_addr': 0}) x = claripy.BVS('x', 8 * 2) state = p.factory.entry_state(stdin=x) simgr = p.factory.simulation_manager(state) simgr.explore(find=0x11c3, avoid=0x11d4)

try: e = simgr.found[0].solver.eval(x, cast_to=bytes) print(e) except IndexError: print('Not found')

実行する

$ python solve.py
WARNING  | 2024-07-04 01:24:34,842 | angr.simos.simos | stdin is constrained to 2 bytes (has_end=True). If you are only providing the first 2 bytes instead of the entire stdin, please use stdin=SimFileStream(name='stdin', content=your_first_n_bytes, has_end=False).
b'05'

WARNINGの内容は分からない無視して良いやつだろう出力はb'05'となっている実際、05を入力すると、Correct!と表示される

$ ./main
05
Correct!

simgr.foundの長さは1だったつまり、05以外の答えは出てきてない方程式の解は5の他に10と15もあったが、これらを求めるためには、シンボルに制約を追加して、解を求めればよい https://docs.angr.io/en/latest/core-concepts/solver.html#constraint-solving

import angr
import claripy

p = angr.Project('./main', load_options={'auto_load_libs': False})
x = claripy.BVS('x', 8 * 2)
state = p.factory.entry_state(stdin=x)

while True:
    simgr = p.factory.simulation_manager(state)
    simgr.explore(find=0x4011c3, avoid=0x4011d4)

    try:
        e = simgr.found[0].solver.eval(x, cast_to=bytes)
        print(e)
        state.solver.add(x != e)
    except IndexError:
        print('Not found')
        break

これを実行すると、10と15も出てくる 5の後に数字以外が来るのは何でも良いので、そのパターンが全部出てくる

$ python solve.py
WARNING  | 2024-07-04 01:32:45,877 | angr.simos.simos | stdin is constrained to 2 bytes (has_end=True). If you are only providing the first 2 bytes instead of the entire stdin, please use stdin=SimFileStream(name='stdin', content=your_first_n_bytes, has_end=False).
b'05'
b'5\xf0'
b'10'
b'5\xa1'
b'+5'
b'15'
b'5\xba'
b'5\xbc'
b'5t'
b'5\x00'
b'5A'
b'5('
b'5\x8a'
b'5\x10'
b'5\x8c'
...

今回の問題を解くならこうなるだろう

import angr
import claripy

p = angr.Project('./gates', load_options={'auto_load_libs': False})
flag = claripy.BVS('flag', 8 * 32)
state = p.factory.entry_state(stdin=flag)
simgr = p.factory.simulation_manager(state)
simgr.explore(find=0x40111d, avoid=0x401105)

try:
    e = simgr.found[0].solver.eval(flag, cast_to=bytes)
    print(e)
except IndexError:
    print('Not found')

が、discordに載せられているプログラムは

import angr, claripy
import sys, logging

logging.getLogger("angr").setLevel(logging.INFO)
project = angr.Project(
    "./gates", main_opts={"base_addr": 0x00100000}, auto_load_libs=False
)
flag = claripy.BVS("flag", 0x20 * 8)
initial_state = project.factory.full_init_state(
    stdin=flag, add_options=angr.options.unicorn
)
simulation = project.factory.simgr(initial_state)

simulation.explore(
    find=lambda state: b"Correct!" in state.posix.dumps(sys.stdout.fileno()),
    avoid=lambda state: b"Wrong!" in state.posix.dumps(sys.stdout.fileno()),
)
if simulation.found:
    print(simulation.found[0].posix.dumps(sys.stdin.fileno()))

とか

import angr, claripy
p = angr.Project("./gates", main_opts={"base_addr": 0x100000}, auto_load_libs=False)

s = p.factory.entry_state(addr=0x1010bc)

vs = [claripy.BVS(f"chr{x}", 8) for x in range(32)]

for i, v in enumerate(vs):
    s.memory.store(0x10404c + (i * 0x10), 1, 1)
    s.memory.store(0x10404c + 1 + (i * 0x10), v, 1)

sm = p.factory.simgr(s, veritesting=True)
results = sm.explore(find=lambda s: b"Correct" in s.posix.dumps(1), avoid=lambda s: b"Wrong" in s.posix.dumps(1))

何をしているのか分からない... とりあえず、自分で書いたプログラムを動かしてみる 20分経っても終わらなかったら諦めよう

23分実行して出てきた angr凄いな

$ python solve_angr.py
WARNING  | 2024-07-04 01:55:37,451 | angr.simos.simos | stdin is constrained to 32 bytes (has_end=True). If you are only providing the first 32 bytes instead of the entire stdin, please use stdin=SimFileStream(name='stdin', content=your_first_n_bytes, has_end=False).
b'FLAG{INTr0dUction_70_R3v3R$1NG1}'

Ghidraのdecompile結果

undefined8 FUN_00101080(void)

{
  int iVar1;
  char *pcVar2;
  char *pcVar3;
  undefined1 *puVar4;
  undefined1 *puVar5;

  puVar4 = &DAT_0010404c;
  do {
    puVar5 = puVar4 + 0x10;
    iVar1 = getc(stdin);
    *puVar4 = 1;
    puVar4[1] = (char)iVar1;
    puVar4 = puVar5;
  } while (puVar5 != &DAT_0010424c);
  iVar1 = 0x100;
  do {
    FUN_00101220();
    iVar1 = iVar1 + -1;
  } while (iVar1 != 0);
  pcVar2 = &DAT_00104e4d;
  pcVar3 = &DAT_00104020;
  do {
    if (*pcVar2 != *pcVar3) {
      puts("Wrong!");
      return 1;
    }
    pcVar2 = pcVar2 + 0x10;
    pcVar3 = pcVar3 + 1;
  } while (pcVar2 != &DAT_0010504d);
  puts("Correct!");
  return 0;
}

void FUN_00101220(void)

{
  char cVar1;
  byte bVar2;
  char cVar3;
  undefined uVar4;
  byte bVar5;
  int iVar6;
  undefined8 *puVar7;
  long lVar8;

  puVar7 = (undefined8 *)&DAT_00104040;
  do {
    iVar6 = *(int *)puVar7;
    if (iVar6 == 3) {
      lVar8 = (long)*(int *)((long)puVar7 + 4) * 0x10;
      if (((&DAT_0010404c)[lVar8] != '\0') &&
         ((&DAT_0010404c)[(long)*(int *)(puVar7 + 1) * 0x10] != '\0')) {
        bVar5 = (&DAT_0010404d)[lVar8];
        bVar2 = (&DAT_0010404d)[(long)*(int *)(puVar7 + 1) * 0x10];
        *(undefined *)((long)puVar7 + 0xc) = 1;
        *(byte *)((long)puVar7 + 0xd) = bVar5 ^ bVar2;
      }
    }
    else if (iVar6 < 4) {
      if ((((iVar6 == 1) || (iVar6 == 2)) &&
          (lVar8 = (long)*(int *)((long)puVar7 + 4) * 0x10, (&DAT_0010404c)[lVar8] != '\0')) &&
         ((&DAT_0010404c)[(long)*(int *)(puVar7 + 1) * 0x10] != '\0')) {
        cVar3 = (&DAT_0010404d)[(long)*(int *)(puVar7 + 1) * 0x10];
        cVar1 = (&DAT_0010404d)[lVar8];
        *(undefined *)((long)puVar7 + 0xc) = 1;
        *(char *)((long)puVar7 + 0xd) = cVar3 + cVar1;
      }
    }
    else if ((iVar6 == 4) &&
            (lVar8 = (long)*(int *)((long)puVar7 + 4) * 0x10, (&DAT_0010404c)[lVar8] != '\0')) {
      uVar4 = (&DAT_0010404d)[lVar8];
      *(undefined *)((long)puVar7 + 0xc) = 1;
      *(undefined *)((long)puVar7 + 0xd) = uVar4;
    }
    puVar7 = puVar7 + 2;
  } while (puVar7 != &stdin);
  return;
}

IDAと見比べながら読み進める

puVar4 = &DAT_0010404c;
do {
  puVar5 = puVar4 + 0x10;
  iVar1 = getc(stdin);
  *puVar4 = 1;
  puVar4[1] = (char)iVar1;
  puVar4 = puVar5;
} while (puVar5 != &DAT_0010424c);

&DAT_0010404cは、IDAでは0x404cになっている

Ghidraでも、Imagebase Offsetというものは0x404cになっている

じゃあ&DAT_0010404cの10404cとは？

処理内容は、 0x404cに1を格納、0x404dに入力文字を格納 0x405cに1を格納、0x405dに入力文字を格納 ... 0x424cに1を格納、0x424dに入力文字を格納としている

iVar1 = 0x100;
do {
  FUN_00101220();
  iVar1 = iVar1 + -1;
} while (iVar1 != 0);

256回、FUN_00101220()している

FUN_00101220は、16バイトの構造体の配列を扱っている、ということを分かってないと読むのがかなり難しい本番は、構造体を扱っているだなんて微塵も考えておらず、処理内容を読めなかった

0x4040を起点として、16バイトの構造体が並んでいるつまり、0x4040 ~ 0x404Fで1つの構造体、0x4050 ~ 0x405Fで1つの構造体、... である

puVar4 = &DAT_0010404c;
do {
  puVar5 = puVar4 + 0x10;
  iVar1 = getc(stdin);
  *puVar4 = 1;
  puVar4[1] = (char)iVar1;
  puVar4 = puVar5;
} while (puVar5 != &DAT_0010424c);

でやっていたのは、構造体のフィールドに値を代入する処理である

FUN_00101220のdecompile結果は間違っているんじゃないかという点がある

まず、puVar7 = puVar7 + 2;は、puVar7 = puVar7 + 16;の間違いだと思う 16バイトの構造体が並んでいるんだから、普通に考えたら後者が自然だし、IDAで確認しても後者である

もう1つはbVar2 = (&DAT_0010404d)[(long)*(int *)(puVar7 + 1) * 0x10];である iVar6 = *(int *)puVar7;で、構造体の1バイト目\~4バイト目をint型として読み出しているだから、2バイト目\~5バイト目をint型として読み出すというのはおかしい

IDAで確認すると、bVar2 = (&DAT_0010404d)[(long)*(int *)(puVar7 + 8) * 0x10];が正しい

while (puVar7 != &stdin)も意味不明である 0x5040なのだが、なぜ&stdin?

構造体の構造について考えよう	位置	値
1バイト目 ~ 4バイト目	32ビット整数	`(int )puVar7`
5バイト目 ~ 8バイト目	32ビット整数	`(long)(int )((long)puVar7 + 4) * 0x10`
9バイト目 ~ 12バイト目	32ビット整数	`(long)(int )((long)puVar7 + 8) * 0x10`
13バイト目	8ビット整数	`(undefined )((long)puVar7 + 0xc)`
14バイト目	8ビット整数	`(byte )((long)puVar7 + 0xd)`
15バイト目~16バイト目(未使用)	-	-

以下のようなイメージだろう

#include <stdio.h>

struct S {
    __int32_t a;
    __int32_t b;
    __int32_t c;
    __int8_t d;
    __int8_t e;
    __int16_t padding;
};

int main(void){
    struct S s = {0x12, 0x34, 0x56, 0, 0, 0};
    s.d = 1;
    s.e = getchar();
}

objdumpするとこうなる

0000000000001139 <main>:
    1139:   55                      push   rbp
    113a:   48 89 e5                mov    rbp,rsp
    113d:   48 83 ec 10             sub    rsp,0x10
    1141:   c7 45 f0 12 00 00 00    mov    DWORD PTR [rbp-0x10],0x12
    1148:   c7 45 f4 34 00 00 00    mov    DWORD PTR [rbp-0xc],0x34
    114f:   c7 45 f8 56 00 00 00    mov    DWORD PTR [rbp-0x8],0x56
    1156:   c6 45 fc 00             mov    BYTE PTR [rbp-0x4],0x0
    115a:   c6 45 fd 00             mov    BYTE PTR [rbp-0x3],0x0
    115e:   66 c7 45 fe 00 00       mov    WORD PTR [rbp-0x2],0x0
    1164:   c6 45 fc 01             mov    BYTE PTR [rbp-0x4],0x1
    1168:   e8 c3 fe ff ff          call   1030 <getchar@plt>
    116d:   88 45 fd                mov    BYTE PTR [rbp-0x3],al
    1170:   b8 00 00 00 00          mov    eax,0x0
    1175:   c9                      leave
    1176:   c3                      ret

writeupには、GhidraのData Type Managerを使って、decompile結果を読みやすくする方法が書かれているが、上手くいかなかった配列を作るところで、長さの最大値がなぜか186になってしまう

ここまで整理する

0x4040を開始地点として、16バイトの構造体が256個ある

0x4040 ~ 0x404F
0x4050 ~ 0x405F ...
0x5030 ~ 0x503F

0x4040, 0x4050, ..., 0x4240を開始とする32個の構造体については、

puVar4 = &DAT_0010404c;
do {
  puVar5 = puVar4 + 0x10;
  iVar1 = getc(stdin);
  *puVar4 = 1;
  puVar4[1] = (char)iVar1;
  puVar4 = puVar5;
} while (puVar5 != &DAT_0010424c);

の処理がされる 256回、FUN_00101220()が呼ばれる FUN_00101220()では、256個の構造体を1個ずつ処理する

検証処理を確認しよう

pcVar2 = &DAT_00104e4d;
pcVar3 = &DAT_00104020;
do {
  if (*pcVar2 != *pcVar3) {
    puts("Wrong!");
    return 1;
  }
  pcVar2 = pcVar2 + 0x10;
  pcVar3 = pcVar3 + 1;
} while (pcVar2 != &DAT_0010504d);
puts("Correct!");

0x4e40を開始とする構造体の5個目のフィールドが、0x4020の値と一致するかを確認
0x4e50を開始とする構造体の5個目のフィールドが、0x4021の値と一致するかを確認 ...
0x5030を開始とする構造体の5個目のフィールドが、0x403fの値と一致するかを確認

している

z3で解いた z3を使わなくても解けるようだが、理解できなかった

from z3 import *

# 0x4040 ~ 0x503f
data = bytes.fromhex('00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 67 00 00 01 00 00 00 00 00 00 00 20 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 C6 00 00 01 00 00 00 01 00 00 00 22 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 69 00 00 01 00 00 00 02 00 00 00 24 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 73 00 00 01 00 00 00 03 00 00 00 26 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 51 00 00 01 00 00 00 04 00 00 00 28 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 FF 00 00 01 00 00 00 05 00 00 00 2A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 4A 00 00 01 00 00 00 06 00 00 00 2C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 EC 00 00 01 00 00 00 07 00 00 00 2E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 29 00 00 01 00 00 00 08 00 00 00 30 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 CD 00 00 01 00 00 00 09 00 00 00 32 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 BA 00 00 01 00 00 00 0A 00 00 00 34 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 AB 00 00 01 00 00 00 0B 00 00 00 36 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 F2 00 00 01 00 00 00 0C 00 00 00 38 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 FB 00 00 01 00 00 00 0D 00 00 00 3A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 E3 00 00 01 00 00 00 0E 00 00 00 3C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 46 00 00 01 00 00 00 0F 00 00 00 3E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 7C 00 00 01 00 00 00 10 00 00 00 40 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 C2 00 00 01 00 00 00 11 00 00 00 42 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 54 00 00 01 00 00 00 12 00 00 00 44 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 F8 00 00 01 00 00 00 13 00 00 00 46 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 1B 00 00 01 00 00 00 14 00 00 00 48 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 E8 00 00 01 00 00 00 15 00 00 00 4A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 E7 00 00 01 00 00 00 16 00 00 00 4C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 8D 00 00 01 00 00 00 17 00 00 00 4E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 76 00 00 01 00 00 00 18 00 00 00 50 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 5A 00 00 01 00 00 00 19 00 00 00 52 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 2E 00 00 01 00 00 00 1A 00 00 00 54 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 63 00 00 01 00 00 00 1B 00 00 00 56 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 33 00 00 01 00 00 00 1C 00 00 00 58 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 9F 00 00 01 00 00 00 1D 00 00 00 5A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 C9 00 00 01 00 00 00 1E 00 00 00 5C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 9A 00 00 01 00 00 00 1F 00 00 00 5E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 66 00 00 03 00 00 00 21 00 00 00 60 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 32 00 00 03 00 00 00 23 00 00 00 62 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 0D 00 00 03 00 00 00 25 00 00 00 64 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 B7 00 00 03 00 00 00 27 00 00 00 66 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 31 00 00 03 00 00 00 29 00 00 00 68 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 58 00 00 03 00 00 00 2B 00 00 00 6A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 A3 00 00 03 00 00 00 2D 00 00 00 6C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 5A 00 00 03 00 00 00 2F 00 00 00 6E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 25 00 00 03 00 00 00 31 00 00 00 70 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 5D 00 00 03 00 00 00 33 00 00 00 72 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 05 00 00 03 00 00 00 35 00 00 00 74 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 17 00 00 03 00 00 00 37 00 00 00 76 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 58 00 00 03 00 00 00 39 00 00 00 78 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 E9 00 00 03 00 00 00 3B 00 00 00 7A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 5E 00 00 03 00 00 00 3D 00 00 00 7C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 D4 00 00 03 00 00 00 3F 00 00 00 7E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 AB 00 00 03 00 00 00 41 00 00 00 80 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 B2 00 00 03 00 00 00 43 00 00 00 82 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 CD 00 00 03 00 00 00 45 00 00 00 84 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 C6 00 00 03 00 00 00 47 00 00 00 86 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 9B 00 00 03 00 00 00 49 00 00 00 88 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 B4 00 00 03 00 00 00 4B 00 00 00 8A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 54 00 00 03 00 00 00 4D 00 00 00 8C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 11 00 00 03 00 00 00 4F 00 00 00 8E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 0E 00 00 03 00 00 00 51 00 00 00 90 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 82 00 00 03 00 00 00 53 00 00 00 92 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 74 00 00 03 00 00 00 55 00 00 00 94 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 41 00 00 03 00 00 00 57 00 00 00 96 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 21 00 00 03 00 00 00 59 00 00 00 98 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 3D 00 00 03 00 00 00 5B 00 00 00 9A 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 DC 00 00 03 00 00 00 5D 00 00 00 9C 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 87 00 00 03 00 00 00 5F 00 00 00 9E 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 70 00 00 02 00 00 00 61 00 00 00 A0 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 E9 00 00 02 00 00 00 63 00 00 00 A2 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 3E 00 00 02 00 00 00 65 00 00 00 A4 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 A1 00 00 02 00 00 00 67 00 00 00 A6 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 41 00 00 02 00 00 00 69 00 00 00 A8 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 E1 00 00 02 00 00 00 6B 00 00 00 AA 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 FC 00 00 02 00 00 00 6D 00 00 00 AC 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 67 00 00 02 00 00 00 6F 00 00 00 AE 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 3E 00 00 02 00 00 00 71 00 00 00 B0 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 01 00 00 02 00 00 00 73 00 00 00 B2 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 7E 00 00 02 00 00 00 75 00 00 00 B4 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 97 00 00 02 00 00 00 77 00 00 00 B6 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 EA 00 00 02 00 00 00 79 00 00 00 B8 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 DC 00 00 02 00 00 00 7B 00 00 00 BA 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 6B 00 00 02 00 00 00 7D 00 00 00 BC 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 96 00 00 02 00 00 00 7F 00 00 00 BE 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 8F 00 00 02 00 00 00 81 00 00 00 C0 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 38 00 00 02 00 00 00 83 00 00 00 C2 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 5C 00 00 02 00 00 00 85 00 00 00 C4 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 2A 00 00 02 00 00 00 87 00 00 00 C6 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 EC 00 00 02 00 00 00 89 00 00 00 C8 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 B0 00 00 02 00 00 00 8B 00 00 00 CA 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 3B 00 00 02 00 00 00 8D 00 00 00 CC 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 FB 00 00 02 00 00 00 8F 00 00 00 CE 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 32 00 00 02 00 00 00 91 00 00 00 D0 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 AF 00 00 02 00 00 00 93 00 00 00 D2 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 3C 00 00 02 00 00 00 95 00 00 00 D4 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 54 00 00 02 00 00 00 97 00 00 00 D6 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 EC 00 00 02 00 00 00 99 00 00 00 D8 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 18 00 00 02 00 00 00 9B 00 00 00 DA 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 DB 00 00 02 00 00 00 9D 00 00 00 DC 00 00 00 01 00 00 00 00 00 00 00 01 00 00 00 00 00 00 00 01 5C 00 00 02 00 00 00 9F 00 00 00 DE 00 00 00 01 00 00 00 04 00 00 00 A1 00 00 00 A1 00 00 00 00 00 00 00 04 00 00 00 A3 00 00 00 A3 00 00 00 00 00 00 00 04 00 00 00 A5 00 00 00 A5 00 00 00 00 00 00 00 04 00 00 00 A7 00 00 00 A7 00 00 00 00 00 00 00 04 00 00 00 A9 00 00 00 A9 00 00 00 00 00 00 00 04 00 00 00 AB 00 00 00 AB 00 00 00 00 00 00 00 04 00 00 00 AD 00 00 00 AD 00 00 00 00 00 00 00 04 00 00 00 AF 00 00 00 AF 00 00 00 00 00 00 00 04 00 00 00 B1 00 00 00 B1 00 00 00 00 00 00 00 04 00 00 00 B3 00 00 00 B3 00 00 00 00 00 00 00 04 00 00 00 B5 00 00 00 B5 00 00 00 00 00 00 00 04 00 00 00 B7 00 00 00 B7 00 00 00 00 00 00 00 04 00 00 00 B9 00 00 00 B9 00 00 00 00 00 00 00 04 00 00 00 BB 00 00 00 BB 00 00 00 00 00 00 00 04 00 00 00 BD 00 00 00 BD 00 00 00 00 00 00 00 04 00 00 00 BF 00 00 00 BF 00 00 00 00 00 00 00 04 00 00 00 C1 00 00 00 C1 00 00 00 00 00 00 00 04 00 00 00 C3 00 00 00 C3 00 00 00 00 00 00 00 04 00 00 00 C5 00 00 00 C5 00 00 00 00 00 00 00 04 00 00 00 C7 00 00 00 C7 00 00 00 00 00 00 00 04 00 00 00 C9 00 00 00 C9 00 00 00 00 00 00 00 04 00 00 00 CB 00 00 00 CB 00 00 00 00 00 00 00 04 00 00 00 CD 00 00 00 CD 00 00 00 00 00 00 00 04 00 00 00 CF 00 00 00 CF 00 00 00 00 00 00 00 04 00 00 00 D1 00 00 00 D1 00 00 00 00 00 00 00 04 00 00 00 D3 00 00 00 D3 00 00 00 00 00 00 00 04 00 00 00 D5 00 00 00 D5 00 00 00 00 00 00 00 04 00 00 00 D7 00 00 00 D7 00 00 00 00 00 00 00 04 00 00 00 D9 00 00 00 D9 00 00 00 00 00 00 00 04 00 00 00 DB 00 00 00 DB 00 00 00 00 00 00 00 04 00 00 00 DD 00 00 00 DD 00 00 00 00 00 00 00 04 00 00 00 DF 00 00 00 DF 00 00 00 00 00 00 00')
# 0x4020 ~ 0x403f
expected_data = bytes.fromhex('3B 09 E5 AE 3E F1 37 81 FC A1 99 AE F7 62 7D F7 D0 CB A2 18 CD 3E 89 0D D9 DD 62 29 8C F3 01 EC')

class S:
    def __init__(self, t, i1, i2, x, y):
        self.t = t
        self.i1 = i1
        self.i2 = i2
        self.x = x
        self.y = y

array = []

for i in range(256):
    d = data[16*i:16*i+16]
    s = S(
        int.from_bytes(d[:4], 'little'),
        int.from_bytes(d[4:8], 'little'),
        int.from_bytes(d[8:12], 'little'),
        int(d[12]),
        int(d[13]),
    )
    array.append(s)

s = Solver()
input_chrs = [BitVec(f'input_chr_{i}', 8) for i in range(32)]

for i in range(32):
    array[i].x = 1
    array[i].y = input_chrs[i]

for _ in range(256):
    for i in range(256):
        t = array[i].t

        if t == 3:
            if array[array[i].i1].x != 0 and array[array[i].i2].x != 0:
                array[i].x = 1
                array[i].y = array[array[i].i1].y ^ array[array[i].i2].y
        elif t < 4:
            if (t == 1 or t == 2) and array[array[i].i1].x != 0 and array[array[i].i2].x != 0:
                array[i].x = 1
                array[i].y = array[array[i].i1].y + array[array[i].i2].y
        elif t == 4 and array[array[i].i1].x != 0:
            array[i].x = 1
            array[i].y = array[array[i].i1].y

for i in range(32):
    s.add(array[224+i].y == int(expected_data[i]))

r = s.check()

if r == sat:
    m = s.model()
    flag = ''.join(chr(m[input_chrs[i]].as_long()) for i in range(32))
    print(flag) # FLAG{INTr0dUction_70_R3v3R$1NG1}
else:
    print('not found')

バイト列は、IDAからコピーしてきた

roaris / ctf-log

WaniCTF 2024 : gates #61