Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The test bench

The bench is how every claim in this book is tested. It builds the real kernel, loader and programs, packs and signs a boot bundle, boots it under QEMU, and judges what appears on the console, over SSH and on the network, from outside the guest. It also runs host tests and source checks. It is part of the system under tenet 6 (the tenets), held to the same standard of simplicity as the kernel: one tool, tools/testbench, and one file per case in tests/.

How to use it

cargo testbench                 # every case but those run only by name
cargo testbench timer           # cases whose name contains "timer"
cargo testbench --arch rv64     # one target
cargo testbench --list          # names and descriptions, those run only by name marked
cargo testbench sched-latency --sweep 1..20 --jobs 4   # one case, a seed sweep, 4 boots at a time
cargo testbench --exact sched-latency   # that case alone, not sched-latency-tcg too
cargo testbench --prebuild target/prebuilt   # build every case's pieces once, both widths
target/prebuilt/testbench --prebuilt target/prebuilt --exact --arch rv64 timer   # run from them
./test                          # the same, from the repository root

The exit status is non-zero if anything fails. Each run keeps its boots’ console logs, SSH transcripts, disk images and captures in a directory of its own, target/testbench/run-<pid>-<time>/, and target/testbench/last names the latest. Only the newest few run directories are kept, so --keep-failed DIR copies a failing boot’s console log, its second boot’s and its sessions’ into DIR as <arch>-<case>.smp<N>…, where they outlive the run (host:testbench::a_failing_boots_logs_are_kept_under_its_jobs_name). Runs may overlap in one worktree: each packs the kernel cargo reports for its own features, never the shared target/ path another run may have rebuilt. A case the host cannot run (no RustSBI firmware, no OpenSSH) fails and says what is missing; --allow-skip reports it as skipped instead. Every run boots the vendored RustSBI prototyper: scripts/build-bios.sh builds it for both widths, or RUSTSBI_PROTOTYPER and RUSTSBI_PROTOTYPER_RV32 name the images. There is no fallback to QEMU’s own firmware.

