Eliminating TOCTOU Path Traversal in Python with Kernel-Enforced Containment and Lean 4 Formal Verification

A developer built PathFence, a zero-dependency, pure-Python path containment library that replaces the standard realpath-then-open idiom with kernel-enforced confinement using openat2 with RESOLVE_BENEATH and RESOLVE_NO_SYMLINKS on Linux 5.6+, component-by-component openat with O_NOFOLLOW on macOS and older Linux, and reparse-point inspection on Windows. The library's decision function is formally verified in Lean 4, with theorems specifying exactly when a path is allowed, and a command-line tool exposes the proven function to any language. The author notes PathFence is v0.1.0, experimental, has had no human security review, and is not a sandbox because its decision is lexical.

When building AI agents, MCP servers, archive extractors, or multi-tenant web backends, confining file operations to a designated directory is critical. Yet the standard Python idiom for path validation—normalizing with os.path.realpath or Path.resolve , checking a string prefix, and then calling open —is fundamentally vulnerable to TOCTOU race conditions. To solve this without requiring C extensions or sacrificing performance, I built PathFence : a zero-dependency, pure-Python path containment library backed by OS kernel primitives and mathematically verified in Lean 4 . A path-confinement check for tools that let an AI agent or any untrusted caller read and write files, written and proven in Lean 4. You give it the directories the caller may use, optionally directories inside them it may not use and a requested path. It answers allow with the resolved path, and the allowed root it is under deny with the resolved path or reject with a reason . Lean theorems state exactly when it allows, and a command-line tool makes the proven function usable from any language. bash $ pathfence check --allow /tmp/allowed dir -- /tmp/allowed dir malicious/secret ../x a/../b {"input":"/tmp/allowed dir malicious/secret","decision":"deny","path":"/tmp/allowed dir malicious/secret"} {"input":"../x","decision":"reject","reason":"escapes"} {"input":"a/../b","decision":"allow","path":"/tmp/allowed dir/b","root":"/tmp/allowed dir","rel":"b"} Status: v0.1.0, experimental. No human security review yet. PathFence is not a sandbox. The decision is lexical. It looks only at the path string, never at the file system. A symlink, a race between the check and the open, a hard link, a mount or a case-insensitive file system… Consider the classic validation pattern found in thousands of production codebases: VULNERABLE: Classic TOCTOU race condition real root = os.path.realpath root real target = os.path.realpath os.path.join root, untrusted path if not real target.startswith real root + os.sep : raise PermissionError "Path traversal detected" An attacker can swap a path component with a symlink right here with open real target, "rb" as f: data = f.read Between the moment os.path.realpath inspects the filesystem and the moment open resolves the path again in the kernel, a local attacker or concurrent process can replace an intermediate directory with a symlink pointing to /etc or another sensitive location. Because the check and the use are two separate operations on path strings, the containment guarantee evaporates under concurrency. sequenceDiagram participant App as Python Process participant Kernel as OS Kernel / VFS participant Attacker as Concurrent Attacker App- Kernel: 1. realpath "/sandbox/work/data.txt" Kernel-- App: "/sandbox/work/data.txt" - Prefix OK Attacker- Kernel: 2. rename & symlink "/sandbox/work" - "/etc" App- Kernel: 3. open "/sandbox/work/passwd" Kernel-- App: Returns file descriptor for /etc/passwd PathFence shifts the root of trust from mutable path strings to pinned directory file descriptors . Every operation resolves relative to an open directory handle using OS-level flags that forbid symlink traversal and upward escape at the kernel level. php graph TD Input "pathfence.safe open / Workspace" -- Lex "Lexical Normalization & Windows Reserved Name Check" Lex -- Platform{"Platform Kernel Strategy"} Platform -- |Linux 5.6+| Openat2 "openat2 syscall + RESOLVE BENEATH / NO SYMLINKS" Platform -- |macOS / Older Linux| StepWalk "Component-by-component openat + O NOFOLLOW + fstat" Platform -- |Windows| WinHandle "Reparse Point Inspection + GetFinalPathNameByHandleW" Openat2 -- Result "Verified File Descriptor / Stream" StepWalk -- Result "Verified File Descriptor / Stream" WinHandle -- Result "Verified File Descriptor / Stream" On modern Linux kernels, PathFence invokes the openat2 2 syscall directly via ctypes with four strict resolution flags: RESOLVE BENEATH : Prevents resolution from escaping above the root directory file descriptor. RESOLVE NO SYMLINKS : Rejects all symbolic links anywhere in the path. RESOLVE NO MAGICLINKS : Blocks procfs magic-link traversal such as /proc/self/fd/ . RESOLVE NO XDEV : Prevents crossing mount-point boundaries. O NOFOLLOW Walk On macOS, BSD, and older Linux kernels, PathFence pins the root directory with O RDONLY | O DIRECTORY | O NOFOLLOW and walks each path segment one at a time using openat ..., O NOFOLLOW . At each step, it verifies fstat device and inode identities to detect concurrent directory replacement. On Windows, PathFence blocks reserved device names such as CON , PRN , AUX , NUL , COM1 - COM9 , and LPT1 - LPT9 , NTFS Alternate Data Streams containing : , trailing dots or spaces, and UNC/device prefixes. It inspects FSCTL GET REPARSE POINT to reject junctions and mount points, and verifies the final handle path via GetFinalPathNameByHandleW . Unit tests and fuzzing can catch bugs, but they cannot prove the absence of edge cases across infinite path combinations. PathFence includes a complete formal specification written in Lean 4 under the formal/ directory. We model path components, depth tracking, lexical normalization, and step-by-step directory resolution, proving 15 theorems with zero sorry placeholders and zero custom axioms : | Theorem | Verified Security Property | |---|---| | normalize rejects escape | Any component sequence whose cumulative depth drops below zero is strictly rejected. | | normalize preserves containment | Every accepted path resolves strictly within the subtree rooted at the pinned base. | | symlink free walk stays in root | Inductive proof that a symlink-free O NOFOLLOW walk can never transition outside the root boundary. | | normalize idempotent | Normalizing an already normalized path yields the exact same result. | | beneath composable | Sub-workspaces created via subworkspace transitively preserve parent containment guarantees. | Beyond opening files, Workspace confines the entire file lifecycle—including mkdir , unlink , rmdir , rename , listdir , and crash-safe atomic write —inside the pinned boundary. python import pathfence from pathfence import Workspace One-liner safe open with pathfence.safe open "/var/sandbox", "notes/hello.txt", "r" as f: print f.read Full lifecycle confinement for AI agents or file processors with Workspace "/var/sandbox" as ws: ws.mkdir "output", exist ok=True ws.atomic write "output/result.json", b'{"status": "verified"}' Sub-workspaces are mathematically guaranteed to stay inside the parent with ws.subworkspace "output" as sub: data = sub.read bytes "result.json" Because PathFence uses direct syscall bindings in pure Python, security comes with virtually zero latency penalty. Benchmarked over 100,000 iterations on Linux 6.8: openat2 fast path realpath + open at 3.9 μs PathFence requires Python 3.9+ and has zero runtime dependencies. pip install pathfence Check out the repository, inspect the Lean 4 proofs in formal/ , and let me know your thoughts in the comments bash $ pathfence check --allow /tmp/allowed dir -- /tmp/allowed dir malicious/secret ../x a/../b {"input":"/tmp/allowed dir malicious/secret","decision":"deny","path":"/tmp/allowed dir malicious/secret"} {"input":"../x","decision":"reject","reason":"escapes"} {"input":"a/../b","decision":"allow","path":"/tmp/allowed dir/b","root":"/tmp/allowed dir","rel":"b"}