タグアーカイブ セキュリティ

BPFバックドアのマジックパケットをZ3で自動生成する手法

Linuxマルウェア解析の現場で、手作業による逆アセンブリがボトルネックになっている。特に、Berkeley Packet Filter（BPF）ソケットプログラムに隠された「マジックパケット」待ち受け型のバックドアは、フィルタが数百命令に及ぶこともあり、解析に膨大な時間を要する。

Cloudflareのセキュリティ研究者らはこの課題に対し、シンボリック実行とZ3定理証明器を組み合わせた自動化手法を開発した。これにより、従来は数時間から数日かかっていたマジックパケットの特定を、数秒で完了させられるようになった。本記事では、その技術的アプローチと実装の詳細を解説する。

BPFがマルウェアに利用される理由

Berkeley Packet Filter（BPF）は、ネットワークスタックから特定のパケットを効率的に取り出すためのカーネル内技術だ。tcpdumpなどのツールでおなじみの「クラシックBPF」は、2つのレジスタしか持たないシンプルな仮想マシンで、高速なパケットフィルタリングを実現する。

ユーザー空間から見えなくなる特性

このBPFがマルウェア作者に好まれる理由は、その「不可視性」にある。カーネル深くで動作するBPFプログラムは、特定の条件を満たすパケットだけをユーザー空間のプロセスに渡すことができる。逆に言えば、条件を満たさないパケットは、ユーザー空間のネットワーク監視ツールから完全に隠蔽できる。

これにより、攻撃者は「マジックパケット」と呼ばれる特定のバイト列を含むパケットが到着するまで、バックドアを完全に休眠状態に保てる。通常のポートスキャンでは検出されず、ネットワーク上に痕跡を残さない、極めて隠密性の高い持続的脅威（APT）が実現する。

手動解析の限界

マルウェア対策の研究者がこの種のバックドアを分析する場合、BPFのバイトコードを逆アセンブルし、条件分岐を一つずつ追跡する必要があった。20命令程度の単純なフィルタなら問題ないが、実際には100命令を超える複雑なロジックを持つサンプルが観測されている。

Cloudflare Blogの記事によると、複雑なBPFプログラムの手動解析には「少なくとも1日」を要する場合があったという。この時間的コストが、脅威の早期分析と対策の迅速な展開を妨げるボトルネックとなっていた。

BPFDoorの実例から見るBPFフィルタ

この手法の具体例として、高度なLinuxバックドア「BPFDoor」のBPFフィルタを見てみる。Fortinetが分析したサンプル（ハッシュ値: 82ed617816453eba2d755642e3efebfcbd19705ac626f6bc8ed238f4fc111bb0）の逆アセンブル結果は次の通りだ。

(000) ldh [0xc]                   ; オフセット12から2バイト読み込み（EtherType）
(001) jeq #0x86dd, jt 2, jf 6     ; 0x86DD（IPv6）なら002へ、そうでなければ006へ
(002) ldb [0x14]                  ; オフセット20から1バイト読み込み（プロトコル）
(003) jeq #0x11, jt 4, jf 15      ; 0x11（UDP）なら004へ、そうでなければ015（DROP）へ
(004) ldh [0x38]                  ; オフセット56から2バイト読み込み（宛先ポート）
(005) jeq #0x35, jt 14, jf 15     ; 0x35（DNSポート53）なら014（ACCEPT）へ、そうでなければ015へ
(006) jeq #0x800, jt 7, jf 15     ; 0x800（IPv4）なら007へ、そうでなければ015へ
(007) ldb [23]                    ; オフセット23から1バイト読み込み（プロトコル）
(008) jeq #0x11, jt 9, jf 15      ; 0x11（UDP）なら009へ、そうでなければ015へ
(009) ldh [20]                    ; オフセット20から2バイト読み込み（フラグメント）
(010) jset #0x1fff, jt 15, jf 11  ; フラグメントされていれば015へ、そうでなければ011へ
(011) ldxb 4*([14]&0xf)           ; インデックスレジスタXに（IHL & 0xF）*4をロード
(012) ldh [x + 16]                ; オフセットX+16から2バイト読み込み（宛先ポート）
(013) jeq #0x35, jt 14, jf 15     ; 0x35（DNSポート53）なら014へ、そうでなければ015へ
(014) ret #0x40000 (ACCEPT)       ; パケット受理
(015) ret #0 (DROP)               ; パケット破棄

このフィルタは、IPv6パケットとIPv4パケットの両方の経路でDNSポート（53）へのUDPパケットを待ち受ける。IPv4の経路ではさらに、パケットがフラグメントされていないこと、IPヘッダ長が標準の20バイトであることなどの追加チェックが入る。

ACCEPTに至る2つの経路

上記のコードから、パケットがACCEPT（受理）される条件は2つの経路で満たされることがわかる。

