User mode and PMP
sysp proves tasks keep to their own memory. The hardware enforces it as well: tasks run in RISC-V user mode, where Physical Memory Protection lets each one touch only its own stack, its own heap, the shared code and constants, and its device if it holds one. Calls into the kernel are traps.
Two privilege modes
RISC-V has machine mode (everything allowed), supervisor mode (for kernels that use the MMU) and user mode. sysk uses no MMU and only two modes: the kernel's scheduler and channels, and the boot and trap assembly, run in machine mode; tasks run in user mode, together with the library code they run on their own memory (the heap allocator, closing a receiving end) and a few assembly helpers (the gate stubs, the heap's block views, and since sysk 023 the loads and stores load8, load32, store8 and store32 a driver reaches its device's registers with). Machine mode can reach everything; user mode can reach only the address ranges PMP gives it, and cannot touch control registers at all. Breaking either rule traps into machine mode, and sysk stops: sysk: task fault, status 3.
Why both proofs and hardware? The proofs hold if the compiler, the assembly and every task are right. PMP catches what they assume away in code that runs in a task, such as a compiler bug in a task's code or a store in assembly that sysp never sees. It does not guard the kernel: the entries are not locked, so machine mode is not bound by them. Nor does it bind a device that reads and writes memory itself, the disk (sysk 023): PMP checks the CPU's accesses, so what the disk may touch is proven instead (Storage). The tests include a task that writes to kernel memory through assembly, and one that writes to the UART without holding it. Both must fault.
What each task may touch
PMP has numbered entries, each covering an address range with read, write and execute permissions. On an access from user mode, the lowest-numbered entry that matches decides; if none matches, the access faults. sysk sets the addresses of entries 0 to 2 once at boot; at every switch it loads the addresses of 3 to 7 and the permissions of all eight (pmpcfg0) from pmp_regions. Pick a task, then try an access.
| Entry | Mode | Range | Allows | What it is | Set by |
|---|
Entries 0, 3 and 5 are off: in TOR mode ("top of range") an entry covers from the previous entry's address up to its own, so each pair of addresses makes one range. Entry 7 is NAPOT, one naturally aligned power-of-two range, which is why a device's page must be aligned to its size; since sysk 023 every page is 4096 bytes, the size the driver's register accesses are proven against (IO and drivers). Addresses come from the last make docs; a heap's words come from the boot arena at boot, so their address is known only then.
The trap path
Every way from user mode into the kernel goes through trap_entry in arch/rv64/trap.S. Pick a cause and step through it.
mscratch does double duty: while a task runs it holds that task's kernel stack, and while the kernel runs it holds 0. The first instruction swaps it with sp; if the result is 0 the trap came from machine mode, which is a kernel bug, and sysk stops with sysk: trap.
Gates
In a task, a call to send cannot just jump to the kernel's send: that code runs in machine mode. When sysp compiles user code it turns each call to a gate into a call to a stub, and tools/gates.rkt writes the stubs from the interface: li a7, n; ecall; ret, plus the table trap.S dispatches through. The gates are the interface's calls, the devices' one (device-ack), and the calls only the generated wiring makes (its wiring clause: task-main's finish, and the job slots' runners' job-await, job-bound and job-done, sysk 017), which no task may name. The arguments stay in registers, so one dispatcher serves every gate, and the real functions are the ordinary sysp ones, contracts and all. The proofs do not change.
| a7 | Gate | Stub | Runs in machine mode |
|---|
The interface: what a task may name
kernel/interface.sysk lists every name a task may use that it does not define itself. tools/interface.rkt reads each file in svc/, prg/, drivers/ and lib/ and rejects any that names something else, even a public kernel function. The kernel is built only if every file passes.
The list starts with its version, now 0.1.0. Below 1.0.0, the MINOR number moves when a task written against the last version may no longer verify: a name removed or renamed, a requires made stronger, an ensures made weaker. Anything else, such as a new call, moves PATCH. tools/interface.rkt rejects a list without one.
Since sysk 028 it lists the files protocol too: the call sys-serve, the library that builds requests and reads replies (fs-request, fs-status, …), and the protocol's constants, from the message's sizes to each header field's offset (Files). sysk 029 added what a server needs as well (0.6.0): fs-begin, which checks a request's header, fs-error, path-ok, the statuses a disk can give (no-space, io-error, busy, already-exists, not-empty) and the open modes for writing, so the disk's server is ordinary user code (Files on the disk). sysk 031 added a service's names (0.6.1): the type Service, its predicates, the calls service-open and service-close, the library's service-reply and service-end, and the protocol's op-lend (Files for jobs). sysk 032 added jobs-output (0.6.2), which says a receiving end is its right's jobs' output, so a launcher can hand that end to a loop of its own, as the shell does with a job in the background (The shell). sysk 033 added a read that waits (0.6.3): mode-wait, and the request's at-since and at-wait (Reads that wait).
sysk 036 made a task's record in a job's table longer, for its arguments (0.7.0, MINOR: a launcher written against 0.6 builds a table the check now refuses); the table's layout is in the list as constants (task-bytes, job-bytes, …), and the slots' runners read arguments through one more wiring gate, job-arg. sysk 046 added a node's kind, type-stream (0.7.1), for a file that never ends, such as /dev/rng (Devices as files). sysk 052 added virtio-reset to the device page (0.7.2), for a buffer a device may never give back, such as one lent to receive a frame (The network).
It also checks that every name in the interface exists in the kernel, so the list cannot go stale, and that no user code has an atomic block: the kernel never holds the timer off a task.
Still trusted
This is step one of two. The kernel still trusts what a task passes to a gate, a handle, a buffer, the kernel pointer k, because sysp proved every task passes good ones. A task not written in sysp would need a kernel that checks every argument. That is a later feature; until then the list of what is assumed is in The trusted base.