Architecture
The authority lives on the other side of the wire
The agent computes wherever it likes, at whatever speed it likes, on hardware we assume is compromised. What it cannot do is reach the actuator lines, because they terminate at a different device.
The effect path
Every effect in the system follows one path, and there are no side doors — not because they are blocked, but because the instruction set does not contain them.
- The agent, running off-board and untrusted, sends a program over a serial link.
- The program executes on the gate under a fuel bound. It terminates by construction; there is no analysis to defeat, only a counter that reaches zero.
- It may invoke exactly three capabilities: read state, propose a setpoint, request a signature. There is no file, no socket, no allocator, no fourth verb.
- Each proposed effect is checked against an envelope validated offline — multi-point limits, predicted stopping position, rate ceilings, deadman.
- Effects that pass are constructed by the trusted side and emitted. Effects that fail degrade to a safe stop. Both outcomes are signed into the audit record.
The emergency-stop chain is wired physically around the gate, in series with the contactor coils. The gate can only ever permit motion. No firmware state, and no failure of ours, can command it.
Two timescales, because the physics demands it
Fast control loops are not ours to sit inside. Current loops run at 8–20 kHz and velocity loops around 5 kHz — inside the servo drive, where they belong. What crosses the network is setpoints, typically at 500 Hz or as PWM.
So enforcement splits. The slow path validates the envelope offline, once, the way every certified safety configuration in industry is validated. The fast path is a constant-time comparison against that envelope on every cycle — table lookups, no allocation, no search.
| Path | Rate | Work | Budget |
|---|---|---|---|
| Offline validation | per configuration | envelope derivation, risk assessment, signed acceptance | hours |
| Admission | per program | capability grant check, dry run under fuel | seconds |
| Enforcement | every cycle | multi-point limits, stop prediction, rate, deadman | < 100 µs |
The latency figure is not chosen for marketing. ISO 13855 converts reaction time directly into required guard distance at 1600 mm/s of human approach — 1.6 mm per millisecond. A sub-100 µs budget costs about 0.16 mm of separation. The gate does not take workspace away from you.
The trusted side constructs the effect
This is the design decision that came directly out of adversarial review, and it replaced an earlier design that inspected agent-supplied bytes.
A gate that validates a byte string is validating a field it believes is the amount, the joint index, the destination. Encodings are adversarial: the same bytes mean different things under different parsers, and the attacker chooses the encoding.
The agent supplies an index into a pre-approved intent set and quantised parameters. The gate serialises the transaction or the setpoint itself.
Effects are named, not described
Quantisation is deliberate too. Snapping parameters to a coarse grid and emitting on a fixed schedule reduces the bandwidth of any channel an agent might modulate — from arbitrary to countable. We would rather publish a residual figure than imply zero.
What is trusted, and what is merely present
A trusted computing base is only meaningful if you enumerate it. Ours is roughly 550 lines, and the parts outside it are listed with equal precision.
| Component | Status | Basis |
|---|---|---|
| Interpreter core | machine-checked | Coq-verified eBPF VM, published, deployed in RIOT OS on RISC-V1 |
| Fuel accounting | machine-checked | part of the verified VM; a counter, not an analysis |
| Memory isolation | machine-checked | proven: all accesses land in designated regions |
| Capability table | engineered | static; callee behaviour is not proven — stated openly |
| Envelope monitors | engineered | native code outside the VM; model-checked arithmetic |
| Audit chain | engineered | Ed25519 over program hash, verdicts, monotonic counter |
| Boot & signature check | engineered | immutable first stage, anti-rollback counter |
| Soft processor | assumed | in-order RV32, no speculation, no cache by default |
| Synthesis toolchain | assumed | open toolchain, reproducible builds intended |
| Physical access | out of scope | no tamper response in the pilot — see below |
The pilot excludes physical attackers, power and electromagnetic side channels, and the gap between a formal hardware model and delivered silicon. Those exclusions are disqualifying for payment-HSM and cross-domain defence use, where tamper response is a baseline requirement — so we are not selling into those markets.
They are defensible for a fenced robot cell, where physical access is already controlled. That is the market we are addressing first.
Deliberately small, deliberately dull hardware
An in-order RISC-V soft core on an FPGA, running from on-chip memory. No operating system. No DMA engine. No network stack. No cache by default, so timing is predictable and the speculative-execution attack classes do not exist to begin with.
The I/O surface is the complete effect vocabulary: a serial link in, PWM or step/direction out, a relay drive that sits in series with the existing safety chain, and an SPI secure element holding keys. Everything the device can do is visible on the pin map — which is the property that makes an independent audit tractable rather than aspirational.
Signing runs off the control path entirely. Verified portable code on this class of core signs in tens of milliseconds; the control loop never waits on it.2
References
- Yuan et al., End-to-end mechanized proof of an eBPF virtual machine for microcontrollers (CertrBPF), CAV 2022. The extracted C is published; proofs cover absence of undefined behaviour and containment of memory accesses within designated regions. Licensed GPL-2.0-or-later.
- Measured figures for portable verified Ed25519 implementations on 32-bit RISC-V are approximately 1.2 million cycles per signature, placing signing in the tens of milliseconds at typical soft-core clocks. Implementation choice materially affects this; some widely used portable libraries are an order of magnitude slower on 32-bit targets.