The executable model

The executable model is a Rust crate, redoubt-model in model/, that states the kernel’s objects, calls, errors, rules and invariants as code, with the steward’s policy core on top. Seeded random sequences of calls drive it, and after every step a checker recomputes each invariant from the objects themselves. Deliberate breaks of each rule, the mutations, show that the checks catch what they claim to catch. Every run can be written as a text trace and replayed; replaying those traces on the real kernel compares the kernel with the model.

Purpose

A rule in prose can be read two ways; a rule in code cannot. The model is the design in a form a machine checks: if any sequence of calls it generates reaches a state that breaks an invariant, it reports the seed and a shrunk trace that shows how. It is the reference the kernel is built to: the same call names, the same errors, the same constants and the same order of argument checks (ABI). A design change is tried in the model first, because a change that breaks a property fails there in seconds, on a laptop, with the failing sequence in hand.

What the model is

Status: built · partly tested: independence from the kernel’s source and the empty dependency list are held by model/Cargo.toml and #![forbid(unsafe_code)], not attacked by a case · tested: host:redoubt-model::overflow_checks_are_on, host:redoubt-model::map_fixed_near_user_top_does_not_starve_map_anon, host:redoubt-model::event_free_tick_matches_slice_reference

• Independent. The crate is no_std with alloc, #![forbid(unsafe_code)], and its [dependencies] table is empty: it links no kernel crate, not redoubt-sys, nothing from crates.io. It states its constants itself, with the kernel’s names and values: WORDS (4), MAX_MSG_HANDLES (4), MAX_HANDLES (4096), MAX_LEND_PAGES (16), MAX_THREADS (255), WAIT_CAP (32), MAX_OPEN_CALLS (256), SLICE (1,000 µs), STRIDE (2^20). Two crates use the model, each as a dev-dependency: redoubt-stride, for its differential test (below), and the test bench, whose scheduling oracle must reject traces from the model’s scheduler with its tie rules broken.
• One method per call. Kernel in model/src/kernel.rs has one method for each call, with the call’s name. Every argument arrives as a raw u64, as from user mode, and the checks run in the kernel’s order: decoding as redoubt-sys decodes, then each argument from left to right, then permission, then resources.
• Overflow is a failure. The root Cargo.toml keeps overflow checks on for this crate in both dev and release builds, so an arithmetic overflow is a panic, and the runner counts any panic as a failure of I14 (no call panics the kernel). overflow_checks_are_on fails if a build turns them off.

What it abstracts

• Memory is page frames with one word of content each. Loads, stores and fetches check the mapping’s permissions. A freed frame is in flight, still holding its word, until a tick, when the one hart the model runs zeroes it and frees it, as several harts do between sections (R81 (frames in flight)); a frame never used since boot holds a word of its own until its first allocation zeroes it. A process’s own mapping, a server’s view of a lend and the lender’s reservation are separate states. Page tables follow Sv39’s layout as a placement rule, even when the cost table is rv32’s.
• Threads have no registers. A call is instantaneous and atomic; time is logical and advances only on a tick. So the model tests accounting and state changes, not real-time latency, and not races between harts. A tick charges time slice by slice, but where nothing is due, to deliver or to wake, its whole slices are charged at once: with one budget queued, or with several (the same picks, charges and requeues, on the queued budgets alone). event_free_tick_matches_slice_reference holds every such tick equal to the slice-by-slice reference, field by field, on boundary worlds of one to five queued budgets and on random histories, with no mutation and under every one.
• Records (the user memory a call reads and writes) are abstracted as a whole: owned, unmapped, read-only, borrowed, device memory, a copy that faults, or an address whose every page, for the call’s record size, is checked against the modelled mappings. Byte layouts are not modelled.
• PIDs are drawn by a seeded generator from 2 to 0xffff; init is 1. This tests reuse and accounting, not unpredictability.
• Addresses the kernel chooses are the kernel’s: a map_anon, map_device or dma_alloc run is placed in the 256 MiB area from DEFAULT_BASE, and a receiver’s lend or transfer in the 4 MiB area from DEFAULT_MESSAGE_BASE, each searched as the kernel searches it (memory). A full area is refused as the kernel refuses it.
• Costs come from a costs table: by default the kernel’s table (one header page per process, one page for each other object, 64 handles per handle-table page). The property tests use 8 handles per page, so handle-table growth and its charge show up in short runs.
• Boot. root, system and users get the kernel’s weight split: root 1,000,000, system 250,000, users 749,000, so root keeps 1,000 free for init. Page and process limits are small fixed numbers (root: 1,024 pages, 24 processes), not derived from RAM. The default boot has seven device objects: an MMIO range without DMA, an MMIO range with DMA, IRQ lines 10 and 11, the reset device, a DMA device whose first reset is not confirmed, and a second DMA device whose resets always confirm.
• Where the design leaves a detail open, the model makes a choice and the code says so at the site.

