俺たちはまだ angr を知らない(Z3py も追記中)

今まであまり深く考えずにテンプレで運用してきた angr ですが、先日「angr で解けそうなバイナリなのに解けない問題」にぶつかったため、いい機会だと思って少し詳しく学んでみることにしました。

実際に使ってみると想像以上に強力なツールでしたので、ほんの一部ではありますがサンプルコードと併せて記事化しておくことにしました。

チートシート的に使う予定なので、内容は今後も追記していきます。

angr とは

angr は、動的シンボリック実行などのバイナリに対する様々な静的解析を実行する機能を持つ解析ツールです。

angr は Python モジュールとして利用することができます。

angr は、まずバイナリをプロジェクトにロードし、angr に用意されているいくつかのクラスに対応するインスタンス化します。

CTF で angr を使用する場合は通常、シンボリック変数を使用するシンボリック実行によるプログラムの状態の変化を追跡するとともに、内部的に使用している z3 などの SMT ソルバを利用して、任意の出力を得るための入力値を逆算することなどができます。

シンボリックリンク実行

angr は、エミュレータではなくシンボリックリンク変数を利用したシンボリックリンク実行により解析を行うツールです。

SimulationManager は stash という単位にレジスタやメモリなどの状態(SimState)を保持しており、処理を進めたりフィルタしたりすることができます。

シンボリックリンク実行では、プログラムの命令を取得し、それを利用して SimState の操作を行った結果を一連のリストとして保持します。

初期化時の stash は active です。ステップ実行を進めた結果次の状態を生成できなくなった SimState は deadended という stash に配置されます。

ここで、SimulationManager の explore() 関数を使用すると、特定のアドレスに到達する SimState のみを検索し、他の SimState を破棄するような探索を行うことができます。

また、この時 Bitvectors として定義したシンボル変数に制約を付与して、任意の出力を得るための入力値を逆算することもできます。

これらを利用して単純に Flag を解析する場合、以下のようなスクリプトを利用できます。

import angr

proj = angr.Project("chall", auto_load_libs=False)
obj = proj.loader.main_object
print("Entry", hex(obj.entry))

find = 0x401654
avoids = [0x4016ca,0x4011a9]

init_state = proj.factory.entry_state()
simgr = proj.factory.simgr(init_state)
simgr.explore(find=find, avoid=avoids)

# 出力
simgr.found[0].posix.dumps(0)

以下では、CTF の問題を解くために angr でシンボリック実行を行う場合によく使用するクラスやオブジェクトについて概要をまとめます。

Factory クラス

Factory は angr で最も頻繁に使用するクラスの一つで、コードブロックやシュミレーションのための SimState オブジェクトを取得するために使用できます。

例えば以下のように、コードブロックの取得やレジスタ、メモリの参照や変更ができます。

import angr
proj = angr.Project("chall", auto_load_libs=False)

# コードの基本ブロックを抽出
block = proj.factory.block(proj.entry)
block.pp()

# プログラムのメモリ、レジスタ、ファイルシステムを含む SimState オブジェクトの作成
state = proj.factory.entry_state()

# 現在の state のレジスタ値を取得
state.regs
state.regs.rax 

# エントリポイントのメモリを取得
state.mem[proj.entry].int.resolved

# レジスタ値を任意の値に書き換え
state.regs.rax = state.solver.BVV(3, 64)

# メモリを任意の値に書き換え
state.mem[0x1000].long = 4

なお、angr では、数値は bitvector オブジェクトとして扱われます。

これは、CPU に合わせて 32bit もしくは 64bit を指定できます。

# int を 32bit の BVV に変換する
bv = state.solver.BVV(0x1234, 32)

# BVV を int に変換する
state.solver.eval(bv)

SimulationManager

CTF で問題を解くときに主に使うのがこのオブジェクトです。

SimulationManager を使用すると、プログラムの実行をシュミレートすることができます。

# シミュレーションマネージャの作成
simgr = proj.factory.simulation_manager(state)

SimulationManager では、状態を stash という単位に保持します。

初期化された場合に初めに与えられる stash は active です。

simgr.step() でシンボリックリンク実行を行うと、active の stash に 1 つずつ状態が追加されていくことがわかります。

そのため、ある程度実行を進めた状態で active 内の要素を参照すると、状態が更新されていることがわかります。

SimulationManager を使用した解析テクニック

Flag 文字列の長さを事前定義する

