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

Memory

A process gets memory only from the kernel, in whole 4 KiB pages, paid for by its budget. Five calls change what a process has mapped: map_anon, map_fixed, unmap, set_flags and process_map. The kernel zeroes every page before a process first sees it, never maps a RAM page writable and executable, and chooses every address but the ones map_fixed and process_map name. Lends and transfers move pages between processes by changing page-table entries, never by copying.

Purpose

Memory is what every process consumes, and a page is the easiest thing to leak between two processes: a frame freed by one and handed to the next still holds what the first wrote. So the memory calls have four jobs. Hand out pages that hold nothing of anyone else’s. Keep every RAM page W^X, so data a process writes cannot run as code. Keep a page’s owner and payer straight as it moves by lend, transfer or process_map. And keep the cost of each call bounded by what the caller has, because the kernel runs a call to its end with interrupts off.

Interface

The mapping calls

Status: built · tested (6)
  • bench:device
  • bench:write-only-attack
  • bench:process-attack
  • bench:map-fixed-attack
  • bench:return-lent-unmapped
  • bench:dma-rules
CallArguments -> resultWhat it does
map_anonlen, flags -> addrMap len bytes of zeroed pages at an address the kernel chooses, each backed and charged to the caller’s budget at once.
map_fixedaddr, len, flagsThe same, at exactly addr. Never replaces a mapping (below).
unmapaddr, lenRemove the caller’s own pages. A RAM frame goes back to the free pool and its charge to the budget; a device’s registers or a dma_alloc page only lose the mapping.
set_flagsaddr, len, flagsGive each of the caller’s own pages exactly these permissions. It may add a permission as well as drop one.
process_maph(process), src, dst, len, flagsMove the caller’s own RAM pages, contents and all, into a process that has not started, at dst, with flags. The child’s budget pays for them and for the page tables that map them (processes).

A range is page-aligned and non-empty, and for every call but map_anon it lies below USER_AREA_END (the end of user space: 0x8000_0000, 2 GiB, on rv32; 0x40_0000_0000, 256 GiB, on rv64). Flags are READ, WRITE and EXECUTE: at least one, never WRITE with EXECUTE, never WRITE without READ. “The caller’s own page” is a live user mapping that is neither side of a loan and is credited to the caller in the kernel’s frame ownership table (or is a dma_alloc page of its own, or device registers it mapped). Only the RAM among them can be made executable (R11). A reservation not yet touched is not a mapping.

Each call checks the whole range before it changes any page, so an error leaves every mapping as it was and charges nothing. process_map counts the untouched pages of its source among what the call must pay for, and backs them only once nothing can refuse it. The errors are InvalidArgument and OutOfMemory, and for process_map also BadHandle, WrongObject and NotPermitted (the child has started). The order of the checks, the same in the kernel and the model, is in the ABI reference.

Backing and zeroing

Status: built · partly tested: that a frame freed with data in it comes back zero is attacked by `smp-inflight-race`, whose witness reads every page it is handed while the trace shows most frames handed out were given back since, but no case ties a page it read to the frame another process filled: `mem-attack` cannot tell which frames it was handed, and `dma-reset-reuse`, which proves reuse by physical address, never reads the reused frames; a frame free since boot is zeroed at its first allocation, which no case can tell from a frame QEMU left zero; QEMU models no cache, so `cbo-user-fault` shows that user cache-block operations trap, not that zeroes could be lost, and the firmware's flush is read from the code · tested (10)
  • bench:device
  • bench:mem-attack
  • bench:map-fixed-attack
  • bench:lend-untouched-page
  • bench:touch-beyond-ram
  • bench:cbo-user-fault
  • bench:scan-bounds
  • bench:smp-inflight-race
  • mutation:R11NoZeroing
  • mutation:R81CommitUnzeroed

map_anon and map_fixed back every page when they map it. Each takes a free frame, charges it to the caller’s budget (R6 (charging)), and only then writes the entry that maps it. Every free frame is already zero: a frame given up is zeroed before it is free again (below), and a frame free since boot, which may hold whatever the loader or the firmware left there, is zeroed through the physmap the first time it is taken. So a page is zero the first time its process can see it, whoever held the frame before, and backing a page writes nothing to it. The page tables a mapping needs are allocated and charged as it goes, to the budget of the process they map into. A free frame is a set bit in a bitmap the kernel keeps, with a summary bit for every word of it, level above level, to a fixed depth set by the most RAM the kernel can map. Taking the lowest free frame reads one word a level, and giving one back sets its bit and at most one word a level, so neither searches RAM, however much of it is in use (bench:scan-bounds). A checked build proves after each destruction that the bitmap is exactly the free frames and every summary is exact.