Property families

A family is a function of one seed and an optional mutation. The runner (model/tests/common/mod.rs) runs seeds on several threads, keeps the lowest failing seed, and counts a panic as an I14 failure. A failing kernel sequence is shrunk to the steps that matter and printed as a trace. Rerunning the seed reproduces the failure exactly.

The generator (model/src/gen.rs) first builds a world worth attacking: principals’ budgets under users, some labelled and with accounts, a system budget, shared endpoints, handles minted into the principals’ budgets, and a process in each budget. One sequence in five skips this setup and starts from init alone. Then it picks operations from the model’s state: a handle the actor holds, a page it has mapped, a message it serves. About one argument in ten is hostile instead (a handle index the actor lacks, an unaligned address, a list over its cap). every_call_and_error_is_reached checks over 5,000 seeds that every call succeeds at least once, every error is returned by some call, and lends, transfers, each exit cause, interrupts and replies all happen, so no property holds only because nothing reached it.

A default run is 65,020 sequences. The bench case model-host-tests runs it but for the steward families, in under two minutes, the build included; steward-model-host-tests runs those two, each a job of its own on four threads (fanout), with the check below, in under two minutes, the build included. REDOUBT_MODEL_SEQUENCES sets the count per family. A bound on cargo’s test threads is a bound on the whole binary: each test’s runner spawns MODEL_THREADS threads if it is set (a positive integer; anything else fails the test, naming it), else one if RUST_TEST_THREADS is set, else one per core. The test million runs 1,000,000 sequences in each of the five non-flood families and 1,000 floods; it is marked ignored and runs only when asked for.

A steward operation, the core’s decision, the embedder’s calls on the kernel model and every check after it, costs tens of microseconds. Most of a steward seed is its ticks of minutes over several queued budgets, which cost a thousand slices a second of model time slice by slice and are charged in batches (what it abstracts). Measured on one thread, in release:

The counts come from what the seeds reach, not from habit. model/tests/steward_reach.rs records, per seed, each rule of the core’s Policy table that held and each that refused, each effect that ran, each filter’s answers, and each property’s first instance (a session’s budget checked, a declassification copied out, a blame, a lockout, a lease ended, an observation after vault work left out). Searched to 20,000 seeds, steward_policy reaches 148 of these, its last new one at seed 439, and to 10,000 seeds steward_noninterference 151, its last at seed 296. A family’s count comes from that measured seed of its last new coverage: four times it, rounded up to a thousand, but never below a seed at which the family’s random search catches a mutation (PolicyDeclassifyUnfit at 1,418, and PolicyDeclassifyLive at 1,166), so 2,000 for each; steward_noninterference runs 3,000, a margin it keeps. The counts are for coverage: the three mutations whose state the random search builds only by chance are held by their named scenarios (mutations), whatever the counts. the_reach_table_is_reproduced checks what the first seeds reach: seeds 0 to 439 of steward_policy reach 148 items and 0 to 296 of steward_noninterference 151, the last of them first at that seed, so a change to the generator, the core or the checks that moves either fails. That no later seed reaches a new item, and the catch floor of 1,418 and 1,166, come from the ignored runs (reach_table, catch_table in model/tests/steward_reach.rs): they are recorded here and checked by no test. Four of the core’s effects, and the refusal of its rule is_context, are reached by neither family (residual risks).

