Exhaustive checks over oring's construction logic. oring's security is
kernel-enforced (Landlock LSM path-walk + the kernel seccomp BPF VM) — formal
methods at oring's level cannot prove "the cage holds." What they verify is that
oring builds the filter/ruleset it intends, exhaustively, where the
tests/containment_matrix.rs matrix only samples on a real kernel.
| Property | Artifact | Tool | Scope |
|---|---|---|---|
x32 guard is TOTAL — eval == KILL_PROCESS iff arch != AUDIT_ARCH_X86_64 || (nr & X32_SYSCALL_BIT), else ALLOW |
seccomp::x32_guard_total |
Kani (bounded model check on the real Rust) | proven over all 2⁶⁴ (arch, nr); matrix samples 1 cell |
tier masks: write_noexec never grants Execute; no tier grants device-node creation; wx == wn | Execute lattice |
landlock::tests::tier_invariants |
#[test] (finite AccessFs flag domain) |
exhaustive by construction (const-eval, not FV) |
The x32 guard is the one genuinely proof-shaped object in the tree: a frozen,
hand-assembled 7-instruction cBPF blob outside seccompiler, where a swapped
jt/jf, JSET-vs-JEQ, wrong offset, or RET fall-through is a silent bypass no
sampled test reliably catches.
Opt-in — not in CI (Kani is minutes/harness):
make verify # cargo kani --harness x32_guard_total
cargo test --lib # the tier_invariants + interpreter corner checks (fast, in the normal suite)- "The cage holds." The Landlock LSM and the kernel seccomp BPF VM are the enforcement TCB.
- Denylist completeness. Whether §5 chose the right syscall / ioctl / flag set is a threat-model judgment, not a theorem — the dominant residual risk, covered by review + the matrix, not by any proof.
- seccompiler's lowering. We verify oring's own cBPF (the x32 guard); the
SeccompFilter → BpfProgramcompilation is Firecracker's TCB, not re-proven. - W^X as a whole / pipeline ordering. Completeness assertions over the kernel syscall surface and integration properties — tests, not theorems.