書籍「詳解セキュリティコンテスト」のReversingを読んだ

前回 は、セキュリティコンテストのためのCTF問題集 という書籍を読みました。

今回は、詳解セキュリティコンテスト: CTFで学ぶ脆弱性攻略の技術 Compass Booksシリーズ という書籍を入手したので読んでいきたいと思います。この書籍は、Web、Crypto、Reversing、Pwnable の順で解説されていて、680ページを超えるボリュームがあります。最初は、hwo2heap の解説が見たくて、Pwnable から読み進めていたのですが、なかなか難しくて、先に Reversing を読むことにしました。

それでは、やっていきます。

• 参考文献
• はじめに
• 23章：Reversingを始める前に
• 24章：アセンブリ言語
• 25章：アセンブリを読んでみよう
• 26章：静的解析に触れてみよう
• 27章：動的解析を組み合わせよう
• 28章：より発展的な話題
  • 28.1：プログラムにパッチを当てる
  • 28.2：アンチデバッグ
  • 28.3：難読化
  • 28.4：PIE
  • 28.5：Z3で制約を解く
  • 28.6：angrによるシンボリック実行
• 29章：実践問題の解答
• おわりに

参考文献

今回、題材にさせて頂いた「詳解セキュリティコンテスト」です。

Ghidra の解説本です。今回は、プログラムのパッチを当てる方法について役に立ちました。

はじめに

「セキュリティ」の記事一覧です。良かったら参考にしてください。

以下は「詳解セキュリティコンテスト: CTFで学ぶ脆弱性攻略の技術 Compass Booksシリーズ」のサポートサイトです。問題ファイルをダウンロードすることが出来ます。

book.mynavi.jp

では、書籍の章を参考に書き進めていきます。

23章：Reversingを始める前に

23章は、10ページぐらいの分量で、Reversingについての導入部分が書かれています。

Reversing とは、リバースエンジニアリングと呼ばれるカテゴリです。表層解析、静的解析、動的解析を使って、答えを探します。

環境構築として、IDA、z3、angr が必要であると書かれています。私の場合は、IDA の代わりに、Ghidra を使ってやっていきます。

24章：アセンブリ言語

24章は、22ページぐらいの分量で、アセンブリ言語の基礎的な内容、文法が解説されています。

この章は、実際に問題に向き合うときに、アセンブリ言語で分からないことがあったときに読む、というぐらいでいいと思います。

実践問題もありますが、この章で解説されていることの確認テストみたいな感じなので、割愛します。

25章：アセンブリを読んでみよう

25章は、10ページぐらいの分量で、ここもアセンブラのソースの読み方について、座学的な内容です。

初めてアセンブラのソースを読む方向けに、丁寧に、アセンブラソースの読み方について解説されています。私の場合は、軽く目を通したので、次の章に行きたいと思います。

26章：静的解析に触れてみよう

26章は、8ページぐらいの分量で、静的解析について解説されています。

具体的なプログラムを対象として、IDA を使って、静的解析を行いながら解説がされています。

ここも、IDA を始めて使う方向けに、丁寧に IDA の操作方法が解説されています。次の章に進みます。

27章：動的解析を組み合わせよう

27章は、14ページぐらいの分量で、動的解析について解説されています。

gdb（gdb-peda）の使い方を含めて、動的解析のやり方について、丁寧に説明されています。また、IDA でアドレスを調べて、それを使って、gdb で解析する方法などについても解説されています。

この章で扱ってるプログラム（rev/05_dynamic/program）について、確認していきます。

$ file program
program: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 3.2.0, BuildID[sha1]=6ed9027941cb76c9c39675092a09d2891db9aad2, not stripped

$ checksec --file=program
RELRO          STACK CANARY  NX          PIE     RPATH     RUNPATH     Symbols     FORTIFY  Fortified  Fortifiable  FILE
Partial RELRO  Canary found  NX enabled  No PIE  No RPATH  No RUNPATH  68 Symbols  No       0          1            program

program のソースコードも付いてました。これを見ることは書籍の趣旨とは違うかもしれませんが（笑）。

10文字のパスワードがあり、それを当てるプログラムのようです。パスワードは計算した結果になっているので、一見では分からないようになっています。