The checker

After every step, Checker::check (model/src/invariants.rs) runs its checks in a fixed order:

• the objects’ structure; the console’s holder is a live process (the console’s one writer); serving state;
• handles: I1 (handles name live objects), I2 (revocation is complete), I3 (minted badges are non-zero and narrow) and I4 (only badge-0 handles receive);
• charging: I5 (usage within limits), and R6 (charging)’s backing: root’s limit and its own page fit in the boot’s ram_frames;
• budgets: I6 (labels only grow downward) and I8 (class and account inherited);
• the step’s flows and call outcomes;
• memory: I9 (pages W^X, zeroed, lends unmapped) and I16 (DMA pages reset before reuse);
• queued messages, then abandoned-call notices: I15 (abandoned calls reported once);
• delivery, exit notices owed, and timeouts: I13 (every blocking call returns by its timeout).

I12 (ids never reused) is checked from ghost records as ids are issued.

Each check recomputes what should be true from the primary objects (handle tables, budgets, frames, each thread’s wait state) and from ghost state, never from the counters and derived fields the kernel model keeps. Ghost state (model/src/ghost.rs) is recorded from the primary objects at the moment of each event, and nothing in the kernel model reads it. So a bug, or a mutation, cannot hide itself by also changing what the check believes.

The flow checks judge each step against the ghost records:

• a delivered message is the one sent: its kind, badge, account, labels and handles are what the sender’s handles and budget gave, a handle revoked meanwhile arriving as 0 and every other keeping its stamp;
• it reached a thread receiving through a badge-0 handle to its endpoint, and between user budgets only equal label sets flow, the receiver being the endpoint’s owner (R1 (flow), I7 (every flow obeys R1));
• LabelDenied and Busy happen only when R1 and R2 say so;
• a caller gets a reply only when its server replied, and an abandoned-call notice goes to the thread holding the call, once;
• every completed call reports the lend disposition its history implies, and a present reply only with success or OutOfMemory.

For I16, the ghost arms each DMA frame against every device its holder could reach, and disarms a device only on a reset that the device object confirms (not on what the kernel model reports). No frame in the free pool may be armed. A confirmed reset at one process’s death disarms only that process’s frames: a live co-holder that still reaches the device can program it again, so its frames stay armed until its own death resets the device. A quarantined frame must be mapped nowhere, and a quarantined device used again is a violation. The default boot’s second healthy DMA device exists so the generator can build the co-holder shape; reset_at_one_death_does_not_cover_a_co_holder builds it by hand.

Scheduler scenarios

scheduler_fairness draws one scenario per seed and drives the scheduler alone through time:

The shares in the last seven are water-filling’s, computed by the scenario from its weights and threads, in thousandths of a hart over 400 slices from one slice after the event, within 50 per thousand of the machine. The scheduler runs any number of harts (Scheduler::set_harts); each pick is one hart’s, of the lowest-ranked budget with a runnable thread no hart runs, and the cap set is found its own way, by water-filling to a fixed point over every queued budget.

The rules themselves are on scheduling.

The flood

flood is the endpoint-flooding attack, in the model. A system server receives on one endpoint with two threads. Bob’s processes, with two label sets under one account (so two R2 groups), run up to a fixed 31 threads each (the attack’s shape, not MAX_THREADS), all calling with no timeout. Enough other accounts that more than MAX_OPEN_CALLS calls can queue (seven to twelve) queue WAIT_CAP calls each, and the server’s budget has a page for each open call. Alice makes one call in the middle of the flood. Most of Bob’s calls must get Busy, no crowd process may get Busy within its own group’s cap, and Alice’s call must be taken within as many receives as there are groups. In half the seeds the server hoards: it receives without replying until the process holds MAX_OPEN_CALLS, spread over both threads, and it must still take a send. The checker runs every 512 steps and at the end.

Scripted contracts

Some cases are rare in random runs, so fixed sequences pin them. The IPC contracts are written from the completion table, not from the model’s output. They cover:

