From bytecode to bytes: automated magic packet generation

claudejamodel: claude-sonnet-4-20250514

バイトコードからバイトへ：自動化されたマジックパケット生成

2026-04-08 Axel Boesenach 6分で読める

Linuxマルウェアは、Berkeley Packet Filter（BPF）ソケットプログラムに隠れることがよくあります。これらは、Linuxカーネルに埋め込まれてネットワークトラフィックの処理方法をカスタマイズできる小さな実行可能ロジックです。インターネット上で最も持続的な脅威の一部は、これらのフィルターを使用して、特定の「マジック」パケットを受信するまで休眠状態を保ちます。

これらのフィルターは数百の命令で構成され、複雑な論理ジャンプを含む可能性があるため、手動でリバースエンジニアリングするのは時間のかかるプロセスであり、セキュリティ研究者にとってボトルネックとなります。

より良い方法を見つけるために、私たちはシンボリック実行を検討しました。これは、コードを単なる命令ではなく、一連の制約として扱う方法です。Z3定理証明器を使用することで、悪意のあるフィルターから逆算して、それをトリガーするために必要なパケットを自動生成できます。

この投稿では、これを自動化するツールの構築方法を説明し、何時間もの手動アセンブリ解析をわずか数秒で完了するタスクに変える方法を紹介します。

複雑さの上限

悪意のあるフィルターを解析する方法を見る前に、それらを実行するエンジンを理解する必要があります。Berkeley Packet Filter（BPF）は、バイトコード命令のセットに基づいてネットワークスタックから特定のパケットを取得することをカーネルに可能にする高効率技術です。

多くの現代の開発者は、可観測性とセキュリティに使用される強力な進化版であるeBPF（Extended BPF）に馴染みがありますが、この投稿では「クラシック」BPFに焦点を当てます。元々tcpdumpなどのツール用に設計されたクラシックBPFは、わずか2つのレジスタを持つシンプルな仮想マシンを使用して、高速でネットワークトラフィックを評価します。

カーネル内部で深く動作し、ユーザー空間ツールからトラフィックを「隠す」ことができるため、ステルスバックドアの構築を目指すマルウェア作成者にとって好まれるツールとなっています。

LLMを使用してBPF命令のコンテキスト表現を作成することで、アナリストの手動オーバーヘッドはすでに削減されていますが、検証条件に対応するネットワークパケットの作成は、LLMが提供する追加コンテキストがあっても、依然として多くの作業が必要です。

BPFプログラムが約20命令しかない場合、これは通常問題になりませんが、私たちが観察したサンプルの一部のように、BPFプログラムが100命令を超える場合、指数関数的に複雑で時間のかかるものになる可能性があります。

問題を分解すると、バッファを読み取って制約をチェックし、結果に応じて実行パスを継続するか停止して最終結果をチェックするかが決まることがわかります。この種の決定論的結果を持つ問題は、与えられた制約のセットで問題を解決する手段を持つ定理証明器であるZ3によって解決できます。

展示A：BPFDoor

BPFDoorは、主にRed Menshen（Earth Bluecrowとしても知られる）を含む中国ベースの脅威アクターによってサイバースパイ活動に使用される、洗練されたパッシブLinuxバックドアです。少なくとも2021年から活動しており、このマルウェアは侵害されたネットワークでステルスな足がかりを維持するように設計されており、アジアと中東での活動に重点を置いて、通信、教育、政府部門を標的としています。

BPFDoorは、特定のネットワークポートを開く必要なく、すべての着信トラフィックを監視するためにBPFを使用します。

BPFDoorの命令例

Fortinetの研究で共有されたサンプル（82ed617816453eba2d755642e3efebfcbd19705ac626f6bc8ed238f4fc111bb0）に焦点を当てましょう。BPF命令を分解し、いくつかの注釈を追加すると、以下のように書くことができます：

