Verifying the Linux kernel's isolation code: user namespaces, a proof, and a patch

In two earlier posts we wrote about our work on Linux kernel hardening: verifying the Binder driver in Rust and rewriting and verifying the UVC camera driver's descriptor parser. This post is about the next target: the kernel code that isolation depends on.

In short, here is what we've found and learned in this work:

• Just by writing the specification, we found a defect in the parser and sent a patch upstream,
• We mapped which kernel functions make isolation decisions and chose the user-namespace ID-mapping table as our first verification target,
• We proved its safety properties and injectivity in Lean 4 (89 theorems proved, with seven lemmas still open),
• We tried handing the specification work to Claude Code, which failed in an instructive way, and that failure became benchmark material,
• And we hit a bug in Aeneas that is now fixed upstream.

The work is public at https://github.com/runtimeverification/linux-isolation-spike.

Why this code

Most containers, most sandboxes for AI agents, most "run this untrusted thing safely" products on Linux come down to the same small set of kernel mechanisms: namespaces, capabilities, seccomp, cgroups, mount isolation. The products differ. The kernel code underneath does not.

If that code has a bug, the product on top cannot fix it.

So instead of looking at one sandbox product, we looked at what all of them share. We wanted to know which kernel functions actually make the isolation decisions, and whether any of them are small enough to prove correct.

The inventory

We started by mapping the surface. The result is INVENTORY.md: nine subsystems, each with the functions that enforce isolation, the line in the source where they do it, the security property they are responsible for, and a short note on why sandboxes depend on it.

Two things came out of the inventory that we did not expect

First, io_uring has changed. Two words of background. seccomp is the kernel mechanism that lets a process restrict which system calls it may make, and sandboxes use it to cut the syscall surface down to a short allowlist. io_uring is a different way of talking to the kernel: instead of one system call per operation, a process puts a batch of operations (reads, writes, network sends, driver commands) into a ring buffer and the kernel executes the batch. seccomp sees the one call that submits the ring and nothing inside it. So allowing io_uring under seccomp means allowing everything in the batch, and most sandboxes block io_uring outright.

Since kernel 7.0, io_uring has its own filter for the operations in the batch, written in the same classic BPF language seccomp uses (io_uring/bpf_filter.c). A sandbox can now allow io_uring under a policy. But the validator behind that policy is a fresh copy of seccomp's validator, not shared code. It has the same opcode allowlist and differs in one constant. Nobody has verified the copy. If you build sandboxes, this is worth knowing. We consider this our next target.

Second, the ID-mapping table in kernel/user_namespace.c is the deepest node in the whole graph. Task identity, idmapped mounts, file capabilities and the admission policy for new namespaces all go through it.

Picking a target

ROADMAP.md scores seven candidates on size, purity, arithmetic density, consequence, translatability through our toolchain, and whether anyone has verified it before. The ID-mapping table won.

Here is what it does. When a container starts, the runtime writes lines like "0 100000 65536" into _/proc/PID/uid_map_. That line says: uid 0 inside the container is uid 100000 on the host, and so on for 65536 ids. Every permission check the kernel makes for that container looks up an id in this table. "Root in the container, nobody on the host" is literally this table.

If two container uids could map to the same host uid, a process would hold a host identity it was never given.

What we proved

We reimplemented the table code in Rust, extracted it to Lean 4 through Charon and Aeneas, and proved properties about it. The full list, with every assumption each theorem rests on, is in VERIFY-REPORT.md. Here is short version:

• Safety: the lookup and write paths do not panic, terminate, never read out of bounds, and never read the slots that growing the table past five extents destroys. That is 28 theorems.
• Injectivity: on a published table, two container uids cannot resolve to one host uid.
• Round trip: mapping a uid out and back gives the original uid or "not mapped", never an unrelated id.
• Preservation of well-formedness by the write path is reduced to two lemmas that are still open.

Seven lemmas in total still carry Lean's sorry. They are listed by name in OPEN_CHALLENGES.md with what each one needs.