#include <stdio.h>
#include <string.h>

unsigned int flist[] = {
  6, 9, 7, 11, 5, 1, 5, 5, 2, 14, 3, 3, 0, 0, 1, 7, 14, 4, 15, 11
};

unsigned char func(int i) {
  return (flist[i*2] ^ i) * 16 + (flist[i*2+1] ^ (i+1));
}

int authenticate(const unsigned char *password) {
  int i, len = strlen(password);

  if (len != 10) {
    return 0;
  }

  for(i = 0; i < len; i++) {
    if (password[i] != func(i)) {
      return 0;
    }
  }

  return 1;
}

int main(int argc, char **argv) {
  char password[0x20];

  printf("Enter password: ");
  scanf("%31s", password);

  if (authenticate(password)) {
    puts("Password is correct!");
  } else {
    puts("Password is wrong...");
  }

  return 0;
}

最後は、Pythonスクリプトを使って、gdb の操作を自動化する方法についても解説されています。

gdb操作の自動化は経験がなかったので、やってみようと思ったのですが、サポートサイトからダウンロードした内容に、この自動化した Pythonスクリプトが含まれていませんでした。代わりに、calc_password.py というファイルがあって、パスワードを計算する Pythonスクリプトでした。改訂などで、書籍の内容が変わったのかもしれません。

書籍を見ながら、gdb操作を自動化する Pythonスクリプト（solve.py）を書きました。

まず、authenticate関数の逆アセンブラを示します。authenticate関数では、入力されたパスワードが 10文字かどうかのチェック、10文字だった場合は、そのパスワードが正しいかどうかを先頭から 1文字ずつチェックして、その結果を返します。

逆アセンブラでは、strlen関数を実行し、その戻り値をローカル変数（スタック）に格納し、それが 10 じゃなければ、戻り値 0 で関数を終了させます。10 の場合は、ローカル変数 i を 0 で初期化して for文に入ります。for文では、func関数を実行し、その戻り値と入力されたパスワードを比較して、一致していたらローカル変数 i をインクリメントして次の文字の比較に進みます。10文字比較が完了したら比較結果を戻り値に設定して authenticate関数を終了します。

gdb の操作は、func関数を実行した後、その戻り値と入力されたパスワードを比較する直前（0x4006f7番地）に、ブレークポイントを設定して、入力されたパスワードを、その戻り値の値に変更する、という操作を 10文字分繰り返すことになります。

pwndbg> disassemble authenticate
Dump of assembler code for function authenticate:
   0x00000000004006ab <+0>:     push   rbp
   0x00000000004006ac <+1>:     mov    rbp,rsp
   0x00000000004006af <+4>:     push   rbx
   0x00000000004006b0 <+5>:     sub    rsp,0x28
   0x00000000004006b4 <+9>:     mov    QWORD PTR [rbp-0x28],rdi
   0x00000000004006b8 <+13>:    mov    rax,QWORD PTR [rbp-0x28]
   0x00000000004006bc <+17>:    mov    rdi,rax
   0x00000000004006bf <+20>:    call   0x400530 <strlen@plt>
   0x00000000004006c4 <+25>:    mov    DWORD PTR [rbp-0x14],eax
   0x00000000004006c7 <+28>:    cmp    DWORD PTR [rbp-0x14],0xa
   0x00000000004006cb <+32>:    je     0x4006d4 <authenticate+41>
   0x00000000004006cd <+34>:    mov    eax,0x0
   0x00000000004006d2 <+39>:    jmp    0x400713 <authenticate+104>
   0x00000000004006d4 <+41>:    mov    DWORD PTR [rbp-0x18],0x0
   0x00000000004006db <+48>:    jmp    0x400706 <authenticate+91>
   0x00000000004006dd <+50>:    mov    eax,DWORD PTR [rbp-0x18]
   0x00000000004006e0 <+53>:    movsxd rdx,eax
   0x00000000004006e3 <+56>:    mov    rax,QWORD PTR [rbp-0x28]
   0x00000000004006e7 <+60>:    add    rax,rdx
   0x00000000004006ea <+63>:    movzx  ebx,BYTE PTR [rax]
   0x00000000004006ed <+66>:    mov    eax,DWORD PTR [rbp-0x18]
   0x00000000004006f0 <+69>:    mov    edi,eax
   0x00000000004006f2 <+71>:    call   0x400657 <func>
   0x00000000004006f7 <+76>:    cmp    bl,al
   0x00000000004006f9 <+78>:    je     0x400702 <authenticate+87>
   0x00000000004006fb <+80>:    mov    eax,0x0
   0x0000000000400700 <+85>:    jmp    0x400713 <authenticate+104>
   0x0000000000400702 <+87>:    add    DWORD PTR [rbp-0x18],0x1
   0x0000000000400706 <+91>:    mov    eax,DWORD PTR [rbp-0x18]
   0x0000000000400709 <+94>:    cmp    eax,DWORD PTR [rbp-0x14]
   0x000000000040070c <+97>:    jl     0x4006dd <authenticate+50>
   0x000000000040070e <+99>:    mov    eax,0x1
   0x0000000000400713 <+104>:   add    rsp,0x28
   0x0000000000400717 <+108>:   pop    rbx
   0x0000000000400718 <+109>:   pop    rbp
   0x0000000000400719 <+110>:   ret