以下のようなコードで Flag 用のシンボリック変数を制約を付与して作成できます。

import angr
import claripy

# 20 文字分のシンボリック変数 flag を作成する(8bit のビットベクタ)
flag = claripy.BVS('flag', 20*8, explicit_name=True)

# プログラムのメモリ、レジスタ、ファイルシステムを含む SimState オブジェクトの作成
# state = proj.factory.blank_state(addr=funcaddr, add_options={angr.options.LAZY_SOLVES})
state = proj.factory.entry_state()

# 20 文字分のシンボリック変数に対して制約を付与する
for i in range(19):
    state.solver.add(flag.get_byte(i) >= 0x21)
    state.solver.add(flag.get_byte(i) <= 0x7f)

Flag 文字列の制約を追加する

特定の文字を特定済みの場合には以下のようにシンボリック変数の制約を追加することでより効果的に探索を行うことができます。

# 特定の位置の文字が特定済みの場合は制約に追加することができる
state.add_constraints(argv1.chop(8)[0] == 'C')
state.add_constraints(argv1.chop(8)[1] == 'T')
state.add_constraints(argv1.chop(8)[2] == 'F')
state.add_constraints(argv1.chop(8)[3] == '{')

Flag 用のシンボリック変数を適切な箇所に適用する

作成した Flag 用のシンボリック変数は問題バイナリの実装に合わせて適切な箇所に適用してあげる必要があります。

# コマンドライン引数に Flag を入力する必要がある場合
argv1 = claripy.BVS("argv1", 0xE * 8)
state = proj.factory.entry_state(args=["./fairlight", argv1])

# 特定の関数の引数に Flag を与えて関数を呼び出す場合
flag = claripy.BVS('flag', 20*8, explicit_name=True)
buf = 0x606000 # buffer to store flag(.data)
funcaddr = 0x400646 # entry point of crazy function

state = proj.factory.blank_state(addr=funcaddr, add_options={angr.options.LAZY_SOLVES})

# insert flag into memory by hand
# state.memory.store(buf, flag, endness='Iend_LE')
state.memory.store(buf, flag, endness='Iend_BE')
state.regs.rdi = buf

パフォーマンスを改善する

deadend の stash などを自動的に破棄するなどのオプションで angr 実行時のパフォーマンスを改善することができる場合があります。

また、angr のデフォルトではメモリから読み込むことができるシンボルのバイト数は 60 バイトに指定されており、これ以上の Flag の場合には上手く解析ができない場合があります。

そのような場合は、state.libc.buf_symbolic_bytesを変更することで、適切なバイトサイズを指定できます。

# 外部ライブラリの自動ロードを無効化してパフォーマンスを改善する
proj = angr.Project('./chall', auto_load_libs=False)

# オプションに LAZY_SOLVES を指定することでシンボル解決を遅延させ、パフォーマンスを改善できる(正確性が低下する場合がある)
state = proj.factory.entry_state(args=["./chall", argv1], add_options={angr.options.LAZY_SOLVES})

# メモリから読み込むことができるシンボルのバイト数を変更
state.libc.buf_symbolic_bytes = input_size + 1

# avoid と deadended の stash を自動的に破棄する
simgr.explore(find=find, avoid=avoids, step_func=lambda lsm: lsm.drop(stash='avoid').drop(stash='deadended'))

シンボリック実行の探索方法を変更する

simgr = proj.factory.simulation_manager(state)
explorer = angr.exploration_techniques.Explorer(find=lambda s: s.solver.eval(s.regs.dl) == 0x43 and s.solver.eval(s.regs.rip) == 0x401641)
simgr.use_technique(explorer)
simgr.run()

探索中のレジスタとスタックの情報を取得する

# simgr.step() などで任意の状態まで処理を進めた stash がある状態
current_state = simgr.active[0]

# RAX レジスタの値を参照する
current_state.regs.rax

# RSP の情報を取得する
current_state.regs.rsp

p_BV64 = current_state.mem[0x7fffffffffeffa8].uint64_t.resolved
current_state.solver.eval(p_BV64)
current_state.solver.eval_upto(p_BV64,10)

angr で CTF の問題を解く

ここからは、angr の公式ドキュメントで紹介されている CTF の問題を angr で解いていきます。

参考：CTF Challenge Examples - angr documentation

HackCon 2016 - angry-reverser

問題バイナリを Ghidra で解析すると、入力値を検証して正しい Flag かどうかを識別していることがわかります。