PathWhat
tools/testbench/the bench: builds, injects programs, boots QEMU, judges the console, sessions and network
tests/*.tomlthe cases, one per file (tests/data/: files they read; tests/keys/: SSH test keys)
tests/programs/no_std programs that run inside Redoubt: the log server, victims, attackers, checkers
tests/net/the network clients and the judge that the net cases start under init, and the host test that checks each net case’s manifest against its case file

A filter takes every case whose name contains it, so cargo testbench timeouts runs timeouts-tcg too; --exact takes the one case it names, run only by name or not, and refuses a name no case has. A run stages each userland disk it boots in a directory named for the recipe’s whole path, as two recipes may share a file name.

Building once

Status: built · tested: host:testbench::an_index_survives_its_rename_and_names_its_tree, host:testbench::the_fingerprint_follows_the_trees_changes, host:testbench::an_exact_filter_runs_one_case, host:testbench::userland_recipes_of_one_name_stage_apart, host:testbench::a_build_asked_for_again_in_a_run_is_not_run_again

A run builds what it boots: cargo run of the bench, then a cargo build of the kernel, the loader and each program, a check that costs about 30 ms when nothing changed and waits on the build directory’s lock while another run compiles, then the bundle and any userland disk. Alone that is a quarter of a second before QEMU starts; beside a train of other runs, each waiting on the others’ compiles, it was most of a case’s time. A run makes each distinct build once, and a case asking for one already made takes its binary without running cargo, since a run takes the tree as it was when it began: the kernel and the loader are built once per profile and target, not once per case. --prebuild DIR does it once for every case:

DIR/testbench            the bench, copied from the --prebuild that made the directory
DIR/redoubt-sshd-host    Redoubt's sshd on its host platform, for the loopback cases against it
DIR/<arch>/index.json    the tree's fingerprint; each case's pieces, or its build's results
DIR/<arch>/...           cargo's copies, the bundles, the userland disks

Every boot and build case is built for each of its targets (--arch for one; a filter for some), the widths one after the other in one process: two userland stages at once would compile the same Mix project in its one build directory. A build that fails is kept as the case’s result, printed by the prebuild and again by each run of the case, as is a build case’s verdict. Each width is built in a directory of its own and renamed into place when done, so a run reading the old pieces never sees a half-written one.

DIR/testbench --prebuilt DIR then runs cases as cargo testbench does, but takes each boot case’s bundle, loader and userland disk from DIR and runs no cargo and packs nothing; what stays per boot is what each boot must have afresh: the QEMU probe, its disk (a disk recipe is still packed for every boot) and its devices. A case starts in about the time QEMU takes to start. The index names the workspace that made it and the tree’s fingerprint: its commit, its uncommitted changes and its untracked files that git does not ignore, taken when the prebuild starts and again before each width is put in place, which a change in between refuses. A run from a directory another workspace made is refused naming it, and so is one from this tree before a change, never a silent test of old code, so the directory is made again after any change. What git ignores is not in the fingerprint: the pinned toolchains (toolchains/, or where BEAMLET_TOOLCHAINS points) and a Mix project’s _build (userland/shell/_build/); a change to those needs a prebuild by hand. The other kinds run as always, with their own cargo where they have one (host-tests). scripts/jobs.mk makes the directory (prebuilt) and runs every case target from it when it is there (“On a shared host” under the case file).

Verdicts

What a case passes on

Status: built · tested (9)
  • bench:bench-console-after-expect
  • bench:bench-poweroff-missing
  • bench:bench-qemu-early-exit
  • bench:rustsbi-boot
  • host:testbench::a_killed_bench_leaves_no_qemu
  • host:testbench::a_line_is_shown_without_its_control_sequences
  • host:testbench::a_qemu_lacking_an_option_is_named
  • host:testbench::a_shown_line_keeps_its_own_prefix_first
  • host:testbench::forbid_matches_the_line_as_it_came_or_as_shown

A boot case passes when every expect pattern matches a console line, in order, no forbid pattern ever matches, and the boot ends as the case says. Four patterns are always forbidden: PANIC, TEST FAILED, WARNING: INSECURE, and ipd: an invariant broke, the line ipd says if a socket’s buffers ever fail to fit its heap, reachable only at a residual of its sizing that no case reaches (ipd). After the last expect, and any sessions, the bench keeps reading for 50 ms (1 s in a checked build), so a forbidden line right after the last expected one still fails the case. With poweroff = true it reads instead until QEMU exits, and requires the exit status the case names (0 by default; 255 for an SBI system failure). A boot that ends, or times out, while an expect is still waited for fails with the first failure a program printed ([name] FAIL) ahead of the line it waited for, since that is the cause. The bench starts QEMU with Linux’s parent-death signal asked for between fork and exec, so a bench killed at its timeout, even outright, takes its QEMU with it and leaves no guest running to skew the next run.

A console line is matched as a terminal shows its text: with its control sequences removed. A CSI sequence goes whole, any other escape with the character after it, and every other ASCII control character but tab, DEL among them, and trailing space after them. Nothing is drawn, so a carriage return does not take the line back to its start, and the prefix the log server or consoled gave the line stays first: no program’s text can be shown in front of it. expect, expect_after, [[input]] and the poke’s after, and distinct_across_boots match the shown line. forbid, the four always forbidden, and the checks on the reporter’s PASSED and DONE lines see both the line as it came and as it is shown, so a forbidden word split by a sequence is caught, and so is a raw sequence a case forbids ('\x1b'). The console log keeps every line as it came, and distinct and a post_check read that log.

Before a width’s first boot the bench runs that width’s QEMU with -version, and a QEMU that cannot run fails every boot case at once with its complaint (skips them, with --allow-skip, as a missing firmware does). A guest that ends before it prints a line, or whose QEMU exits with a failing status, fails with QEMU’s exit status and the last lines of its stderr, which go to the console log too; one that printed and then died fails as it did, with QEMU’s exit status.

In-guest programs print through the log server and finish with <NAME> TEST PASSED or <NAME> TEST FAILED; attack programs end with attempts done instead. The log server starts every line it prints for a client with the sender’s badge, as the kernel reports it, on every path that takes client text: [pid N] for a badge below 0x100, and [badge N] for any other. The tester numbers a case’s programs by their place, 2 on (it is 2), at most 16, and gives each its place as its badge, and every badge a test program mints is 0x100 or more, so a minted badge can never print as a place and forge a case program’s line (tests/programs/src/logsrv.rs). Lines without a prefix come from the kernel, the loader, the log server’s own fixed templates, or a program that owns the UART.

Rule F (trusted verdicts)

Status: built · tested: bench:bench-attack-forgery, bench:bench-reporter-mismatch, bench:logsrv-badge-forgery, bench:bench-init-reporter-forged, bench:init-console-forgery

A verdict comes only from a party the attacker cannot impersonate. The console does not say who wrote a line, and an attacker can print anything, including another program’s PASSED, so an attack case passes only on a line the attacker cannot write:

  • The kernel or the loader, refusing: a line with no [pid prefix, with KMAIN or a later stage forbidden so that no program ever ran (loader-rejects-*), or an anchored line the kernel prints at boot before any program starts, which a relayed line cannot match (kernel-wx).
  • A victim that owns what is attacked and still has it afterwards: the log server still hears UART input after every attempt (irq-attack); a victim inspects its pages (mem-attack, uaf-lent-page).
  • The log server’s DONE. The program in init’s place owns the console: it holds the console’s device handles, and every other program’s text reaches the UART only through it, prefixed with the sender’s [pid N] or [badge N]. A victim, or with no victim the attacker once it is done, calls the checker’s done(); the log server prints one [server] done: line naming the caller by the badge the kernel delivers with the call, which the tester chose, and powers off. A case that names a reporter passes only if exactly one line starts [server] done: and it names the reporter’s place; any other such line fails it, as does one in a case with no reporter.
  • consoled‘s prefix, under init. In a servers’ case the real init holds the UART until consoled starts, and consoled starts every line written through a child’s connection with that connection’s [con N], so only init’s lines are bare. The bench learns the reporter’s N from init’s bare announcement and takes a TEST PASSED only under it (the servers’ cases under init).
  • A sole first program judging the kernel. In map-fixed-attack, write-only-attack and process-attack one program runs, alone: it holds the console and the reset, makes every refused call itself, and prints its own unprefixed ok: lines. It is trusted because nothing else runs that could impersonate it, and because what it attacks is the kernel, not another party in the case: each ok: line reports a kernel result it read back (the error, the budget’s usage, the mapping left in place), and the case also needs a clean power-off, which a fault in the program prevents. The residual: a kernel bug that corrupted this program’s own memory could make it misreport, and no second party would see it.

Program order. A program that attacks another program, or the fixture, is never the first. In a case with several programs, the first is the trusted tester (the log server, unless the case is one of the sole-program cases above), and the case’s programs list fixes the order of the rest, so which place and which handles each program gets is the case’s choice, never a race.

Every verdict pattern is anchored with ^ and pinned to its writer, with a comment beside it saying why it cannot be forged. The attacker’s own lines may be required as progress (so a refusal for the wrong reason fails) and forbidden as evidence of a breach, but are never the verdict. Where the attacker itself reports to the checker, the case shows only that the system survived, and its description says so (“verdict: survival only”).

Cases

The case file

Status: built · partly tested: that an unknown field or table is refused is read from the code, not attacked by a case · tested: bench:bench-console-after-expect, bench:bench-poweroff-missing, host:testbench::a_case_out_of_the_whole_run_runs_only_by_name, host:testbench::host_tests_route_only_to_a_requested_workspace_and_forward_features, host:testbench::an_oracles_tools_must_be_on_the_path, host:testbench::sweep_seeds_are_ranges_or_lists, host:testbench::a_sweep_is_refused_before_anything_builds, host:testbench::sweep_boots_have_their_own_files, host:testbench::the_join_prints_in_seed_order_and_counts_failures, host:testbench::a_sweeps_boots_hold_disjoint_slices_of_the_lease, host:testbench::two_boots_at_once_run_in_different_slots, host:testbench::smp_is_one_list_or_a_list_per_width, host:testbench::a_boot_runs_its_widths_own_hart_counts, host:testbench::a_fanout_is_of_values_files_or_tests, host:testbench::a_job_passes_fails_or_runs_past_its_deadline, host:testbench::a_cpu_list_counts_its_ranges, host:testbench::a_failing_boots_logs_are_kept_under_its_jobs_name, bench:rt-miri, bench:model-mutations

A case is one TOML file. Paths in it are relative to the workspace root, and an unknown field or table is an error, so a misspelling cannot silently drop a check. The one exception is a programs entry (and a bundle file’s from): its forms are told apart by their keys, so an extra key in one is ignored rather than refused (tools/testbench/src/case.rs).

description = "What this proves"
arch = ["rv64", "rv32"]      # targets to run on
whole_run = true             # false: run only when the filter is the case's name
kind = "boot"
programs = [                 # the first in init's place, the rest started by it
    "log-server",                                  # a binary of the test programs
    { package = "my-crate", bin = "my-server" },   # any workspace binary, built for the target
    { package = "my-crate", bin = "my-probe", features = ["probe"] },  # built with these features, in a target directory of its own
    { package = "beamlet-redoubt", bin = "beamlet", workspace = "userland/otp" },  # a binary of a workspace of its own, built there
    { path = "prebuilt/thing.elf" },               # or a prebuilt ELF
    { erlang = "path/to/module.erl" },             # an Erlang module, compiled by the pinned erlc (a bundle file's)
    { otp = "io" },                                # an OTP module's .beam from the pinned toolchain (a bundle file's)
    { zeros = 6291456 },                           # that many zero bytes, an entry only its length matters for (a bundle file's)
]
smp = [1, 4]                 # one boot per hart count (default [1]), or per width (below)
keep_smp = true              # the counts stand under `--smp N` (a comment says why)
timeout_secs_smp = 90        # the bound under `--smp N` instead (a comment says why)
memory_mib = 32              # guest RAM (default 256)
memory = false               # true: stop an init guest and measure its servers' painted stacks
timeout_secs = 60            # default 60; fractions allowed
icount = "shift=3,sleep=off" # virtual time: 2^3 ns per guest instruction, the RTC on it too
qemu_seed = 1                # pin the guest's randomness (QEMU -seed)
kernel_features = []         # extra kernel features
debug_assertions = false     # true: a checked build of the kernel and the loader
expect = ['regex 1', 'regex 2']   # each must match a console line, in this order
forbid = ['regex']                # must never match
poweroff = false             # true: the guest must power off after the last expect
reporter = "checker"         # the program whose done() is the verdict (rule F)
launch = false               # true: boot `./launch --system`'s own QEMU command line (launch-*)
post_check = "sched_oracle"  # a host-side check of the console after a passing boot

[[input]]                    # typed on the console once a line matches `after`
after = "claimed irq 10"
send = "xyz"

A boot case also takes allow_panic, tamper_bundle, sign_bare_archive, short_initrd, device_tree, distinct_across_boots and distinct (hostile inputs), [[file]] (bundle files), [disk] and [net] (devices), [[session]] (SSH sessions), must_fail (self-checks), and poweroff_status: the QEMU exit status a poweroff case requires (0 by default; 255 for an SBI system failure, which a rejection case asks for).

smp is one list for every width the case runs on, or a list per width: smp = { rv64 = [1, 2], rv32 = [1] } boots rv64 at one and two harts and rv32 at one, for a case whose count on one width is a finding of its own, so that the other width’s run does not go into a copy of the case. A width the map leaves out runs the default, [1]; a key that is not one of the case’s arch, and an empty list in either form, are refused before anything builds (a case leaves a width out of arch, never boots it zero times). jobs.mk leases the width’s own largest count, and --smp N replaces a map as it does a list.

With icount, QEMU runs the guest at a fixed instruction rate, skips idle time to the next timer deadline and puts the RTC on the same clock (-rtc clock=vm). A time a case asserts is then a count of guest instructions (at shift=3, 1 ms is 125,000), the same on any host however loaded. It does not make a run repeat on its own: QEMU fills the guest’s boot RNG seed from host entropy on every boot, the kernel draws PIDs from it, and that moves every later event. qemu_seed = N pins it (QEMU -seed N, which fills the device tree’s /chosen/rng-seed), and with icount a run then repeats exactly. The bench prints the seed before the result, and TESTBENCH_QEMU_SEED=M replaces the pinned seed of every case that has one, to replay a run or to sweep. An idle guest’s clock skips to its next armed timer deadline, sleep on or off: with sleep=off at once, so while blkd waits for the host’s virtio completion the next deadline is its own 10 s request timeout, the read fails and the volume is poisoned, which is why a case with a disk keeps sleep on (icount = "shift=3"); with sleep on the skip was measured too, once the guest idled with no timer armed nearer than a lease’s deadline 1,337 s ahead, which it reached inside a 295 s boot, the lease destroyed at it as its rule says. So a case under the virtual clock whose guest can idle while a lease it means to outlive the case is live either runs on the host’s clock or expects the lease’s end; with sleep on such a run repeats closely, not exactly, and a time a case is held to comes with a sweep’s spread. --sweep SEEDS runs one case once per seed (1..20, or 3,5,9), from one build, and prints each seed’s result in seed order and a summary line; each boot keeps its files in seed-<N>-<arch>/ inside the run’s directory. --jobs J boots up to J seeds at once. Under scripts/q the sweep cuts the job’s port lease (q run --ports N, REDOUBT_PORTS=lo-hi) into J disjoint slices from its start, one per concurrent boot, and each boot forwards on its slice alone, so no two meet on a port; a lease shorter than J times the case’s forwards (its forward ports and its poke) is refused before anything builds, naming the --ports to ask for, and no boot is ever handed a slice another holds. One boot at a time takes the range’s start, as a single run does; outside q each boot asks the OS for its ports, with that path’s race. --jobs is never the default; what a result under it is worth is the shared-host rule below. A timing gate runs one pinned seed and states its target from a sweep of seeds (responsiveness).

Which cases run in guest time. A boot case runs under icount = "shift=3,sleep=off" unless something in it waits on the host, and 145 of the 226 do. What keeps a case on the host’s clock: a disk or a userland disk (38 cases; the rule for a disk is above); host sockets, a forward, a poke, a peer or a dial (8); input the host types on the console, [[input]] (4; under icount the rv32 UART lost a burst of it); and a run whose purpose is the host’s time (asid-cost-host, sched-latency-tcg, timeouts-tcg, and smp-evict-mttcg, smp-shootdown-mttcg, console-one-writer, sched-lock-contention-4-mttcg and beamlet-schedulers-mttcg, which need QEMU’s multi-threaded TCG; its one-hart twin beamlet-schedulers-one-hart runs in guest time, since on one hart what it measures is the instructions two schedulers’ switching costs). Several harts do not keep a case on the host’s clock: under icount QEMU runs the harts in turn on one host thread, and a hart waiting for the kernel lock halts rather than spending its turn (R78 (fair kernel entry)). One case reads no host clock and stays on it for now: redoubt-ipc fails under icount on both widths (189 calls abandoned of the 256 it wants), until that is understood. A timeout_secs is the bench’s bound, never a measurement: a case in guest time is given at least four times its slowest pass alone on either width, rounded up to 10 s, and more than any wait of its own program, so that a stuck check reports itself; it is never raised without a measurement. bench-poweroff-missing keeps its 3 s: there the deadline is the oracle, the timeout its must_fail waits for.

On a shared host. cargo testbench runs its cases one after another; what may run beside the invocation, another invocation in its own run directory, a seed under --jobs, a build, is decided by the clock each case measures with. A boot case with icount measures in guest time: the host’s load does not move a guest time, so its pass, and a failure the guest itself reports, are verdicts whatever ran beside it (a pinned seed adds only that the run repeats exactly). Its one exposure to the host’s clock is timeout_secs, the bench’s deadline for the boot: a case that only ran out of that deadline beside other work has no verdict, and is rerun alone. A boot case without icount (68 of them) keeps the host’s clock in the guest, so load lengthens every wait it makes: its pass is a verdict unless what it expects is a timeout or a bound on a time, and a failure beside other work has no verdict until it fails alone. Every bound a case states on a time, a step’s, a probe’s or a notice’s, is the box’s under one condition, one whole bench at a time with QEMU its alone for the run and any other work on the machine host-only and off the bench’s cores: measured under it, held to under it, and a bound missed beside another boot is no verdict until the case misses it under it. A [net] table by itself changes neither class: an empty one gives the guest a card that reaches nothing, and binds no host port. A table with a forward, a poke, a peer or a dial puts host sockets beside the boot, in wall time: its dials retry until the case’s deadline, so a pass stands and a failure is rerun alone, as for any host-clock wait. Its host ports come from the job’s lease under scripts/q (q run --ports N, the forwards and the poke; the job sees REDOUBT_PORTS=lo-hi, a range no other lease holds, and the bench takes the forwards’ ports from its start), so two such boots run side by side without meeting on a port; a sweep’s --jobs J boots are J such boots inside one lease, each on its own slice of it (the sweep paragraph above: the lease must hold J times the case’s forwards, or the sweep is refused); what remains under q is a stranger to q taking a pooled port between the daemon’s probe and QEMU’s bind, which fails that boot loudly, as before. Outside q the bench picks a forwarded host port by binding and releasing it before QEMU takes it, so two such boots at once may race for one port, and there the rule asks that two such boots not run at once; a lost race fails the boot rather than hiding (QEMU cannot bind). An ssh-loopback case is the same kind of case: its sshd runs in inetd mode through ssh‘s ProxyCommand and binds no port, its guest’s stdio is a virtio-serial port, and the kind’s probe (one loopback session with a 30 s connect timeout) runs once before any case and decides whether the host can serve the kind, never a case’s verdict. So a loopback case that asserts no time (13 of the 14) passes as a verdict, and a failure that is only its deadline is rerun alone. A case that measures with the host’s clock is a verdict only alone: the rule asks that no other invocation and no build run beside it, and for a whole bench scripts/jobs.mk holds that rather than asks it, through the scheduler’s qemu lock (the scripts/q paragraph below). Those are a host-tests case whose crates’ tests assert a wall-clock bound (redoubt-rt, redoubt-client, redoubt-keyd and redoubt-consoled do; redoubt-ipd, redoubt-model and testbench only read the clock), which no tolerance would make load-proof; a boot case whose bound is a ratio of two host times (sched-lock-contention-4-mttcg: a stalled vCPU thread lengthens a wake but not the search it is counted in; beamlet-schedulers-mttcg: a stalled vCPU thread lengthens one of the two runs it compares, and on the quiet set’s four cores alone its one-hart twin read 81 to 95 for a ratio that is 94 in guest time, which is why that twin runs under icount); a case whose expectation is a timeout (bench-ssh-guest, and bench-ssh-loopback-deadlock, whose must_fail is the mark it never gets); and a host-clock case with a VM session whose console goes through the hub’s hold and which must still be alive after a hold boundary (the steward’s SSH session cases): a stall of the guest of a second or more at the boundary reads, inside the guest, as the server’s silence past its promise, so the session’s completion call times out and the session ends as at Ctrl-D. A host-tests case whose crates assert no bound measures nothing with the host’s clock; it may run beside other work, and the rule asks that its test threads be bounded then (RUST_TEST_THREADS), so that it cannot oversubscribe the host by itself. A bound the platform under test keeps on the kernel’s clock is such a bound too when the kernel is the fake’s and its clock the host’s: beamlet-lookup-host’s system tests once let a bind’s ATTACH_US and a call’s timeout run against a fixture server under a whole bench’s load, and about one train in two the host’s second ran out first; they hold the fake’s clock now (Fake::hold_clock), so each such bound, a retry’s RETRY_US and a file operation’s FILE_WAIT_US included, is a step the test takes once the state it waits on is reached, and the ten-second waits are gone with the race. Its console.rs tests held the host’s clock the same way — one, input_nobody_reads_holds_no_idle…, read the idle’s 200 ms deadline against the host and under load a read’s submit timeout ran out, queued the read, and woke the idle early — and hold the fake’s clock too now, each deadline a step, the console server’s session bound crossed by the ticks that cross it. A tick is taken only once every other thread of the fake is in a wait, and a thread a change has woken counts as waiting only when it waits again: before that, a tick could fall between a server’s answer and the waiter’s hand-over of it whenever the host had not yet run the waiter, and on a loaded host the busy-retry test’s retry fell past its last tick and the platform’s end waited for it on a clock nobody moved, about one ./test-shell run in ten. The kinds that boot nothing (build, fmt, no-cruft, the size and unsafe budgets, the docs checker, the Elixir oracles) have no clock, and are verdicts anywhere, but for a timeout_secs: as for a boot, a host-tests job or an Elixir case that only ran out of its deadline beside other work is rerun alone.

scripts/q applies that rule for a whole machine. It is one scheduler process that leases real cores: q run --cores N -- <command> waits for N free cores, runs the command pinned to them (taskset; cargo’s jobs and RUST_TEST_THREADS follow the lease) and returns its exit code; --quiet runs a host-clock case on a reserved core set (the daemon’s --quiet, by default its last four cores, "" for none), one such case at a time, while the rest of the machine keeps working; --ports N leases N host ports from the daemon’s pool (23000-23999, below the ephemeral range; a port a stranger holds is skipped) and hands them to the job as REDOUBT_PORTS=lo-hi, so a [net] case’s forwards never meet another’s, where before one machine-wide --lock net ran every such case in turn (train 40: 30 cases, 12,360 s of summed waiting, 1,353 s once for a 0.5 s case); a lease ends with the client process, so a killed job frees its cores and ports, and a restarted daemon adopts the jobs still running, their pins and their ranges, until they end (scripts/q-test checks the lease on a daemon of its own). --lock NAME takes a named lock exclusively and --share NAME the same lock shared: sharers run beside each other, an exclusive taker runs alone among the jobs naming the lock, and from the moment it waits no new sharer starts ahead of it, so a stream of sharers cannot hold it off. The lock qemu is how the condition every bound on a time holds under, one whole bench at a time with QEMU its alone, is held rather than asked: a whole bench (jobs.mk’s cases-*, quiet-* and all-* targets, and a set holding every case of the boot, quiet or net class) takes it exclusively as a lock-only lease (q run --cores 0 --lock qemu, the qemu-held target) before its first case and keeps it to the make invocation’s own exit, the lease’s command ending when make’s pid is gone, so the hold ends with the lease by any exit path, a killed make or a dead train included, never by a trap or a file; a second whole bench waits for the first. Every single boot case, a case with an arch run by name or in a smaller set, a sweep by hand (q run --share qemu --cores M -- cargo testbench --smp N) and launch‘s boot take it shared: single boots run beside each other as before, and one started while a whole bench holds the lock waits, printing one line naming the holder (its tenant, its name and its checkout) and since when, then runs when the hold ends; it never fails for the wait. Under the whole bench’s own make its cases take no lock, since the make holds it, and a case that boots nothing (no arch: the host-tests, Elixir, build, formatting and docs cases) takes none: what it measures the lock does not protect, and the quiet set keeps the host-clock host tests off the bench’s cores. A restarted daemon adopts a running hold as it adopts cores and ports (Q_LOCK and Q_SHARE in the job’s environment), q ls names the holder and since when, and a daemon from before the shared take runs a --share job unlocked and says so, as it does for ports (restart it). scripts/q-test checks the lock as it checks the lease: the sharers beside each other, the waits, the line, the hold’s end with its client and its adoption. A job’s scratch goes to $REDOUBT_TMP, by default .tmp at the checkout’s root, which git ignores, so removing the checkout removes it; the job gets it as TMPDIR too, since a host’s /tmp may be a RAM filesystem a sweep would fill. scripts/jobs.mk names every case as a make target (rv64/<case>, cases-rv64, quiet-rv64, build-rv64, prebuilt, docs) and picks the class for it: a boot takes one core per guest hart, a host-tests case or an Elixir case four (an Elixir case is mostly the build of beamlet and the model’s trace writer, under that lease but outside its deadline, so it stays in this class: Elixir oracles), a case with a fanout two for its build while each of its jobs asks q for its own, and the host-clock cases go quiet. A case target runs that case alone (--exact), from target/prebuilt when its width is there (building once), else through cargo testbench; its output is target/jobs/<arch>-<case>.log, and a failing boot’s console and session logs are kept beside it (--keep-failed), so a transcript is never lost to the run directories’ pruning; the scheduler oracle judges a kept console log again by hand, through its ignored host test (SCHED_ORACLE_LOG=<log> SCHED_ORACLE_ARGS='<the case's post_check arguments>' cargo test -p testbench a_kept_log_judged_again -- --ignored --nocapture). A failing host-tests case’s log holds the test harness’s failures block, from its failures: line: each failed test’s panic and name and the test result line (a block past 400 lines keeps its first panics and the names list), then Cargo’s line naming the test file that failed and how its binary ended, never the warnings Cargo printed last (train 49 kept twelve of those and no test name). A case with no arch boots nothing, so it runs under rv64/<case> alone, and rv32/<case> does nothing. Case targets may run at once (set CASES="..." runs a set on both widths) only while each still takes its own lease, the quiet ones run alone on the quiet set and the [net] ones hold their port leases, as every case target does: the leases, not make, keep the host from being oversubscribed. q ls shows the core map and the queue; q log the recent jobs with the time each waited and ran. cargo testbench --smp N boots every boot case once at N harts instead of its own counts, but a case that keeps them (keep_smp), and bounds it by timeout_secs_smp where a case gives one; since jobs.mk leases a case’s cores from its own counts, such a sweep runs as q run --share qemu --cores M -- cargo testbench --smp N, M at least N.

The heavy host cases. What each costs on the 24-core build host, and the deadline it has (each a measured run and a third, unless its row says otherwise):

CaseIts costtimeout_secs
model-mutations175 jobs, one per mutation, in release, one core each; a mutation’s steward families stop at 500 seeds, and the three they catch only after many seeds are caught first by directed scenarios (mutations). About two and a half minutes of wall, the build included; the longest job R2NoWaitCap’s, 18.7 sper job, 25
model-host-testsone cargo test on four cores, every model test but the mutations, the steward families and their coverage check: under two minutes, the build includednone
steward-model-host-teststhe two steward families at their counts and the check that their coverage table is reproduced (property families), each a job on four cores and threads: under two minutes of wall, the build included; the longest job steward_policy’s, 26 sper job, 35
rt-miri12 jobs, one per file, about 100 s of wall: heap’s 60 to 96 s; connection 25 s; the rest under 10 sper job, 128
elixir-oracles, bench-elixir-oracles-broken-guarda cold build of beamlet and the model’s trace writer, 29 s alone on four cores and up to 46 s beside a bench, outside the deadline (Elixir oracles); then the scripts, 2.5 and 1.3 s alone, 3.2 and 1.7 s beside two prebuildsthe scripts’, 10: four times elixir-oracles’ alone

A case with whole_run = false is left out of a run with no filter and out of one whose filter is only part of its name; it runs when the filter is its whole name, and --list marks it “by name only”; jobs.mk’s cases-* and quiet-* leave it out too, and its own target runs it. It has one reason: a measurement too long to repeat at every train.

The kinds, and the fields each takes besides description, arch and whole_run:

KindWhat it doesIts fields
bootboots the kernel with programs as its first processes and judges the runthose above
buildonly checks that a package compiles for each target: coverage for what the bench does not boot; with forbid_in_binary, that the binary holds none of the byte strings named (self-checks)package, features, debug_assertions (the checked profile instead of the release), forbid_in_binary, must_fail (the build’s error, or the scan’s finding)
host-testsruns cargo test on the host for the named workspace packages, for what no boot can reach (a constant the loader and the bench share is right in the machine’s eyes even when it is wrong); with miri, under nightly Miri. These cases are the bench’s only host tests; cargo test --workspace is not run, though it compiles. The kernel and the test programs have no host tests (test = false on their targets)packages, tests (the test files to run; default all), miri, workspace, features, tools, filter (only the tests whose names contain one of these), skip (tests left out, by part of their name), profile (Cargo’s, such as release), fanout (each, env, values, cores, vars, late, late_cores), timeout_secs (each fanned job’s deadline)
ssh-loopbackruns [[session]]s against a host OpenSSH server with no guest, to check the session runner on its ownauthorized (the test keys the server accepts), [[session]], timeout_secs, host_key (default: the server’s own), server_log (patterns each of which must match a line of the server’s own log), must_fail
unsafe-budgetthe ratchet on unsafe (below)[[budget]]: name, paths, max_unsafe, max_undocumented; [[uncounted]]: path, reason
size-budgetthe ceiling on each trusted crate’s size (below)[[crate]]: name, paths, max_lines
no-cruftthe source gate (below)paths, [[forbidden]] (pattern, unless, within), no_allow_dead, one_definition, definition_paths, [[allow]] (path, rule, reason)
fmtthe formatting gate (below)roots, [[skip]] (path, reason)
elixirruns scripts that check an Elixir oracle on beamlet against the Rust it shadows, each of which must exit 0, on the pinned toolchain (below)otp, elixir, build (commands run first, outside the deadline), scripts (each a path and its arguments), must_fail, timeout_secs (the scripts’ together)

For host-tests, workspace defaults to the repository root and otherwise names a relative directory below it with a Cargo.toml; an absolute path, a path outside the repository or a missing workspace fails before Cargo runs. features defaults to none and passes the named features to Cargo. For example, beamlet-lookup-host runs the VM and Redoubt tests from userland/otp with beamlet-redoubt/fake; beamlet-lookup-cli-host runs separately without that feature, so the two cases do not combine their Cargo features. tools names host programs the tests run as an oracle (erofs-oracle’s mkfs.erofs, fsck.erofs and dump.erofs): each must be an executable on the path, or the case fails naming the first missing, and skips it with --allow-skip, as for any other host lack.

A fanout runs a long case as many jobs instead of one cargo test, one per each: "value", one per line the shell command values prints, each running the case’s one test file with that line in the variable env (model-mutations, one job per mutation, the names cargo run --example mutations prints, in REDOUBT_MODEL_MUTATIONS); "file", one per entry of tests (rt-miri); "test", one per test of every test binary the case builds, by libtest’s own list, each run alone, those filter takes and skip does not (steward-model-host-tests). The bench builds the tests once, first, with no deadline; then each job runs its test binary as cargo test would, from its package’s directory (under Miri, which runs no binary by itself, cargo miri test of the one file), through scripts/q on cores cores of its own (default one), as many at once as the machine has room for. vars are set for every job: a test that spawns its own threads is told how many it has (the model’s MODEL_THREADS), since under q its RUST_TEST_THREADS is the lease’s. Where q does not answer, the jobs run one after another. Each job’s output is a file in <case>/ of the run’s directory, and <case>.log lists every value with the time its tests took; the case passes when every job does, and its failure names each value whose job failed. A job that runs past timeout_secs fails, saying so: a deadline on the cores the job asks for, stretched in proportion when q, once the job has waited, grants it fewer. late names values known to pass only past a bound their test keeps, each with the follow-up that removes it: their jobs run with TESTBENCH_LATE=1, the test’s leave to go past it, and a pass is reported as “caught late, known” in the result and as LATE in the log, never hidden; any other value past the bound, an entry that names no job, and one whose test now passes within the bound fail the case. late_cores gives a late value’s job, the long search, its own count of cores; a {cores} in a vars value becomes the count each job is granted, which q may lower from its ask once it has waited, so a test that spawns its threads runs one per core it holds (the model’s MODEL_THREADS, in model-mutations and steward-model-host-tests). No case names a late value now.

A post_check judges the console after the boot has passed. sched_oracle rebuilds the scheduler’s order from the raw events a tracing kernel prints and checks every pick against its own reading of the rules (scheduling); a limit such as r10_p99_us=30000 bounds a measured cost. Two arguments judge a sibling’s first run: round, that it comes before any other budget is picked twice, and lift-delay, that it comes within a round of what the lift on its parent predicts. A walk-trace kernel’s walks are bounded by their longest, net of the audits inside them (pump_max_us, expiry_max_us, reconcile_max_us), judged before r10_p99_us, so a run whose destruction is over its bound still has its walks judged. gate_harts=2 judges the latency targets on a trace of at most two harts (its F record) and only reports them on more, marked recorded at N harts, not gated: the targets are gated at one hart and two and recorded at four (responsiveness). smp_fence reads only the same trace’s shootdown records: a page made executable was shot down on another hart running its process, which acknowledged (memory). smp_inflight reads only an inflight-trace kernel’s records of each RAM frame’s way through R81 (frames in flight): retired (i, the frame and the process whose entry for it was cleared), each shootdown (s), pending (d), given back to the bitmap (b) and taken from it (o). Each frame is pending only on the hart that retired it and, if it was mapped, only after that hart shot its process down; given back only once pending, so its hart has zeroed it; and never taken in between. A run where no frame from a live space was retired, given back and taken again fails as racing nothing.

Starting a case’s programs

Status: built · tested (7)
  • bench:rng
  • bench:budget
  • bench:budget-carve-attack
  • bench:budget-destroy-kills
  • bench:programs-unknown-budget-attack
  • bench:programs-unknown-program-attack
  • bench:bundle-mapped

The loader loads only the kernel and init (boot), so a kernel case’s first program is packed as the bundle’s second entry and runs in init’s place. It gets init’s handoff: the three budgets, the Reset right, every device and the bundle. It is the trusted tester. When it is the log server, it starts the case’s other programs itself, through the loader stub and from the bundle’s pages, each in a budget of its own carved from system. Each program gets the same slots:

  • slot 1, the boot endpoint: its receive right for the first program started, a send badged with its place for each later one;
  • slot 2, the log endpoint, badged with its place;
  • slot 3, its own budget;
  • slot 4 on, the budgets the case names for it (budgets = ["system"]), in the line’s order.

Its own budget’s handle gives a program nothing it lacks: the pages are already its own to spend, a carve from it comes out of its own share (R7 (carving)), and destroying it ends only the program and what it started (R10 (destruction)), which the tester sees as a killed notice. It lets a program read its own charges and run measured work in a budget it carves. The budget is system-class, as its parent is, so a program may add labels below it; a kernel case has no server those labels could reach.

The builder tells the tester which programs to start, and with which budgets, in one more data entry, programs. It has one ASCII line per program after the first, in the case’s order: the program’s entry name, then the names of the budgets it gets (root, system, users), separated by spaces. The tester reads it from the bundle’s pages, which the loader verified with the rest, and reads every line before it starts anything. It refuses the boot, and powers off, on a line that is not printable ASCII, names an entry the bundle lacks or a budget other than the three, or names a budget twice, and on more programs than system has processes. Each program’s own budget gets an equal share of what system has free (pages and processes) and weight 1,000, a driver’s, so no program’s limits depend on another’s name or order. A case that needs other sizes builds its own tree from the budgets it is given.

The log server badges each program’s handles with the program’s place in the case, 2 on, and names programs by that place, because the kernel draws every PID but the first. A case matches a PID in a kernel line with a pattern. Each program gets an exit endpoint of its own, so the tester tells their notices apart (processes) and prints each under the program’s name and place, with the kernel’s PID beside it.

A program the tester starts holds no device, and every page it has is backed, its stack included: only the process the loader starts has a stack reservation (memory). So a case that needs a device, or a page never touched, runs its program alone in init’s place, where its own budget is root.

init itself never takes a case’s place and has no mode for the bench. The kernel’s cases need root and system, which no program under init may hold (R33 (no server holds a system budget)), so they run a tester in init’s place instead.

The servers’ cases under init

Status: built · tested (5)
  • bench:init-servers
  • bench:init-console-forgery
  • bench:bench-init-reporter-forged
  • bench:init-boot
  • bench:littlefsd-reboot

A servers’ case boots the real init with a manifest of its own, packed as the manifest entry, and its test programs are servers entries in that manifest. They get no budget handle, their own included, as no server does (R33 (no server holds a system budget)). init prints its own lines bare, and consoled starts every other program’s line with its connection id, [con N] with N in 16 lowercase hex digits (consoled). A case’s reporter names a manifest entry, and the bench reads that entry’s connection id only from init’s bare line announcing it, init: started NAME, console N; a second such line in one boot fails the case. A restarted server is announced as init: restarted NAME, console N, and the bench never reads a reporter’s id from that line, so a reporter that restarts cannot pass its case. A case that judges a reboot expects init’s reboot line and then the next boot’s first line, the loader’s. The machine resets in the same QEMU run, with the same disk, and from that line on the bench reads the reporter’s id afresh from the next boot’s announcement, so a case may go on to its verdict in the next boot; still only one TEST PASSED line, in the whole run, may pass it. The case passes only if exactly one line says TEST PASSED and it starts with that [con N] ; any other such line fails it, wherever it came from. Such a case ends at its last expect, which waits for the verdict, since no test program holds the Reset right. The test programs are redoubt-init-programs (tests/init-programs): boot-reader reads a public entry through the root badge at bootfsd its entry is handed, con-forger prints its arguments as lines, and the rest are the servers, clients and drivers of init’s restart cases. Since init restarts a program that exits, each parks when it is done, unless its exit is the point of its case.

The scheduler oracle

Status: built · tested (38)
  • bench:sched-ties
  • bench:sched-capped
  • bench:sched-lock-contention
  • bench:sched-lock-contention-4
  • bench:sched-lock-contention-4-mttcg
  • bench:sched-timer-entry
  • host:testbench::kernel_sections_say_what_the_lock_waits_waited_behind
  • host:testbench::the_driver_wake_is_judged_in_searches_of_its_own_run
  • host:testbench::a_pick_passes_over_only_a_budget_that_other_harts_run
  • host:testbench::the_oracle_decides_whether_a_timer_interrupt_ended_the_slice
  • bench:sched-wake-no-preempt-harts-mttcg
  • host:testbench::a_pick_in_place_is_a_slice_end_that_requeued_its_runner
  • host:testbench::lock_waits_are_reported_per_mille_of_the_harts_time
  • host:testbench::lock_waits_take_the_lock_in_ticket_order
  • host:testbench::a_shootdown_record_is_passed_over
  • host:testbench::a_trace_that_keeps_every_clause_passes
  • host:testbench::each_broken_clause_is_caught
  • host:testbench::a_broken_trace_is_rejected
  • host:testbench::the_models_own_ranks_pass
  • host:testbench::the_models_broken_ties_are_caught
  • host:testbench::lifts_are_recomputed
  • host:testbench::weight_changes_are_recomputed
  • host:testbench::the_floor_and_the_passes_are_checked_on_their_own
  • host:testbench::destructions_are_timed_and_bounded
  • host:testbench::audits_are_subtracted_inside_each_window
  • host:testbench::water_filling_caps_a_budget_at_its_threads
  • host:testbench::a_charged_share_across_harts_is_judged_by_water_filling_net_of_lock_waits
  • host:testbench::a_hart_share_is_judged_of_every_charge_against_water_filling
  • host:testbench::timer_work_billed_elsewhere_in_a_budgets_time_is_bounded_inside_its_share
  • host:testbench::idle_sections_that_found_nothing_are_bounded
  • host:testbench::an_unmatched_audit_fails
  • bench:sched-irq-wake
  • bench:sched-deadline-preempt
  • bench:call-bounds
  • host:testbench::a_device_wake_that_preempts_is_caught
  • host:testbench::a_device_interrupt_bills_its_devices_owner
  • host:testbench::a_deadline_that_does_not_preempt_is_caught
  • host:testbench::call_bounds_hold_each_call_to_its_empty_system_section

The oracle is independent of the kernel’s code: it reads what the queue did (woke, requeued, left, pass changed, picked), never why, and rebuilds the order from the events alone: the lowest pass first; at an equal pass a budget that woke ahead of one requeued; of two that woke, the later kernel entry’s first, and within one entry the lower id; requeued ones in the order they were requeued. On several harts it also reads which budget each hart runs (H) and how many of each budget’s threads wait for a hart (J, those no hart runs): a pick takes the first budget in that order with a thread waiting, and passes over one ranked ahead only if another hart runs it and none of its threads waits, never one it runs itself. A slice’s end that picks where it is (preemption points) records the requeue and the pick of the hart’s own runner, with no H and no J: the oracle counts the preempted thread as waiting, as the round trip’s J counted it, only at a timer interrupt on that hart that requeued the budget, began no destruction and decided the slice over (=), and only for a budget with no other thread waiting; anything else is refused, and the rank clauses judge the pick as any other. One that picks another budget’s thread records that pick inside the interrupt and the hart’s new runner at its return (H), and is judged as any pick. It recomputes each lift and each weight change from the rule, and lets a pass fall only at a weight change. A kernel built with lock-trace, a test feature that implies the trace, also records each wait for the kernel lock’s ticket after the wait (k: the ticket and the sections ahead of it when drawn); a release build carries neither the feature nor the record. The records are written holding the lock, so the waits appear in the order they took it, and the oracle requires that order to be the tickets’, each drawn behind fewer sections than the harts: no wait outlasts the sections queued ahead of it (R78 (fair kernel entry); sched-lock-contention at two harts, sched-lock-contention-4 at four). A kernel built with hold-trace, which implies lock-trace, also records each section of the lock as it is released (h: its first and last tick; then j: its cause, a system call’s number, an interrupt’s or an exception’s code, and the ticks of audits inside it). The oracle reports the sections’ lengths net of their audits, the longest by cause, and splits the lock waits into the part another hart’s section covered (its audits pro rata) and the part with the lock free, the hand-off to the halted waiter. The contention cases carry it and judge nothing by it. fault_section_max_ticks=N bounds the longest section a page fault began, net of its audits (fault-report-bound), and timer_section_max_ticks=N the longest a timer interrupt began and timer_section_p99_ticks=N their p99, the steady entry’s cost, which the few cold sections (a program’s first preemptions) cannot hide a regression of; both are gated up to gate_harts as the latency targets are, since under icount a section on several harts counts the others’ instructions too (sched-timer-entry, at one hart; recorded at two). With the trace beside it, idle_sections_max=<mark>:<N> bounds the kernel sections a hart entered from the idle and left with no record of its own but an audit’s, a lock take that found nothing due and nothing runnable, from the first run of the budget the program marks (the mark’s weight, as a share’s): timer-flood-at-rest‘s two sleepers each sleep a thousand short timeouts on two harts, and a kernel that arms every hart’s timer for a timeout whose payer runs nowhere wakes each hart for the other’s naps too (the hart timer). Where the clock is the host’s, driver_wake_p50_searches=K and driver_wake_p99_searches=K judge the driver wake’s net p50 and p99 against K searches of the same run alone, from the program’s one search alone line, at any hart count (sched-lock-contention-4-mttcg). Three checks read the interrupts’ brackets (preemption points, charging): irq_wake_no_preempt=N needs N device interrupts from user mode that claimed a source, woke one budget and returned to the runner with no pick inside, whose hart’s next pick or interrupt was the runner’s slice’s end (sched-irq-wake), and refuses any device interrupt that began no destruction yet did not return to user mode; irq_billed_to=<mark> needs every device interrupt that claimed a source to charge the budget the program marks after the claim, and lets it charge only that budget and, for its return, the one it interrupted: the owner is the program’s to name, and sched-irq-wake names the boot’s, system; deadline_preempts=N needs every timer interrupt from user mode that destroyed another budget by its deadline to leave for kmain with its runner requeued and the hart’s next event a pick, and N of them (sched-deadline-preempt). With hold-trace, a CALL-BOUNDS line names two windows in the kernel’s ticks, a factor and a floor: for every system call made in the first, its longest section in the second, net of audits, is held to factor times its longest in the first or the floor; a call made in the second alone is reported; at least eight must be judged (call-bounds, R12 (scheduling)). sched-capped runs the model’s capped scenarios (model) on the machine at two, three and four harts, each budget’s share judged as below; hart_shares_from=4 records the shares on a trace of fewer harts, since under icount QEMU’s turns move them, and sched-capped-mttcg judges the two- and three-hart shares where the harts run at once (QEMU’s turns). It is itself checked against the model’s ranks and against traces broken one clause at a time. The tracing kernel is a test build only (R23 (no test channels)).

Elixir oracles

Status: built · tested (5)
  • bench:elixir-oracles
  • bench:bench-elixir-oracles-broken-guard
  • host:testbench::another_version_is_refused
  • host:testbench::the_scripts_share_the_case_deadline
  • host:testbench::the_deadline_starts_after_the_build

An elixir case runs its scripts in order from the workspace root, each judged by its exit status: elixir-oracles runs the steward core’s reference over its traces (the trace encoding) and the wire codec’s vectors. The scripts source userland/otp/tools/oracle.sh, which puts the pinned toolchain on the path and runs a module on beamlet. Before any script the case checks the toolchain: the erl that userland/otp/tools/env.sh puts on the path must be of the OTP release otp (its releases/<major>/OTP_VERSION), and elixir --version must say elixir. A missing or other toolchain fails the case even with --allow-skip, and no must_fail waits for it: an oracle that does not run catches nothing; the dev image carries both, and scripts/setup.sh --with-beam builds both on your own machine. Then the case runs its build commands, each of which must exit 0, together within 600 s, a bound only a hung build reaches (a cold build’s times are below). A failed or late build fails the case as a build, never as the oracle’s timeout, and is never what a must_fail waits for. Both cases name userland/otp/tools/build-oracles, which builds beamlet, the model’s trace writer and the trace checker as the scripts build them, so the scripts’ own builds find nothing to do. With timeout_secs, the scripts together have that deadline, counted from the end of the build, each run under timeout with what the ones before it left; one past it fails the case, saying so, and is never what a must_fail waits for. The build is most of a cold run (29 s alone on four cores), and its time is the host’s load: beside a whole bench, the two cases building the same targets at once on loaded cores, it has taken 46 s. Built, the scripts take 1.3 s (the self-check) and 2.5 s (elixir-oracles), so the deadline measures the oracles alone. The case’s log says what the build and the scripts each took.

Checked builds

Status: built · tested (20)
  • bench:bench-debug-assertions
  • bench:bench-debug-assertions-off
  • bench:boot-profile
  • bench:boot-profile-unverified
  • bench:sched-latency
  • bench:sched-budget-churn
  • bench:sched-exit-churn
  • bench:timer-flood-at-rest
  • bench:sched-exit-churn-mttcg
  • bench:sched-timer-flood
  • bench:sched-carve-return
  • bench:deadline-flood-billed-traced
  • bench:deadline-flood-billed-traced-mttcg
  • bench:deadline-placement
  • host:testbench::audits_are_subtracted_inside_each_window
  • host:testbench::a_hart_share_is_judged_of_every_charge_against_water_filling
  • host:testbench::an_unmatched_audit_fails
  • host:testbench::cluster_credit_is_the_certified_interior_only
  • host:testbench::cluster_lower_witness_counts_the_union_of_outer_bins
  • host:testbench::a_device_interrupt_that_claims_nothing_bills_nobody

debug_assertions = true builds the kernel and the loader (the trusted base, not the programs) with the workspace’s checked profile: release with debug assertions and overflow checks on. It is the same kernel checked harder, not a special build. Three things that are silent in a release build then panic, and every case forbids PANIC:

  • core’s preconditions on raw-pointer calls (slice::from_raw_parts, ptr::read, copy_nonoverlapping): a misaligned or null pointer, which is undefined behaviour and silent in a release build;
  • the kernel’s own debug_assert!s: every error a call returns must be in that call’s row of the error table (the ABI), which budget-syscall-attack exercises over every call and thousands of hostile values;
  • arithmetic overflow, wherever the kernel or the loader does not use a checked or wrapping operation on purpose.

A checked build also runs the kernel’s audits, full scans that check the indexes, frame owners and handle chains after a destruction and when a process object is freed, and the live PIDs, the frame owners and the IRQ index when one of them changes outside a destruction (a process’s end scans all of RAM, about 7 ms under icount). Every scan of a whole table is an audit; the checks a return to user mode or a shootdown makes, a few entries each, are not. They hold the hart while they run, and a release build has none of them. So a latency target or a share, which is measured in a checked build because the scheduler trace needs one, excludes them: an audit neither fills a window nor moves the schedule. The scheduler charges an audit’s time to no budget and moves the running slice’s end past it, so the thread that ran it is picked and preempted as in a release build; a kernel built with audit-billed, which keeps the old charge, misses the containment gate’s deadline notice, in a recorded negative run. On several harts an audit also holds every hart that waits for the kernel lock behind it, and that wait is the audit’s too: each hart marks when it came from user mode, each audit’s end gives every marked hart the part of the audit it waited through, and the waiter, once it holds the lock having waited, bills its runner none of it and moves its slice’s end by it, as the auditor does. The trace records it after the wait (y: the ticks), never more than the wait by the waiter’s own clock (harts’ clocks differ by a few ticks under icount), and the oracle takes out of a share only the part of a wait that was billed. A hart’s zeroing, idle, of the frames it freed (frames in flight) is billed when it takes the lock back, to the budgets that freed them; the trace records it (0: the ticks, the frames), and the oracle reports the total. A destruction gives any hart’s zeroing still to bill to a budget it ends to its own payer, lifted with the rest of that budget’s debt (p: the payer, the entries), which the oracle counts and refuses outside a destruction; the checked kernel stops if a bill names a budget that is gone. A kernel built with audit-wait-billed bills the whole wait as before: sched-budget-churn-shell at two harts reads 329 and 339 of 1000 on rv64 and rv32 against 404 and 509, in a recorded negative run. The traced kernel stamps each audit’s start and end (records U and V: which audit, and the time). The program prints each latency sample’s window, its end on time_now and its length (LATENCY-SAMPLE <group> <measure> <end> <gross>) and how many it took of each, so a window lost on the way fails the check, and it judges none of them. A program whose run goes on past its measurement marks the window’s end, LATENCY-END <time> on the kernel’s clock: sched_oracle then judges no sample printed after it and no destruction ending after it, reporting their count (the real steward’s steward-latency, whose marker-file exits reap every lease). sched_oracle subtracts the audit time inside each window, counting only the part of an audit that falls in it, and then applies the case’s bounds (deadline_notice_p99_us=40000). It reports the gross, the net and the audit time beside each target (responsiveness). A share is the kernel’s charges, never a count: under icount a count is the machine’s instructions, not a hart’s time (R12 (scheduling)). The program prints its window, marks the budget it judges (an empty child of the mark’s weight, carved and destroyed, so the trace’s lift names the parent), and names by weight and runnable threads each budget it runs against it (HART-SHARE <name> <start> <end> <tolerance>[+|-][@<harts>] <mark>:<threads> <weight>:<threads>...; + for at least, - for at most, @ judged only at that many harts and reported at any other). sched_oracle sums what the kernel charged each budget in the window, its pass’s rises times its weight as the trace states it (each hart’s runner, H, carries its weight), less the part of each hart’s waits for the kernel lock billed to the waiting hart’s runner though no thread of it ran (a Q less its y); a lift out of the cap set (u, followed by z with the floor then, which the lift may not pass) is no charge. The part is the marked budget’s and what was lifted into it, the whole every budget’s, and what the budget is owed is its water-filling share of the trace’s harts (F) among the budgets the program names, which on one hart is its weight’s share; every want is stated in the result. An audit is charged to no budget, so the share is net of the audits; on several harts they fall mostly on the hart that switches budgets each slice, so sched-large-weight keeps one hart. Each program notes its counts beside with no verdict, and sched-share reports what the three counted of the calibrated rate (counted <n> of the calibrated 1000), the efficiency the slice ends leave. The release twins (sched-share-release, sched-large-weight-release, deadline-flood-billed) have no trace and judge their counts at one hart, in their expect lines; deadline-flood-billed-traced judges the same run’s share across harts. Where the budgets a share is judged among are hostile agents the program cannot name one by one, the share is of the charges under marks (CHARGED-SHARE <name> <start> <end> <tolerance> <mark>[:<threads>]..., the containment gate’s bystander against the leases under users). The program prints its window and marks the budgets it means, each by carving an empty child of the mark’s weight and destroying it, so the trace’s lift names the parent; sched_oracle sums each budget’s pass rises in the window times its weight as the trace states it, for the first mark’s budget against every marked budget and those lifted into them. What the budget is owed is its weight over the weights of those the kernel charged in the window, its competitors, at one hart, and on several its water-filling share of the harts among them, net of their harts’ lock waits as above, a mark naming its runnable threads; the share must lie within the tolerance of it; a window in which a budget under the marks is reweighed or ended is refused, since its competitors changed. The audits are charged to no budget, so the share is net of them by construction; what a budget is charged out of the queue shows only under its next wake’s floor lift and is not counted, so the wakes in the window are reported beside, with every budget charged in it that no lift places under a mark. The residual: it judges what the kernel charged, so a kernel that under-bills every budget under the marks alike (idle or switch time charged to no one) passes it; the gate’s own expect lines and its latency clauses bound that, not this one. An audit that never ends, ends without beginning or runs inside a destruction fails the check. The oracle subtracts only what the trace shows it: a kernel built with audit-unstamped, which leaves the audit after a destruction unstamped, misses the containment gate’s deadline notice, in a recorded negative run. The audits themselves stay full. The cluster’s envelopes (responsiveness) are credited more strictly: a stamp is a floored microsecond, so an audit stamped u and v ran from somewhere in [u, u + 1) to somewhere in [v, v + 1), and only its certified interior [u + 1, v) (empty unless v > u + 1) is subtracted, where it meets the envelope. The uncertain edge bins stay counted as elapsed time, so the credit is never more than the audit time inside, and an audit outside an envelope lowers nothing. The credit is summed with checked arithmetic and may not exceed the envelope. The other cases keep the whole-stamp subtraction above. The same trace records each timer interrupt from user mode with every charge inside it, and sched_oracle checks that the budget it interrupted pays only for its own items or its slice’s end (charging); a kernel built with timer-tail-billed, which keeps the old billing, fails that check in a recorded negative run. It records each device interrupt from user mode the same way (x), with its claim (c: the source, or 0 when another hart claimed it first), and checks that one that claims nothing is billed as a timer interrupt that ends no slice: after its expiry, to the budget the expiry billed last or to nobody, never to the budget it interrupted; one a deadline answered at its entry preempted before its claim (a destruction inside it, O 2 and no c) the same way, and any other missing claim fails. It reports the timer interrupts that charged a budget other than the one they interrupted and those ticks: another budget’s timer work in the interrupted budget’s time on its hart (timer); with foreign_timer_in=<share>:<N> it bounds them inside that share’s window, the ticks of timer interrupts from user mode that interrupted the judged budget (or one lifted into it) and charged a budget outside its marks, at N of 1000 of what the judged budget was charged there, on a trace of two harts or more (at one every interrupt is on the victim’s hart: recorded). Only timer interrupts count against the bound: an item that has passed when a call’s entry or kmain’s comes is served there, so the kernel records an expiry’s charges outside an interrupt too ($: the payer, the ticks and the time in µs, which wraps after 2^32 µs, 71 minutes, longer than any case), and the check reports beside each share the ticks they charged others at the judged budget’s own entries and in kmain on a hart it had just left, judging nothing by them, and in its summary how many such charges the trace holds, at a call’s entry and in kmain, and their ticks. The bound is judged where the harts run at once (deadline-placement, deadline-flood-billed-traced-mttcg, sched-exit-churn-mttcg, host-clock cases on the quiet core set): under icount which hart’s entry first reaches an item that has passed is the order of QEMU’s turns, and a run locks into one phase (timer). An interrupt’s return (O) says where it goes: 1 to user mode with the interrupted runner’s slice running, 0 the slice ended at this entry (to kmain, or in place to user mode, where the return is recorded as the entry’s handling ends), 2 to kmain without, a preemption. Whether the slice is over the oracle decides itself: the kernel records its decision’s inputs after the entry’s expiry (=: the slice’s end and now, µs), the slice is over if its end is not after now, and a return that says otherwise fails, as does a decision outside a timer interrupt on its hart or a second one. With wake_no_preempt=N the oracle proves a timeout only wakes: at one hart N naps each against the slice that follows it; on several, each wake of the one budget that woke N times or more at the entry that made it, a return to user mode or a call its runner goes on from counting as a witness and a preemption (O 2, or the runner requeued outside an interrupt, with no destruction) failing it, with at least wake_witnesses=K witnesses and at least wake_mid_slice=M of them mid-slice. A kernel built with wake-preempts, whose timeout wake preempts as a deadline does, fails sched-wake-no-preempt-harts and sched-wake-no-preempt-harts-mttcg on both widths in recorded negative runs. The trace ends with one record of the kernel’s time (C): every hart’s ticks in the kernel, from a trap’s entry or kmain‘s loop to the return to user mode or the idle, in its id; the ticks charged to budgets in its pass; and in its entry field, which it alone uses so, the ticks the checked build’s audits took. sched_oracle reports nobody N of 1000 (kernel K ticks, audits A, charged C), the share of the kernel’s time net of audits that no budget was charged, and judges nothing by it (residual risks). Ahead of it, one record (F) holds the ticks since boot and the harts started, and each wait for the kernel lock from user mode, the lock held by another hart, is a record (Q: its start and end in ticks); sched_oracle reports lock waits N of 1000, the waits as a share of the harts’ time, judging nothing by it either. The counters read the billing’s clock and move no schedule, and a kernel without sched-trace compiles none of them. A kernel built with alloc-first-fit, which takes each frame by the first-fit scan of RAM the bitmap replaced, fails scan-bounds on both widths in a recorded negative run (R12 (scheduling)).

Many cases use the profile: every case file with debug_assertions = true, most of them over both widths (budget, budget-syscall-attack, lend-untouched-page, ipc and smp-boot among them), and some, such as all-together, on rv64 only. The kernel prints one line under cfg!(debug_assertions): bench-debug-assertions expects it, and bench-debug-assertions-off forbids it in an ordinary boot. To check the whole suite:

CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true CARGO_PROFILE_RELEASE_OVERFLOW_CHECKS=true cargo testbench

That run fails bench-debug-assertions-off, as it should; everything else must pass.

sched-trace keeps the trace in a 64 MiB ring, and a trace that drops a record fails its case; sched-trace-large is the same ring at 256 MiB, and two cases build it. The containment gate does, at 576 MiB of RAM, since at the 1 ms slice its run of nine leases a slot writes about ten records a slice, and at two harts each hart’s picks, waiting counts and lock waits besides, some 7.1 million, past 192 MiB’s 6.3 million. The ring’s frames are kept as 32-bit page numbers, so its table fits the kernel’s RAM region. So does worst-walk, whose run at full occupancy writes about 2.6 million records on rv64 and 2.9 million on rv32, past the 64 MiB ring’s 2.1 million.

boot-stats is a diagnostic feature like sched-trace and walk-trace, but of programs, not the kernel: a Cargo feature of init, blkd, verityd, littlefsd, erofsd and beamlet-redoubt, off by default and never in the image’s build. Without it the release binaries of init, blkd, verityd, littlefsd, erofsd and beamlet have the section sizes they had before it, on rv64 and rv32 (measured with llvm-size against the commit before it, both built from the same path: beamlet’s sizes move with its build path). With it, init’s lines and beamlet’s line for its first object carry [t=N], time_now in µs; blkd, littlefsd and erofsd say their counts at each power of two of their requests from 2^12 and verityd from 2^7, and littlefsd and erofsd once more, exactly, on a walk of Elixir.BootStats.beam, a name no volume holds; at the VM’s first console read beamlet says beamlet: first console read [t=N] and what its lookups cost: their count and the guest time spent in them; and when the shell’s driver has drawn its first prompt, beamlet: first prompt drawn [t=N], the end of the boot’s span (beamlet on Redoubt). The feature needs no checked build. boot-profile and boot-profile-unverified boot the image’s programs with it under icount and a pinned seed: measurements, which bound only the boot’s time to its prompt (the boot-time target).

Hostile inputs

Status: built · tested (17)
  • bench:loader-rejects-kernel-address
  • bench:loader-rejects-kernel-entry
  • bench:loader-rejects-truncated-elf
  • bench:loader-rejects-segment-data-cut
  • bench:loader-rejects-wx-segment
  • bench:verified-boot-rejects-tamper
  • bench:verified-boot-rejects-bare-archive
  • bench:verified-boot-rejects-short-initrd
  • bench:boot-rejects-no-seed
  • bench:boot-rejects-short-seed
  • bench:boot-rejects-no-timebase
  • bench:boot-rejects-irq-past-plic
  • bench:rng
  • host:testbench::a_dropped_property_is_gone_and_the_rest_still_reads
  • host:testbench::a_shortened_property_keeps_its_first_bytes
  • host:testbench::an_overwritten_property_has_the_words_and_its_length
  • host:testbench::a_property_the_tree_lacks_is_an_error_not_a_quiet_boot

A program entry can be a good binary the bench corrupts before injecting it:

programs = ["log-server", { corrupt = "rng-test", with = { segment-vaddr = "0xffffffffffd00000" } }]

with is segment-vaddr, entry, truncate (a byte count smaller than the file), segment-flags (letters of rwx for the first loadable segment: "rwx" asks for a page no loader may map) or truncate-segment-data (the section table dropped and the file cut this many bytes before the end of the last loadable segment’s data, so the headers parse and the data runs past the end). tamper_bundle = true flips one bundle byte after signing, sign_bare_archive = true signs the archive without its domain and length, and short_initrd = 63 hands the loader only that many bytes of the signed bundle; the loader must refuse all three (R15 (verified boot), R17 (fail closed)).

device_tree changes the device tree QEMU built for the case’s own command line: the bench dumps it (-machine dumpdtb=), edits it in place and boots it with -dtb, so the firmware, the loader and the kernel see the one machine with that one difference. Each edit names a property by path and must find it:

device_tree = [{ drop = "/chosen/rng-seed" }]                                  # removed
device_tree = [{ shrink = "/chosen/rng-seed", to = 8 }]                        # its first 8 bytes
device_tree = [{ set = "/cpus/timebase-frequency", words = [0] }]              # its cells, as many as it has

A dropped or shortened property leaves FDT_NOP tokens behind, so no byte moves and the header stays true (tools/testbench/src/fdt.rs). A case that expects a deliberate panic sets allow_panic = true, which drops only PANIC from the always-forbidden list, and forbids what must not happen instead. distinct_across_boots = ['id: (.*)'] boots twice and requires the captured text to differ; distinct = ['console (.*)'] requires, within one boot, two or more lines it matches and no capture twice, such as a restarted program’s new console. A hostile program is an ordinary programs entry; hostile data for a program to use, such as a malformed ELF for a parent to launch, is a bundle file.

The file systems’ parsers are also fuzzed, by hand with cargo fuzz and outside the bench, each from its crate’s own fuzz/ workspace: littlefs’s image and mutate (littlefsd), and beside them walfs’s image, arbitrary bytes mounted, walked and written, and mutate, a valid volume with bytes changed and its hashes forged or not (walfsd).

Files in the bundle

Bundle files

Status: built · tested: bench:bench-bundle-file, bench:programs-unknown-budget-attack, bench:littlefsd-reboot, host:testbench::a_file_s_servers_merge_into_its_manifest_by_name

[[file]]                     # a data entry, after the programs
name = "trace"
from = { path = "tests/data/bundle-file.txt" }   # or any `programs` form, corrupted ones included

[[file]]                     # a manifest, with entries merged into its `servers`
name = "manifest"
from = { path = "tests/data/littlefsd/boot.json" }
servers = [{ name = "client", args = ["reboot", "littlefsd:data"] }]

[[file]]                     # a manifest pinning the userland disk's root, from the run's pack
name = "manifest"
from = { path = "image/manifest.json" }
verity = "image/userland.toml"

A file read from a path may be a manifest with servers entries merged in by name: each replaces the members it gives in the entry of its name, or is added after the rest if none has it, so cases that differ in one entry share one manifest, and a case can boot the image’s own manifest with a client added.

Entry names must differ from each other and from kernel. A file named programs replaces the listing the builder writes, so an attack case can hand the tester a hostile one. The bench refuses a [[grant]] table: a program reaches a device only through the handles it is given (R18 (device authority)). The loader starts only the kernel and the program in init’s place, so a data entry reaches the guest signed and is never run. bench-bundle-file reads its entry back: the program in init’s place finds it in the bundle’s pages and compares it, byte for byte, with the file it was built with.

Data entries for init

Status: built · partly tested: no model trace is replayed under `init` yet · tested (1)
  • bench:init-servers

init receives the verified bundle and hands the public entries to bootfsd, and a data entry is how a model trace reaches an in-guest replayer, which compares results itself and prints its verdict (boot). The program in init’s place already reads a data entry from the bundle’s pages (bundle files); under init, a program reads it again through /boot once the manifest’s public list names the entry.

Devices and the network

Disks and network cards

Status: built · tested (38)
  • bench:bench-virtio-devices
  • bench:bench-virtio-legacy-off
  • bench:erofs-corrupt
  • bench:erofs-read-only
  • bench:image-disk
  • bench:init-boot
  • bench:net-tcp
  • bench:userland-boot
  • bench:userland-read-only
  • bench:verity-flipped-tree
  • bench:verity-wrong-root
  • bench:verity-signed
  • bench:verity-bad-signature
  • host:testbench::a_recipe_can_generate_a_directory_of_files
  • host:testbench::a_recipe_packs_a_table_and_a_volume_per_partition
  • host:testbench::a_stage_is_walked_parents_first_in_name_order
  • host:testbench::devices_sit_on_fixed_slots
  • host:testbench::the_vault_disk_sits_beside_the_data_disk
  • host:testbench::each_disk_holds_the_volumes_on_its_device
  • bench:walfsd-boot
  • host:testbench::every_network_is_restricted
  • host:testbench::a_lease_slices_into_disjoint_ranges_or_none
  • host:testbench::virtio_devices_are_modern
  • host:testbench::the_userland_disk_sits_on_its_slot_read_only
  • host:testbench::the_userland_pack_is_deterministic_and_stages_each_object_by_name
  • host:testbench::a_verified_partition_is_its_volume_then_its_tree
  • host:testbench::an_erofs_partition_is_its_stage_and_each_damage_is_corrupt_where_it_is
  • host:testbench::a_walfs_partition_is_its_stage_and_two_packs_are_the_same_bytes
  • host:testbench::the_manifest_pins_the_packs_root
  • host:testbench::a_signed_partition_ends_in_its_root_block_signed_deterministically
  • host:testbench::the_cases_volume_seed_is_the_development_seed
  • host:testbench::a_volume_s_bytes_are_held_to_its_partition
  • host:testbench::the_image_s_volumes_are_its_disk_s_partitions
  • host:testbench::a_case_s_manifest_is_held_to_its_disk
  • bench:launch-keep-disk
  • host:testbench::a_kept_disk_is_attached_as_it_is
  • host:testbench::a_kept_disk_of_another_layout_is_refused
  • host:testbench::a_kept_disk_is_held_to_its_recipe_s_manifest
[disk]                       # a virtio-blk disk, zeroed, created afresh for every boot
size_kib = 4096
partitions = 1               # optional: a GPT of this many equal partitions, by blkd's builder
# or, instead of both: a disk recipe packed for every boot as ./mkimage packs it
# recipe = "image/disk.toml"
# stage = "tests/data/littlefsd/stage"   # optional: what every partition holds instead of its stage
# flip_version = true        # optional, with a recipe: one bit of each signed volume's version flipped
# keep = true                # optional, with two boots: the second boots the disk the first left

[vault]                      # optional, with [disk]: a second writable disk, disk2, the same keys
size_kib = 2048
partitions = 1

[userland]                   # the userland disk, attached read-only, packed once per run
recipe = "image/userland.toml"
# flip = "Elixir.Enum.beam"  # optional: one bit of this file's data flipped on the disk
# flip_tree = true           # optional: one bit flipped in the first level-1 tree block
# wrong_root = true          # optional: the manifest pins a root one digit off the pack's

[net]                        # a virtio-net card on QEMU's user-mode network
forward = [22]               # guest TCP ports reachable from the host (default: none)
host_key = "ssh-ed25519 AAAA..."   # optional: the only SSH host key sessions accept

[idle]                       # with launch = true: measure a session's `idle` step (one)
interrupts_per_hart = 9.0    # optional ceilings, each per second of the window
user_ecalls = 18.0
host_cores = 0.01

A disk recipe (image/disk.toml) is packed by the code ./mkimage runs (testbench --pack-disk): a GPT of equal partitions by blkd’s builder, then each partition as its fs says, holding its stage’s tree: littlefs, a writable volume written through littlefsd’s own code; erofs, a read-only volume written by libs/erofs’s writer (erofsd); or walfs, a writable volume written by libs/walfs itself (walfsd), so a case boots the disk the image ships.

A disk with keep = true is made for the case’s first boot and booted again, as that boot left it, by the second (distinct_across_boots): launch-keep-disk writes a file at the prompt in one boot and reads it in the next, as ./launch --system --keep-disk keeps a person’s disk between launches. A kept disk whose size or partition table is not the one a fresh disk would have is refused, never reformatted.

A manifest’s volume that gives bytes (init) must be exactly its partition’s size, which init never reads. A recipe names the manifest its disk serves (manifest = "image/manifest.json"), and the pack is refused if a volume’s bytes differs from its partition’s, or the partition at its index has another name; at load the bench refuses a case whose manifest file gives a volume bytes its disk’s partition does not have, whether the disk is a recipe or size_kib and partitions. With a [vault], each disk holds the volumes of the blkd its device goes to: a volume’s disk names its blkd, whose devices entry is disk0 or disk2.

[vault] is a second writable disk beside [disk], with the same keys and its own recipe or layout, for a manifest that keeps the unlabelled home volume and the vault on separate devices, as a confined one must (R34 (confined placement): one blkd serves one label set, so two label sets need two disks). It is disk2 on its own slot, made and kept as the data disk is, beside it. walfsd-boot boots both: a blkd on each, a walfsd on each disk’s one volume, and a client writing and reading back on both. Its slot, bus 4, is the one tests/data/init/driver.json names slot5: the empty slot dma-driver is given in init-driver-restart and init-quarantine-reboot, empty only because no disk sits there. A case carries [vault] or that manifest, never both.

A recipe’s volume may also generate files, for a case that needs many and not their contents: generated = { files = 600, read = "f000" } makes f000 to f599 in the volume’s root (as many digits as the last needs), all empty except read, which holds its own name and a newline. They sit beside the stage’s tree, if there is one, and a name in both is refused.

A volume may be verified, verity = true: it holds the largest volume that fits beside its hash tree, then the tree (verityd), and the pack says its root and data blocks. An erofs volume is followed in its range by zeros, which the tree covers too. A verified partition may be signed, sign = { key = PATH, version = N }: its last whole block is then a root block holding N, the version and the root, signed with the 32-byte Ed25519 seed in the file PATH (relative to the workspace root) under the volume domain (verityd), the volume and tree fit before it, and the pack says the version too. Signing is on the build host only; a manifest names the key, never the seed. The cases’ seed, tests/data/verity/dev-seed, is 32 bytes of 0x42 (B): the bundle builder’s development seed (DEV_SEED in tools/testbench/src/build.rs), so "key": "bundle" verifies it. Ed25519 is deterministic, so two packs are byte-identical. A case’s flip_version flips one bit of each signed volume’s version after the signing, on the disk and never in the manifest.

For erofs-corrupt, an erofs partition may be damaged after its pack, through the parser erofsd uses to find the place: damage = { what = "magic" } flips a bit of the superblock’s magic; { what = "block-past-count", path = "tail.txt" } starts that file’s blocks at the volume’s block count; { what = "compressed", path = "motd" } lays that file out compressed; { what = "name-offset", path = "lib" } starts the last name of that directory’s first block past the block’s end.

The userland disk (image/userland.toml) is packed by the same code: first its objects are staged, each module of the applications the recipe names, compiled by the pinned toolchain and stripped, as a plain file under its own name, then its one partition is packed as a verified volume of those files. The bench stages and packs it once per run: a bundle file read from a path with verity = "image/userland.toml" is a manifest, and the builder writes the pack’s root and data blocks into the verity of the volumes entry of the partition’s name, so the signed manifest pins the disk; [userland] attaches the same pack. A case’s damage goes on its own copy of the disk after the pack, never on the root: flip flips one bit of a file’s data where the volume holds it, and flip_tree one bit of the first level-1 tree block. wrong_root changes the manifest’s root by one digit instead, never the disk (R76 (verified volumes)). Nothing is generated beside the objects.

Devices use virtio-mmio’s modern transport, which blkd and netd require. Each sits on a fixed virtio-mmio slot, whether or not the case has the others, so a case’s manifest names its devices as the image’s does (image/manifest.json names the first three):

device[table]QEMU busbaseirqmanifest line
data disk[disk]virtio-mmio-bus.70x100080008{ "name": "disk0", "base": "268468224", "irq": 8, "dma": true }
network card[net]virtio-mmio-bus.60x100070007{ "name": "net0", "base": "268464128", "irq": 7, "dma": true }
userland disk[userland]virtio-mmio-bus.50x100060006{ "name": "disk1", "base": "268460032", "irq": 6, "dma": true }
vault disk[vault]virtio-mmio-bus.40x100050005{ "name": "disk2", "base": "268455936", "irq": 5, "dma": true }

The userland disk is attached read-only (readonly=on): QEMU refuses every write to it, so nothing on the box can change it. The guest reaches nothing outside QEMU (restrict=on, checked for every [net] case): there is no outside peer, only forwarded connections coming in, unless a case adds one deliberately. Nor is it offered IPv6 (ipv6=off), which it does not speak: slirp would otherwise send it router advertisements. Each boot gets its own host ports, from the job’s lease under scripts/q (a sweep’s concurrent boots each from their own slice of it) and chosen by the operating system otherwise, so benches running side by side do not collide.

Peers, dials and the capture

Status: built · tested (16)
  • bench:bench-net-peer
  • bench:bench-net-peer-twice
  • bench:bench-net-peer-count
  • bench:bench-net-peer-pcap-empty
  • bench:netd-restart
  • bench:sshd-login-bound
  • host:testbench::a_dial_with_a_line_waits_for_it
  • host:testbench::a_held_dial_ends_when_the_far_side_closes
  • host:testbench::a_poke_gets_a_udp_forward
  • host:testbench::peers_are_judged_on_records_and_capture
  • host:testbench::a_capture_is_read_fail_closed
  • host:testbench::what_the_guest_sends_is_checked
  • host:testbench::records_are_counted_per_peer
  • host:testbench::a_dial_needs_its_echo
  • host:testbench::prefixes_and_peers_are_checked
  • host:testbench::peers_get_the_wider_network_and_a_capture

A network case can give the guest hosts to reach, and judge what it sent, all from outside the guest, after the boot has passed:

[net]
forward = [8000]
self_forbidden = ["10.0.2.0/24", "127.0.0.0/8"]   # the guest must never send a SYN to these

[[net.peer]]                 # a host the guest may connect to, and exactly how often
addr = "10.0.9.100:7"
connections = 1

[[net.dial]]                 # the bench connects in through a forwarded port and needs the echo
port = 8000
send = "hello\n"
expect = "hello\n"
after = '^\[con [0-9a-f]{16}\] judge is up$'   # optional: dial only once a console line matches
until_closed = true          # optional: then hold the connection until the guest closes it

[net.poke]                   # one UDP datagram into the guest, sent when a console line matches
port = 47000
payload = "redoubt netd restart probe"
after = '^\[con [0-9a-f]{16}\] judge knows netd.s instance: poke it$'
  • Peers are QEMU guestfwds to a program: for each connection the guest makes, the bench’s own binary starts as a helper on it, records the connection as a file before it echoes a byte, and then echoes. After the boot each peer’s count must equal its connections. There is no host listener another process could take.
  • The poke is one UDP datagram, sent once, through a host port QEMU forwards to its guest port, when a console line first matches its after: a trigger from outside that nothing resends, as TCP would. netd-restart faults netd with it, through a test-only feature.
  • A dial is a TCP connection the bench makes into the guest through a forwarded port, retried every 100 ms until one connection echoes expect for send, from the boot’s start or, with after, from the console line that matches it; one never echoed by the deadline fails the case, with what came. With until_closed the bench then keeps the connection, typing nothing, until the guest closes it, and notes under the case’s result how long it was held; one still open at the deadline fails. That is a client that connects and never goes on, which the guest must end itself: sshd-login-bound holds every sshd slot that way and the verdict is the login the box then serves, never the dials, which write nothing on the console.
  • The network. A case with peers widens slirp’s network to a /16 in which its host, resolver and the guest’s address stay where they were; the peers sit outside the /24 the guest is configured for, reached through its gateway. restrict=on still holds.
  • The capture. A case with peers records every frame on the guest’s card, before slirp, and reads it fail closed: missing, empty, cut or malformed fails the case (net.truncate_capture cuts it on purpose, for the self-checks). The guest may send only ARP requests for the gateway, ARP replies (to any address) and IPv4 TCP, never a fragment and never a SYN to a self_forbidden prefix. Each peer’s count must also match the distinct SYNs to it in the capture, and a case with peers needs one that expects a connection, whose SYN shows the capture was live.

The guest’s own claims about the network are never trusted.

SSH sessions

Sessions and the loopback server

Status: built · tested (20)
  • bench:bench-ssh-loopback
  • bench:bench-ssh-loopback-openssh
  • bench:bench-ssh-loopback-deadlock
  • bench:bench-ssh-loopback-forbid
  • bench:bench-ssh-loopback-exit
  • bench:bench-ssh-loopback-host-key
  • bench:bench-ssh-loopback-aborted-text
  • bench:bench-ssh-guest
  • bench:steward-ssh-two-principals
  • host:testbench::expect_after_matches_in_order_and_names_the_first_miss
  • host:testbench::the_reference_proxy_quotes_only_what_the_bench_chose
  • host:testbench::the_cpio_writer_writes_newc
  • host:testbench::the_guest_recipe_parses_and_hashes
  • host:testbench::a_bad_package_is_broken_and_no_network_is_the_hosts
  • host:testbench::the_keeper_finds_what_names_the_case
  • host:testbench::the_keeper_waits_to_the_deadline
  • host:testbench::resize_needs_a_pty
  • host:testbench::only_marks_follow_exit
  • host:testbench::ended_keeps_the_input_open_until_sshs_own_exit
  • host:testbench::no_other_child_inherits_a_sessions_terminal

Sessions need net.forward = [22]. They start once every expect has matched and run concurrently while the bench keeps watching the console; a session whose first steps are waits starts its ssh only once those marks are set, so its login follows what they mark. Each drives the host’s OpenSSH ssh, an implementation independent of the box’s, to the guest’s port 22 with a test key. What the box says about them, a login it refused or a session’s budget given back, is asked for with the case’s expect_after: console patterns matched in order from the sessions’ start to the case’s deadline, a miss failing the case with the first pattern unmatched. expect cannot ask for those lines, since the sessions start only once it has all matched.

[[session]]
user = "alice+secrets"       # the login name
name = "vault"               # optional; unique in the case, names its log; defaults to `user`
key = "alice"                # optional; defaults to `user` up to any '+' or '.'
pty = false                  # true asks for a terminal
forbid = ['bob-secret']      # never in this session's output, until ssh exits
steps = [
    { expect = '\(1\)> ' },     # wait for the prompt
    { send = "File.read(\"/work/x\")\n" },
    { expect = 'id ([0-9a-f]+)' },  # a pattern with groups keeps its captures...
    { send = "approve $1\n" },     # ...for a send to type back ($1 to $9; $$ is a $)
    { mark = "alice-ready" },    # tell other sessions this one got here
    { wait = "bob-ready" },      # wait for another session's mark
    { resize = [132, 43] },      # with `pty = true`: resize ssh's terminal
    { idle = 60 },               # with [idle]: type nothing for 60 s while the bench measures
    { within = 30 },             # the next step must finish within 30 s, before the case's deadline
    { exit = 0 },                # close input, read until ssh exits, require this status
    { ended = 0 },               # or: input open, read until ssh exits on its own, require this status
    { mark = "alice-gone" },     # only marks follow `exit` or `ended`: this session's ssh is gone
]
ssh_args = ["-W", "host:9"]  # optional: more ssh arguments, before the host
command = "echo hi"          # optional: a command (with `-s`, a subsystem) in place of a shell

A session the box ends, after a line it must act on (a call that ends the session, say), follows that line with ended, not exit: exit closes the input first, and with pty = true that close hangs up the terminal ssh reads and discards what it has not read yet, so the line may never leave the host; the box’s end of a channel whose input is still open has nothing to race. exit stays for the sessions the bench itself closes. The log notes when the end came, as it does an expect’s match. Every session’s exit status is checked and all of its output passes forbid; a session that fails stops the others. Its log notes each expect that matched and when, in seconds after its ssh started, and the bench prints under the case’s result those matched before the session first typed: a login’s latency to its first prompt, re-measured by every run (sshd). A pty = true session’s ssh reads its input from a pseudo-terminal the bench opens at 80x24, so that ssh reports a size change as OpenSSH does for a user; its output stays on pipes. resize sets that terminal’s size and signals ssh (SIGWINCH), which then sends a window-change if the size changed. The terminal is the client’s input and never a verdict. With net.host_key set, ssh refuses any other host key. Test keys live in tests/keys/; they are public and marked not for production, and a boot manifest that lists one must never ship. A launch = true case (launch-system) boots the command line ./launch --system builds, unchanged, and its sessions log in with a key made beside the bundle when it is packed, which alice alone holds in that bundle’s manifest, as launch gives her the checkout’s key (try the system). The ssh-loopback kind runs sessions against a server that ssh starts itself for each session as its ProxyCommand, so nothing listens on a port: Redoubt’s sshd on its host platform (against Redoubt’s sshd), or with server = "openssh" OpenSSH’s server in inetd mode, in a QEMU guest. Its log goes to a file beside the transcripts, never to ssh’s output; the standard error ssh would otherwise share with it goes to that log for Redoubt’s sshd and is discarded for QEMU’s. So a late line of the server’s, such as the broken pipe it may meet writing to an ssh that has refused its host key and hung up, cannot stand in for the session’s last output, which is ssh’s own. The bench creates the log, empty, before the first session, so a case whose sessions time out before ssh starts the server reads it empty. A case’s server_log asks what the server saw (a refused key, say), not only what the client printed, and its server_log_forbid what the server must not have done (a console started, say).

OpenSSH’s server runs in a QEMU guest. On a host that enforces SELinux, sshd moves every login shell into the user’s default context, and a bench running in a service’s context may not enter it, so the host’s own sshd cannot serve the reference case. A container needs a runtime and user namespaces that the bench’s host may refuse. A guest under the bench’s own qemu-system-riscv64 needs neither; the client, the session runner and the case are unchanged, so the case is still a witness independent of Redoubt’s server. The guest is not Redoubt, and it boots QEMU’s own OpenSBI: the rule that only RustSBI boots is Redoubt’s.

  • The image is a Linux kernel and an initramfs built from tests/ssh-reference/guest.toml: Debian’s riscv64 kernel, openssh-server, the libraries it links and busybox-static, each pinned by version and sha256 in one timestamp of snapshot.debian.org, which keeps every version it has published; with them the guest’s /init, its logins (root and sshd’s privilege-separation user), the kernel module it loads (virtio_mmio) and what it leaves out, each with its reason. The bench fetches each package with curl, checks its sha256, unpacks it with dpkg-deb, and writes the initramfs’s newc archive itself. It keeps the image in target/ssh-reference/ under the first 16 hex digits of the recipe’s sha256, and builds it only when that is missing, so only the first run after a change to the recipe needs the network.
  • Each session boots its own guest: ssh‘s ProxyCommand is QEMU with no network and no host filesystem. The case’s configuration and keys reach the guest in its initramfs: the bench writes, for each case, the image’s archive followed by an archive of the case’s files. The session’s stdio is a virtio-serial port; the guest’s /init runs sshd -i on it, reading and writing one open of the port, and powers off when sshd is done. Every sshd process opens its log anew and a port takes one open at a time, so they share a FIFO that one reader carries, a line per write, to a second port, which QEMU appends to the case’s log: a line of up to 4 KiB, the most a FIFO takes in one write, reaches the log whole among other sessions’ lines. The guest’s console goes to guest.log beside it, for people reading a failed run, and is never a verdict; a failed boot powers off rather than reboots. The server logs in only root, inside the guest, runs /bin/sh for every login and allows nothing else.
  • ssh ends each guest. Once the session ends, ssh exits without waiting for the server and hangs up on its proxy. What sshd logs after that is lost; the lines the cases ask for come earlier. ssh has no parent-death signal, so a bench killed outright leaves it running until its session ends, and its guest with it. The keeper: once a case’s sessions have all exited, any qemu-system-riscv64 whose command line names the case’s directory (the run’s own) has until the case’s deadline, and at least five seconds, to go, as a loaded host may slow a guest’s shutdown with nothing wrong; one still running then is killed, and the case fails, naming it, unless a session has already failed it.
  • Before the first OpenSSH loopback case the bench logs in once and runs exit 0, and the server’s log must name OpenSSH’s version, so that no other server can pass for it. Its ssh waits at most 30 seconds for the server’s banner, so a guest that never boots fails the probe rather than hanging the bench. Without a qemu-system-riscv64 the bench can use, without curl, dpkg-deb or xz to build the image, or with no image and snapshot.debian.org not answering, every OpenSSH loopback case fails with that reason, as on a host without OpenSSH, and --allow-skip skips them. A package whose sha256 is not the recipe’s, a fetch that fails while the snapshot answers, a build that fails and a probe that fails all fail every OpenSSH loopback case. The check connects directly: on a host whose only way out is an HTTP(S) proxy that curl uses, a fetch that fails there finds the snapshot silent, and is a host lack that --allow-skip skips.

The machine at rest

Status: built · tested (11)
  • bench:launch-idle
  • host:testbench::the_log_is_counted_by_hart_and_name
  • host:testbench::a_rate_over_its_ceiling_fails
  • host:testbench::a_window_that_measured_nothing_fails
  • host:testbench::the_monitor_is_reached_and_left_by_the_mux_escape
  • host:testbench::an_idle_step_needs_idle_and_launch
  • host:testbench::the_window_opens_once_the_frames_in_flight_are_back
  • host:testbench::the_window_opens_after_the_lines_already_queued
  • host:testbench::a_drain_that_never_ends_fails_at_the_bound
  • host:testbench::no_drain_seen_fails_at_the_bound
  • host:testbench::only_the_kernel_s_lines_open_a_drain_and_one_inside_is_named

What an idle Redoubt costs its host is measured from outside the guest. A launch = true case with an [idle] table and one session step { idle = N } boots ./launch --system’s command line; when the session reaches the step, it types nothing for N seconds, still reading its output, and the bench measures that window:

  • Traps, from QEMU’s own log. -nographic multiplexes QEMU’s monitor on the console, so the bench types Ctrl-A c, logfile <case>.int.log and log int, and Ctrl-A c back, when the window starts, and log none when it ends: QEMU logs each trap a hart takes (riscv_cpu_do_interrupt: hart:H, async:A, … desc=NAME) for the window alone, and the command line stays launch’s. The session’s quiet starts once the bench has typed log int, and its next step waits until the bench has typed log none, so no other step’s work falls in the window. Logged from the boot on, every system call would be a line. The bench counts each hart’s interrupts per second by name (timers, software interrupts the firmware and the kernel send between harts, devices) and the exceptions per second by name, every hart’s (user_ecall, the system calls; supervisor_ecall, the kernel’s calls to the firmware).
  • QEMU’s host CPU time, its user and system time from /proc/<pid>/stat at both ends, per second of the window: the host cores the idle machine takes. The kernel counts that time in clock ticks (getconf CLK_TCK, 100 a second here), so a 60 s window reads it to 1/6000 of a core: 0.002 cores is about 12 ticks, and a 0.01 ceiling is 60.

The case log gets one [idle] line with every rate, and a rate over its ceiling fails the case; a ceiling left out is measured and printed only. A window that measured nothing fails too, never passing under its ceilings for want of data: no log, no timer interrupt on any hart (an idle hart may take none in a whole window, since a timeout whose payer runs nowhere is armed on one hart: the hart timer), no system call from user mode, or no host CPU time. launch-idle’s ceilings are twice the most that ten 60 s windows measured, five a width (the case’s comment gives each), so a ceiling catches a cost that doubles, not the window-to-window spread: 3.8 interrupts a second on the busiest hart (1.6 to 1.9 measured), 12.2 system calls from user mode (6.0 to 6.1), and 0.01 host cores, the measure’s own resolution (0.001 to 0.002). Before the one-hart rule the busiest hart took 3.4 to 3.5 a second, three quarters of them the kernel lock’s hand-off interrupts, each timeout waking every hart (the hart timer).

The window never holds the zeroing of the frames in flight (frames in flight): about 35,000, which the boot and the login leave in flight and one hart zeroes once every hart first idles after the login, about half of a window’s host time when the window held them. The kernel says on the console when a drain of 1,024 frames or more begins (mem: 1024 frames in flight) and when the frames in flight are back to 0 (mem: frames in flight 0, at most N). When the session reaches its idle step, the bench reads the console lines already queued, until it falls silent for 50 ms (a host-clock settle, for those lines only), and holds the session and the window until a drain has ended since the sessions began, none being open. Six runs a width alone, at four harts, saw them back 0.32 to 0.39 s after the step began on rv64, at about 0.6 host cores, and 5.8 to 6.2 s on rv32, at about 0.15; why rv32’s every hart idles that much later after the prompt is not yet measured. The bench waits at most 30 s from the step’s start, about five times rv32’s most, the margin for a loaded host; a drain still open then, none ended, or a console never silent fails the case, and the failure names which; the drain’s end is the kernel’s line, never a settle time. The case log’s [idle] drain: line, before the window’s own, says what the wait came to: the drain’s most frames, the wall time from the step’s start to its end and QEMU’s host CPU meanwhile, or that none ended in the wait. A drain that opens inside the window is named on the window’s own [idle] line, written once it has ended: the window’s work, measured. Before R81 the busiest hart took 3.1 interrupts a second on rv64 and 2.8 on rv32, at 0.002 cores; with the wait, those twelve windows read 2.9 to 3.5 at 0.001 to 0.003 cores. The measures are the hardware’s view: they say how often the guest wakes, not which budget woke it; that would take the kernel’s own trace, which prints only at a reset. launch-idle is a host-clock case, run in the quiet class.

Against Redoubt’s sshd

Status: built · partly tested: agent forwarding is refused inside `sunset`, which no case sees, since `ssh` asks for it without a reply ([residual risks](servers/sshd.md#residual-risks)) · tested (13)
  • bench:sshd-loopback-logins
  • bench:sshd-loopback-r67
  • bench:sshd-loopback-interrupt
  • bench:sshd-loopback-independent
  • bench:sshd-loopback-window-change
  • bench:sshd-loopback-window-change-zero
  • bench:sshd-loopback-env-refused
  • bench:bench-ssh-loopback
  • bench:bench-ssh-loopback-host-key
  • bench:sshd-host-tests
  • host:testbench::an_ssh_lacking_an_option_is_named
  • host:testbench::the_redoubt_proxy_keeps_its_errors_off_ssh
  • host:testbench::the_redoubt_servers_log_exists_before_any_session

ssh-loopback cases run the host’s OpenSSH ssh against Redoubt’s own sshd on its host platform, redoubt-sshd-host (the core and its platforms), which the bench builds and ssh starts as its ProxyCommand. Its host key is loopback-host, and each of the case’s authorized keys is a principal of the same name. Nothing there needs a shell, a login context or a guest. The box’s platform, on the guest’s port 22 with the steward’s logins and real sessions, is the steward-* boot cases’ (steward-ssh-two-principals and the rest, sshd).

  • The self-checks run on it, their steps written for its scripted console, and their server_log patterns for its log.
  • Cases, verdicts from ssh’s exit status and the server’s log: a login key the server’s keyd holds is refused and never reaches the login table, and so is an unknown principal; alice+secrets gets the labels {alice-secrets}; on a labelled channel a shell without a pty, exec, a subsystem, and remote and local port forwarding are refused, and no console starts (R67 (a channel keeps its labels)), and the log names each refusal, the shell’s as shell-without-pty; a break reaches the console as its interrupt; one connection’s end leaves another’s session running; a host key other than the case’s is refused. A resized terminal’s window change reaches the console as its new size, and one to no size (0x0) is refused and never reaches it. env is refused, and the log names only the request’s kind, never the client’s name or value. ssh wants no reply to either refusal, so the server’s log is the whole evidence: each case requires the refusal’s line and forbids its opposite.
  • One reference case stays on OpenSSH’s own sshd, with server = "openssh": concurrent sessions, marks, exit statuses, a pty and a refused key. It is the session runner’s independent witness, so a bug the runner shares with Redoubt’s server cannot pass every self-check (bench-ssh-loopback-openssh). Its server runs in a QEMU guest (sessions and the loopback server).
  • ssh gets WarnWeakCrypto=no-pq-kex against Redoubt’s server, whose exchange is not post-quantum: OpenSSH’s warning would otherwise be session output. OpenSSH 10.1 introduced the warning and the option together, so the bench has ssh -G parse the option once per run, with no configuration file as the sessions run it, and passes it only to an ssh that takes it: an older one has no warning to quiet, and none to filter from its output (OpenSSH 9.6 prints nothing over such an exchange). When it drops the option, the run’s output says why.

Self-checks

Status: built · tested (17)
  • bench:bench-attack-forgery
  • bench:bench-console-after-expect
  • bench:bench-poweroff-missing
  • bench:bench-reporter-mismatch
  • bench:bench-init-reporter-forged
  • bench:bench-debug-assertions
  • bench:bench-debug-assertions-off
  • bench:bench-net-peer-twice
  • bench:bench-net-peer-count
  • bench:bench-net-peer-pcap-empty
  • bench:bench-net-self-unrefused
  • bench:bench-cbo-self-unrefused
  • bench:bench-qemu-early-exit
  • bench:bench-elixir-oracles-broken-guard
  • bench:bench-no-trace
  • bench:bench-trace-scan-catches
  • bench:bench-test-only-refused

The harness can fail, and each feature shows it. Cases named bench-* check the bench itself: each feature has a case that passes only if the feature works and, where the bench can be misconfigured on purpose, a case that must fail:

must_fail = '^regex$'        # passes only if the run fails with a matching reason

must_fail is judged against the run’s verdict only (console, sessions, devices); a build error or the bench’s own trouble is a failure regardless, and so is an elixir case’s toolchain. A build case’s must_fail alone matches its build’s error, or its binary scan’s finding (below). Each case writes its pattern anchored and quoting the evidence, so it cannot pass by failing for some other reason; the bench does not enforce the anchoring, so a reviewer checks it. An attack case can have a self-check of its own: bench-net-self-unrefused runs net-attacks’s boot with ipd not told one of the box’s addresses, and must fail on the SYN the capture then shows. bench-cbo-self-unrefused runs cbo-user-fault’s boot with a kernel that leaves senvcfg permissive: all four cache-block operations must be seen running, and the run must fail on the verdict line that never comes. bench-elixir-oracles-broken-guard runs the steward core’s reference with its not_locked guard held always, and must fail on the first event where its output leaves the core’s (the trace encoding). A build case with forbid_in_binary reads the binary it built and fails on the first byte string named that it holds anywhere, quoting the offset and what is around it: bench-no-trace builds the production kernel, the release profile with the board feature alone as ./build makes it, and forbids the scheduling trace’s console-line prefix and its module’s mangled path: the scan proves this trace absent, not every channel (R23 (no test channels)); bench-trace-scan-catches builds a checked kernel with sched-trace (debug_assertions = true: a test-only feature compiles into no other) under the same scan and must fail on the trace’s console line; and bench-test-only-refused asks the release profile for sched-trace and must fail on the kernel’s own refusal, a test-only feature needing a checked build, in the compiler’s words.

The unsafe budget

Status: built · tested (13)
  • bench:unsafe-budget
  • host:testbench::actual_source_counts_still_enforce_the_budget
  • host:testbench::empty_configuration_is_not_coverage
  • host:testbench::every_configured_root_must_contain_rust_source
  • host:testbench::missing_paths_fail_regardless_of_extension
  • host:testbench::unreadable_source_reports_its_path
  • host:testbench::broken_nested_symlink_is_not_silently_skipped
  • host:testbench::zero_unsafe_source_is_valid_as_a_file_or_nested_directory
  • host:testbench::every_on_target_source_is_in_a_budget
  • host:testbench::a_long_safety_block_directly_above_justifies
  • host:testbench::a_raise_needs_its_unsafe_budget_line
  • bench:rt-miri
  • host:testbench::a_miri_case_runs_its_files_under_miri

unsafe-budget.toml lists every source directory of the trusted computing base that runs on the target, each with the most uses of unsafe it may hold and the most that may lack a justification (zero everywhere): a // SAFETY: comment above an unsafe block, and a # Safety section in the doc comment of an unsafe fn or unsafe impl, in the comment block directly above or within a few lines. The case counts both and fails if either is over. Budgets only go down. Raising either limit, dropping a budget or narrowing its paths needs a line Unsafe budget: <name>: <reason> in the commit that does it, which the case reads the way the size budget reads its own (below), with the same history check. A page that quotes the ceilings, in a `unsafe` (pinned) column like the kernel’s TCB table, is held to them by the docs checker (below), so a ceiling cannot move without the page.

A configured path with no Rust source in it fails. So does coverage left out: every workspace member that can be built for the target (its crate root is no_std) must have each of its Rust sources in some budget, unless the file lists it under [[uncounted]] with a reason (the test programs, the model, host tools, vendored code), and an uncounted entry that names no such member fails too. Vendored third-party crates are outside the ratchet (below). So are crates outside the workspace: the gate reads only the workspace’s members, and userland/otp is its own workspace whose no_std crates (re, crypto, vm) no budget counts. They are not in the trusted computing base; if one ever joins it, it joins the workspace and the gate sees it.

The ratchet counts unsafe; it does not check it. rt-miri runs the native runtime’s host tests under Miri (Stacked Borrows, isolation off), which checks the heap’s free lists, page buffers, lends and device registers that a native run only executes. It runs the files that finish in seconds, among them registers over the fake kernel’s real device memory, and the heap’s own, heap, in a minute or two (fewer random rounds under Miri), each file a job of its own (fanout); ipc and echo take minutes under Miri and are run by hand. Its files assert no wall-clock bound, only hang guards, so it is not a host-clock case. Without nightly Miri the case is missing, not passed. With the runtime’s page-buffer aliasing fix reverted, mapping_views fails it with the Stacked Borrows error not granting access to tag <wildcard> because that would remove [Unique for <…>] which is strongly protected.

The size budget

Status: built · tested (12)
  • bench:size-budget
  • host:testbench::only_code_lines_count
  • host:testbench::a_test_module_does_not_count
  • host:testbench::a_test_module_file_does_not_count
  • host:testbench::a_shipped_file_always_counts
  • host:testbench::a_form_the_case_cannot_follow_fails
  • host:testbench::a_raise_needs_its_reason
  • host:testbench::the_ratchet_reads_the_commit_that_raised
  • host:testbench::a_merge_is_judged_against_its_first_parent
  • host:testbench::merged_history_is_not_read_again
  • host:testbench::a_new_budget_file_needs_every_reason
  • host:testbench::a_deleted_budget_file_fails

The size of the trusted computing base is budgeted, not observed (the tenets). size-budget.toml lists each trusted crate (the kernel, the loader, the stub, the libraries they and the servers link, the model and the servers) with a ceiling in lines of code: every line of every .rs file under its paths that is not blank, a // comment (doc comments included) or inside a /* */ comment. Tests are left out, so writing them costs a crate nothing: a #[cfg(test)] item counts for nothing, and neither does a file only test modules reach (mod tests;, the modules it declares in turn, and those declared inside an inline test module). A file any other module declaration reaches counts, whatever else names it; a module is found by its name, its enclosing inline modules and its #[path] or cfg_attr path, and one whose file is not under the crate’s paths fails the case. So does a form the case does not follow, which could reach a file past a test’s #[path] to it: a mod whose name is not a plain identifier (r#name, a macro’s $name) and the word include, however it is invoked. The case fails when a crate is over its ceiling. The ceilings started at each crate’s size when the case landed and only fall: the case reads the commits that changed its file on the branch it runs on, merges included, and where one raised a ceiling over the file in its first parent, dropped a crate (a rename drops the old name) or narrowed a crate’s paths (fewer lines counted under the same ceiling), requires a line Size budget: <crate>: <reason> for each such crate, in its message or, for a merge, in a commit it brings in. A commit whose parent lacks the file is judged against the last version before it; where there is none, as for a file the main branch lacks (new or renamed), every entry in it needs its line. A commit that deletes the file fails the case, so deleting it and adding it back raised cannot escape. A raise not yet committed fails, and so does a path with no Rust source in it; uncommitted changes do not stop the committed ones being judged.

