Reference · L1

The trusted base

Everything sysp does not check, in one place. It is kept small on purpose, and every list on this page is generated from the code or from docs/trusted.md, so it cannot fall behind.

Assembly: lines

Code that has to touch registers, control and status registers, or memory as raw addresses. A test fails if the total reaches lines, or if docs/trusted.md states a stale count.

Generated, and also trusted: build/gates.S, one three-instruction stub per gate and the table trap.S dispatches through (User mode and PMP).

Extern contracts:

Where sysp calls into assembly, the function is declared extern with a contract that sysp assumes instead of proving. Each one below is what every proof that calls it rests on. All are private to their file, so only the kernel can call them. A driver reaches its device through verified wrappers instead: mmio-read8 and its kin prove each access inside the driver's page, and the virtqueue functions hand a device only the address of memory it was lent (IO, Storage).

Assumptions sysp cannot see

Facts about the machine, the layout and the boot that the proofs rely on, from docs/trusted.md:

What the deadlock check assumes

The deadlock check reads the tasks from their code, but what a channel step means is written by hand as a description of kernel/sched.sysp. The rule rests on it in four ways: a task waiting for a message and one waiting for room on the same channel cannot both be blocked; several senders share only a channel with a count, so none waits for room forever; a task that is not blocked keeps moving and its loops end when their channels do; and every task keeps its counts and closes its handles, which sysp proves. The exact check adds when each step waits and that steps on channels nobody else uses commute. docs/trusted.md states it in full.

Outside the image

The relay make run uses (tools/attach.rkt) and postterm's pt-attach stand between the person and the serial line. No proof relies on them: the terminal task accepts any bytes, so a raw terminal or a pipe works as well. They are trusted only for the experience, that a line is edited at the person's end and Ctrl-D becomes 0x04. See Input.

Borrowed for now

sysk owns its kernel and its language, not yet its whole stack. The C compiler (clang) and linker (lld) turn sysp's output into machine code, and QEMU stands in for hardware. sysp itself runs on Racket and asks the Z3 solver for its proofs. All of these are trusted too; docs/borrowed.md lists them and what replacing each would take.