• 経路1（IPv6）: EtherTypeが0x86DD（IPv6）→ プロトコルが0x11（UDP）→ 宛先ポートが0x35（53）
• 経路2（IPv4）: EtherTypeが0x0800（IPv4）→ プロトコルが0x11（UDP）→ フラグメントなし → IPヘッダ長が5（20バイト）→ 宛先ポートが0x35（53）

手動で分析すれば、これらの条件から「DNSポート53へのUDPパケット」がマジックパケットの候補だと推測できる。しかし、より複雑な算術演算やビット演算が絡むフィルタの場合、この推測は困難を極める。

シンボリック実行とZ3による自動化

Cloudflareの研究者らは、この「制約条件を満たす入力値の発見」という問題を、シンボリック実行と定理証明器Z3によって自動化するアプローチを取った。

シンボリック実行の基本概念

シンボリック実行とは、プログラムの入力を具体的な値ではなく「記号（シンボル）」として扱い、実行経路を数学的な制約の集合として表現する手法だ。BPFプログラムの場合、入力となるネットワークパケットの各バイトを未知の変数とみなす。

プログラムが条件分岐（jeqなど）に到達すると、「変数Aが値Bと等しい」という制約が真となる経路と、偽となる経路の両方を探索する。最終的にACCEPT命令に到達する経路において、変数が満たすべきすべての制約を収集する。

Z3定理証明器による制約解決

収集された制約を、Microsoft Researchが開発した定理証明器「Z3」に与える。Z3はこれらの制約を満たす具体的な変数値（つまり、パケットの各バイトの値）を自動的に計算する。

このプロセスは、複数の連立方程式を解くことに似ている。ただし、方程式が単純な等号ではなく、ビット演算、比較、条件分岐を含む複雑な論理式となる点が異なる。

最短経路の探索アルゴリズム

すべてのACCEPT経路を探索する前に、まず最短の経路を見つける。これは、後続のシンボリック実行の計算コストを抑えるためだ。擬似コードで示すと、次のような幅優先探索（BFS）が用いられる。

paths = []
queue = deque([(0, [0])])  # (プログラムカウンタ, 経路履歴)

while queue:
    pc, path = queue.popleft()
    if pc >= len(instructions):
        continue

    instruction = instructions[pc]

    if instruction.class == return_instruction:
        if instruction_constant != 0:  # ACCEPTの場合
            paths.append(path)
        continue  # DROPまたはACCEPTでこの経路の探索終了

    if instruction.class == jump_instruction:
        if instruction.operation == unconditional_jump:
            next_pc = pc + 1 + instruction_constant
            queue.append((next_pc, path + [next_pc]))
            continue

        # 条件付きジャンプの場合、真偽両方の経路を探索
        pc_true = pc + 1 + instruction.jump_true
        pc_false = pc + 1 + instruction.jump_false
        queue.append((pc_true, path + [pc_true]))
        queue.append((pc_false, path + [pc_false]))
    else:
        # 逐次実行命令の場合、次の命令へ
        queue.append((pc + 1, path + [pc + 1]))

このアルゴリズムを先ほどのBPFDoorフィルタに適用すると、より短いIPv6経路（命令000→001→002→003→004→005→014）が最短経路として特定される。

BPFシンボリック実行マシンの実装

最短経路がわかれば、次はその経路上でシンボリック実行を行うマシンを実装する。Cloudflareが開発した「BPFPacketCrafter」クラスの骨格は以下のようになる。

class BPFPacketCrafter:
    MIN_PKT_SIZE = 64           # 最小パケットサイズ
    LINK_ETHERNET = "ethernet"  # イーサネットヘッダから始まる
    MEM_SLOTS = 16              # スクラッチメモリM[0]〜M[15]

    def __init__(self, instructions, pkt_size=128, ltype="ethernet"):
        self.instructions = instructions
        self.pkt_size = max(self.MIN_PKT_SIZE, pkt_size)
        self.ltype = ltype

        # シンボリックなパケットバイト（各バイトが独立した変数）
        self.packet = [BitVec(f"pkt_{i}", 8) for i in range(self.pkt_size)]

        # シンボリックなレジスタ（32ビット）
        self.A = BitVecVal(0, 32)  # アキュムレータ
        self.X = BitVecVal(0, 32)  # インデックスレジスタ

        # スクラッチメモリ
        self.M = [BitVecVal(0, 32) for _ in range(self.MEM_SLOTS)]

ここでBitVecはZ3が提供するビットベクトル（固定長のビット列）型で、パケットの各バイトを8ビットの未知変数として表現する。レジスタAとXも同様に32ビットのビットベクトルとしてモデル化される。

BPF命令のZ3操作へのマッピング

シンボリック実行マシンは、BPFの各命令を対応するZ3の操作に変換しながら実行する。例えば、加算命令（ADD）は次のように処理される。