The one exception is the stack of a program the loader starts: it is reserved, its entries holding permissions but no frame. A page of it is backed with a zeroed, charged frame on first touch: a load or store fault, or a call that lends, transfers or process_maps it. A process started by process_start has no reservations: its parent gave it every page it has.

Running out is the caller’s error: map_anon of more than the budget or RAM can supply is OutOfMemory, and every page and page table it had taken goes back.

The zeroes cannot be discarded from user mode. Until they are evicted they may live only in a data cache, and a cbo.inval of the page would drop them and expose the frame’s old contents in DRAM. So the kernel writes senvcfg 0 on every hart at entry, whatever the reset left, and every cache-block operation traps in user mode; the boot stops unless it reads the 0 back. The firmware turns a supervisor cbo.inval into a flush, so no mode below M can discard a line. The kernel requires privileged architecture 1.12, where senvcfg first appears: on an older hart the write traps and the boot stops.

A test kernel’s trace ring (sched-trace, never in a release build; R23 (no test channels)) takes its frames at boot, the highest free ones, before the budget tree counts what the kernel keeps, and holds each as its page number in 32 bits, so the 256 MiB ring’s table of 65,536 frames fits the kernel’s 1 MiB RAM region. Every frame the kernel takes lies in the physmap, which ends at 128 GiB on rv64 and below 4 GiB on rv32: page numbers to 2^25, where 32 bits reach 16 TiB of physical address. A compile-time assertion in kernel/src/sched.rs holds the physmap’s last page number within 32 bits.

Frames in flight

Status: built · partly tested: QEMU drops a hart's TLB at its next `satp` write, so no case lands a stale store in a frame being zeroed; the order that keeps one out is the trace's, and a stale store cannot be told apart from the recorded negative's · tested (4)
  • bench:smp-inflight-race
  • bench:smp-shootdown
  • mutation:R81InFlightAllocatable
  • mutation:R81CommitUnzeroed

A frame its owner gives up, by unmap, a process’s end, a page table emptied, an abandoned lend or a kernel object freed, is not free at once. Under the kernel lock it goes in flight: the ownership table names it as IN_FLIGHT’s, a reserved owner no process has, so every call that checks who owns a frame refuses it, and its bit in the bitmap stays clear, so no allocation takes it. Its budget is uncharged then, as before. It is zeroed later, outside the lock by the hart that freed it when that hart idles, or under the lock by an allocation that finds the bitmap empty, and the lock’s next holder, on any hart, gives it back to the bitmap (R81). So zeroing, the one piece of a frame’s work long enough to matter, leaves the calls that free and the calls that allocate whenever a hart has idle time to do it, and a call never pays for frames it did not free or take.

A frame waits for its zeroing on one of two lists the freeing hart keeps:

  1. Staged, while another hart may still hold a translation to it: the call cleared its entry in a process’s space and has yet to shoot that process down. The list holds the frame’s number, never anything in the frame, since a store through a stale translation could still change it. The call’s shootdown (residual risks) moves the process’s staged frames on; a call that frees more than the 64 a hart stages shoots the process down early, once for every 64.
  2. Pending, once no hart can store to it: an ended process’s frames (its harts left its space before its frames were freed), a kernel object’s (never mapped), and the staged ones after their shootdown. The list is linked through one word of each frame, the word a destruction already links the object frames it frees through, so that chain joins the list whole.

Pending frames are zeroed in one of two places, and never in a third:

  • Idle, when every hart is idle. A hart with nothing to run, when every started hart is idle too, takes one frame off its pending list while it still holds the lock, gives the lock up, zeroes it and pushes it onto its done list, the link still in that word. With more left it does not halt, but goes back through kmain’s interrupt-enabled top, where an interrupt that came meanwhile is taken and anything woken runs first, and then takes the next. So an idle hart answers an interrupt within one frame’s zeroing, about 30 µs under icount. One hart drains at a time: each frame costs its drainer a release and a take of the lock, and two drainers would find it held at nearly every take, each take a halt and each release the other’s interrupt. At rest after a login on launch’s four harts that was about 33,000 interrupts in two seconds, where alone a drainer finds the lock free. A hart that idles while another drains halts; the drainer, its list empty, wakes the next hart with frames pending once it gives the lock up, and so does a hart that idles last with none of its own, for a hart that halted with frames while another worked. A drainer woken to work drains no more until every hart is idle again, and gives the drain up at its next idle pass if one is not. While any hart is busy, an idle hart halts instead, as before, and a hart with nothing pending halts as it always did. So the system at rest, once drained, takes the interrupts it took before R81 (the machine at rest).
  • On demand. An allocation that finds the bitmap empty with frames in flight gives back the done frames first, then takes one frame off any hart’s pending list and zeroes it under the lock, as every allocation once did: one frame for each allocation, main’s cost. Only when every frame in flight is one an idle hart is zeroing does it wait, still holding the lock, and then for one frame at most: that hart needs no lock to finish it, and its push wakes the waiter. So a budget can always pay for the frames it can buy, and they always exist, because the frames in flight are RAM no budget is charged for.
  • Never at an exit to user mode. The thread a hart returns to did not free those frames, and the caller of a destruction waits for the walk of R10 (destruction), not for the zeroing of the lease it freed: a lease’s 4,300 frames, zeroed there, put 140 ms into the steward’s deadline notice in the containment gate.

