seacomb 0.1.0

A formally verified seccomp compiler.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

# seacomb: formally verified seccomp compiler

`seacomb` is a Rust library for compiling and enforcing
[seccomp](https://man7.org/linux/man-pages/man2/seccomp.2.html) policies,
which is a Linux kernel feature for filtering/intercepting syscalls and sandboxing.
For example, [Chrome](https://chromium.googlesource.com/chromium/src/+/main/sandbox/linux/README.md)
and [Firefox](https://wiki.mozilla.org/Security/Sandbox/Seccomp)
use seccomp to sandbox the processes that render web pages,
and [Docker](https://docs.docker.com/engine/security/seccomp/)
and [systemd](https://www.freedesktop.org/software/systemd/man/latest/systemd.exec.html#SystemCallFilter=)
use it to restrict containers and services.

By declaring rules in a similar style to [libseccomp](https://github.com/seccomp/libseccomp),
`seacomb` compiles and registers these rules using a *formally verified* compiler to cBPF.

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

// Allow any syscall when no rule matches.
let mut filter = Filter::new_native(Action::Allow).unwrap();

// Make write to stderr (fd 2) fail with EPERM.
filter.add_rule(Action::Errno(1), Syscall::Write, vec![ArgCmp::eq(0, 2)]).unwrap();

// Kill the process on execve.
filter.add_rule(Action::KillProcess, Syscall::Execve, vec![]).unwrap();

#[cfg(target_os = "linux")]
{
    filter.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));
}
```

Supported architectures: x86, x86-64, 32-bit ARM (little-endian), and AArch64.

## What has been formally verified

`seacomb` is developed using [Verus](https://github.com/verus-lang/verus),
an automated program verifier for Rust.

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](https://github.com/seccomp/libseccomp/issues/139):
    64-bit `<`, `<=`, `>`, `>=` argument comparisons were generated incorrectly,
    so filters could be bypassed.
  - [#148](https://github.com/seccomp/libseccomp/issues/148):
    the optimizer merged code blocks that were not actually duplicates,
    which broke Tor's sandbox.
  - [GHSA-4q85-33p6-j5g6](https://github.com/seccomp/libseccomp/security/advisories/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.

To verify the proofs, [install Verus](https://github.com/verus-lang/verus/blob/main/INSTALL.md),
and run:
```sh
cargo verus verify
```
Without verification, this crate is also completely compatible with `cargo`.

## Testing

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

To run all tests on all supported architectures, or on one:
```sh
python3 tests/run.py
python3 tests/run.py aarch64
```

## Related work

- [Jitk: A Trustworthy In-Kernel Interpreter Infrastructure](https://dl.acm.org/doi/10.5555/2685048.2685052)
- [libseccomp](https://github.com/seccomp/libseccomp)
  (Rust binding: [libseccomp-rs](https://github.com/libseccomp-rs/libseccomp-rs))
- [seccompiler](https://github.com/rust-vmm/seccompiler)