A branch is judged on its own commits: those since its merge-base with the main branch (redoubt, or origin/HEAD in a clone that has no such branch), so a package is judged before it merges and merged history is never read again. On the main branch itself only a raise not yet committed is judged. With neither branch to measure from, as in a shallow clone that lacks the merge-base, the case fails rather than passing unchecked.

The residual: a macro defined outside the budgeted paths, a dependency’s macro_rules! or a proc macro, can emit mod x; or include! at a call site, and the case reads only the call. No trusted crate’s dependencies are known to, and adding one is a Cargo.toml change reviewed as part of the trusted computing base (tenet 5).

The memory budget

Status: built · tested: bench:init-boot, bench:userland-boot, bench:userland-read-only, bench:beamlet-footprint, bench:beamlet-compile-footprint, bench:steward-session-ends, bench:steward-ssh-two-principals, bench:init-refuses-stack, bench:memory-host-tests, host:testbench::a_qmp_socket_is_private_and_binds, host:testbench::heap_fits_holds_an_eighth_of_the_cap_over_the_peak

A boot case under init can set memory = true. After its console verdict the bench stops QEMU over QMP and dumps the guest’s physical RAM beside the case’s log, as <case>-<arch>-smp<N>.ram. The runtime writes each server’s heap record before main, so the record is the witness that a server has started: a dump missing a declared server’s record lets the guest run on and is taken again, until every record is present or the case’s deadline passes, when the case fails. A server’s peak is therefore the most pages its heap had held when the last declared server had started, or later, never earlier than the stop line. A wait is printed first, as memory: dumped twice, waited S s for NAMES. The launcher has painted each server’s first-thread stack with a tag for that server and an index for every eight-byte unit. The bench scans the RAM for those tags at their encoded offsets within physical pages. That ignores paint words copied into ordinary stack slots, while refusing a missing server, a duplicate unit or an out-of-range index at an encoded offset. A stack page’s units are counted from the one physical page that holds the most of them, so a stack word copied into a buffer or a message is not a duplicate. The lowest missing unit marks the stack’s deepest touched point; two pages holding equally many of a stack page’s units are refused for that unit’s stack page or one below it, and ignored above it, where either leaves the peak where it is. The bench prints stack NAME PEAK of PAGES pages for each server and fails when the declared pages are less than twice the measured peak rounded up to a page. The runtime paints each stack it spawns a thread on the same way, with the server’s tag, the spawn’s number from 1 and each unit’s index from the top, since the stack’s size is the program’s, not the manifest’s (redoubt-rt); the bench prints stack NAME thread N PEAK for each it finds, the peak the deepest unit overwritten under the deepest one found, which is the stack’s bottom short of an overflow (which ends the process at the guard page), and checks no margin: the program’s constant (beamlet’s SCHEDULER_STACK_PAGES) is sized from the largest by hand. The dump, the size of the guest’s RAM, is deleted once scanned; a scan that fails on a duplicate or out-of-range unit, or cannot read the dump, keeps it as the evidence. The QMP socket is in a directory of the run’s own under the temporary directory, made 0700 under a name drawn at random, so whatever the bench’s umask only its user can reach the socket and no other user can leave a file where it will be; the directory and the socket go when the run ends, passed, failed or in error. A bench killed outright leaves the directory, empty of any listener since QEMU dies with the bench, under $REDOUBT_TMP, the job’s scratch. A temporary directory so deep that the socket’s path would reach a Unix socket’s 108 bytes is refused before QEMU starts, naming the limit. The manifest’s stack_pages defaults to 16 and cannot exceed 128 (the boot manifest).