End of assembler dump.

gdb操作を自動化する Pythonスクリプト（solve.py）について、簡単に解説します。上で説明したように、0x4006f7番地にブレークポイントを 設定し、実行します。ブレークポイントで止まったら、Pythonスクリプトが動き始めるのだと思います。password という変数を空文字で初期化し、10文字分のループを実行します。

ループでは、func関数の戻り値の al を取得して password変数に格納し、blレジスタに設定し、実行を再開します。再び、ブレークポイントで止まったら、次のループを実行します。10文字分が完了したら、password変数の内容を表示して終了します。

import gdb

gdb.execute( 'break *0x4006f7' )
gdb.execute( 'run' )

password = ''

for ii in range( 10 ):
    
    al = gdb.parse_and_eval( '$al' )
    password += chr( al )
    
    gdb.execute( f'set $bl = {al}' )
    gdb.execute( 'continue' )

print( "=" * 10 )
print( password )
print( "=" * 10 )

では、動かしてみます。

うまくいったようです。Pythonスクリプトで、手軽に gdb操作の自動化ができるのはいいですね。

$ gdb program -x ./solve.py
GNU gdb (Debian 13.1-3) 13.1
Copyright (C) 2023 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<https://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Poetry could not find a pyproject.toml file in /home/user/svn/experiment/shokai_security_contest/files/rev/05_dynamic or its parents
pwndbg: loaded 169 pwndbg commands and 47 shell commands. Type pwndbg [--shell | --all] [filter] for a list.
pwndbg: created $rebase, $base, $bn_sym, $bn_var, $bn_eval, $ida GDB functions (can be used with print/break)
Reading symbols from program...
(No debugging symbols found in program)
Breakpoint 1 at 0x4006f7
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
Enter password: 0123456789

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()

Breakpoint 1, 0x00000000004006f7 in authenticate ()
Password is correct!
[Inferior 1 (process 950824) exited normally]
==========
hirakegoma
==========
------- tip of the day (disable with set show-tips off) -------
Use contextprev and contextnext to display a previous context output again without scrolling

28章：より発展的な話題

28.1：プログラムにパッチを当てる

プログラムのバイナリを一部変更して、プログラムの動作を変えることを解説しています。書籍では、IDA を使った方法を解説しています。

IDA は、プログラムのバイナリを変更しても、変更後のバイナリをエクスポートする機能が無いそうですが、変更前と変更後の差異は出力できるそうです。その差異をファイル出力して、バイナリを変更する Pythonスクリプトが紹介されています。

一方、Ghidra には、変更後のバイナリをエクスポートする機能があるようです。参考書籍の マスタリングGhidra ―基礎から学ぶリバースエンジニアリング完全マニュアル の 22章の「バイナリのパッチ」に解説があります。これを見ながら、ちょっとやってみます。

まず、main関数の逆アセンブラを示します。0x400768番地で、authenticate関数が実行されます。その次の行（test eax,eax）は、AND をとって、結果がゼロかどうかをレジスタに反映します。その次の行で、ゼロなら、0x40077f番地に飛び、異常処理になり、ゼロじゃなければ正常処理（パスワード一致）になります。