• every row of the completion table and the rollback of a reply that cannot be written, for R13 (one outcome per call); reply masks that are positional, not a count (model/tests/current_contracts.rs);
• a timeout wakes without preempting, a timeout and a budget deadline at one instant expire in that order, budgets with no free weight are refused a process, and the pick and switch into a budget are billed to the budget picked, not to the one whose thread blocked before it; at two harts, a budget whose last thread ends on its hart raises the floor to no pass of its own (R12EmptyHoldsFloor), and a heavy budget whose slice ends before any other floor raise saw it run is capped by the raise its own slice end makes (R12RequeueWaitsForCap), and one whose running thread blocks while its sibling waits is not, so the sibling holds the floor (R12BlockLeavesAsRequeued);
• a PID is reused only after its exit notice is received or dropped;
• a destruction delivers nothing until its end: a notice owed during it goes to the receiver that survives, not to one the destruction ends later, and a send stamped with the dying budget fails with Dead;
• a destruction among live siblings ends exactly its own subtree: sixteen children of one parent with a process each, every one reporting to one endpoint, end as a sponsor’s leases do (the process exits 0, the notice is taken, the budget destroyed), in five orders, and after every end each other child still holds its budget, which counts its one process, and its process (model/tests/destroy_contracts.rs);
• DMA frames stay held through unmap, return to the pool only after a confirmed reset, and are quarantined, with the co-holder’s, when a reset is not confirmed (model/tests/dma_contracts.rs);
• map_fixed’s ranges, flags, overlap and cost checks (model/tests/map_fixed_contracts.rs).

The mutation check runs the IPC and scheduling contracts first, for every variant, and a steward scenario for each of the three breaks the steward families catch only after many seeds (mutations).

Mutations

Status: built · tested: host:redoubt-model::every_rule_has_a_mutation, host:redoubt-model::mutations_are_caught, host:redoubt-model::declassify_unfit_scenario, host:redoubt-model::one_cursor_scenario, host:redoubt-model::agent_other_set_scenario, host:redoubt-model::end_lease_admitted_scenario

A mutation is one deliberate break planted in the model. Each variant of enum Mutation (model/src/mutation.rs) breaks one rule, at the sites in the model marked self.broken(Mutation::...): one site for most variants, two or three where the rule is kept in more than one place, and a direct comparison with the mutation for AbandonNoticeMissing and R11LendStaysMapped. With no mutation, the model is the specified kernel. Mutation::ALL lists all 176 variants. Mutation::rule() returns the ID each one breaks, as in the table below; the steward’s variants, named Policy..., break the server rules the steward model checks. Each of those but four is one broken entry of the core’s Policy table (mutation::policy), since the crate that ships has no mutation switch; the other four break the model’s embedder: its entropy, its admission, a volume’s write check and the server’s start.

• every_rule_has_a_mutation requires at least one variant for every kernel rule the model holds (each R row of the table below, before the steward’s) and for I16.
• mutations_are_caught plants each variant in turn. It runs the scripted IPC and scheduling contracts, the variant’s steward scenario if it has one (below), then every property family, the one that pressures the rule first (scheduler_fairness for R12, the steward families for the Policy variants, flood for the open-call limit, steward_noninterference for the breaks that show as one domain’s work in another’s view, R2OneCursor’s turns among them), up to 20,000 seeds each (20 for the flood) but 500 in each steward family. A variant not caught within those caps fails it, by name: one the steward families catch only past seed 500 is caught too late, and so is a failure, not a wait. It prints the property and seed that caught each one. REDOUBT_MODEL_MUTATIONS narrows the run to the variants whose names contain one of its comma-separated words, or to the one a word names whole. The bench case model-mutations runs it once per variant, each a job of its own in release, the names coming from cargo run --example mutations (fanout); model-host-tests skips it. Every variant is caught within the caps, each job in under 20 seconds on one core.
• Four variants whose state the steward families’ random search builds only by chance, or too slowly for the bench’s deadline, have a directed scenario each (model/tests/common/contracts.rs), a few operations that build the state the break needs, tried before any family. Each is a named test that holds on the specified model and catches its variant with the property it names, so these catches are deterministic and the random search is the backstop:
  • declassify_unfit_scenario: a {7} session writes an item one byte over DECLASSIFY_MAX, or one with a control character, asks to declassify it and its owner approves; without the item’s check, P6 sees it copied out. The random search: steward_policy’s seed 1,418.
  • one_cursor_scenario: alice’s and bob’s unlabelled sessions and bob’s {9} session call the server, which takes alice’s call, then the {9} call, then bob’s and alice’s next; with one cursor over every group the last round starts after the {9} group with the vault’s work and after alice’s without, so P10 sees the unlabelled calls taken in another order. The random search: steward_noninterference’s seed 944.
  • agent_other_set_scenario: a {7} session asks for an unlabelled agent and its owner approves; without the own-set check, P10 sees the request in the unlabelled audit view. The random search: steward_noninterference’s seed 48.
  • end_lease_admitted_scenario: alice’s session starts an agent, the two fill her domain’s pending requests, and the session ends the agent; with the embedder ignoring the tables’ ahead-of-admission mark, the full domain refuses it and P13 sees a sponsor that could not end its agent. The random search: steward_policy’s seed 36 and steward_noninterference’s seed 126.