Each server’s runtime also keeps a heap record, 32 bytes in its data: a magic word, the server’s launch tag, its heap cap and the most pages its heap has held at once (the native runtime). The runtime writes the magic word and the tag before main, so the program’s file and the launcher’s copies of it hold none. The same scan finds each server’s record by its magic word and tag and prints heap NAME PEAK of CAP pages, or heap NAME PEAK pages uncapped. It fails a missing or duplicated record, a record whose cap is not the manifest’s heap_pages, and a capped server whose cap is less than twice its peak; an uncapped server is reported only. A case that drives a workload within a server another case sizes from its idle peak sets heap_fits = true, and its capped servers pass instead when the peak leaves at least an eighth of the cap unused: the question there is whether the work fits, not what the server’s size should be (beamlet-compile-footprint).

The standard image is scanned after init-boot, userland-boot and userland-read-only on both widths, and after steward-session-ends and steward-ssh-two-principals, whose SSH logins are the most its servers do. Its declarations are twice the largest peak across those runs: each stack rounded up to pages, each heap cap in pages. sshd is sized for its four slots (its entry’s buckets=4, sshd) busy at once: its heap held 8 pages at boot, 54 with one login (rv32, before the boot pack) and 56 with two at once, so at most 46 a connection, and its cap is twice 8 pages and four connections, 384. Its declared stack is a page over twice its peak. ipd’s cap is not twice its peak either: it holds a base of twice its peak apart from its socket tables, 2 × 37 = 74 pages, and every socket its buckets may charge, its buffers, its slot and its table entries, 108 × 4.25 = 459 pages, since a socket the heap could not hold would fail an allocation in a shared server (ipd). Its peak of 61 pages holds those tables, sized at start for its 108 sockets, 24 pages beside the 37 of everything else. consoled’s row is from the runs once it serves each session’s console as a multiplexed session. The two walfsd rows are one server’s, from six runs of walfsd-quota, three on each width, which writes through it, as the image’s memory cases do not (their boots peak at 16,040 bytes of stack and 9 heap pages); its heap cap is also above what a transaction of the format’s 32 blocks adds to that case’s peak, 32 pages, since no case writes that many at once (walfsd). The read-only case also scans its additional client from the merged manifest.