この行を反転させれば、間違ったパスワードを入力すると、パスワードが一致した、という結果に出来ます。具体的には、0x40076f番地の je 0x40077f <main+101> を jnz に変更したいということです。

pwndbg> disassemble main
Dump of assembler code for function main:
   0x000000000040071a <+0>:     push   rbp
   0x000000000040071b <+1>:     mov    rbp,rsp
   0x000000000040071e <+4>:     sub    rsp,0x40
   0x0000000000400722 <+8>:     mov    DWORD PTR [rbp-0x34],edi
   0x0000000000400725 <+11>:    mov    QWORD PTR [rbp-0x40],rsi
   0x0000000000400729 <+15>:    mov    rax,QWORD PTR fs:0x28
   0x0000000000400732 <+24>:    mov    QWORD PTR [rbp-0x8],rax
   0x0000000000400736 <+28>:    xor    eax,eax
   0x0000000000400738 <+30>:    lea    rdi,[rip+0xf5]        # 0x400834
   0x000000000040073f <+37>:    mov    eax,0x0
   0x0000000000400744 <+42>:    call   0x400550 <printf@plt>
   0x0000000000400749 <+47>:    lea    rax,[rbp-0x30]
   0x000000000040074d <+51>:    mov    rsi,rax
   0x0000000000400750 <+54>:    lea    rdi,[rip+0xee]        # 0x400845
   0x0000000000400757 <+61>:    mov    eax,0x0
   0x000000000040075c <+66>:    call   0x400560 <__isoc99_scanf@plt>
   0x0000000000400761 <+71>:    lea    rax,[rbp-0x30]
   0x0000000000400765 <+75>:    mov    rdi,rax
   0x0000000000400768 <+78>:    call   0x4006ab <authenticate>
   0x000000000040076d <+83>:    test   eax,eax
   0x000000000040076f <+85>:    je     0x40077f <main+101>
   0x0000000000400771 <+87>:    lea    rdi,[rip+0xd2]        # 0x40084a
   0x0000000000400778 <+94>:    call   0x400520 <puts@plt>
   0x000000000040077d <+99>:    jmp    0x40078b <main+113>
   0x000000000040077f <+101>:   lea    rdi,[rip+0xd9]        # 0x40085f
   0x0000000000400786 <+108>:   call   0x400520 <puts@plt>
   0x000000000040078b <+113>:   mov    eax,0x0
   0x0000000000400790 <+118>:   mov    rdx,QWORD PTR [rbp-0x8]
   0x0000000000400794 <+122>:   xor    rdx,QWORD PTR fs:0x28
   0x000000000040079d <+131>:   je     0x4007a4 <main+138>
   0x000000000040079f <+133>:   call   0x400540 <__stack_chk_fail@plt>
   0x00000000004007a4 <+138>:   leave
   0x00000000004007a5 <+139>:   ret
End of assembler dump.

一応、0x40084a と 0x40085f のどちらが正常パスなのかが分からないので、文字列を確認しておきます。0x40084a の方が、正常パスでした。

pwndbg> x/20c 0x40084a
0x40084a:       80 'P'  97 'a'  115 's' 115 's' 119 'w' 111 'o' 114 'r' 100 'd'
0x400852:       32 ' '  105 'i' 115 's' 32 ' '  99 'c'  111 'o' 114 'r' 114 'r'
0x40085a:       101 'e' 99 'c'  116 't' 33 '!'

では、Ghidra でパッチを当ててみます。0x40076f番地で右クリックして、Patch Instruction をクリックします。すると、命令を編集できるので、JE を JNZ に変更します。JNZ に変更すると、命令のバイト列が出るので、長さが変わらないことを確認して実行します。

その後、保存して（File → Save All）、エクスポートします（File → Export Program... で、Format を Original File にする）。エクスポート結果を確認します。1byteだけが差分になっています（74→75に変化）

$ hexdump -C program > program.hex

$ hexdump -C program_patch > program_patch.hex