(000) ldh [0xc]              ; オフセット12でハーフワードを読み取り（EtherType）
(001) jeq #0x86dd, jt 2, jf 6 ; 0x86DD（IPv6）-> ins 002 else ins 006
(002) ldb [0x14]             ; オフセット20でバイトを読み取り（Protocol）
(003) jeq #0x11, jt 4, jf 15 ; 0x11（UDP）-> ins 004 else DROP
(004) ldh [0x38]             ; オフセット56でハーフワードを読み取り（Dst Port）
(005) jeq #0x35, jt 14, jf 15; 0x35（DNS）-> ACCEPT else DROP
(006) jeq #0x800, jt 7, jf 15; 0x800（IPv4）-> ins 007 else DROP
(007) ldb [23]               ; オフセット23でバイトを読み取り（Protocol）
(008) jeq #0x11, jt 9, jf 15 ; 0x11（UDP）-> ins 009 else DROP
(009) ldh [20]               ; オフセット20でハーフワードを読み取り（fragment）
(010) jset #0x1fff, jt 15, jf 11; フラグメント化 -> DROP else ins 011
(011) ldxb 4*([14]&0xf)      ; インデックス（x）レジスタをロード ihl & 0xf
(012) ldh [x + 16]           ; オフセットx+16でハーフワードを読み取り（Dst Port）
(013) jeq #0x35, jt 14, jf 15; 0x35（DNS）-> ACCEPT else DROP
(014) ret #0x40000           ; (ACCEPT)
(015) ret #0                ; (DROP)

上記の例では、ACCEPT結果につながる2つのパス（ステップ5とステップ13）があることがわかります。また、オフセットと値を含む、チェックされる特定のバイトも明確に観察できます。これらの検証を取り、ACCEPTパスに一致するものを追跡することで、パケットを自動的に作成できるはずです。

最短パスの計算

BPF命令で提示された条件を検証するパケットへの最短パスを見つけるには、好ましくない条件で終わらないパスを追跡する必要があります。

小さなキューを作成することから始めます。このキューは、いくつかの重要なデータポイントを保持します：

次の命令へのポインタ
実行された命令の現在のパス + 次の命令

条件をチェックする命令に遭遇するたびに、ブール値を使用して結果を追跡し、これをキューに格納して、ACCEPT条件に到達する前の条件の数でパスを比較し、最短パスを計算できます。

疑似コードでは、これを最もよく表現できます：

