AIエージェントやMCPサーバーにローカルのファイル操作を任せる機会が急増しています。しかし、Python標準のパス検証には検査と実行の時間差を突かれる致命的なセキュリティリスクが潜んでいます。
本記事では、OSカーネルのシステムコールと定理証明支援系である Lean 4 による形式検証を組み合わせ、パストラバーサルやシンボリックリンク攻撃を根本から遮断する純粋Pythonライブラリである PathFence の設計と実装を解説します。
従来のパス検証が抱えるTOCTOU脆弱性の罠
特定のディレクトリ配下のみアクセスを許可したい場合、多くの開発者は os.path.realpath() や pathlib.Path.resolve() でパスを正規化し、startswith() や is_relative_to() で文字列比較を行ってから open() を呼び出します。
- # 危険な実装例：Check-then-UseによるTOCTOU脆弱性がある
- real_root = os.path.realpath(root)
- real_target = os.path.realpath(os.path.join(root, user_path))
- if not real_target.startswith(real_root + os.sep):
- raise PermissionError("Escape detected")
- f = open(real_target, "rb") # 検査からここまでの数マイクロ秒の間にシンボリックリンクへすり替え可能
+ # PathFenceによる安全な実装例：OSカーネルレベルでアトミックに解決して開く
+ import pathfence
+ f = pathfence.safe_open(root, user_path, "rb")
上記の旧実装には、TOCTOUと呼ばれる検査時と使用時の競合状態が存在します1。realpath() で安全性を確認した直後かつ open() が実行される前のわずかな隙間に、攻撃者が途中のディレクトリやファイルを外部へのシンボリックリンクに置き換えると、境界を突破されてしまいます。
PathFenceのアーキテクチャとOS別カーネル防御
PathFence は、パス文字列ではなくファイルディスクリプタを信頼の基点とすることでこの問題を解決します。外部のC拡張に一切依存しない Pure Pythonかつゼロ依存 でありながら、ctypes 等を介してOSの低レイヤーAPIを直接呼び出します。
-
Linux環境でのアトミック解決
Linux 5.6以降ではopenat2(2)システムコールとRESOLVE_BENEATH | RESOLVE_NO_SYMLINKS | RESOLVE_NO_MAGICLINKS | RESOLVE_NO_XDEVフラグを使用します。カーネル内部でルートディレクトリからの脱出やシンボリックリンクの追跡が即座に拒否されるため、わずか1回のシステムコールで完全なTOCTOU耐性を実現します。 -
POSIXフォールバックとmacOS環境
openat2が利用できない環境では、ルートディレクトリをO_RDONLY | O_DIRECTORY | O_NOFOLLOWで開き、各パス要素を1段階ずつopenatとO_NOFOLLOWで辿ります。さらにfstatによってデバイスIDやinodeを検証し、オープン後のディレクトリ移動やすり替えを検知します。 -
Windows環境での多層防御
予約デバイス名であるCONやNULやCOM1等、NTFS代替データストリームである:、末尾のドットやスペース、UNCパス等を厳格に拒否します。さらにFSCTL_GET_REPARSE_POINTによるジャンクションやシンボリックリンクの検出と、GetFinalPathNameByHandleWによるハンドルベースの実体パス検証を行います。
Lean 4による形式検証：なぜ数学的証明が必要なのか
セキュリティライブラリにおいて「テストが通っている」だけでは、未知のエッジケースを完全に排除できません。そこで PathFence では、定理証明支援系である Lean 4 を用いてパス正規化と境界判定アルゴリズムの仕様をモデル化し、いかなる入力に対しても境界外への脱出が不可能であることを数学的に証明しています2。
具体的には、ルートからの相対的な深さを表す状態遷移モデルにおいて、任意のパス要素列 $P = (c_1, c_2, \dots, c_n)$ を処理した際の深さ関数を以下のように定義します。
\forall k \in \{1, \dots, n\}, \quad \text{depth}(c_1, \dots, c_k) \geq 0 \implies \text{ResolvedPath}(P) \subseteq \text{Subtree}(\text{Root})
リポジトリ内の formal/ ディレクトリには、sorryや独自公理を一切使わずに完遂された15個の定理が収められています。
| 定理名 | 証明されているセキュリティ特性 |
|---|---|
normalize_rejects_escape |
親ディレクトリへの遡上により深さが負になるパスは必ず拒否される |
normalize_preserves_containment |
正規化を通過したすべてのパスはルート配下の部分木に厳密に含まれる |
symlink_free_walk_stays_in_root |
シンボリックリンクを許可しない段階的探索は常にルート境界内に留まる |
normalize_idempotent |
正規化関数を2回適用しても結果は変わらず、二重正規化による不整合が起きない |
beneath_composable |
サブワークスペースの境界制約は親ワークスペースの境界制約を推移的に満たす |
クリックでWorkspaceを用いた安全なファイル操作コード例を展開
# PathFenceにおけるWorkspaceを用いた安全なファイル操作ライフサイクル
from pathfence import Workspace, PathTraversalError, SymlinkError
# ルートディレクトリをピン留めしてWorkspaceを初期化
with Workspace("/var/app/sandbox") as ws:
# 1. 安全なディレクトリ作成とアトミックなファイル書き込み
ws.mkdir("user_data", exist_ok=True)
ws.atomic_write("user_data/config.json", b'{"role": "guest"}')
# 2. 安全な読み込み
data = ws.read_bytes("user_data/config.json")
# 3. 境界外への脱出試行はカーネルおよび正規化層で即座にブロック
try:
ws.read_text("../../etc/passwd")
except PathTraversalError as e:
print(f"Blocked traversal: {e}")
パフォーマンス：数マイクロ秒で動作する超高速設計
セキュリティとパフォーマンスはトレードオフになりがちですが、PathFence はカーネルAPIを直接叩くことで極めて低いオーバーヘッドを実現しています。Linux 6.8環境での10万回イテレーションによるベンチマーク結果は以下の通りです。
| 実行パス・操作内容 | 平均レイテンシ | 1秒あたりの処理回数 |
|---|---|---|
openat2 高速パスでのファイルオープン |
3.6 μs | 約277,000 ops/sec |
O_NOFOLLOW フォールバックでの1階層探索 |
9.8 μs | 約102,000 ops/sec |
O_NOFOLLOW フォールバックでの3階層探索 |
17.4 μs | 約57,000 ops/sec |
realpath + open による従来の非安全な方法 |
3.9 μs | 約256,000 ops/sec |
Linuxの openat2 が使える環境では、従来の非安全なコードよりもむしろ高速な3.6マイクロ秒で完全な境界防御が完了します。
まとめと導入方法
AIエージェントのツール実行基盤や、ユーザーからアップロードされたアーカイブの展開処理、マルチテナント環境のストレージ操作において、PathFence はわずか1行でカーネルレベルの安全性を提供します。
pip install pathfence
ぜひお手元のプロジェクトに導入し、フィードバックやStarをいただけると嬉しいです。
Zennでも記事を書いています。