このコンテンツは自動機械翻訳サービスによる翻訳版であり、皆さまの便宜のために提供しています。原本の英語版と異なる誤り、省略、解釈の微妙な違いが含まれる場合があります。ご不明な点がある場合は、英語版原本をご確認ください。
Linuxのマルウェアは、Serkeley Packet Filter（BPF）ソケットプログラムに潜んでいます。BPFは、Linuxカーネルに埋め込んだ実行可能なロジックで、ネットワークトラフィックの処理方法をカスタマイズすることができます。インターネット上の最も執拗な脅威の一部は、これらのフィルターを使用して、特定の「マジック」パケットを受信するまで休止状態を維持します。これらのフィルターは何百もの命令になり、複雑な論理ジャンプを含むため、手作業によるリバースエンジニアリングはセキュリティ研究者にとってボトルネックとなります。
私たちはより良い方法を見つけるために、シンボリック実行を検討しました。これは、コードを単なる命令ではなく、一連の制約として扱う方法です。Z3証明者を使うことで、悪意のあるフィルターから逆算して、トリガーに必要なパケットを自動的に生成することができます。この記事では、何時間もかかる手作業による組み立て分析をわずか数秒で完了するタスクに、これを自動化するツールをどのように作ったかを説明します。
悪意のあるフィルターの分解方法を見る前に、フィルターを実行しているエンジンを理解する必要があります。バークレーパケットフィルター（BPF）は、カーネルが一連のバイトコード指示に基づいてネットワークスタックから特定のパケットを引き出すことができる、非常に効率的な技術です。
可観測性とセキュリティに使用される強力な進化であるeBPF（拡張BPF）は、多くの現代の開発者がご存知でしょうが、この記事では「classic」BPFに焦点を当てます。もともとtcpdumpなどのツール用に設計された従来のBPFは、わずか2つのレジスタを持つシンプルな仮想マシンを使用し、ネットワークトラフィックを高速に評価します。カーネルの内部で深く実行され、ユーザー空間のツールからトラフィックを「隠す」ことができるため、巧妙なバックドアを構築しようとするマルウェア作成者にとってお気に入りのツールとなっています。
LLMを使用してBPF指示のコンテキスト表現を作成することで、アナリストの手作業によるオーバーヘッドはすでに削減されていますが、検証条件に対応するネットワークパケットを作成するには、LLMが提供するコンテキストが追加されても、依然として多くの作業が必要です。
ほとんどの場合、BPFプログラムに20個の命令しかない場合は問題ありませんが、一部のサンプルで観察されたように、BPFプログラムが100以上の命令で構成されている場合、指数関数的に複雑になり、時間がかかります。
問題を分解すると、結果に応じて実行パスを継続するか、停止して最終結果を確認するかの、バッファの読み取りと制約のチェックに確認できます。
決定論的な結果を持つこの種の問題は、与えられた制約で問題を解決する手段を持つ理論証明者であるZ3が解くことができます。
BPFDoorは、高度なパッシブLinuxバックドアであり、主に中国拠点の脅威アクター（別名：Earth Bluecrow）によるサイバースパイ活動に使用されます。少なくとも2021年以来活動しているこのマルウェアは、電気通信、教育、政府部門を標的とし、侵害されたネットワークに隠れた足掛かりを維持するように設計されており、特にアジアと中東での活動に重点を置いています。
BPFDoorは、BPFを使用して、特定のネットワークポートを開くことなく、すべての着信トラフィックを監視します。
Fortinetの調査で共有されたサンプル（82ed617816453eba2d755642e3efebfcbd19705ac626f6bc8ed238f4fc111bb0）に焦点を当ててみましょう。BPFの指示を分解して、注釈を追加すると、次のようになります。
(000) ldh [0xc] ; Read halfword at offset 12 (EtherType)
(001) jeq #0x86dd, jt 2, jf 6 ; 0x86DD (IPv6) -> ins 002 else ins 006
(002) ldb [0x14] ; Read byte at offset 20 (Protocol)
(003) jeq #0x11, jt 4, jf 15 ; 0x11 (UDP) -> ins 004 else DROP
(004) ldh [0x38] ; Read halfword at offset 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] ; Read byte at offset 23 (Protocol)
(008) jeq #0x11, jt 9, jf 15 ; 0x11 (UDP) -> ins 009 else DROP
(009) ldh [20] ; Read halfword at offset 20 (fragment)
(010) jset #0x1fff, jt 15, jf 11 ; fragmented -> DROP else ins 011
(011) ldxb 4*([14]&0xf) ; Load index (x) register ihl & 0xf
(012) ldh [x + 16] ; Read halfword at offset 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 ; Read halfword at offset 12 (EtherType)
(001) code=0x15 jt=0 jf=4 k=0x86dd ; IPv6 packet
(002) code=0x30 jt=0 jf=0 k=0x14 ; Read byte at offset 20 (Protocol)
(003) code=0x15 jt=0 jf=11 k=0x11 ; Protocol number 17 (UDP)
(004) code=0x28 jt=0 jf=0 k=0x38 ; Read word at offset 56 (Destination Port)
(005) code=0x15 jt=8 jf=9 k=0x35 ; Destination port 53
(014) code=0x06 jt=0 jf=0 k=0x40000 ; Accept
これは、BPF指示を分析し、バックドアのために受け入れられたパケットがどのように見えるかを理解する際に、BPF制約を自動的に解決するのに役立つ自動化機能です。しかし、さらに一歩踏み込むことができるとしたらどうでしょう。
もし、期待されたパケットを自動化された方法で返してくれる小さなツールを作成できたらどうなるでしょうか？
一連の制約が与えられた問題を解決するのに最適なツールの1つが、Z3です。Microsoftが開発したこのツールは、定説証明者と名付けられ、内部で非常に複雑な数学的操作を行う使いやすい関数を公開します。
有効なマジックパケットを作成するために使用するもう1つのツールは、対話型のパケット操作のための人気のPythonライブラリであるscapyです。
受け入れられたパケットへのパスを見つける方法がすでにあるので、この問題自体を解決し、この解決策をネットワークパケットのそれぞれのオフセットのバイトに変換するだけです。
あるプログラムで実行されるパスを調べるのは、シンボリック実行と呼ばれるのが一般的な手法です。このテクニックでは、制約を含め変数として使用できる入力を与えています。成功したパスの結果を知ることで、ツールを調整してこれらの成功したパスをすべて見つけ、最終結果をコンテキストに基づいた形式で表示することができます。
これを機能させるためには、定数、レジスタ、さまざまなブール演算子などの状態を、チェックされている条件の結果として追跡できる小さなマシンを実装する必要があります。
class BPFPacketCrafter:
MIN_PKT_SIZE = 64 # Minimum packet size (Ethernet + IP + UDP headers)
LINK_ETHERNET = "ethernet" # DLT_EN10MB - starts with Ethernet header
LINK_RAW = "raw" # DLT_RAW - starts with IP header directly
MEM_SLOTS = 16 # Number of scratch memory slots (M[0] to 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
# Symbolic packet bytes
self.packet = [BitVec(f"pkt_{i}", 8) for i in range(self.pkt_size)]
# Symbolic registers (32-bit)
self.A = BitVecVal(0, 32) # Accumulator
self.X = BitVecVal(0, 32) # Index register
# Scratch memory M[0-15] (32-bit words)
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」（累積コンピュータ）レジスタをベースの状態に初期化します。
成功パスとして識別されたパスからの指示をループさせます。
Z3check()関数を使用して、与えられた制約(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 Logic (0x0800):
pkt_14 & 240 == 64: Byte 14はIPヘッダーの始まりです。0xF0マスクは、ハイニブル（Versionフィールド）を分離して、バージョンが4（0x40）かどうかを確認します。
pkt_14 & 15 == 5: 15 (0x0F)、ローニブル（IHL - インターネットヘッダー長）を分離これは、ヘッダーの長さ5（20バイト）を必須とします。これは、オプションのない標準サイズです。
IPv6 Logic (0x86dd):
異なる値がチェックされている2番目の部分を見ると、ネットワークパケット値が確認できます。
0x86DD: IPv6ヘッダーのパケット条件。
0x11: UDPプロトコル番号。
0x35: 宛先ポート（53）。
予想される値の横に、指定されたパケット（例：pkt_12, pkt_13)。
これで、どのバイトが特定のオフセットに存在すべきかが確立されたので、それをscapyを使って実際のネットワークパケットに変換することができます。以前のZ3制約のバイトから新しいパケットを生成すると、パケットがどのようなものになるかを明確に確認でき、これをさらなる処理のために保存することができます。
###[ Ethernet ]###
dst = 00:00:00:00:00:00
src = 00:00:00:00:00:00
type = IPv6 <-- IPv6 Packet
###[ IPv6 ]###
version = 6
tc = 0
fl = 0
plen = 0
nh = UDP <-- UDP Protocol
hlim = 0
src = ::
dst = ::
###[ UDP ]###
sport = 0
dport = domain <-- Port 53
len = 0
chksum = 0x0
これらの新しく作成されたパケットは、ネットワーク上でこれらをスキャンすることで、これらのインプラントの存在を特定するために、さらなる調査や特定に使用することができます。
特定のBPF指示が何をしているのかを理解するのは、面倒で時間のかかる作業です。この例は、合計16の指示に過ぎませんが、私たちは、理解するのに少なくとも1日はかかる200以上の命令を検出したことがあります。Z3リゾルバーを使って、この時間をわずか数秒に短縮し、受け入れられたパケットへのパスだけでなく、そのためのパケットスクレイピングも表示できるようになりました。
当社は、コミュニティがBPFベースのインプラントの分解を自動化できるように、filterforgeツールをオープンソース化しました。ソースコードと使用例は、弊社のGitHubリポジトリでご覧いただけます。
この調査結果を公開し、アナリストがBPFの指示を理解するのに費やす時間を削減するためのツールを共有することで、他の人がこの形態の自動化を拡大するためにさらに研究を進めることを願っています。