One protocol rule, compiled into five targets for hardware, kernel, firmware and logs
The same protocol rule can end up written out by hand several times: once for chip verification, once for firmware, once for network software, and the copies can drift apart. The lab writes the rule once, as a state machine, and compiles it into five targets. The claim says each target's mutants, broken copies of the rule, are caught in that target's own output; for four targets that is where they run, and the kernel object has not yet been loaded into a kernel.
What it shows
A protocol rule says which events may follow which. A state machine writes such a rule as a set of states and the events allowed in each; the kernel documentation linked below calls this kind of object an automaton. The evidence file's result line gives the size of the lab's machine in events and bits of state, and it is small.
The lab compiles that one machine into five outputs, and the lab's claim names all five: assertions for chip designs in SystemVerilog, an eBPF object (the format the Linux kernel uses for small, checked programs that run inside it), firmware in C, a trace checker in Python, and a test suite for continuous integration.
Testing each output with mutants
The claim says each target's mutants are caught in its own target. A mutant is a copy with one small change that makes it wrong, and a checker that catches its mutants has shown that it can fail. The claim also reports no false alarm on a set of traces that follow the rule, and gives its size.
Why it matters, and to whom
This could help teams that must check the same protocol behaviour in several places: chip verification, device firmware and network software. When each team writes its own copy of a rule, a fix in one copy does not reach the others, and a mistake in one copy is not caught by the rest. Generating every checker from one checked source is meant to remove that drift. Testing each generated checker with mutants shows that it can fail, which a checker that is never seen to fail cannot show.
The value is in the method: one source for a protocol rule, and evidence that each copy made from it can fail.
How it was checked
The evidence file names Verilator, an open-source hardware simulator, as a tool that the re-run needs. It records the check's result line from a clean run, including the number of targets and the size of the trace set, and a note that a failure in any of the five targets fails the whole check.
The lab also tested the check by changing the code number of one event in the C source on purpose. The evidence file records that the check then failed, so it is not blind to a broken firmware target.
What it does not claim
The most important limit, in the lab's words in our claim file, is this. The kernel object has never been loaded into a running kernel, because the computer it was built on, running macOS, has no system call for loading one. So the kernel's own verifier, which the limit names, has never seen it, and the evidence file's scope note adds that the object was parsed by hand. Until it is loaded, one of the five targets is shown only as a compiled file, not as a working kernel monitor.
- It does not claim that the approach is new. Generating runtime monitors from a specification is published and in use. NASA's Ogma generates runtime monitoring applications, for example for NASA's Core Flight System. The Linux kernel's runtime verification tools turn an automaton model into the skeleton of an in-kernel monitor. Baumeister and colleagues monitor real-time properties in hardware on field-programmable gate arrays (FPGA). What this result adds is this particular set of five targets from one source, and the discipline of testing each target with its own mutants.
- It does not claim that the rule is large. The machine is small, as its size in the evidence file shows. Nothing here shows that the generator scales to a full protocol.
How to reproduce it
The evidence file names the command that re-runs the check. It needs the lab's code at the commit named in the evidence file, Python, and Verilator.
The most useful next test is the one the limits point to. On a Linux machine, load the kernel object, attach it to live traffic, replay the same traces, and compare its verdicts with those of the Python trace checker. If they agree, the fifth target is shown working as deployed. If they differ, the kernel target needs a fix before anyone relies on it.
Prior art
- NASA, Ogma: generates runtime monitoring applications, for example for NASA's Core Flight System
- The Linux kernel documentation, "Deterministic Automata Monitor Synthesis": turns an automaton model into the skeleton of an in-kernel monitor
- Baumeister, Finkbeiner, Schwenger and Torfah, "FPGA Stream-Monitoring of Real-time Properties": monitoring of real-time properties in hardware, on field-programmable gate arrays
Evidence
- The evidence file for this result
- Our claim file, with its limits
- All our published files, each with a fingerprint you can check
Related results across the group
- Ultra Ethernet ordered delivery: one recovery design checked in a model against the standard's rule
- The chip netlist whose area and delay are published matches its design: a formal equivalence proof
- Thousands of candidate code patches scored by proof: each one certified sound, proven unsound, or left undecided