paths = []
queue = dequeue([(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 or accept, stop parsing this instruction
    
    if instruction.class == jump_instruction:
        if instruction.operation == unconditional_jump:
            next_pc = pc + 1 + instruction_constant
            queue.append((next_pc, path + [next_pc]))
            continue
        
        # Conditional jump, explore both
        pc_true = pc + 1 + instruction.jump_true
        pc_false = pc + 1 + instruction.jump_false
        
        if instruction.jump_true <= instruction.jump_false:
            queue.append((pc_true, path + [pc_true]))
            queue.append((pc_false, path + [pc_false]))
        # else: same as above but reverse order of appending
    
    # else: sequential instruction, append to the queue

先ほどのBPFDoorの例に対してこのロジックを実行すると、受け入れられたパケットへの最短パスが提示されます：

(000) code=0x28 jt=0 jf=0 k=0xc     ; オフセット12でハーフワードを読み取り（EtherType）
(001) code=0x15 jt=0 jf=4 k=0x86dd  ; IPv6パケット
(002) code=0x30 jt=0 jf=0 k=0x14    ; オフセット20でバイトを読み取り（Protocol）
(003) code=0x15 jt=0 jf=11 k=0x11   ; プロトコル番号17（UDP）
(004) code=0x28 jt=0 jf=0 k=0x38    ; オフセット56でワードを読み取り（Destination Port）
(005) code=0x15 jt=8 jf=9 k=0x35    ; 宛先ポート53
(014) code=0x06 jt=0 jf=0 k=0x40000 ; Accept

これは、BPF命令を分析し、バックドアの受け入れられたパケットがどのように見えるかを理解する際に、BPF制約を自動的に解決する上で既に有用な自動化です。しかし、さらに一歩進めることはできるでしょうか？自動化された方法で期待されるパケットを返してくれる小さなツールを作成できるでしょうか？

Z3とscapyの採用

制約のセットが与えられた問題を解決するのに最適なツールの1つがZ3です。Microsoftによって開発されたこのツールは定理証明器として分類され、内部で非常に複雑な数学的操作を実行する使いやすい関数を公開しています。

有効なマジックパケットを作成するために使用するもう1つのツールはscapyで、インタラクティブなパケット操作のための人気のあるPythonライブラリです。

受け入れられたパケットへのパスを見つける方法が既にあるので、問題自体を解決し、その解決策をネットワークパケット内のそれぞれのオフセットでのバイトに変換することが残されています。

シンボリック実行

与えられたプログラムで取られるパスを探索するための一般的な技術は、シンボリック実行と呼ばれます。この技術では、制約を含む変数として使用できる入力を提供します。成功したパスの結果を知ることで、これらすべての成功したパスを見つけて、コンテキスト化された形式で最終結果を表示するようにツールを調整できます。

これが機能するためには、定数、レジスタ、およびチェックされている条件の結果としてのさまざまなブール演算子などの状態を追跡できる小さなマシンを実装する必要があります。

class BPFPacketCrafter:
    MIN_PKT_SIZE = 64  # 最小パケットサイズ（Ethernet + IP + UDPヘッダー）
    LINK_ETHERNET = "ethernet"  # DLT_EN10MB - Ethernetヘッダーで開始
    LINK_RAW = "raw"  # DLT_RAW - IPヘッダーで直接開始
    MEM_SLOTS = 16  # スクラッチメモリスロット数（M[0]からM[15]）
    
    def __init__(self, ins: list[BPFInsn], pkt_size: int = 128, ltype: str = "ethernet"):
        self.instructions = ins
        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)  # インデックスレジスタ
        
        # スクラッチメモリM[0-15]（32ビットワード）
        self.M = [BitVecVal(0, 32) for _ in range(self.MEM_SLOTS)]

上記のコードで、シンボリック実行中に状態を保持するためのマシンの大部分をカバーしました。もちろん、追跡する必要がある条件は他にもありますが、これらは解決プロセス中に処理されます。

ADD命令を処理するために、マシンはBPF操作をZ3加算にマップします：

def _execute_ins(self, insn: BPFInsn):
    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

幸い、BPF命令セットは実装が比較的簡単な小さな命令セットのみです。追跡する必要があるレジスタが2つだけというのは、確実に歓迎すべき制約です！

このシンボリック実行の全体的な動作は、以下の抽象化された概要で示すことができます：

"x"（インデックス）と"a"（アキュムレータ）レジスタを基本状態に初期化
成功したパスとして識別されたパスからの命令をループ処理
非ジャンプ命令をそのまま実行し、レジスタ状態を追跡
ジャンプ命令に遭遇した場合、分岐を取るべきかどうかを判断
Z3のcheck()関数を使用して、与えられた制約（ACCEPT）で条件が満たされているかをチェック
Z3ビットベクトル配列をバイトに変換
scapyを使用して変換されたバイトのパケットを構築

Z3ソルバーによって構築された制約を見ると、パケットバイトを構築するためにZ3が取った実行ステップを追跡できます：

[If(Concat(pkt_12, pkt_13) == 0x800, pkt_14 & 0xF0 == 0x40, True),
 If(Concat(pkt_12, pkt_13) == 0x800, pkt_14 & 0x0F >= 5, True),
 If(Concat(pkt_12, pkt_13) == 0x800, pkt_14 & 0x0F == 5, True),
 If(Concat(pkt_12, pkt_13) == 0x86DD, pkt_14 & 0xF0 == 0x60, True),
 0x86DD == ZeroExt(16, Concat(pkt_12, pkt_13)),
 0x11 == ZeroExt(24, pkt_20),
 0x35 == ZeroExt(16, Concat(pkt_56, pkt_57))]

Z3表示制約の最初の部分は、リンク層BPF命令を扱う際に有効なイーサネットIPを構築していることを確認するために追加された制約です。"If"文は、検出されたプロトコルに基づいて特定の制約を適用します：

IPv4ロジック（0x0800）：

pkt_14 & 240 == 64：バイト14はIPヘッダーの開始です。0xF0マスクは上位ニブル（Versionフィールド）を分離して、バージョンが4（0x40）かどうかをチェックします。
pkt_14 & 15 == 5：15（0x0F）で下位ニブル（IHL - Internet Header Length）を分離します。これは、オプションなしの標準サイズである5（20バイト）のヘッダー長を義務付けます。

IPv6ロジック（0x86dd）：

pkt_14 & 240 == 0x60：バージョンフィールドがバージョン6（0x60）かどうかをチェック

異なる値が設定されている第2部分を見ると、ネットワークパケット値を観察できます

Summary