def _execute_ins(self, insn):
    cls = insn.cls
    if cls == BPFClass.ALU:  # 算術論理演算命令
        op = insn.op
        src_val = BitVecVal(insn.k, 32) if insn.src == BPFSrc.K else self.X
        if op == BPFOp.ADD:
            self.A = self.A + src_val  # Z3の加算演算でレジスタAを更新

比較命令（jeq）の場合は、条件式を制約として記録し、分岐先のプログラムカウンタへ実行を進める。クラシックBPFの命令セットは小さいため、このマッピングは比較的容易に実装できる。

制約の収集とパケット生成

最短経路に沿ってシンボリック実行を進めると、ACCEPT命令に到達した時点で、パケット変数が満たすべき制約の集合が完成する。Z3ソルバーはこの制約集合を解き、各pkt_i変数に具体的なバイト値を割り当てる。

得られた制約の例を、Z3が内部で生成する式の形で示すと以下のようになる。

0x86DD == ZeroExt(16, Concat(pkt_12, pkt_13))
0x11 == ZeroExt(24, pkt_20)
0x35 == ZeroExt(16, Concat(pkt_56, pkt_57))

これは、「オフセット12-13の2バイト（ビッグエンディアン）が0x86DD（IPv6）と等しい」「オフセット20の1バイトが0x11（UDP）と等しい」「オフセット56-57の2バイトが0x35（ポート53）と等しい」という3つの制約を表す。

Z3がこれらの制約を満たす解（例えばpkt_12=0x86, pkt_13=0xDD, pkt_20=0x11, ...）を求めると、それを実際のバイト列に変換する。最後に、Pythonのパケット操作ライブラリscapyを使って、このバイト列からネットワークパケットオブジェクトを組み立てる。

###[ Ethernet ]###
  dst       = 00:00:00:00:00:00
  src       = 00:00:00:00:00:00
  type      = IPv6
###[ IPv6 ]###
     version   = 6
     nh        = UDP
     src       = ::
     dst       = ::
###[ UDP ]###
        sport     = 0
        dport     = domain  # ポート53

生成されたパケットは、分析者がネットワーク上でバックドアの活性化テストを行う際の入力として、または検出用のシグネチャ作成のベースとして利用できる。

ツール「filterforge」と今後の展望

Cloudflareはこの研究成果をオープンソースツール「filterforge」として公開している。このツールを使えば、BPFバイトコードを含むファイルを入力とするだけで、マジックパケットの条件を満たすパケットのスケルトンを自動生成できる。

ツールの公開により、セキュリティコミュニティ全体でBPFベースの脅威に対する分析速度が向上することが期待される。特に、以下のような応用が考えられる。

• マルウェアサンプルの自動分類: 生成されたマジックパケットの特徴から、同一グループによる活動を関連付けられる。
• ネットワーク監視の強化: 生成されたパケットをプローブとして送信し、感染ホストの検出に利用する。
• 教育・研究: 複雑なBPFフィルタの動作を、具体的なパケット例とともに理解する教材となる。

LLMとの組み合わせ可能性

Cloudflare Blogの記事では、LLM（大規模言語モデル）を用いてBPF命令の文脈的説明を生成する取り組みにも言及している。シンボリック実行による自動パケット生成とLLMによる自然言語説明を組み合わせれば、分析者の作業負荷はさらに軽減される。

ただし現状では、LLMだけに複雑なBPFフィルタの解析とパケット生成を任せるには限界がある。Z3を用いた形式的な手法は、その正確性と完全性において依然として重要な役割を果たす。

この記事のポイント

• Linuxマルウェアは、カーネル内で動作するBPFソケットプログラムを利用し、特定の「マジックパケット」が到着するまで休眠する隠密性の高いバックドアを構築する。
• 手動でのBPFバイトコード逆解析は、数百命令に及ぶ複雑なフィルタの場合、数日を要するボトルネックだった。
• シンボリック実行によりBPFプログラムの入力を記号化し、定理証明器Z3で制約を解くことで、マジックパケットを数秒で自動生成できる。
• この手法は、最短経路探索、BPF仮想マシンのシンボリックモデル化、Z3制約ソルバー、scapyによるパケット組み立ての4ステップから構成される。
• Cloudflareが公開したオープンソースツール「filterforge」は、BPFベース脅威の分析速度をコミュニティ全体で向上させる可能性を秘めている。

海田 洋祐

・ 複数業界における17年間のデジタルビジネス開発経験
・ ウェブサイト開発のためのHTML、PHP、CSS、JavaScript等の実用的知識
・ 15ヶ国語対応の多言語SaaSの開発経験
・ 17年間にも及ぶ、Eコマース長期運営経験
・ 幅広い業界でのSEO最適化の豊富な経験

www.aandgweb.co.jp