$ diff program.hex program_patch.hex
--- program.hex 2024-12-28 20:23:36.566180939 +0900
+++ program_patch.hex   2024-12-28 20:23:44.252843329 +0900
@@ -116,7 +116,7 @@
 00000730  00 00 48 89 45 f8 31 c0  48 8d 3d f5 00 00 00 b8  |..H.E.1.H.=.....|
 00000740  00 00 00 00 e8 07 fe ff  ff 48 8d 45 d0 48 89 c6  |.........H.E.H..|
 00000750  48 8d 3d ee 00 00 00 b8  00 00 00 00 e8 ff fd ff  |H.=.............|
-00000760  ff 48 8d 45 d0 48 89 c7  e8 3e ff ff ff 85 c0 74  |.H.E.H...>.....t|
+00000760  ff 48 8d 45 d0 48 89 c7  e8 3e ff ff ff 85 c0 75  |.H.E.H...>.....u|
 00000770  0e 48 8d 3d d2 00 00 00  e8 a3 fd ff ff eb 0c 48  |.H.=...........H|
 00000780  8d 3d d9 00 00 00 e8 95  fd ff ff b8 00 00 00 00  |.=..............|
 00000790  48 8b 55 f8 64 48 33 14  25 28 00 00 00 74 05 e8  |H.U.dH3.%(...t..|

パッチを当てたバイナリを実行してみます。

バッチリです！

$ ./program_patch
Enter password: 0123456789
Password is correct!

今回の場合は変更後の命令のサイズが、変更前の命令のサイズと同じだったので、簡単にパッチを当てることが出来ました。もし、変更後の命令のサイズが、変更前の命令のサイズよりも小さい場合は、空いたところに、nop命令を埋めればいいですね。変更後の命令のサイズが、変更前の命令のサイズよりも大きい場合は難しいです。このケースについても参考文献の マスタリングGhidra ―基礎から学ぶリバースエンジニアリング完全マニュアル に解説があるので、必要になったら理解したいと思います。

28.2：アンチデバッグ

動的解析を防ぐ仕組みのことをアンチデバッグと言うそうです。

ここでは、ptrace の is_debugged という関数を使うと、現在デバッグされているかどうかを判断できるようです。これを使って、デバッグ時は終了する、などのコードを実装することが出来そうです。

また、procfs についても解説があります。/proc/self/status というファイルには、デバッグされているかどうかを示す内容があります。TracerPid という項目が 0 ならデバッグされてなくて、それ以外の場合はデバッグしているプロセス番号が入っています。

ちょっと見てみます。確かに、0 が入っていました。

$ cat /proc/self/status
Name:   cat
Umask:  0022
State:  R (running)
Tgid:   1186670
Ngid:   0
Pid:    1186670
PPid:   239148
TracerPid:      0
Uid:    1000    1000    1000    1000
Gid:    1000    1000    1000    1000
FDSize: 256
Groups: 20 24 25 27 29 30 44 46 106 113 114 121 1000
NStgid: 1186670
NSpid:  1186670
NSpgid: 1186670
NSsid:  239148
Kthread:        0
VmPeak:     3740 kB
VmSize:     3740 kB
VmLck:         0 kB
VmPin:         0 kB
VmHWM:      1664 kB
VmRSS:      1664 kB
RssAnon:               0 kB
RssFile:            1664 kB
RssShmem:              0 kB
VmData:      360 kB
VmStk:       132 kB
VmExe:        20 kB
VmLib:      1520 kB
VmPTE:        44 kB
VmSwap:        0 kB
HugetlbPages:          0 kB
CoreDumping:    0
THP_enabled:    1
untag_mask:     0xffffffffffffffff
Threads:        1
SigQ:   0/7556
SigPnd: 0000000000000000
ShdPnd: 0000000000000000
SigBlk: 0000000000000000
SigIgn: 0000000000000000
SigCgt: 0000000000000000
CapInh: 0000000000000000
CapPrm: 0000000000000000
CapEff: 0000000000000000
CapBnd: 000001ffffffffff
CapAmb: 0000000000000000
NoNewPrivs:     0
Seccomp:        0
Seccomp_filters:        0
Speculation_Store_Bypass:       vulnerable
SpeculationIndirectBranch:      always enabled
Cpus_allowed:   3
Cpus_allowed_list:      0-1
Mems_allowed:   00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000000,00000001
Mems_allowed_list:      0
voluntary_ctxt_switches:        0
nonvoluntary_ctxt_switches:     1

もう少しいろいろあると思うのですが、アンチデバッグの解説は以上でした。

28.3：難読化

静的解析を困難にする手法として、難読化があります。

最初に紹介されているのがパッカーです。以前、「セキュリティコンテストチャレンジブックの「付録」を読んでx86とx64のシェルコードを作った - 土日の勉強ノート」で、パッカーについて紹介しました。

次に紹介されているのが、1つの機械語を 2つ以上の意味で使う方法です。一般的に機械語は複数バイトで表現される場合があります。例えば、5byteの機械語があったとして、その末尾の 3byte だけを見ると、別の命令に見えることがあります。jmp命令で、その末尾の 3byte にジャンプすることが可能です。これは、逆アセンブラを見ても分かりません。そういう意味で難読化という仕組みになります。

28.4：PIE

セキュリティ機構の PIE（Position Independent Executable）です。プログラム自身がどのアドレスに配置されても動作するように構成されます。このプログラムを IDA や Ghidra で見ると、表示されるアドレスは先頭からの相対アドレスであり、実際に配置された後のアドレスはベースアドレスを足して考えなければなりません。というような内容が解説されています。

28.5：Z3で制約を解く

Z3 というツールの紹介です。Z3 とは、SATソルバと呼ばれるものだそうです。そもそもソルバとは、方程式や最適化問題を数値的に解いたり、制約条件を満たす解を見つけたりします。実際にやってみた方が、イメージが分かると思います。

サポートサイトからダウンロードしたファイルのうち、rev/06_advanced/z3/z3sample.c です。

main関数は、ユーザから入力された符号なし整数を code というローカル変数に格納します。次に check_input関数に code を渡し、その戻り値が 1 だったら Correct! と表示し、それ以外だったら Wrong... と表示します。

check_input関数は、引数の code を使って、いろいろな計算をします。その結果、if文が真になったら 1 を返し、それ以外の場合は 0 を返します。この check_input関数の引数の code はユーザが与える符号なし整数であり、ユーザはどんな数値を与えればいいかを考える問題です。

#include <stdio.h>

int check_input(unsigned int n) {
  int a, b, c, d;
  a = n & 0xff;
  b = (n >> 8) & 0xff;
  c = (n >> 16) & 0xff;
  d = (n >> 24) & 0xff;
  if ((a + b + c + d == 824)
      && (a - b + c - d == 0)
      && (a * b + c * d == 83816)
      && (a * b - c * d == 7004)) {
    return 1;
  } else {
    return 0;
  }
}

int main() {
  unsigned int code;
  printf("CODE: ");
  scanf("%u", &code);
  if (check_input(code)) {
    puts("Correct!");
  } else {
    puts("Wrong...");
  }
}

人があれこれ考えても、いずれ解ける問題ですが、ここで Z3 というツール（Pythonライブラリ）を使って解きましょうということです。

以下は、サポートサイトが提供している Pythonスクリプトで、Z3 を使って、上の問題を解いています。書籍では、Z3 については、ネットや文献を見てね、となっており、解説は全くありません（笑）。

それではあんまりなので、以下のサイトが詳しいそうです。ざっと読めば、何となく使えるようになると思います。

https://wiki.mma.club.uec.ac.jp/CTF/Toolkit/z3py

変数 n を作っているところがポイントですね。この変数 n が解であり、いろんな型の変数を作ることが出来ます。あとは、Z3 に制約を設定して、Solver.check() を実行すると、下位を見つけてくれます。

from z3 import *

s = Solver()
n = BitVec("code", 32) # 32-bitのビット列とする

# 普通の変数のように扱える
a = n & 0xff
b = (n >> 8) & 0xff
c = (n >> 16) & 0xff
d = (n >> 24) & 0xff

# 制約を追加
s.add(And( # ブール式の積はAndを使う
    a + b + c + d == 824,
    a - b + c - d == 0,
    a * b + c * d == 83816,
    a * b - c * d == 7004
))

r = s.check()
if r == sat:
    # 解が見つかった
    m = s.model()
else:
    # 解が存在しない
    print("[-] Solution not found")
    exit(1)

answer = m[n].as_long()
print("[+] CODE: {0} (0x{0:x})".format(answer))

早速実行してみます。

$ python z3solve.py
[+] CODE: 2917068734 (0xaddeefbe)

$ gcc -o z3sample.out z3sample.c

$ ./z3sample.out
CODE: aaa
Wrong...

$ ./z3sample.out
CODE: 2917068734
Correct!

大した時間もかからず、制約条件の問題を解くことができました。

28.6：angrによるシンボリック実行

angr とは、Python 向けのシンボリック実行のフレームワークだそうです。簡単に言うと、内部に上の Z3 を使ってソルバ機能を実現することが出来る CPUエミュレータという感じです。動的解析のように実際にプログラムを実行することなく、仮想的にプログラムを動かして解を探させる、ということが出来るようです。

Z3 を使って解いた問題を angr を使って解いてみます。

サポートサイトが提供している angr を使ったソースコードです。program というところを上でコンパイルした z3sample.out に書き換えればいいです。

import angr
import claripy

# プロジェクトの作成
p = angr.Project("./program", load_options={"auto_load_libs": False})
# 10バイトの入力codeを作成
code = claripy.BVS("code", 8 * 10)
# 初期状態を通常実行の最初の状態とする
state = p.factory.entry_state(stdin=code) # 標準入力をcodeとする
simgr = p.factory.simulation_manager(state)

# 解を探索する
simgr.explore(find=0x4006f9, avoid=0x400707)
try:
    found = simgr.found[0]
    # 0x4006f9に到達できるような入力codeを表示
    print(found.solver.eval(code, cast_to=bytes))
except IndexError:
    print("Not Found")

では、実行してみます。うーん、うまくいきませんでした。理由は分かりません。

$ pip install angr
Successfully installed CppHeaderParser-2.7.4 GitPython-3.1.43 ailment-9.2.134 angr-9.2.134 archinfo-9.2.134 bitstring-4.2.3 cachetools-5.5.0 cart-1.2.2 claripy-9.2.134 cle-9.2.134 future-1.0.0 gitdb-4.0.11 itanium-demangler-1.1 markdown-it-py-3.0.0 mdurl-0.1.2 mpmath-1.3.0 mulpyplexer-0.9 nampa-0.1.1 networkx-3.4.2 numpy-2.2.1 pefile-2024.8.26 ply-3.11 protobuf-5.29.2 pydot-3.0.3 pyformlang-1.0.10 pyparsing-3.2.0 pyvex-9.2.134 rich-13.9.4 smmap-5.0.1 sympy-1.13.3 typing-extensions-4.12.2 unique-log-filter-0.1.0

$ ln -s ../z3/z3sample.out program

$ ll
合計 8.0K
drwxr-xr-x 1 user user  38 12月 28 22:51 ./
drwxr-xr-x 1 user user  62  4月 10  2022 ../
-rwxr--r-- 1 user user 625  4月 10  2022 angrsolve.py*
lrwxrwxrwx 1 user user  18 12月 28 22:51 program -> ../z3/z3sample.out*

$ python angrsolve.py
WARNING  | 2024-12-28 22:54:13,685 | angr.simos.simos | stdin is constrained to 10 bytes (has_end=True). If you are only providing the first 10 bytes instead of the entire stdin, please use stdin=SimFileStream(name='stdin', content=your_first_n_bytes, has_end=False).
Not Found

angr はうまくいかなかったので、まずは、Z3 で対応していくようにします。

29章：実践問題の解答

各章末の実践問題の解説です。割愛します。

おわりに

今回は、詳解セキュリティコンテスト: CTFで学ぶ脆弱性攻略の技術 Compass Booksシリーズ の Reversing（リバースエンジニアリング）を読みました。新しめの CTF の実践的な解説本です。非常にオススメですが、難易度は高めです。また、解説が十分ではなく、自分で調べてね、というところも多いです。とはいえ、最近の本で CTF の解説をしてる本は多くないので、少しずつでも読んだ方がいいと思います。次回は、Pwnable の章を読んでいきます。Reversing に比べて、だいぶ難しいです（笑）。

最後になりましたが、エンジニアグループのランキングに参加中です。

ランキング参加中

エンジニアグループ

気楽にポチッとよろしくお願いいたします🙇

今回は以上です！

最後までお読みいただき、ありがとうございました。