Why only when every hart is idle: under icount the harts share one virtual clock, so a hart that zeroes while another works slows that one’s time as surely as if the work were its own; a refused search in map-anon-search-bound took 406 µs instead of 116 at two harts while the other hart zeroed. On a real machine that zeroing would run beside the work for free; that is forgone for now (residual risks).

A pending list is read and written only under the lock, and the frame an idle hart zeroes only by that hart, so a frame in flight is in exactly one place: staged, pending, being zeroed, done or being given back. The kernel’s checked build counts them, list by list, against the ownership table at each destruction’s audit, so a list lost or linked twice stops the boot. Every acquisition of the lock gives back up to 64 done frames from every hart’s list, clearing each link, so a frame enters the bitmap all zero and the step adds a bounded piece to each kernel section. Pending frames are bounded only by RAM.

Every build, the release one too, keeps a count of the frames in flight and says on the console when a large drain begins and ends: mem: 1024 frames in flight when the count first reaches 1,024 since it was last 0, and mem: frames in flight 0, at most N when the frame that brings it back to 0 is given back, N the most it held meanwhile. Both are ordinary kernel lines, under the console’s hold like the rest (the console’s one writer), and the common give-back pays one comparison with 0. The bench waits on them before it measures a system at rest, so that window never holds the zeroing of the boot’s and the login’s frames (the machine at rest). Why 1,024 frames (4 MiB): on launch’s machine the boot and the first login leave about 35,000 in flight, the first line coming during the boot and the second only once every hart first idles after the login, and the shell’s step after the bench’s window frees about 4,600, while a system at rest frees a page or two every few seconds, which never reaches it, so at rest the console stays quiet; and a drain under 1,024 frames takes under 10 ms to zero, too short to matter to the window. A pair of lines needs 1,024 frames retired and then a drain back to 0, so the console gets at most two lines for every 4 MiB freed and drained. What they tell a reader of the console is that some process freed 4 MiB or more and when the zeroing ended: a timing channel, out of scope (TENETS). The last frames come back at the lock’s next acquisition, at rest the next timer interrupt, so the second line can follow the drainer’s last frame by up to about a second.

The zeroing an idle hart does is the work of whoever freed the frames, so it is billed to them: the budget paying for the kernel time when the frame was retired (the caller, a destroyer, or a deadline’s payer (R10 (destruction))), when the hart takes the lock back, for the frames it zeroed, the newest first as the list gives them; the hart keeps at most four such payers, and what it has not zeroed stays theirs until it does. A frame zeroed on demand is the allocation’s own kernel time, as on every allocation before: it comes off the freeing hart’s payers unbilled, the newest first by count, since a frame does not record its payer, so the split among those payers is by counts, not by frame.

Page tables

Status: built · tested: bench:page-table-reclaim, mutation:R6EmptyTableKept

A page table is made when a mapping first needs it, charged to the budget of the process it maps into, and freed, with its charge, by the call that leaves it mapping nothing: every entry empty, with no page, no reservation and neither side of a loan. So unmap frees the tables its range empties, and so do a failed map_anon’s rollback, process_map in its source, and a transfer in its sender. A lend’s tables in the server go at the reply that returns it; an abandoned lend’s go from the caller when the call is abandoned, and from the server at the reply that frees the lend. A call frees tables once it has finished, never between making a table and filling it. It reads at most ENTRIES entries for each table the range reaches, so the cost follows the pages it unmapped (R22). The root table goes only with its process.

Where map_anon puts pages

Status: built · tested (4)
  • bench:map-anon-search-bound
  • bench:map-anon-placement
  • bench:map-fixed-attack
  • bench:touch-beyond-ram

