Checks and evidence

What make ci runs and what each check shows, the ground rules every crate keeps, how to read an image's seL4 record and bill of materials, and how the gate stays fast.

NoWayOS makes few claims, and backs each one with a check you can run. This page explains what each check shows, and what it does not.

One command for all of it

make ci

make ci runs everything CI runs, in order: the secrets scan, lints, tests, documentation, the demo, the no_std build, licence and advisory checks, the glyph atlases, the bills of materials, fuzzing and the Kani proofs, then the system checks and QEMU boots. A change passes only if every step does.

What each check shows

Command	What it shows
`make test`	Unit, property, doc and golden-image tests: the code does what its tests say, and every screen draws exactly as approved
`make lint`	rustfmt and clippy, with warnings as errors
`make nostd`	Every device crate builds for bare metal (`aarch64-unknown-none`), with no standard library
`make deny`	The baseline every workspace must keep, then cargo-deny: licences, sources, banned crates and known advisories
`make secrets`	The tree and every commit, scanned offline for keys and credentials
`make fuzz`	Every fuzz target, built with libFuzzer and run against generated input, for `FUZZ_SECONDS` (10 s) each
`make kani`	Kani's bounded proofs: that each record decoder never panics, overflows or reads out of bounds for any input up to the longest record, with mutation checks that show each proof can fail
`make unsafe-audit`	`unsafe` code appears only where the approved list allows it
`make pds-miri`	Miri runs the tests of the crates allowed `unsafe`, checking for undefined behaviour
`make sbom`	A CycloneDX bill of materials for every workspace
`make image-sbom SYSTEM=NAME`	An image and its bill of materials: kernel, loader, monitor and every protection domain, with the crates in each and their hashes
`make sel4-config-check`	The seL4 verification position on record is the one for the pinned Microkit SDK
`make qemu-test-all`	Every system boots in QEMU, in each configuration it lists, and prints what its expect file says

Bounded proofs are proofs up to a stated size of input, not for every input there could ever be. Fuzzing finds crashes; it cannot show there are none. Tests show the cases they test. Each is worth having for what it does show.

The ground rules every crate keeps

These are lints and checks in every workspace, not guidelines:

No unsafe, except in a short, approved list of crates and files that reach hardware or memory directly. Adding to the list needs a stated reason and review.
No panics on outside input: no unwrap, expect or panic! in library code, no unchecked indexing or arithmetic, and every exception to a lint gives its reason.
Device crates are no_std and allocate nothing. Release builds keep overflow checks, and a panic stops the part rather than carrying on.
Parsers refuse oversized input before copying it, return typed errors, and have property tests and a fuzz target.
No secrets anywhere, not even development keys. Test keys are made when a test runs, and never stored.

Reading an image's records

Every image is written to build/BOARD/SYSTEM/ with two records beside it.

sel4-config.txt names the image, its hash, the board, the Microkit SDK and the kernel, then says where the image stands against seL4's proofs, one status: line per reason, and lists each kernel option that decides it beside the verified configuration's value. A debug kernel is a development build. A multi-core or mixed-criticality kernel, or a board not on seL4's list, is outside seL4's proofs. A kernel that matches every option is still never called "verified": the record gives the facts and leaves it there.

sbom.cdx.json is the image's CycloneDX software bill of materials: what it is made of, down to each crate in each protection domain, each with its sha256.

Keeping the gate fast

The full set of proofs and fuzzing takes a long time, so the everyday make ci runs Kani, fuzzing and Miri only where a change reaches. It follows the change through every crate that depends on it, and skips any check whose inputs have not changed since it last passed. make ci CI_SCOPE=full runs every one of them, with nothing cached; make kani, make fuzz and make pds-miri always run in full.

Kani is the hungriest step: each proof job is given about 10 GB of memory, and KANI_JOBS sets how many run at once. If make kani runs out of memory, give Podman's virtual machine more, or set KANI_JOBS=1.