Five of the steward’s former variants are retired, because the core’s types or another rule’s keeper keep their rules and they cannot be written: blame or a pending cap counted per account and a session carved from another label set’s sub-budget each need a second domain, R41 (narrowing by revocation scope)’s narrowing to a session’s budget needs a budget where the core’s Connect takes only a scope, and an approval granting more than its approver holds needs a request whose labels its principal does not own, which owns_labels refuses at entry and at submission (PolicyVaultWithoutOwnership) (guards and effects).

Six rules are outside the model and have no variant: R15 (verified boot), R16 (image confinement), R17 (fail closed), R19 (kernel W^X), R23 (no test channels) and R24 (SUM and MXR clear). The model has no loader, no bundle, no kernel mappings of its own and no test build.

Traces

A trace is a run as ASCII text: the boot, then each event with the result the model gave. trace::record writes one, trace::parse reads it back, and trace::check replays it on the model and requires every line to match. The module is no_std and works on &str, so a replayer running on the kernel can use trace::tokens as it is.

Names mark the values the kernel chooses, so a replayer can bind each to its own: p: a PID, t: a TID, h: a handle index, m: a message id, a:BASE+OFF an address OFF bytes into a region the kernel placed, pa: a physical address, tm: a time read (compared only for order). A call’s result carries the three facts of R13: call status=... lend=none|returned|consumed reply=absent|present, with the reply’s words and handles only when present. A reply’s result is ok reply delivery=delivered|discarded mask=N.

Results alone miss a kernel whose state has diverged but not yet shown it, such as a handle that should have been revoked but is never used again. So random traces end with an epilogue (check::epilogue): time passes until every finite timeout has returned; each process with a runnable thread reads one word of every readable page it maps and the usage of every budget it holds; init destroys the budgets it made, one at a time, reading usage after each; and each live process closes every handle index from 1 to EPILOGUE_HANDLES (64). A thread blocked for ever, a budget’s account (it travels only in messages) and an IRQ source’s mask stay unseen.

model/traces/lender-dies-mid-call.trace is the checked-in example: a client lends two pages to a system server, and init destroys the client’s budget while the server holds them (R3). Its end:

do p:61415 t:3 call h:1 [1,2,3,4] [] a:0x60000000+0x0@2 forever -> blocked
wake p:38622 t:2 -> ok message call m:1 badge=5 account=1001 labels=[] words=[1,2,3,4] handles=[] buffer=[lend,a:0x40000000,2]
read p:38622 t:2 a:0x40000000+0x0 -> ok word 42
write p:38622 t:2 a:0x40000000+0x0 99 -> ok
do p:1 t:1 budget_usage h:13 -> ok usage [32,10,1,1,50,0]
do p:1 t:1 budget_destroy h:12 -> ok
read p:38622 t:2 a:0x40000000+0x0 -> ok word 99
do p:1 t:1 budget_usage h:13 -> ok usage [32,10,1,1,50,0]
do p:38622 t:2 receive h:1 0 0 -> ok abandoned m:1
do p:38622 t:2 reply m:1 [0,0,0,0] [] -> ok reply delivery=discarded mask=0
do p:1 t:1 budget_usage h:13 -> ok usage [32,5,1,1,50,0]
do p:38622 t:2 receive h:1 0 0 -> ok exit p:61415 cause=killed code=0 blamed=0 blamed_labels=[]

