Milestone 6.5 Complete: Linux Internal Contract Validation
M6.5 is a validation milestone. Instead of adding new features, we systematically verified that Kevlar implements the undocumented behavioral guarantees that real Linux software depends on — the contracts between kernel and userspace that aren't in any man page but that glibc, systemd, and GPU drivers all assume.
The core idea: compile a C test, run it on Linux and Kevlar, compare output. If they disagree, the kernel has a bug.
What we built
19 contract tests across five categories, validated on both Linux
(host) and Kevlar (QEMU). Each test exercises a specific kernel
contract and prints CONTRACT_PASS or CONTRACT_FAIL with a diagnostic.
tools/compare-contracts.py — test harness that compiles tests with
gcc (host) and musl-gcc (Kevlar), runs both, compares output, and
reports PASS/DIVERGE/FAIL with timing.
tools/diff-syscall-traces.py — when a test fails, this tool runs
it under strace (Linux) and debug=syscall (Kevlar), aligns the two
syscall sequences, and pinpoints the first divergence. Short-circuits
the "read kernel source for an hour" debugging cycle.
Runtime debug=syscall — kernel cmdline parameter that enables
full JSONL syscall tracing without recompilation. Previously required
KEVLAR_DEBUG=syscall at build time.
Results: 18/19 PASS
| Category | Tests | Pass | Notes |
|---|---|---|---|
| VM | 8 | 8/8 | brk, mmap, mprotect, fork CoW, demand paging, file mmap, TLB flush |
| Scheduling | 4 | 4/4 | getpriority, nice values, sched_yield, fork scheduling |
| Signals | 4 | 3/4 | delivery order, handler context, mask semantics |
| Subsystems | 2 | 2/2 | /dev/null+zero, /proc/self/stat+exe |
| Programs | 1 | 1/1 | fork/exec/wait lifecycle |
| Total | 19 | 18/19 |
The single failure (sa_restart) requires alarm()/setitimer() to
deliver SIGALRM during a blocking syscall — tracked for M7.
Kernel bugs found and fixed
1. brk() returned negative errno — Linux's brk() never returns an
error. On failure it returns the unchanged program break; the caller
detects failure by comparing. Our implementation used ? to propagate
-ENOMEM, which confused musl's sbrk.
2. musl 1.2.x deprecated sbrk() — The musl binary's sbrk(N) was a
stub that always returned -ENOMEM without making a syscall. The
contract test was rewritten to use syscall(SYS_brk, addr) directly.
3. mprotect(PROT_NONE) killed instead of delivering SIGSEGV — The
page fault handler called Process::exit_by_signal(SIGSEGV), killing
the process immediately. The correct behavior is
current.send_signal(SIGSEGV) and return — the interrupt return path
redirects RIP to the user's signal handler trampoline.
4. sched_getaffinity returned 0 — Should return the number of bytes
written to the mask buffer. musl uses this to determine how many bits
to scan; returning 0 made CPU_COUNT() always report 0 CPUs.
5. Missing /dev/zero — Added kernel/fs/devfs/zero.rs, a character
device that returns infinite zeros on read.
6. Missing getpriority/setpriority — Added syscall implementations with per-process nice value tracking.
7. Dockerfile COPY bug — ADD testing/etc/passwd /etc silently
failed in FROM scratch images. Switched to COPY with explicit full
destination paths.
Phase breakdown
- Phase 1: Test harness infrastructure
- Phase 1.5: Syscall trace diffing + runtime debug cmdline + brk/mprotect/getpriority fixes
- Phase 2: VM contract tests (demand paging, file mmap, TLB shootdown)
- Phase 3: Scheduling contracts + sched_getaffinity fix
- Phase 4: Signal contracts (delivery order, handler context)
- Phase 5: Subsystem contracts + /dev/zero
- Phase 6: Program compatibility (fork/exec lifecycle)
What M6.5 enables
Every contract test is a regression gate. When M7 adds /proc files or
M8 adds namespaces, make test-contracts catches any breakage in
existing behavior. The trace diff tool makes diagnosis fast: instead of
printf-debugging, make trace-contract TEST=brk_basic shows exactly
which syscall returned the wrong value.
The known gaps (MAP_SHARED+fork, CFS weights, alarm delivery) are documented and tracked. M7-M10 authors won't discover them the hard way.