What we did not prove matters as much. The kernel publishes the table lock-free, with a write barrier on one side and a read barrier on the other. A sequential model cannot see that protocol, and our toolchain cannot check it. Every theorem is about a table already in memory. If there is a real bug in this code, that is where it would most likely be.

What would check it is a different kind of tool. The kernel ships its own memory model, LKMM, in tools/memory-model, together with herd7, which takes a small litmus test (here: the writer's two stores with the smp_wmb() between them, the reader's two loads with the smp_rmb() between them) and enumerates every outcome the model allows. That is the right tool for the four accesses in question, and it is a day of work, not a research project. For the whole write path under concurrency one would need a model checker with a weak memory model, such as Dartagnan or CBMC, or a concurrent separation logic like Iris.

The bug we found, and how

While writing the specification we had to read the parser that turns the _uid_map_ text into table entries. It reads each number with _simple_strtoul()_, which returns a 64-bit value, and stores it in a 32-bit field:

extent.first = simple_strtoul(pos, &pos, 10);

Nothing checks whether the value fits. So we tried it on a running kernel. Write to the uid_map of a fresh user namespace, read it back:

The write succeeds. The kernel installs a different mapping than the one requested and reports no error.

This is not a security bug: the truncated values are legal ids and every later check still applies to them. But a runtime that computes id ranges and gets one wrong ends up with a table it did not ask for and no way to find out. That is a class of bug the kernel could catch with a simple validation check.

We sent a two-patch series to LKML: parse each field with kstrtou32() so out-of-range values are rejected with -EINVAL, plus a selftest for all three fields. Eric Biederman, who wrote the original parser, reviewed v1 and suggested kstrtou32() over our first attempt. v2 is at https://lore.kernel.org/all/20260930112854.373184-1-natalie.klaus@runtimeverification.com and is under review.

Notice how this was found. Not by the proof. By reading the code closely enough to write a spec for it, seeing something odd, and spending five minutes testing it. The verification work forces that kind of reading. Bugs turn up at every stage of the pipeline, not only at the end, and each spike so far has found them in a different place: fuzzing for UVC, specification for this one.

A note on tooling: benchmarks and more findings

We used Claude Code to build most of the 89 theorems. That saves a lot of time and costs nothing in trust: every proof it produces is checked by the Lean kernel. Where it failed was two levels up: reading logic across several source files, and making specification decisions.

Four times during this spike the assistant stated a property of the kernel confidently, and four times it was wrong. Three examples. It read the integer parser across three files and concluded that very large literals saturate and get rejected; on the 6.8 kernel we tested they wrap modulo 2^64 instead, and only a measurement showed the difference. It read the no-wrap check first + count <= first and stated the bound as 2^32; brute force over the boundaries showed it is 2^32 - 1, one bit stronger, which closed an ambiguity we had flagged as open. And it argued that the overlap check guarantees distinct keys for the reverse-sorted array; it does, but on the wrong values, because the sort key is rewritten after the check runs. The last one turned a premise into the target's central theorem. Each was caught by running the kernel, or brute-forcing the arithmetic, rather than reading the source.

We wrote more about this in our The proof is in the spec blog post: proof search is getting automated fast, but the specification has to be right, and that is the part an unsupervised model gets wrong.

We now mark any claim that comes from multi-file source reasoning as unverified until it has been checked empirically. This experiment also left us with benchmark material: pairs of wrong statement, corrected statement and proof, taken from real kernel code, plus seven open lemmas with no published answer.

One more side effect: a five-line Rust program crashed Aeneas at the version we pinned. We reduced it, filed an issue with the reproducer, and the maintainer opened a fix the same day.

What is next

The remaining steps are described in the roadmap: agreement of the two lookup paths, the admission policy, and differential fuzzing against the C to test the three assumptions the proofs route to testing rather than proof. The second target we would pick is the io_uring validator: proving it equivalent to seccomp's would tell sandbox authors whether the new filter layer inherits an audited allowlist or a fresh one.

If you have code you'd like to see verified, get in touch with us at contact@runtimeverification.com!