Figure: the end of the example trace. The server keeps the lent pages after the lender’s budget is destroyed, is told the call was abandoned, and frees them by replying.

The tests:

• traces_round_trip writes 3,000 random sequences, reads each back to the same operations and replays it.
• a_rule_breaking_kernel_fails_replay lets a mutated model stand in for a kernel that breaks a rule. It replays 2,000 random traces with epilogues, plus seven scripted ones (a partial reply, current-call blame, the equal-instant expiry order, a quarantined device named again, a record gone bad as an abandoned-call notice or an interrupt comes, and a notice owed during a destruction), and requires some trace to fail for every variant that results can show. Not required, because results cannot show them: the Policy variants; R12’s, since scheduling shows only in timing; R5NoMaskOnFire, since every result is the same and the model’s own R5 check catches it; the three open-call-limit variants, since random traces never reach the limit (the flood does); and DmaResetClearsCoHolderReach, which only the I16 ghost check sees.
• the_example_trace_is_what_the_model_does rebuilds the example and requires the same text.
• hostile_traces_are_refused_cleanly feeds fixed worst cases and 500 randomly damaged traces to the replayer. Each worst case must give an error; a damaged trace must not panic, and may still replay (a damaged line can be one the model accepts).

flowchart LR
    S[seed] --> G[generator]
    G --> K[kernel model:<br/>one step]
    K --> C[checker:<br/>invariants, ghost]
    C -- fails --> X[shrink and<br/>print the trace]
    K --> R[trace::record]
    R --> T[trace text]
    T --> P[trace::check:<br/>replay on the model]
    T -.-> Q[replayer on the<br/>real kernel]
    Q -.-> V[every line<br/>matches]

Figure: how a run becomes a trace and where it is replayed. Solid parts are built; dashed parts are planned.

The steward model

model/src/steward.rs embeds the steward’s policy core, the crate that ships (the policy core), on the kernel model, and model/src/policy.rs holds its properties. init creates the shared server’s endpoint and the steward’s own, and starts the steward in system, with handles to users, system and both endpoints. The steward starts the server, a system-class process standing in for littlefsd that holds no budget handle, receiving on the shared endpoint. Every principal’s budget and its fixed sub-budget per label set is a budget_create at boot. Then the core decides every call, and the embedder runs each batch it returns as calls on the kernel model, in order, stopping at the first failure, and reports it back. So each session and each agent’s lease is a budget carved from its domain’s sub-budget, a revocation scope inside it, connections to the steward’s endpoint and the server narrowed to that scope, and a process holding them. Sessions’ work is real calls to the server; crash blame comes from the kernel’s exit notices of the server, and a session’s end from those of its process. So every kernel check runs under everything the policy does. The embedder keeps only its own half: admission, the volumes and their write check, an ideal keyd signing every audit record, and entropy, one stream per domain for the events that draw ids. The policy is described on the steward.

steward_policy runs 20 to 160 random policy operations per seed and checks the properties and the kernel’s checks after each, and that the steward never exits. Its manifest gives alice’s top 18 processes, so a label set’s share, a third, holds three sessions, one over the cap of two contexts: some top must hold one more session than the cap, or the kernel’s refusal of the third login for processes stands in for the cap’s and the cap rule is invisible to the model (PolicyNoContextCap went uncaught when the one principal with a single label set, carol, became sponsored and her sessions moved under alice’s share). Bob’s top keeps 12, a share holding two, so his domains still fill and a start fails there. steward_noninterference runs one sequence twice, the second time without the vault sessions’ work (their item writes, requests and calls to the server, and the owner’s approvals and denials of their requests), and compares everything an unlabelled session observes, the order the server takes its calls in included. The other host tests pin connection lineage (a delegated badge shares its root’s pending share, checked by an oracle that walks parent edges itself, with a deliberate break it must catch), audit signatures bound to purpose, signer, domain, length and every byte, a confined session refused a read of lower data while its owner pushes one approved item up, and approve and deny refused on a channel that did not open, before any effect.