しかし、Flag の検証を行っている関数は以下のように非常に複雑な演算を繰り返し行っており、静的解析で Flag を特定するのはかなり難しいです。

angr を使って正しい入力値を特定することを目指すのですが、このバイナリではシンボリックリンク実行に記載のシンプルな SimulationManager を使用するスクリプトで探索を行っても一向に処理が終わりません。

そこで、回答サンプルのスクリプトを読んでいきます。

import angr
import claripy

def main():
    flag    = claripy.BVS('flag', 20*8, explicit_name=True) # symbolized flag, we know the length by looking at the assembly code
    buf     = 0x606000 # buffer to store flag
    crazy   = 0x400646 # entry point of crazy function
    find    = 0x405a6e # end of crazy function

    # Offset of 'FAIL' blocks in Crazy(from pwntools--e.search(asm('mov ecx, 0')))
    avoids = [0x402c3c, 0x402eaf, 0x40311c, 0x40338b, 0x4035f8, 0x403868,
              0x403ad5, 0x403d47, 0x403fb9, 0x404227, 0x404496, 0x40470a,
              0x404978, 0x404bec, 0x404e59, 0x4050c7, 0x405338, 0x4055a9,
              0x4057f4, 0x405a2b]

    proj = angr.Project('./yolomolo', auto_load_libs=False)
    # Create blank state starting from crazy function
    # LAZY_SOLVES is very important here because we are actually collecting constraints for an equation Ax=b, where A is 20 by 20, x and b are 20 by 1
    state = proj.factory.blank_state(addr=crazy, add_options={angr.options.LAZY_SOLVES})
    # insert flag into memory by hand
    # state.memory.store(buf, flag, endness='Iend_LE')
    state.memory.store(buf, flag, endness='Iend_BE')
    state.regs.rdi = buf

    # each character of flag should be between 0x30 and 0x7f
    for i in range(19):
        state.solver.add(flag.get_byte(i) >= 0x21)
        state.solver.add(flag.get_byte(i) <= 0x7f)

    simgr = proj.factory.simulation_manager(state)

    simgr.explore(find=find, avoid=avoids)
    found = simgr.found[0]
    return found.solver.eval(flag, cast_to=bytes)

def test():
    assert main() == b"HACKCON{VVhYS04ngrY}"

if __name__ in '__main__':
    import logging
    logging.getLogger('angr.sim_manager').setLevel(logging.DEBUG)
    print(main())

このコードでは、flag というシンボリック変数を作成して、ASCII の可読文字列を制約としています。

そして、state.memory.store(buf, flag, endness='Iend_BE')でビッグエンディアン形式で data セクションの空き領域に格納した後、このアドレスを rdi にセットした状態で Flag 検証を行う GoHomeOrGoCrazy 関数のアドレスを entry にした SimState を作成しています。

この辺りは重要なテクニックっぽいですね。

SecurityFest 2016 - fairlight

次はコマンドライン引数に Flag を含めて実行する必要があるパターンの Solver です。

ここでは、entry_state の args に定義したシンボリック変数を与えることで Flag の特定を行っています。

import angr
import claripy

def main():
    proj = angr.Project('./fairlight', load_options={"auto_load_libs": False})
    argv1 = claripy.BVS("argv1", 0xE * 8)
    state = proj.factory.entry_state(args=["./fairlight", argv1]) 

    simgr = proj.factory.simulation_manager(state)
    simgr.explore(find=0x4018f7, avoid=0x4018f9)
    found = simgr.found[0]
    return found.solver.eval(argv1, cast_to=bytes)

def test():
    res = main()
    print(repr(res))
    assert res == b'4ngrman4gem3nt'


if __name__ == '__main__':
    import logging
    logging.getLogger('angr.sim_manager').setLevel(logging.DEBUG)
    print(main())

z3py で制約を解く

angr では、制約を解決するための SMT ソルバとして内部的に z3 を使用しています。

そのため、z3py で制約を解く記法を知ることは angr を使う上でも有効です。

また、デコンパイル結果から特定した条件を元に制約を細かく指定して Flag を特定するようなことも可能です。

ビットの和を計算する関数を定義して一致させる制約

from z3 import *
from math import *

s = Solver()
i1 = BitVec('i1', 64)
i2 = BitVec('i2', 64)

# ビットの和を計算する関数を定義
def HW(bvec):
  return Sum([ZeroExt(int(ceil(log2(bvec.size()))), Extract(i,i,bvec)) for i in range(bvec.size())])