The kernel chooses the address, and nothing may depend on it. map_anon takes the first free run of pages in its placement area, 256 MiB from DEFAULT_BASE (0x6000_0000 to 0x7000_0000), searching from the start of the run it placed last to the last start that fits, then from the area’s start. Every start up to the last one that fits is tried, so a run that fits only at the area’s end is found, and so is the whole of an empty area; every run placed lies inside the area. A page is free only if its entry is empty: a reservation or either side of a loan is taken. A request that finds no run, or is larger than the area, is OutOfMemory. The search looks at each page of the area at most once (R22). map_device and dma_alloc place their mappings the same way (devices). A receiver’s lends and transfers land in a second area, 4 MiB from DEFAULT_MESSAGE_BASE (0x4000_0000), found the same way. The rest of the user layout is on memory layout.

The model places runs in the same two areas, searched the same way, so the two agree on addresses as well as outcomes.

map_fixed

Status: built · tested (7)
  • bench:map-fixed-attack
  • bench:map-fixed-tables
  • bench:map-fixed-tables-rv32
  • bench:return-lent-unmapped
  • host:redoubt-model::bad_ranges_are_refused
  • host:redoubt-model::partial_overlap_is_refused_whole
  • host:redoubt-model::page_tables_half_of_the_charge_check

map_fixed(addr, len, flags) maps zeroed pages at exactly addr in the caller’s own address space, charged as map_anon’s are. It is the one call that puts new pages at an address the caller names, so that the loader stub can place a program’s segments at their link addresses from inside the process it is loading.

Unlike POSIX MAP_FIXED it never replaces a mapping. A range that touches any occupied entry of the caller’s (a mapping, a reservation, either side of a loan) is InvalidArgument, and nothing is mapped. The checks run in this order, all before anything is allocated:

  1. the range: aligned, non-empty, no overflow, below USER_AREA_END (page 0 is user space);
  2. the flags;
  3. the pages alone against the budget, by arithmetic;
  4. the overlap, over the whole range;
  5. the pages and every page table the range still lacks, counted across table boundaries.

Only then does the mapping loop run, and it cannot fail. So a map_fixed maps everything it was asked or nothing, and a refused one charges nothing.

Instruction fetch after mapping

Status: built · partly tested: no case can see a missing fence.i, because QEMU keeps instruction fetch coherent with stores; smp-fence shows from the trace that the other hart fenced · tested: bench:smp-fence

A hart may fetch stale instructions from a page just written unless it fences. After any call that installs an executable mapping (map_anon, map_fixed, set_flags or process_map with EXECUTE), the kernel runs fence.i, so the hart’s later fetches see every store it made before. It runs one more at boot, before the first process, for the images the loader wrote.

W^X makes one fence per call enough: a page is written while it is writable and not executable, and becomes executable only through one of these calls. On several harts the call also shoots the process down on every other hart running it, and that hart runs fence.i before it acknowledges; a hart also runs fence.i before it runs a process. A thread that moves between harts needs no fence of its own: a RAM frame has at most one user entry, so a process’s code changes only through these calls.

Lending at the page-table level

Status: built · tested (9)
  • bench:process-lifecycle
  • bench:return-lent-unmapped
  • bench:ipc-outcomes
  • bench:map-fixed-attack
  • bench:move-borrowed-page
  • bench:uaf-lent-page
  • bench:lend-untouched-page
  • bench:smp-shootdown
  • mutation:R11LendStaysMapped

A lend or a transfer is page-table edits:

  • When the message is sent, each page is checked first: backed (a reserved page is backed at this point), the sender’s own RAM, and for a lend writable. Then each is taken out of the sender: its entry keeps the frame, loses VALID and gains the lent bit S (a software bit of the entry; memory layout). That entry is the loan’s only record.
  • When a receiver takes it, the frames are mapped read-write in the receiver’s message area. A lend’s entries there carry S too, marking them as the borrower’s side.
  • At the reply the kernel checks that the borrower’s entry and the lender’s entry name the same frame, clears the borrower’s, and makes the lender’s valid again. A message refused or timed out while still queued was never mapped in a receiver: the lender’s entries are simply made valid again.
  • A transfer’s sender entry is cleared when the receiver takes it, and the frame’s owner and payer change together (R4 (delivery)). A lend whose call is abandoned goes the same way to the server (R3 (lends and abandoned calls)).

Only these steps of the kernel’s own (the return, a transfer’s delivery, an abandonment) touch an entry with S. unmap, set_flags, map_fixed and map_anon’s search treat both sides of a loan as occupied, so the lender cannot unmap, remap or re-flag a lent page, and the borrower cannot unmap or re-flag its side. A borrowed page stays credited to its lender, so the borrower cannot lend it on, transfer it or process_map it. The kernel never reads or writes a call’s record in a borrowed page. When caller and server are the same process, both sides of the loan sit in one address space, and the return still checks both markers and the frame before changing either.

