Skip to main content

Crate seacomb

Crate seacomb 

Source
Expand description

§seacomb: formally verified seccomp compiler

crates.io docs.rs

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:

§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.

Modules§

cbpf
Abstract syntax and semantics of a subset of cBPF accepted by seccomp.
prop
Top-level theorems about the semantics of policies and cBPF.

Macros§

cond
Parses a Rust-like expression into a Cond.
expr
Parses a Rust-like expression into an Expr.
policy
Parses a policy into a Result<Policy, Error>.
rule
Parses a rule into a Rule.

Structs§

Event
A model of a syscall event generated by the kernel (i.e., seccomp_data).
InstallFlags
Options for installing a policy, named after libseccomp’s SCMP_FLTATR_CTL_* flags.
Policy
A set of rules with default actions for no-match and bad-arch cases.
Rule
A policy rule, which applies an action to a syscall event if certain condition is satisfied.

Enums§

Action
Actions that a policy can take on a syscall event.
Arch
All supported architectures.
BinOp
A binary operator in the policy language.
CheckError
An error while validating a filter policy.
CmpOp
A comparison operator in the policy language.
CompileError
Possible errors when compiling a policy to cBPF.
Cond
Boolean expressions in the policy language.
Error
All possible errors when creating or using policies.
Expr
Arithmetic expressions in the policy language.
PrimType
Primitive types in the policy language.
Syscall
All syscall identifiers from Linux v7.0.

Traits§

ToCond
A Rust value that cond! accepts as an operand.
ToExpr
A Rust value that expr! accepts as an operand.