バイトコードからパケットへ！BPF マルウェアを自動で起こす filterforge！

やっほー、しぃちゃんだよ！今日はね、マルウェア解析の「めんどくさい」を丸ごと自動化しちゃう、とっても賢い話を見つけたの。BPF のバイトコードとにらめっこする時間が、時間単位から秒単位になるんだって。わくわくするよね！

Cloudflare Blog blog.cloudflare.com

なにが発表されたの？

Cloudflare の Blog が、BPF マルウェアを起こすための「マジックパケット」を自動生成するツールの話を公開したの。

BPF(Berkeley Packet Filter)はカーネルの中で動く小さな仮想マシンで、ネットワークパケットをバイトコードで判定する仕組みなんだ。本来はパケットフィルタリングのための技術なんだけど、これを悪用するマルウェアがいるの。たとえば BPFDoor みたいなバックドアは、100 命令を超える複雑なフィルタを仕込んで、「特定のパケットが来るまでじっと眠って隠れる」の。だからカーネルの外(ユーザー空間)の監視ツールからは気づかれにくいんだよ。

ちなみに、最近よく聞く eBPF は、この BPF が進化した観測性向けのバージョン。今回の主役は、その元祖にあたるクラシックな BPF のほうなの。

なぜ重要なの？

眠っているバックドアを起こすには、フィルタの条件を全部満たす「マジックパケット」を作ってあげないといけないの。でもね、100 命令を超えるバイトコードを人間が手で読み解いて、「どのバイトを、どの値にすれば ACCEPT になるか」を逆算するのは、ものすごく大変。解析者の何時間もが溶けちゃうんだ。

しかもこの手のフィルタは、Fortinet が報告している Symbiote や BPFDoor みたいに、実際に使われている脅威なの。だから「速く・確実に条件を満たすパケットを作れる」ことは、防御側にとってすごく大事なんだよ。

これで何が変わるの？

このツールを使うと、BPF のバイトコードを渡すだけで、それを ACCEPT させるパケットが自動で出てくるの。手作業で何時間もかかっていた逆算が、数秒で終わっちゃう。

うれしいのは、解析者が「このフィルタは、どんなパケットに反応するように作られているのか」を素早くつかめること。マルウェアの通信条件が分かれば、検知ルールを書いたり、挙動を再現したりするのがぐっと楽になるんだ。

深く潜ってみよう

しぃちゃんが一番おもしろいと思ったのは、フィルタを「順番に実行するプログラム」じゃなくて「数式の制約の集まり」として扱うところ。仕組みは大きく 3 つのパーツでできているの。

1 つめは最短経路探索。BPF の命令を枝分かれのある木とみなして、幅優先探索で「なるべく少ない条件で ACCEPT にたどり着く道」を探すの。命令ポインタと分岐を追いかけながら、通るべきルートを決めるんだ。

2 つめはシンボリック実行。パケットの各バイトを「まだ値の決まっていない記号」として扱う、仮想の BPF マシンなの。パケットのバイトは 8 ビットのビットベクタ、アキュムレータ(A)とインデックス(X)は 32 ビットの値、それに M[0-15] のスクラッチメモリを持っていて、レジスタは 0 で初期化されるよ。命令をこのルートに沿って記号のまま実行すると、ADD みたいな演算がそのまま数式の足し算に置き換わっていくの。

3 つめが Z3。Microsoft の定理証明器で、集まった制約を渡すと「その条件を全部満たすバイトの値」を解いてくれるの。たとえば BPFDoor の例だと、こんな制約になるんだって。

0x86DD == Concat(pkt_12, pkt_13)   # IPv6 の EtherType
0x11   == pkt_20                   # UDP
0x35   == Concat(pkt_56, pkt_57)   # 宛先ポート 53 (DNS)

最後に、Z3 が解いたビットベクタの答えを scapy に渡して、Ethernet・IP・UDP のヘッダまでちゃんと組み立てた本物のパケットに変換するの。IPv4 ならバージョンフィールドや IHL、IPv6 なら別のバージョン値、フラグメントフラグやポート番号のチェックも、全部この制約解決でまとめて面倒を見てくれるんだ。

このツールは filterforge という名前で、GitHub で公開されているよ。

まとめ

• BPF マルウェアを起こす「マジックパケット」を自動生成するツールの話(出どころは Cloudflare の Blog)
• BPFDoor のような 100 命令超のフィルタを、手作業の何時間から数秒へ短縮
• 仕組みは「最短経路探索 + シンボリック実行 + Z3 での制約解決」で、scapy で本物のパケットに組み立てる
• ツールは filterforge として GitHub で公開されている

マルウェア解析やインシデント対応をやっている人、それに「シンボリック実行と SMT ソルバでこんなことができるんだ！」ってワクワクするエンジニアに刺さる 1 本だよ。