What the steward model leaves out: SSH (a login is “this key for this user name”), the approval terminal (a channel is “a connection that authenticated with this key”), and real entropy: the words come from a keyed mixer, where the server draws them from the kernel’s random. Audit signatures are ideal tokens, and no chaining, truncation detection or ordering is claimed. The volumes are maps the steward’s batches read and write directly; its reader and writer budgets stand for the processes that would. The steward’s constants are the core’s: PENDING_CAP (4), DECLASSIFY_MAX (256 bytes of printable ASCII), FIELD_CAP (64 characters), MAX_LEASE (24 hours), and the blame window (3 crashes in 10 minutes).

Where the model meets the kernel’s code

Status: built · tested: host:redoubt-stride::the_crate_and_the_model_agree, host:redoubt-stride::a_broken_model_disagrees, host:redoubt-ipclist::the_groups_follow_the_model

redoubt-stride (libs/stride) holds the stride arithmetic and ranks that the kernel links. Its differential test drives the crate, wired as the kernel’s sched.rs calls it, and the model’s Scheduler through the same random sequences: budget creations and destructions (a leaf whose threads blocked first, the budget on the CPU, a whole subtree bottom-up), wakes, blocks, runs, slice ends and preemptions, each on a hart drawn at random. Over 3,000 seeds at each of 1, 2 and 4 harts every pass, entry, remainder, tie, queue membership, the floor, the tie counters, the cap set and each hart’s running thread must agree after every step; at 4 harts some 360,000 of the steps hold two capped budgets or more. a_broken_model_disagrees shows the comparison bites: with any of 30 of the 35 R12 variants planted in the model, some sequence disagrees (the ten of several harts at 2 or 4 harts). It leaves out R12TimeoutWakePreempts, whose site is the kernel model’s timer path, not the scheduler, and R12SliceCountsExitWork, R12DeadlineWorkUnbilled, R12TimerWorkUnbilled and R12SwitchBilledToPrevious, kernel work around a run (the exit work before a slice starts, a deadline’s destruction, a timer’s expiry, the switch into a budget), which the differential does not drive; the model’s own checks catch all five. The bench case stride-host-tests runs both tests. This compares one kernel crate with the model, on the host; the kernel’s own use of it runs in boot cases (scheduling).

redoubt-ipclist (libs/ipclist) holds the kernel’s IPC lists: the links of what waits on each endpoint, device and budget, of the exit notices owed on an endpoint and the processes that report there, of the process objects charged to each budget and counted in it, and of each process’s waits with a deadline; R2’s groups in the order their turns fall due, the expiry’s sort, and each list’s audit. The kernel links it and keeps every rule in message.rs. the_groups_follow_the_model states R2 beside it as the model’s next_sender and served do, and in 200 seeds of 300 random queues, leaves and takes each, the two must pick the same message, for a receiver below MAX_OPEN_CALLS and for one at it. The host-tests case runs it.

Replaying traces on the real kernel

Status: planned · M3 (agents, approvals and the attack suite)

A bench case boots the real kernel with a replayer program and a set of model traces as files in the bundle (test bench). The replayer reads each trace with trace::tokens, binds each name to the value the kernel gives, makes each call from the process and thread the line names, and compares every result, note and wake, the epilogue included. A trace passes only if every line matches. A line the replayer cannot drive is a failure, never a pass, and a trace that exercises a question the design has not settled does not count until it is settled. Usage is compared under the model’s placement of page tables. Traces include the timer-driven rows of the completion table (a taken call timing out, a budget deadline firing), run on the real timer. The case passes when 100,000 model traces replay with identical results.

Replay is what turns the model from a reference into evidence about the kernel.

Open: how the replayer gets init’s boot handles and devices without an interface that exists only for testing; how tick, irq, fault and record lines are produced on the real machine; the boot sizes (the model’s fixed limits against the kernel’s, which follow RAM); map_device’s result (the kernel returns the address and the length, the model only the address); a receive record that passes decoding but faults when written (Record::CopyFault), which has no kernel counterpart and stays out of traces; completion races between harts, which a sequential trace cannot express; scheduling and IRQ masking, which results do not show.