Image serverLargest stack peak (bytes)Declared stack (pages)Largest heap peak (pages)Heap cap (pages)
keyd7,368448
consoled10,38461122
bootfsd7,32041,0892,304 (the image publishes beamlet, piped, consrelay and crossing, and the cap follows each manifest’s own published total)
blkd4,52031938
netd4,296324
ipd13,768761533 (twice its peak apart from its socket tables, 74, and its buckets’ 108 sockets’ buffers, which the cap must hold, ipd)
walfsd:data28,616141564
walfsd:alice-secrets28,616141564
blkd:system4,52031734
verity:system8,264559118
erofsd:system9,70451326
steward16,39291530
sshd5,256456384

The read-only client’s largest stack peak is 6,616 bytes and its heap’s 31 pages; its case uses the 16-page stack default and no cap. A session’s beamlet is no manifest server: the steward launches it with an 18-page stack, twice beamlet’s stack peak of 36,136 bytes (beamlet-footprint on rv64, with the boot pack read before its VM starts and its console on the hub; a compile at the prompt peaks at 34,280 on rv64 and 25,832 on rv32 in beamlet-compile-footprint, whose heap is judged under heap_fits: 9,135 and 8,798 pages of the 11,220 cap), its second scheduler’s thread with a stack of the same size (its peak at the prompt between 21,496 and 25,200 bytes on rv64 over three runs, 21,752 on rv32, stack beamlet thread 3; the platform’s three other threads stay under 1,600, beamlet-footprint), and a heap cap of what its share holds beside its two schedulers’ stacks and thread pages, its locks’ endpoints and its process’s page, 11,220 pages of the 11,264 the steward gives it of the 11,392 sizes gives a session, the rest its console relay’s (budgets, the steward): 108 pages over twice its heap’s largest peak across the memory cases on each width, 5,556 pages (rv64 at 1 hart), above what its prompt holds (beamlet). beamlet-footprint scans the VM alone, under its own copy of the single-VM manifest. Its cap leaves its process heap, ETS and persistent_term limits, a sixteenth of its budget each (696 pages), reachable: a flooding process, about four times its limit, still fits under the cap (beamlet). A context’s console relay is no manifest server either: consrelay-footprint has init start it under a manifest of its own, beside a stand-in that takes its hello, and scans it once it says it serves, since it reserves every buffer before then. Its first thread’s stack peaked at 8,360 bytes on rv64 and 7,392 on rv32, its heap at 22 pages on both; the steward launches it with a 5-page stack and a 44-page heap cap (consrelay). The steward’s own cleanup thread and launch thread are the two threads it spawns painted (stack steward thread 1 and thread 2): in steward-session-ends the cleanup thread’s stack peaked at 1,432 bytes on rv64 and 1,168 on rv32, and the steward gives it one page, twice 1,432 being 2,864; the launch thread’s at 4,840 and 3,808, and it gets three pages, twice 4,840 being 9,680 (the steward).

