Verifying the Linux kernel's isolation code: a policy bypass in io_uring's sandbox filter

In our previous post we inventoried the Linux kernel’s isolation layer: the nine subsystems covering mechanisms used to secure containers, microVM guests and AI-agent sandboxes, and verified the first of them, the user-namespace ID map. That first target gave 89 proved theorems (injectivity, round trip, no stale reads after the map grows), and writing its specification exposed a parser that silently truncated 64-bit values into a 32-bit field; the fix is now in vfs.git for 7.4. This post is about the second target and what unfolded over the four days after we started it.

This post is more technical than the previous ones in the series: it goes into the kernel code, the reproducer and the timeline. If you want only the outcome: we found a policy bypass, the fix was in mainline within a day of reporting, and the rest of this post is how it happened.

Picking the target

Classic BPF (cBPF) is a small instruction language for filtering rules. seccomp uses cBPF programs to restrict system calls; io_uring uses them to restrict operations submitted through its ring. Before a filter is installed, a validator checks that the program is well-formed and safe to execute.

From the nine components we chose the classic-BPF validators. Two reasons. Since kernel 7.0 io_uring carries its own cBPF filter mechanism, added so that containers can restrict io_uring where seccomp cannot see into the submission ring. Its validator is a near-verbatim clone of seccomp’s, never independently verified. New code that copies old code is where mismatches live. And a validator bug is a security bug by construction: it is the trust boundary.

The method is the one we have used throughout the series. Reimplement the C in Rust, confirm equivalence by differential testing against the real kernel, extract to Lean 4 through Charon and Aeneas, prove properties. This time the first phase alone produced the result.

Phase 0: inventory

We asked Claude Code (running Opus 4.8) to trace the full admission path for both consumers, function by function with file and line, and to write a line-by-line diff of the two validators. The two are byte-for-byte identical in source apart from one constant: the size of the context struct the filter reads (64 bytes for seccomp, 40 for io_uring). Compiled, they differ in three immediate values, the constants baked into the instructions: the context-size bound and two length rewrites. So far, no bug.

The inventory also covered the other side: not only what the filter reads from the context struct, but which kernel code writes each field there, and under what condition. For io_uring, a per-opcode populate hook copies request data into the fields a filter can inspect. For IORING_OP_CONNECT, the hook copies the destination port and address out of the user’s sockaddr. That is where the mismatch was.

The bug

A sockaddr_in6 is 28 bytes, but the last four are optional. The IPv6 stack accepts a 24-byte address, because the port and the address are already inside those 24 bytes; only sin6_scope_id is missing:

/* include/uapi/linux/in6.h */
struct sockaddr_in6 {
  unsigned short  sin6_family;    /* bytes  0..2  */
  __be16      sin6_port;  /* bytes  2..4  */
  __be32      sin6_flowinfo;  /* bytes  4..8  */
  struct in6_addr sin6_addr;  /* bytes  8..24 */
  __u32       sin6_scope_id;  /* bytes 24..28 */
};

/* include/net/ipv6.h */
#define SIN6_LEN_RFC2133    24

The two sides of the kernel disagree about the minimum. The connect path accepts 24:

/* net/ipv6/tcp_ipv6.c, tcp_v6_connect() */
if (addr_len < SIN6_LEN_RFC2133)
    return -EINVAL;

The filter populate hook requires 28, and leaves the port and address at zero for anything shorter:

