seacomb: formally verified seccomp compiler

seacomb is a Rust library for compiling and enforcing seccomp policies, which is a Linux kernel feature for filtering/intercepting syscalls and sandboxing. For example, Chrome and Firefox use seccomp to sandbox the processes that render web pages, and Docker and systemd use it to restrict containers and services.

In seacomb, you can write seccomp policies as readable, type-checked rules, and a formally verified compiler turns them into a cBPF filter that provably does exactly what you wrote.

use seacomb::*;
use std::io::Write;

let policy = policy! {
    // Allow any syscall when no rule matches.
    default allow on native;

    // Make write to stderr (fd 2) fail with EPERM.
    errno(1) write(fd, _, _) if fd == 2u32;

    // Kill the process on execve.
    kill execve(_, _, _);
}.unwrap();

#[cfg(target_os = "linux")]
{
    // Compile and install the policy.
    policy.install().unwrap();

    assert!(std::io::stdout().write_all(b"Hello from stdout!\n").is_ok());
    let err = std::io::stderr().write_all(b"Hello from stderr!\n").unwrap_err();
    assert_eq!(err.raw_os_error(), Some(1));
}

For larger examples, see how Docker's default profile and Flatpak's filter can be written in seacomb. On Linux, cargo run --example docker -- COMMAND [ARGS..] runs a command under Docker's profile.

Currently, seacomb supports Linux syscalls on x86, x86-64, 32-bit ARM (little-endian), and AArch64.

What has been formally verified

seacomb is written in pure Rust and verified using Verus, an automated program verifier for Rust.

To verify the proofs, install Verus, and run:

cargo verus verify

Without verification, this crate is also completely compatible with cargo.

Formally verified properties:

• Compiler correctness: seacomb's policy compiler always produces cBPF filters equivalent to the source policy, relative to the formal semantics of policies and cBPF in src/spec. This rules out miscompilations like these in libseccomp:
  • CVE-2019-9893: 64-bit <, <=, >, >= argument comparisons were generated incorrectly, so filters could be bypassed.
  • #148: the optimizer merged code blocks that were not actually duplicates, which broke Tor's sandbox.
  • GHSA-4q85-33p6-j5g6: merging overlapping 64-bit comparison rules let denied syscalls through.
• Determinism: A policy picks exactly one action for each syscall.
• Chaining: Installing multiple policies is equivalent to evaluating them in order, verified against the kernel's precedence and tie-breaking rules.

Futhermore, in seacomb's policy language, rule conditions are type-checked against each syscall's C signature, and the compiler correctness theorem implies that compiled filters ignore unused high bits. This prevents bypasses where a filter compared all 64 bits of a 32-bit argument:

• CVE-2019-10063 in Flatpak (CVSS 9.0 critical).
• CVE-2019-7303 in snapd (CVSS 7.5 high).

Testing

QEMU is a prerequisite for testing (install with, e.g., brew install qemu).

To run all tests:

python3 tests/run.py
python3 tests/run.py aarch64 # Only run for aarch64

Trusted computing base and how AI agents are involved

Formal verification helps reducing the amount of code we need to trust, by machine-checking the executable code against simpler formal/mathemtical specifications and properties.

Using this method, this repo implicitly has two kinds of code/proofs: (a) trusted specifications that need to be carefully edited and manually audited, and (b) executable code and proofs that do not need to be trusted.

Part (a) is mostly contained in src/spec/, including the syntax and semantics of seacomb's policy DSL, cBPF, and type signatures of all supported syscalls. These specs were written with assistance of AI agents, but heavily audited and understood manually.

Part (b) notably includes the compiler implementation and its correctness proofs in src/compiler.rs and src/compiler/. They are mostly generated using Claude Code and Codex, but their correctness against the specs in src/spec/ is automatically verified by Verus.

There are some other components that are in a "gray area," which are verified for simpler properties like panic-freedom and termination, but they are not verified to be functionally correct or lacking formal specs. The assembler in src/asm.rs is an example, which is used for converting an AST of cBPF program to actual binary formats used by the kernel. The actual installaion of the policies (Policy::install_with_flags and RawProgram::install_with_flags) is also not verified and marked unsafe since it requires low-level syscalls.

Related work

• Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
• libseccomp (Rust binding: libseccomp-rs)
• seccompiler