This is a measurement of the paths the case drove. Other requests or deeper call paths may need more stack or heap, and any guest, including another server, can forge the public paint pattern and the heap record. The result is evidence for the image’s declarations, not a proof against hostile guest code.

Vendored dependencies

Crates as published

Status: built · partly tested: provenance against crates.io needs the network, so no bench case runs it; it is run by hand in the review of any change to `vendor/` · tested (11)
  • bench:vendor-check
  • bench:vendor-build
  • host:redoubt-vendor-check::the_real_structure_passes
  • host:redoubt-vendor-check::a_renamed_header_fails_before_any_download
  • host:redoubt-vendor-check::a_missing_row_fails
  • host:redoubt-vendor-check::a_row_without_its_directory_and_a_stray_directory_fail
  • host:redoubt-vendor-check::vendored_files_are_the_published_bytes
  • host:redoubt-vendor-check::the_vendored_copies_are_the_ones_that_build
  • host:redoubt-vendor-check::the_patches_point_at_vendor
  • host:redoubt-vendor-check::the_readme_records_each_crate
  • host:redoubt-vendor-check::every_vendored_file_is_tracked

vendor/ holds third-party crates exactly as crates.io published them, each used through a [patch.crates-io] path, and vendor/README.md records each one’s version, license and published checksum. Git must track every vendored file: a crate’s own .gitignore applies inside vendor/, and many name Cargo.lock. Two checks guard them, and they prove different things:

  • Integrity since vendoring (vendor-check, every bench run): every file is byte for byte what vendor/SHA256SUMS records, nothing is added or removed, and the build takes the crates from vendor/, never from a registry copy. The checksums were taken from the tree itself, so this proves the crates have not changed since they were vendored, not that they are what crates.io published. vendor-build checks they build no_std for both widths.
  • Provenance (tools/vendor-check/provenance.sh, in review): downloads each published crate, checks its SHA-256 against the live crates.io index and against vendor/README.md, and compares it with the vendored copy. It fails closed: before any download it checks that the README’s table and vendor/ name the same crates, in the same number, and it exits 0 only if every crate it checked matches on all three counts and it checked as many crates as vendor/ holds.