Residual risks

• The model checks its own abstraction. Properties that hold and mutations that are caught show that the model agrees with itself and that its checks bite on it. They say nothing about the kernel. No trace has been replayed on the real kernel, so every “attacked only in the model” on the kernel pages rests on the model and the kernel agreeing, which nothing has shown. A model that has drifted from the design keeps passing its own tests; only replay or a reader finds the drift.
• Host tests do not reach the kernel’s boundaries. Timer-driven cancellation, the kernel’s locking and completion races between harts are outside the model: a step is atomic and time is a counter. Passing model runs establish none of them. The kernel crate itself has no host tests: its binary says so (test = false), and its rules are tested on the target by the bench.
• One boot case copies model results by hand. tests/programs/src/bin/budget-test.rs runs a short budget sequence whose expected results were read off the model. Nothing re-derives them from the model, so a change to the model leaves them stale without a failure.
• Finite worlds. The default run is 65,020 sequences on small boots (the testing boot’s root has 1,024 pages and 24 processes), and random record changes target blocked calls only. Sizes and mapping geometry bound what the runs explore. The million-sequence run is a separate test that the bench does not run.
• The steward model’s embedder is the model’s own. The core it runs ships, but the server’s embedder (transport, admission, running batches) is not this one. Its entropy is ideal, and the non-interference comparison leaves out a server crash on its own and one a vault’s call causes: which call such a crash blames, and when the server takes the calls before it, is service timing, a stated residual of R37 (vault non-interference).
• No property checks that a takeover tells the old channel. The attachments property checks that every note a relay is given is printable, not that a takeover gives the old channel one, so a core that let the old channel go in silence would pass; no mutation drops the note. The server’s host test a_login_to_an_attached_context_takes_it_over and the bench’s steward-context-login check the note.
• The steward families reach no failed crossing, and no login to a starting context. Neither family, searched to 20,000 seeds, makes a declassification’s copy out or a push fail, so the core’s effects for a failed crossing (audit_copy_failed, audit_push_failed, pass_failure) never run in the model and no property is checked on their outcome. The model runs a session’s batch to its end within the login, so no second login finds a context still starting, and the in_use refusal (refuse_in_use) runs only in the core’s host tests. The model has no console session, so every session it detaches is a context and the rule is_context never refuses; its refusal runs only in the core’s host tests too. steward_policy never calls the audit filter (audit_visible), which only steward_noninterference’s audit view reaches. The counts are set from what the families reach (property families), which bounds what a lower count gives up, not what the generator never builds. The four breaks whose state the random search builds only by chance, or too slowly, (PolicyDeclassifyUnfit at the policy family’s seed 1,418) are caught first by directed scenarios, which pin the state each break needs rather than show that the generator finds it.
• Rules outside the model (R15, R16, R17, R19, R23, R24) have no model check at all; their boot cases are their only attack.

Why

• Independent of the kernel’s source. A model that shared code with the kernel would share its bugs. Its one dependency is the steward’s policy core, which it embeds so that the steward’s families attack the code that ships. Otherwise the model can be read side by side with the design, and every failure is reproduced from one seed.
• Ghost state apart from the kernel model. The checks read facts recorded at each event from the primary objects, never the kernel model’s own counters, so a wrong update cannot also correct the check that should catch it.
• Mutations, because a property can hold for the wrong reason. A check that nothing reaches passes every seed. A planted break that no property catches names the gap, and every rule keeps at least one planted break so that a weakened check shows up as a surviving variant.
• Text traces, with an epilogue. Text is easy to diff, to shrink and to carry into a bundle, and a no_std parser serves the model and a replayer alike. The epilogue exists because a kernel can diverge silently; probing memory, usage and handle tables at the end makes the divergence show in a result.
• The steward on the kernel model, not beside it. Running the policy on real modelled calls means every kernel invariant holds under everything the policy does, and non-interference is judged on what the kernel actually returns.