A page’s life

Status: built · tested (7)
  • bench:device
  • bench:ipc-outcomes
  • bench:lend-untouched-page
  • bench:uaf-lent-page
  • bench:process-attack
  • bench:dma-rules
  • bench:dma-reset-reuse

A RAM frame is taken from the free-frame bitmap and given back to it, so backing a page, a page table or an object searches nothing, however much of RAM is in use; a dma_alloc run comes from the DMA pool instead, a fixed 1024 pages (devices).

stateDiagram-v2
    state "DMA-held" as DMA
    state "In flight" as Flight
    [*] --> Free: free at boot<br/>(zeroed when first taken)
    Free --> Mapped: map_anon, map_fixed,<br/>first touch of a reservation
    Mapped --> Flight: unmap, a reply to an<br/>abandoned call, or the process ends
    Flight --> Free: zeroed (its hart idle, or an<br/>allocation), then given back
    Mapped --> Mapped: process_map<br/>(moves to the child)
    Mapped --> Lent: call with a lend<br/>(unmapped from the caller)
    Lent --> Mapped: reply, or the call fails<br/>(back to the caller)
    Lent --> Mapped: call abandoned<br/>(the server's own)
    Mapped --> Transferred: send with a transfer<br/>(unmapped from the sender)
    Transferred --> Mapped: taken (the receiver's), or<br/>the send fails (the sender's)
    state "DMA pool" as Pool
    [*] --> Pool: taken at boot
    Pool --> DMA: dma_alloc (zeroed first)
    DMA --> Pool: its process ended and every<br/>device that could hold it was reset

Figure: the states of a RAM frame. A frame is mapped by at most one process at a time, and is zero whenever it leaves Free or the DMA pool: zeroed in flight, on its way back, or at its first allocation if it has been free since boot. A frame in flight is no one’s and not free (R81). A pool frame is never Free, and a Free frame is never DMA-held.

Authority

Status: built · partly tested: that no call names a physical frame is argued from the call table, not attacked · tested (4)
  • bench:process-attack
  • bench:device
  • bench:ipc-outcomes
  • bench:map-fixed-attack
  • A process maps only into its own address space. map_anon, map_fixed, unmap and set_flags act on the caller’s own pages; none names another process.
  • process_map needs a process handle to a child that has not started. A started process is closed to its parent: nothing can be slipped into a process that is already running.
  • Pages come from the budget. Every frame and page table is charged to a budget, so a process can map no more than its budget allows (budgets).
  • No call names a physical frame. There is no call that maps RAM by physical address, so holding memory never gives a way to reach anyone else’s.
  • The memory calls create no authority: they change pages the caller already has, or move them to a child it already holds.

Security properties

R11 (memory)

Status: built · partly tested: that a frame freed with data in it comes back zero is attacked by `smp-inflight-race`'s witness, which no case ties to the frame another process filled ([above](#backing-and-zeroing)); the absence of any physical-address argument is argued from the call table, not attacked; that the zeroes stay is shown only as user cache-block operations trapping, since QEMU models no cache · tested (19)
  • bench:wx
  • bench:write-only-attack
  • bench:map-fixed-attack
  • bench:device
  • bench:mem-attack
  • bench:process-attack
  • bench:return-lent-unmapped
  • bench:dma-rules
  • bench:dma-reset-reuse
  • bench:device-exec-refused
  • bench:cbo-user-fault
  • bench:smp-inflight-race
  • mutation:R11NoZeroing
  • mutation:R11SetFlagsAllowsWx
  • mutation:R11SetFlagsAllowsWriteOnly
  • mutation:R11LendStaysMapped
  • mutation:R11MapFixedSkipsOverlap
  • mutation:R11ExecOnDeviceMemory
  • mutation:R11ProcessMapSkipsFlags
  • No RAM page is ever mapped writable and executable (W^X): not by one entry, and not by two, since a RAM frame has at most one user entry at a time (the kernel’s physmap aside). W+X is refused when any call is decoded (WRITE with EXECUTE, or an unknown bit, is InvalidArgument), again by map_fixed and process_map before they charge, and again by the page-table layer, which refuses to build such an entry, so no check rests on another. set_flags may add EXECUTE only to a page it makes not writable in the same call.
  • W^X holds per frame, not only per mapping. Only RAM that a process owns is ever executable. Device registers and DMA frames are never mapped executable: the device, or another mapping of the same registers (in this process or a co-holder’s, since a mapping outlives its handle), can write them underneath. map_device and dma_alloc map read-write and never executable, set_flags refuses EXECUTE on either, and process_map refuses device and DMA pages.
  • Writable implies readable. The privileged architecture reserves the write-only entry, so map_anon, map_fixed, set_flags and process_map refuse WRITE without READ.
  • Flags are checked before anything is charged or moved for the new mapping, so a step that cannot fail never meets bad flags. process_map checks them before it backs any page of its source.
  • Every page is zero before a process first sees it: anonymous and fixed pages, backed reservations, page tables, and dma_alloc pages. Every free frame is zero, by R81, and a frame free since boot is zeroed when first taken, so backing a page writes nothing to it; dma_alloc pages are zeroed as they leave the pool. Pages moved by lend, transfer or process_map carry their contents, because moving them is the point.
  • The zeroes stay. senvcfg is 0 on every hart and the firmware turns supervisor cbo.inval into a flush, so no process can discard the zeroes the kernel wrote to its page and read what the frame held before (above).
  • No physical addresses. No call takes one, and none maps RAM by one: map_device maps a device object’s registers, and the boot refuses any device object that overlaps RAM. The one physical address a process learns is that of its own dma_alloc pages, which its device needs (devices).
  • DMA pages are held until reset. A dma_alloc page stays with the process that allocated it until that process ends: unmap drops only its mapping, and it is never lent, transferred or process_mapped. It returns to the pool only after every DMA device that could hold its address has confirmed a reset, and a quarantined device never counts as reset (devices, I16 (DMA pages reset before reuse)).
  • A lent page is unmapped from its lender until the call ends (above).
  • map_fixed never replaces a mapping, so it can neither discard a page nor alias one.

Together these are I9 (pages W^X, zeroed, lends unmapped) of the invariants.

R81 (frames in flight)

Status: built · partly tested: QEMU drops a hart's TLB at its next `satp` write, so the order that keeps a stale store out of a zeroed frame is checked from the trace, not seen as a store landing; an allocation that finds the bitmap empty while frames are in flight (it gives back the done ones, zeroes a pending one or waits for the hart zeroing its list) runs in no case, since no case fills RAM while it frees · tested (3)
  • bench:smp-inflight-race
  • mutation:R81InFlightAllocatable
  • mutation:R81CommitUnzeroed

A freed RAM frame is in flight until it is zero: it belongs to no process and is not free.

  • No one can name it. Its owner in the ownership table is IN_FLIGHT, which no process is, so every call that frees, lends, transfers or process_maps a frame refuses it, as it refuses a frame of another process’s; and no call names a physical frame (authority).
  • No allocation takes it. Its bit in the free-frame bitmap is clear until it is given back, and every frame a mapping, a page table or an object gets comes from the bitmap.
  • One hart writes it at a time, and only once no other can. Its number is staged until the shootdown of the process whose entry for it was cleared has been acknowledged by every hart asked; only then is it linked through a word of its own, and later zeroed, by the hart that freed it while that hart idles, or under the lock by an allocation that took it off that hart’s list. Pending lists change only under the lock, and an idle hart zeroes only the frame it took off its own, so no two harts hold one frame. A frame of an ended process, whose harts left its space first, or of a kernel object, never mapped, is linked at once.
  • It is given back only zero, and only under the lock, by the lock’s next holder, which clears the link it held.

So every free frame is zero and allocation writes nothing. The kernel’s checked build samples every frame it takes from the bitmap and counts the frames in flight against the ownership table in its destruction audit (I1 (handles name live objects)); smp-inflight-race’s kernel checks each frame it gives back word by word, and its trace shows the order above for every frame (the frames in flight). In the model, a free puts the frame in flight with what it held, and time passing zeroes and frees it; a frame is held, in flight or free, never two, and a free frame is zero (the model).

R19 (kernel W^X)

Status: built · partly tested: no case plants a writable kernel code page to show that the check stops the boot · tested: bench:kernel-wx

The kernel’s own mappings are W^X. At boot, before any process runs, the kernel walks its own area of the address space and, for every executable page there, checks three things: the page is not writable, its frame’s alias in the physmap is not writable, and that alias is not executable. The check reads only the aliases of executable kernel frames; it does not walk the rest of the physmap, whose entries the loader builds never executable. If one fails, the kernel panics instead of running. It then prints W^X verified: N executable kernel pages, none writable under any alias, the line the case checks. Every mapping the kernel makes later goes through the same entry constructor that refuses W+X; its one later window, for DMA device registers, is read-write and never executable.

R22 (range cost)

Status: built · tested: bench:map-fixed-attack, bench:map-anon-search-bound, host:redoubt-model::huge_len_is_refused_promptly

A call that takes a range costs what the page tables hold and what the budget can pay for, never what the length asks. A process could otherwise ask for a huge range for free, and the kernel, running the call to its end with interrupts off, would stall every other process.

  • unmap, set_flags and process_map check the range page by page and stop at the first page that is not the caller’s, so their cost follows what is mapped there.
  • map_fixed first refuses a range the budget cannot pay for by arithmetic alone, before any walk. It then checks overlap by walking the page-table tree and skipping every absent subtree whole: at most the root entries the range spans, plus ENTRIES (512 on Sv39, 1024 on Sv32) for each table present in it, and only then counts page tables. A map_fixed of the whole of user space, which no budget in the case can pay for, is refused well inside the case’s 10 ms bound, over mappings or not.
  • A lend or transfer checks at most the pages mapped in its range, and a lend is at most MAX_LEND_PAGES (16).
  • map_anon’s search, which also places map_device, dma_alloc and a received message, never tests a start twice: when a page is taken, the next start tried is the page after it, and a missing page table skips its whole span. So it looks at each page of its fixed area at most once, 65536 for map_anon’s and 1024 for the message area, whatever the request asks. With every page table of the area present, the worst case, a refusal takes about 9.6 ms in a checked build under virtual time; the case bounds it at 12 ms, and a timer wake during it at 15 ms.

Failure and restart

Status: built · tested (8)
  • bench:touch-beyond-ram
  • bench:lend-untouched-page
  • bench:wx
  • bench:uaf-lent-page
  • bench:map-fixed-attack
  • bench:process-map-untouched-attack
  • bench:return-lent-unmapped
  • bench:fault-report-bound
  • Out of memory is the caller’s error. A mapping call that cannot be paid for returns OutOfMemory; a process that exhausts RAM gets OutOfMemory and every other process keeps running. A refused map_fixed charges nothing, a refused process_map charges neither the child nor the caller, and a refused map_anon gives back every page and page table it took.
  • A permission fault ends the process. A store to a page that is not writable, or a fetch from one that is not executable, is never mistaken for a page to back. The process faults, and its exit notice carries the RISC-V cause (12 for an instruction page fault, 15 for a store page fault; processes). The console gets one line, PROGRAM HALT: CPU Exception on PID n: <cause> of <address> at <pc>, printed holding the kernel lock; the thread’s registers and the address space’s map, a line a mapped page, are printed only for a fault in the kernel and in a debug-print build. Printed for every fault, they held the lock for as long as the process was large: 837 ms on rv64 for a process of 4096 pages, against 7.5 ms for its teardown now (bench:fault-report-bound, under icount).
  • A process ends: every frame it owns returns to the pool and its charge to its budget. A page it had lent is its server’s until the server replies (R3), and is never reused while the server has it mapped. Its dma_alloc pages wait for the device reset (R11).
  • No argument to any memory call makes the kernel panic (I14 (no call panics the kernel)). Lending untouched or half-mapped ranges, unmapping a lent page, and exhausting RAM are each attacked by a case that passes only on a clean power-off.

Residual risks

  • map_fixed can fill map_anon’s area. A process that maps the whole area with map_fixed makes its own later map_anon calls fail with OutOfMemory. It harms only that process. The same for the runtime’s thread-stack area (memory layout): a map_fixed of the program’s own there takes a slot, or a guard page, from its own later spawn, which is then refused.
  • Several harts. fence.i and the TLB flush act on the hart that runs the call. A process’s translations carry its ASID, and a hart that ran it may keep them; it flushes that ASID before it next runs the process if any of its mappings were removed meanwhile or its PID was given out again. Every call that clears or narrows one of a process’s entries, frees one of its tables or makes one executable first shoots the process down on each other hart running it now, which flushes its ASID, runs fence.i and acknowledges before the call returns; a destruction’s shootdown also makes the hart leave the process’s space before any of its frames is freed. The asking hart waits for the acknowledgements halted, and each hart sends it an interrupt as it acknowledges, as a hart waits for the kernel lock (R78 (fair kernel entry)): spinning, under QEMU’s icount it spent the turns the other hart needed to acknowledge, and the p99 of a destruction’s kernel time (R10 (destruction)) in sched-latency at two harts was 51.9 ms on rv64 against 3.0 ms halted. The asking hart holds the kernel lock while it waits: measured under icount the waits total 0.9 ms over the whole containment gate at two harts, so they stay under it, where the asker is the lock’s one holder. So no stale translation reaches a page unmapped, lent or returned, or a frame’s next owner. A missed shootdown cannot be seen on QEMU, which empties a hart’s TLB at every satp write: the checked build stops when a process loses an entry while another hart runs it and is not shot down there (bench:smp-shootdown, the case’s recorded negative), and smp-fence checks from the trace that the fence was taken.
  • The physmap maps every user frame writable for the kernel, code included. Only the kernel can use that alias (memory layout).
  • A freed frame may still be mapped on another hart. A free writes nothing into the frame until the shootdown that clears its last translation is acknowledged: the frame waits staged by number, and is linked through a word of its own, then zeroed, only after (R81). So a stale mapping could reach only a frame no one has written since, never the kernel’s link nor its next owner’s data. Every path that frees a mapped frame unmaps it and flushes the TLB first, or frees an ended process’s frames or a refused process_create’s, whose cached translations carry that process’s ASID, which nothing runs under again until the PID is given out, and that flushes it first (satp); on one hart that leaves no stale mapping. On several, the call shoots the process down on any other hart running it before the frame can be given out again, and a destruction before the free (above, bench:smp-evict, bench:smp-shootdown).
  • Freed frames are not zeroed beside the work. An idle hart zeroes frames in flight only when every hart is idle (frames in flight), because the bench runs harts under icount, whose one virtual clock bills a working hart for another’s zeroing. On a real machine an idle hart could zero while others work, at no cost to them; while any hart is busy, frames are zeroed on demand instead, one per allocation under the lock, as before R81. To revisit when the bench can judge an idle hart’s work without that shared clock, as sched-lock-contention-4-mttcg judges the four-hart tail without icount. So R81 saves nothing on a busy machine: in the containment gate, at two harts, no hart is idle while another works and 576 MiB never runs short, so allocations zero never-used frames at their first allocation, as before, and frames in flight reach about 79,500 (about 310 MiB), nearly all held to the end of the run, the longest given back 113 s after it was freed. A process that keeps one hart busy keeps every allocation at that cost, never worse than before R81. Meanwhile a freed frame’s old contents stay in RAM, though no call names the frame and no process maps it.

Why

  • Back at map time, not on first touch. A process told it has memory, which then faults for want of it, has been told a lie. map_anon charges and backs every page before it returns, so a process’s memory is its own the moment it has the address. Only the loader-started stacks are reserved, because their programs have no parent to map them.
  • Zero on reclaim, when the harts are idle. A freed frame is zeroed outside the kernel lock by the hart that freed it when every hart idles, or under the lock by an allocation that needs it, and the bitmap holds only zero frames, so no path that hands a frame to a process can forget to zero it. An allocation writes nothing when idle time has zeroed ahead of it; under load, with no idle time, it zeroes its own frame under the lock as before R81 (a frame never used since boot, or one in flight), so it is never worse than before. No hart zeroes on its way back to user mode: that taxes whatever runs next for frames someone else freed, and a lease’s 4,300 frames, zeroed there, put 140 ms into the steward’s deadline notice in the containment gate. Measured at two harts under icount before R81, zeroing was the one piece of a frame’s work long enough to matter: 220 µs a page while it checked every word, about a fifth of that after, and 15 s of the containment gate went to zeroing in 68,218 endpoint creations. The other way, zeroing at allocation outside the lock, splits every mapping call in two around a second wait for the lock, and the second must find its process alive and its range still free; zeroing on reclaim needs neither, since a freed frame is already no one’s. Frames free since boot are zeroed at their first allocation, under the lock, rather than all at boot, which would cost seconds of boot under icount for the RAM the cases give.
  • The kernel chooses addresses, so no program depends on a layout and no call lands on another mapping. map_fixed exists because a program’s segments must sit at their link addresses and the loader stub, running inside the new process, is the only code that parses its ELF. The other ways were worse: mapping the segments from the parent would make the launcher parse ELF images, and relocatable programs would differ from every other binary’s fixed-address link. map_fixed never replaces, so it cannot discard or alias a page.
  • The lender’s entry is the loan’s record. There is no side table to fall out of step. The S bit makes the entry one that only the kernel’s own lend steps may overwrite, and the return checks both sides against each other first.
  • Flags checked more than once, and before charging. Decoding and the page-table layer each refuse W+X, and map_fixed and process_map check again, so a slip in one leaves the others. Checking before anything is charged means the steps after it cannot fail, so a bad combination is a clean InvalidArgument, never a half-done call or a kernel panic.
  • Cost follows occupancy. The kernel does not preempt itself, so every loop in a call must be bounded by something the caller paid for: pages it has mapped, or pages its budget can buy.
  • One fence per executable mapping. A frame reused from another process may still sit in a hart’s instruction cache. That is a correctness hazard, not a privilege one, since the code runs in the new owner’s context, and the fence each executable mapping gets on this hart clears it.