The residuals: provenance is only as current as the last review that ran it, and the vendored crates’ unsafe is checked by recorded Miri runs, not by a bench case (ipd under Miri, sshd under Miri).

Patched crates

Status: built · tested (4)
  • bench:vendor-check
  • host:redoubt-vendor-check::vendored_files_are_the_published_bytes
  • host:redoubt-vendor-check::a_patched_crate_differs_only_by_its_patch
  • host:redoubt-vendor-check::every_patch_is_a_vendored_crates_and_recorded

A crate we must change is still vendored from its published bytes, with exactly one patch file, vendor/patches/<crate>.patch, holding every change. vendor/<crate>/ is the published crate with that patch applied, since that is what Cargo builds, and nothing else differs.

  • Integrity: vendor/SHA256SUMS records the published bytes. vendor-check copies the crate, reverses the patch on the copy, and requires the result to match the sums byte for byte, so the patch file is the whole difference.
  • Provenance: provenance.sh downloads the published crate, applies the patch, and compares the result with vendor/<crate>/.
  • The README records each patched crate’s patch: what it changes and why, as its own section.
  • A new release of the crate means taking the published bytes again and redoing the patch on them; a patch the crate’s author has taken goes away with the release that carries it.

sunset is patched (sshd), and what its patch does is tested through its public API (tools/vendor-check/tests/sunset_patch.rs). ascii is patched too: rustc 1.98 refuses to build it from a path as published, since Cargo caps a registry crate’s lints, not a vendored one’s. miniz_oxide is patched to box the deflater’s 64 KiB code buffer under with-alloc, as it is on wasm32, so its state is never a 65 KiB stack local on a scheduler thread (beamlet; tests/zlib_codec.rs measures the inline and the boxed parts).

