俺たちはまだ angr を知らない

渗透技巧 1年前 (2023) admin

462 0 0

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

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

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

angr とは

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

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

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

参考：angr documentation

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

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 の可読文字列を制約としています。

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

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

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 を使う上でも有効です。

以下は、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

まとめ

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

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

原文始发于kashiwaba-yuki：俺たちはまだ angr を知らない

版权声明：admin 发表于 2023年6月27日上午9:05。
转载请注明：俺たちはまだ angr を知らない | CTF导航

Curl CVE-2023-38545 分析

admin

232

Sliver C2についての調査

admin

739

SQL注入之绕过安全狗WAF思路学习

admin

727

Django下防御Race Condition漏洞

admin

226

FOFA_Tips

admin

1,873

基于工作量证明（PoW）的验证码系统的简单实现

admin

暂无评论

您必须登录才能参与评论！

立即登录

暂无评论...

俺たちはまだ angr を知らない

もくじ

angr とは

シンボリックリンク実行

Factory クラス

SimulationManager

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

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

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

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

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

angr で CTF の問題を解く

HackCon 2016 – angry-reverser

SecurityFest 2016 – fairlight

z3py で制約を解く

n00bz CTF 2023 – zzz

まとめ

Writing Small .NET PE's

One Drive 用户名无限无声爆破

相关文章

暂无评论

相关文章

俺たちはまだ angr を知らない

もくじ

angr とは

シンボリックリンク実行

Factory クラス

SimulationManager

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

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

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

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

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

angr で CTF の問題を解く

HackCon 2016 – angry-reverser

SecurityFest 2016 – fairlight

z3py で制約を解く

n00bz CTF 2023 – zzz

まとめ

Writing Small .NET PE's

One Drive 用户名无限无声爆破

相关文章

暂无评论

广告位

相关文章