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

# スクラッチメモリ 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))] 制約の最初の部分は、リンク層BPF命令を扱う際に有効なイーサネットIPパケットを構築することを保証するために追加されたものです。「If」文は、検出されたプロトコルに基づいて特定の制約を適用します: IPv4ロジック (0x0800): pkt_14 & 240 == 64: バイト14はIPヘッダーの開始位置です。0xF0マスクは上位4ビット（バージョンフィールド）を分離し、バージョンが4（0x40）であるかをチェックします。 pkt_14 & 15 == 5: 0x0Fは下位4ビット（IHL - インターネットヘッダー長）を分離します。これにより、オプションなしの標準サイズであるヘッダー長5（20バイト）が義務付けられます。 IPv6ロジック (0x86dd): pkt_14 & 240 == 0x60: バージョンフィールドがバージョン6（0x60）であるかをチェックします。 異なる値がチェックされている後半部分を見ると、ネットワークパケットの具体的な値を確認できます: 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パケット ###[ IPv6 ]### version = 6 tc = 0 fl = 0 plen = 0 nh = UDP <-- UDPプロトコル hlim = 0 src = :: dst = :: ###[ UDP ]### sport = 0 dport = domain <-- ポート53 len = 0 chksum = 0x0 このように新しく作成されたパケットは、さらなる研究や、ネットワークをスキャンしてこれらのインプラントの存在を特定するために使用できます。 実際に試す 特定のBPF命令セットの動作を理解するのは、面倒で時間のかかる作業になる可能性があります。ここで使用した例は合計16命令だけですが、200命令を超えるサンプルに遭遇したこともあり、それを理解するには少なくとも1日はかかったでしょう。Z3ソルバーを使用することで、この時間をわずか数秒に短縮でき、ACCEPTされるパケットへのパスだけでなく、そのパケットの骨組みも得られるようになりました。 コミュニティがBPFベースのインプラントの解析を自動化するのを支援するため、filterforgeツールをオープンソース化しました。ソースコードと使用例は、GitHubリポジトリで確認できます。 この研究を公開し、アナリストがBPF命令を理解するのに費やす時間を短縮するツールを共有することで、この形式の自動化をさらに発展させる研究を促すことを願っています。

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

背景や根拠まで確認しますか？

調べる

選ぶ

サイト