The no-cruft gate

Status: built · tested: bench:no-cruft, host:testbench::a_rule_scoped_where_nothing_is_searched_fails

no-cruft.toml reads the sources and boots nothing. It fails on:

  • a name of an interface the tree has dropped (its forbidden patterns);
  • the native runtime handing out the raw call: libs/rt/src re-exporting redoubt-sys whole (alias, glob, self or extern crate), or a pub item or one-line re-export there naming syscall (forbidden patterns held within that path; a within that is missing or outside the case’s paths fails the case);
  • allow(dead_code) or allow(unused...) in the kernel, the loader, the layout and paging crates or the test programs;
  • a Cargo feature that no cfg(feature) reads;
  • a second literal definition of PAGE_SIZE or USER_AREA_END, or any const PAGE alias; the model is searched too, and its own PAGE_SIZE in model/src/spec.rs is an [[allow]], because the model is the independent oracle and depends on no implementation crate.

Its [[allow]] entries (path, rule, reason) are the only exemptions, and an entry that no longer covers anything fails the case too.

The formatting gate

Status: built · partly tested: that a skip with no reason, or one that names no workspace, fails is read from the code, not run by a self-check · tested: bench:formatting, host:testbench::only_tracked_workspaces_are_reported, host:testbench::diff_headers_of_both_rustfmt_forms_name_the_file, host:testbench::every_elixir_file_is_walked_from_its_deepest_root

formatting.toml holds the tree to the formatting rule: in each cargo workspace root it names (the main workspace, each host-only fuzz or oracle crate that is its own workspace, and userland/otp), it runs cargo +nightly fmt --all --check and fails on every file that is not formatted with the repository’s rustfmt.toml. It also fails on a tracked Cargo.toml with a [workspace] table that is neither a root nor a [[skip]], so a new crate outside the main workspace cannot drift unchecked, and on a skip with no reason or no workspace. Two are skipped: bios/, the upstream RustSBI firmware with its own configuration, and the docs checker’s fixture crate, whose layout is the checker’s input. The generated wire codecs (libs/wire/src/proto/) are in rustfmt.toml’s ignore: the generator is their one definition, and its own test holds them to its output. Without nightly rustfmt the case fails, unless --allow-skip. The case file is not called rustfmt.toml: rustfmt would read it as the configuration for everything under tests/.

The Elixir is held the same way, and by the file rather than by the project: the case lists every .ex and .exs git tracks or has not ignored (so a file about to be added counts, wherever it is put) and runs mix format --check-formatted on them, under the pinned toolchain, from the deepest of the [elixir] roots above each, which is where its .formatter.exs is: the repository root, whose .formatter.exs (110 columns, as rustfmt.toml sets) covers the steward’s and the wire’s Elixir, the OTP test programs, the bench’s script and the docs checker’s fixtures; and userland/shell, the shell’s own. Each root must hold a .formatter.exs, and one anywhere else is a finding, as a configuration the walk would not use; a file under no root is one too. Three directories are skipped with their reason, as the Rust codecs are: libs/wire/elixir/proto and client, redoubt-wire-gen’s output, and libs/steward/elixir/gen, redoubt-steward-gen’s; each generator’s test holds its files to its output. A skip over no Elixir, or without a reason, fails. Before this walk only the shell’s ./test-shell ran mix format, over the shell’s own inputs, and the bench ran none: the steward’s reference, the wire’s hand-written Elixir and the OTP test programs went unformatted for as long as they existed. Without the pinned mix the case fails, unless --allow-skip.

The docs checker

What it checks

Status: built · tested (9)
  • host:redoubt-doccheck::good_tree_is_clean
  • host:redoubt-doccheck::narrow_cases_fire
  • host:redoubt-doccheck::c1_reports_each_failure
  • host:redoubt-doccheck::c13_reports_each_failure
  • host:redoubt-doccheck::index_over_its_ceiling_names_the_largest_pages
  • host:redoubt-doccheck::pages_scope_keeps_only_the_listed_pages
  • host:redoubt-doccheck::pages_scope_keeps_a_directory
  • host:redoubt-doccheck::untracked_code_is_not_checked
  • host:redoubt-doccheck::a_copy_under_an_ignored_directory_is_checked_whole

redoubt-doccheck (tools/doccheck) holds this book to its own rules: cargo run -q -p redoubt-doccheck prints each finding as path:line: C<n>: message; --pages <path>... keeps only the findings on those pages, and --code adds C11, the check of code comments and case descriptions for the documentation switch-over. It checks that every section has one well-formed status line and every test it names exists; that milestones carry their names; that no page carries process references; that every rule ID is defined once and cited by its short name; that every relative link resolves; that the security register agrees with the pages; that no binary sits under docs/; that pages keep their templates; that every wire table is included once; that every page is in the table of contents; and that every count in a `unsafe` (pinned) column equals the ceilings in unsafe-budget.toml (the unsafe budget), summed over the budgets under a row’s Where paths or read by the name in its Ratchet budget cell. Each rule has a small bad tree it must fire on and a good one it must not. mdbook build docs renders the book; its search index is held to the ceiling the book’s rules state, a failure naming the size and the three largest pages, and the check has its own small book over the ceiling.

Running its tests. cargo test -p redoubt-doccheck runs them from any directory and any shell the project supports (through scripts/q too); the bench’s docs case runs the same suite (below). The fixtures are found by the crate’s own path, not the working directory. C11 asks git which files under the tree it checks are tracked, so that a checkout’s untracked files (reference sources, scratch) are not Redoubt’s code; a tree that is no tracked part of a repository, outside one or under an ignored directory such as .tmp/ or target/, is checked whole, and the caller’s GIT_DIR does not redirect the question.

The docs checker in the bench

Status: built · tested: bench:docs

A host-tests case runs the checker’s tests, among them one that checks this whole book and one that builds it with mdbook and fails on any warning, on a search index over its ceiling and on an indexer older than the book needs; the checker also reads code comments and case descriptions, so they cite pages and rule IDs that exist.