/* io_uring/net.c, io_connect_bpf_populate(), before the fix */
case AF_INET6: {
   struct sockaddr_in6 *sin6 = (struct sockaddr_in6 *)ss;

  if (conn->addr_len < (int)sizeof(*sin6))  /* 28 */
        break;
  bctx->connect.port = sin6->sin6_port;
 memcpy(bctx->connect.v6_addr, &sin6->sin6_addr, /* 16 bytes */);

io_uring passes the user’s addr_len to the socket layer unchanged. So a process confined by a CONNECT filter submits the connect with addr_len = 24. The kernel connects to the real destination. The filter sees family = AF_INET6, port = 0, addr = ::. A filter written to deny a specific IPv6 port or address never matches and allows the request. No privilege is needed; ring-level filter registration requires none.

This required multi-file reasoning: io_uring/net.c against net/ipv6/*. In the previous spike, that kind of reasoning was wrong four times out of four until checked by execution. So we did not call it a bug yet. We recorded it as hypothesis H1 and went to test it.

Confirming it

The reproducer runs inside a virtme-ng VM booting the target kernel (7.3-rc6), never on the host. It binds a listener on [::1]:P, registers a ring-level CONNECT filter through the real IORING_REGISTER_BPF_FILTER ABI, and submits the same connect at two lengths. We ran a 2×2 matrix: two filters (deny when port == P, deny when port == 0) against two lengths (28, 24).

The top row is the bypass. The bottom row is the cross-probe: it shows the filter read the port as 0 at length 24, pinning the cause to the unpopulated field rather than anything else. Two runs on fresh ephemeral ports gave identical raw results.

A note on calibration. The first two VM runs printed a self-contradictory matrix. The cause was a display bug in our harness, not the kernel: a shared static buffer aliased by two %s. The raw -EACCES and 0 values had been stable from the first run. We added a raw-integer line to the output and re-ran. Trust the integers, not the rendering.

The fix

One line plus an include: populate once addr_len >= SIN6_LEN_RFC2133. sin6_scope_id stays zero when absent, as it did before. We rebuilt, booted the patched kernel and re-ran the unchanged reproducer. The matrix inverted the way it should: deny_on_P denies at both lengths, deny_on_0 connects at both, and the filter observes the real port at both.

git log -L on the function showed it unchanged since the commit that introduced CONNECT filtering, which shipped in released 7.2. So the fix carries Fixes: 899bea8248ce and Cc: stable # 7.2.

Disclosure, by the clock

We treated it as a security bug in a released kernel and followed Documentation/process/security-bugs.rst.

• Friday 10:18 UTC +3: report, patch and reproducer to security@kernel.org, cc Jens Axboe.
• Friday 15:58: Jens replied, cc security: no embargo needed, send it to the list.
• Friday 16:38: patch posted to io-uring@vger.kernel.org.
• Friday 17:33: “Applied, thanks!”, commit aa5d5f8e5023.
• Monday 15:19: Greg Kroah-Hartman’s automated note that the commit is in mainline and queued for 7.2 stable.

Seven hours from first report to applied. The commit message discloses the AI assistance in prose, as the kernel’s new Documentation/process/generated-content.rst asks: the mismatch was found by Claude Code comparing the populate hook against the IPv6 length checks on our instructions; it drafted the reproducer and the patch; we verified the bypass and the fix in the VM and checked that 7.2 carries the same code. The disclosure was included in the accepted upstream commit, alongside the patch and its test evidence.

What else we checked

The inventory produced eighteen hypotheses. The one with the highest potential impact was H3: whether seccomp’s constant-allow cache, the fast path that skips the filter for syscalls the filter always allows, can disagree with actually running the filter. A disagreement there would be a permanent seccomp bypass. We extracted the kernel’s own emulator and validator verbatim at build time, compiled them in userspace against the tree’s UAPI, and ran a differential fuzz: 1.5 billion (program, arch, nr) emulations, 8.6 billion reference runs, zero divergences. The only “bypass” it found is the intentional uprobe/uretprobe passthrough, documented upstream. Refuted, and recorded as such.

What is not done

No theorem is proved yet. The validators are still to be reimplemented in Rust and extracted to Lean. The remaining hypotheses are on the list. The repository is public now: inventory, diff, hypotheses with verdicts, reproducers, logs.

What we take from it

The bug did not come from reading the validator harder. It came from writing down, for each field the filter can inspect, who fills it and under what condition, and then asking whether that condition matches the one the rest of the kernel enforces. That is specification work. It is where the bugs have come from, in both spikes.