# ビットの和に応じて0か1を返す関数を定義
def volcano(x):
  w = HW(x)
  return If(And(w > 16, w < 27), 1, 0)

def digitValue(c):
    dv = StrToInt(c)
    return If(dv == -1, 1, dv)

if s.check() == sat:
    print(s.model())
else:
    print("unsat")

10 進数にしたときの桁数を一致させる制約

from z3 import *

s = Solver()
i1 = BitVec('i1', 64)
i2 = BitVec('i2', 64)

# 文字列化して 10 進数の桁数カウント
# https://stackoverflow.com/questions/tagged/z3py
i1 = BV2Int(i1)
i2 = BV2Int(i2)
s.add(Length(IntToStr(i1)) == Length(IntToStr(i2)))

if s.check() == sat:
    print(s.model())
else:
    print("unsat")

10 進数にしたときに各桁の和が一致する制約

from z3 import *
from math import *

s = Solver()
i1 = BitVec('i1', 64)
i2 = BitVec('i2', 64)

# xとyの10進数の各桁の和が同じであることを制約に追加
# https://stackoverflow.com/questions/76654949/z3-iterate-over-string-to-add-up-only-numbers-python-api
add_only_numbers = RecFunction('add_only_numbers', StringSort(), IntSort())
w = FreshConst(StringSort())
RecAddDefinition( add_only_numbers
                , [w]
                , If ( Length(w) == 0
                     , 1
                     , digitValue(Extract(w, 0, 1)) + add_only_numbers(Extract(w, 1, Length(w) - 1))
                     )
                )
s.add(add_only_numbers(IntToStr(i1)) == add_only_numbers(IntToStr(i2)))

if s.check() == sat:
    print(s.model())
else:
    print("unsat")

z3py でシフトやローテートシフトの演算を行う

z3Py で BitVec のシフト演算を行うことができます。(普通にシフト演算することも可能)

# 4 バイト分の BitVec を作成し、各文字のバイトに制約を追加
buf = BitVec("buf", 32)
for i in range(4):
    # LShR(>>)
    s.add((LShR(buf,8*i) & 0xFF) >= 0x21)
    s.add((LShR(buf,8*i) & 0xFF) <= 0x7e)
    
# 同じように、 3 バイト分だけ利用したい場合は以下のように制約を指定する
buf2 = BitVec("buf2", 32)
s.add(buf2 >> 24 == 0)
for i in range(3):
    # LShR(>>)
    s.add((LShR(buf2,8*i) & 0xFF) >= 0x30)
    s.add((LShR(buf2,8*i) & 0xFF) <= 0x39)
    
    
# ローテートシフト(以下の実装に対して ror(1*b,15) とする場合に等しい)
# def ror(a,b): return (LShR(a,b)|(a<<(32-b))) & N
RotateRight((a * b), 15)

# 以下の実装に対して rol((a * b), 11) とする場合に等しい
# def rol(a,b): return ror(a,32-b) # RotateLeft
RotateLeft((a * b), 11)

参考：Z3: z3py Namespace Reference

z3py で CTF の問題を解く

以下は、CTF の問題の制約を z3py で解く場合の例です。

n00bz CTF 2023 - zzz

問題バイナリとして与えられた ELF ファイルを Ghidra でデコンパイルすると以下のような結果が得られました。

read 関数で fd=0 から 0x1e を読み取っているようですので、標準入力からデータを受け取って check 関数に流していることがわかります。

check 関数は以下のようなデコンパイル結果でした。

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

SEKAI CTF - Guardians of the Kernel

ローテートシフトの活用
z3Py 内での途中の演算すべてを制約にする必要はなく、普通に変数に代入した上で最後の値のみを制約にすることも可能

参考：SEKAI CTF 2023 Writeup

まとめ

今まで何も考えずにコピペで使ってた angr ですが、実際のところかなり強力なツールであり、今回書ききれなかった内容も含めてあらゆる CTF の問題を解くうえで非常に有効になりうるものだと感じました。

この記事の内容はチートシート的に使っていきたいので適宜追加していこうと思います。

Published Jun 26, 2023

リバースエンジニアになりたいCTF Player(Team: 0nePadding)。WinDbgとYARAが好き。OSCP / CISSP / AtCoder 緑 Microsoft Japanに所属してます。発言はすべて個人の見解。かしわば on Twitter