Requirement traceability
Generated by ./tools/check-trace.py --write; mise run trace:check fails when
this file is stale, a requirement is in no file under verify/spec/traced/, or a
traced requirement is missing a layer. Requirements are defined in
verify/spec/core.symspec.json and verify/spec/agentd.symspec.json.
| Requirement | model | gherkin | fuzz | test | impl | live |
|---|---|---|---|---|---|---|
| AGENTD-1 | 1 | waived | waived | 2 | 1 | waived |
| AGENTD-2 | 1 | waived | waived | 2 | 1 | 1 |
| AGENTD-3 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-4 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-5 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-6 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-7 | 1 | 1 | 1 | 4 | 4 | 1 |
| AGENTD-8 | 1 | 1 | 1 | 4 | 2 | 1 |
| AGENTD-9 | 1 | 1 | 1 | 2 | 1 | 1 |
| AGENTD-10 | 1 | 1 | 1 | 2 | 1 | 1 |
| AGENTD-11 | 1 | 1 | 1 | 4 | 3 | 1 |
| AGENTD-12 | 1 | 1 | 1 | 2 | 3 | 1 |
| AGENTD-13 | 1 | 1 | 1 | 3 | 1 | 1 |
| AGENTD-14 | 1 | 1 | 1 | 4 | 3 | 1 |
| AGENTD-15 | 1 | 1 | 1 | 2 | 2 | 1 |
| AGENTD-16 | 1 | 1 | 1 | 4 | 4 | 1 |
| AGENTD-17 | 1 | waived | 1 | 2 | 1 | waived |
| AGENTD-18 | 1 | waived | waived | 3 | 1 | 1 |
| AGENTD-19 | 1 | waived | waived | 1 | 1 | waived |
| AGENTD-20 | 1 | waived | 1 | 3 | 1 | waived |
| AGENTD-21 | 1 | waived | 1 | 1 | 1 | waived |
| AGENTD-22 | 1 | 1 | 1 | 4 | 3 | 2 |
| AGENTD-23 | 1 | 1 | 1 | 2 | 2 | 2 |
| AGENTD-24 | 1 | 1 | 1 | 2 | 1 | 1 |
| AGENTD-25 | waived | waived | waived | 2 | 1 | 1 |
| AGENTD-26 | waived | waived | waived | 1 | 1 | 1 |
| ARCH-1 | waived | waived | waived | 1 | 2 | waived |
| ARCH-2 | waived | waived | waived | 1 | 4 | waived |
| ARCH-3 | waived | waived | waived | 1 | 1 | waived |
| ARCH-4 | waived | waived | waived | 1 | 1 | waived |
| ARCH-5 | waived | waived | waived | 1 | 1 | waived |
| ARCH-6 | waived | waived | waived | 1 | 6 | waived |
| ARCH-7 | waived | waived | waived | 2 | 4 | waived |
| ARCH-8 | waived | waived | waived | 1 | 1 | waived |
| BIND-1 | waived | waived | waived | 1 | 2 | waived |
| BIND-2 | waived | waived | waived | 3 | 7 | waived |
| BIND-3 | waived | waived | waived | 1 | 1 | 1 |
| BIND-4 | waived | waived | waived | 1 | 1 | 1 |
| BIND-5 | waived | waived | waived | 2 | 2 | waived |
| BIND-6 | 1 | 1 | 1 | 5 | 7 | 1 |
| BIND-7 | 1 | 1 | 1 | 4 | 4 | 1 |
| BIND-8 | 1 | 1 | 1 | 4 | 2 | 1 |
| BIND-9 | 1 | 1 | 1 | 4 | 2 | 1 |
| BIND-10 | 1 | 1 | 1 | 5 | 6 | 1 |
| BIND-11 | 1 | 1 | 1 | 4 | 1 | 1 |
| BIND-12 | 1 | 1 | 1 | 5 | 3 | 1 |
| BIND-13 | 1 | 1 | 1 | 4 | 3 | waived |
| BIND-14 | waived | 1 | 1 | 3 | 3 | waived |
| BIND-15 | 1 | 1 | waived | 6 | 6 | 1 |
| BIND-16 | 1 | 1 | waived | 5 | 5 | 1 |
| BIND-17 | 1 | 1 | 1 | 2 | 4 | 1 |
| BIND-18 | 1 | 1 | 1 | 6 | 3 | 1 |
| BIND-19 | 1 | 1 | 1 | 3 | 1 | 1 |
| BIND-20 | 1 | 1 | 1 | 6 | 4 | 1 |
| BIND-21 | 1 | waived | 1 | 1 | 1 | 1 |
| BIND-22 | waived | waived | 1 | 1 | 1 | waived |
| BIND-23 | 1 | waived | 1 | 2 | 1 | 1 |
| BIND-24 | 1 | waived | 1 | 1 | 1 | waived |
| BIND-25 | waived | waived | waived | 1 | 1 | waived |
| BIND-26 | waived | waived | waived | 1 | 1 | waived |
| BIND-27 | waived | waived | waived | 1 | 1 | waived |
| CLI-1 | waived | waived | waived | 1 | 2 | waived |
| CLI-2 | waived | waived | waived | 1 | 5 | waived |
| CLI-3 | waived | waived | waived | 2 | 1 | 2 |
| CLI-4 | waived | waived | waived | 3 | 5 | 2 |
| CLI-5 | waived | waived | waived | 4 | 4 | waived |
| CLI-6 | waived | waived | waived | 5 | 6 | waived |
| CLI-7 | 1 | 1 | 1 | 3 | 8 | 1 |
| CLI-8 | 1 | 1 | 1 | 2 | 3 | 2 |
| CLI-9 | 1 | 1 | 1 | 2 | 3 | 1 |
| COST-1 | waived | waived | waived | 1 | 3 | 1 |
| COST-2 | waived | waived | waived | 2 | 3 | waived |
| COST-3 | waived | waived | waived | 1 | 3 | 1 |
| COST-4 | waived | waived | waived | 3 | 5 | 1 |
| COST-5 | waived | waived | waived | 3 | 2 | waived |
| COST-6 | waived | waived | waived | 1 | 1 | waived |
| COST-7 | waived | waived | waived | 1 | 1 | waived |
| COST-8 | waived | waived | waived | 1 | 1 | waived |
| COST-9 | waived | waived | waived | 3 | 4 | waived |
| COST-10 | waived | waived | waived | 4 | 3 | 1 |
| IMAGE-1 | 1 | 1 | 1 | 2 | 1 | waived |
| IMAGE-2 | 1 | 1 | 1 | 2 | 2 | 2 |
| IMAGE-3 | 1 | 1 | 1 | 2 | 2 | waived |
| IMAGE-4 | 1 | 1 | 1 | 1 | 2 | 1 |
| IMAGE-5 | waived | waived | waived | 2 | 2 | waived |
| IMAGE-6 | waived | 1 | 1 | 2 | 2 | 1 |
| IMAGE-7 | waived | 1 | 1 | 3 | 5 | 1 |
| IMAGE-8 | 1 | 1 | 1 | 2 | 4 | 1 |
| IMAGE-9 | 1 | 1 | waived | 2 | 1 | 1 |
| IMAGE-10 | 1 | 1 | waived | 2 | 1 | 1 |
| IMAGE-11 | 1 | 1 | waived | 1 | 1 | 1 |
| IMAGE-12 | waived | waived | waived | 2 | 2 | waived |
| STATE-1 | 1 | waived | waived | 2 | 3 | waived |
| STATE-2 | 1 | waived | waived | 2 | 4 | waived |
| STATE-3 | 1 | waived | waived | 2 | 3 | waived |
| STATE-4 | 1 | waived | waived | 2 | 1 | waived |
| STATE-5 | 1 | waived | waived | 2 | 6 | waived |
| STATE-6 | 1 | waived | waived | 2 | 1 | 1 |
| STATE-7 | 1 | waived | waived | 2 | 5 | 1 |
| STATE-8 | 1 | waived | waived | 5 | 5 | waived |
| STATE-9 | 1 | waived | waived | 2 | 1 | waived |
| STATE-10 | 1 | waived | waived | 2 | 1 | 1 |
| STATE-11 | 1 | waived | waived | 2 | 3 | waived |
| STATE-12 | 1 | waived | waived | 4 | 6 | 2 |
| TRAP-1 | waived | waived | waived | 9 | 19 | waived |
| TRAP-2 | waived | waived | waived | 1 | 5 | waived |
| TRAP-3 | waived | waived | waived | 1 | 6 | 1 |
| TRAP-4 | waived | 1 | 1 | 2 | 4 | waived |
| TRAP-5 | waived | waived | waived | 2 | 6 | waived |
| TRAP-6 | waived | 1 | waived | 3 | 11 | waived |
| TRAP-7 | waived | waived | waived | 5 | 7 | 1 |
| TRAP-8 | waived | waived | waived | 3 | 7 | waived |
| TRAP-9 | waived | waived | waived | 5 | 10 | waived |
| TRAP-10 | waived | waived | waived | 5 | 7 | waived |
| TRAP-11 | waived | waived | waived | 2 | 6 | waived |
| TRAP-12 | waived | waived | waived | 1 | 6 | waived |
| TRAP-13 | waived | waived | waived | 1 | 3 | 1 |
AGENTD-1
Section titled “AGENTD-1”While the agent token is not installed, the agentd shall reject the control request.
- model:
crates/model/src/lib.rs - gherkin: waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon’s routes, which a scenario would restate
- fuzz: waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
- test:
crates/agentd/tests/model_conformance.rs,crates/agentd/tests/turmoil_transport.rs - impl:
crates/agentd/src/auth.rs - live: waived: the platform runs the hook before it forwards any traffic (AGENTD-2’s live check), so a live run never reaches the daemon before bootstrap
AGENTD-2
Section titled “AGENTD-2”When a bootstrap request presents a token and the agent token is not installed, the agentd shall install the agent token.
- model:
crates/model/src/lib.rs - gherkin: waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon’s routes, which a scenario would restate
- fuzz: waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
- test:
crates/agentd/src/state.rs,crates/agentd/tests/turmoil_transport.rs - impl:
crates/agentd/src/state.rs - live:
conformance/lanes/lifecycle.py
AGENTD-3
Section titled “AGENTD-3”When a bootstrap request presents a token that differs from the installed agent token, the agentd shall reject the bootstrap request.
- model:
crates/model/src/lib.rs - gherkin: waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon’s routes, which a scenario would restate
- fuzz: waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
- test:
crates/agentd/src/state.rs - impl:
crates/agentd/src/state.rs - live:
conformance/lanes/bootstrap.py
AGENTD-4
Section titled “AGENTD-4”When a bootstrap request presents a token equal to the installed agent token, the agentd shall accept the bootstrap request.
- model:
crates/model/src/lib.rs - gherkin: waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon’s routes, which a scenario would restate
- fuzz: waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
- test:
crates/agentd/src/state.rs - impl:
crates/agentd/src/state.rs - live:
conformance/lanes/bootstrap.py
AGENTD-5
Section titled “AGENTD-5”When a control request presents a token that differs from the installed agent token, the agentd shall reject the control request.
- model:
crates/model/src/lib.rs - gherkin: waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon’s routes, which a scenario would restate
- fuzz: waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
- test:
crates/agentd/tests/turmoil_transport.rs - impl:
crates/agentd/src/auth.rs - live:
conformance/lanes/bootstrap.py
AGENTD-6
Section titled “AGENTD-6”When a control request presents a token equal to the installed agent token, the agentd shall accept the control request.
- model:
crates/model/src/lib.rs - gherkin: waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon’s routes, which a scenario would restate
- fuzz: waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
- test:
crates/agentd/tests/turmoil_transport.rs - impl:
crates/agentd/src/auth.rs - live:
conformance/lanes/bootstrap.py
AGENTD-7
Section titled “AGENTD-7”When a start request names its user or its group with a JSON string, the agentd shall resolve the name against the guest’s /etc/passwd or /etc/group before it spawns the child.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
bindings/microvms-js/__test__/exec_start.mjs,bindings/microvms-py/tests/test_exec_start.py,crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
bindings/microvms-js/src/session.rs,bindings/microvms-py/src/session.rs,crates/agentd/src/exec_start.rs,crates/microvms-cli/src/cli.rs - live:
conformance/lanes/exec.py
AGENTD-8
Section titled “AGENTD-8”If a start request names a user or a group that the guest’s /etc/passwd or /etc/group does not contain, then the agentd shall answer Bad Request with the unknown_user or unknown_group error naming the value and spawn no child.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
bindings/microvms-js/__test__/exec_start.mjs,bindings/microvms-py/tests/test_exec_start.py,crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - live:
conformance/lanes/exec.py
AGENTD-9
Section titled “AGENTD-9”When the user of a start request resolves to a passwd row, the agentd shall set HOME, USER and LOGNAME from the passwd row beneath the launch environment and the request environment.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
crates/agentd/src/exec_start.rs - live:
conformance/lanes/exec.py
AGENTD-10
Section titled “AGENTD-10”While a start request leaves inherit_image_env unset, the agentd shall build the child environment from the passwd identity, the launch environment and the request environment only.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
crates/agentd/src/exec_start.rs - live:
conformance/lanes/exec.py
AGENTD-11
Section titled “AGENTD-11”When a start request sets inherit_image_env, the agentd shall place the environment the agentd inherited at startup beneath the passwd identity, the launch environment and the request environment.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
bindings/microvms-js/__test__/exec_start.mjs,bindings/microvms-py/tests/test_exec_start.py,crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
bindings/microvms-js/src/session.rs,crates/agentd/src/exec_start.rs,crates/microvms-cli/src/cli.rs - live:
conformance/lanes/exec.py
AGENTD-12
Section titled “AGENTD-12”The agentd shall exclude each AGENTD_ variable and the agent token from the image environment snapshot.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
crates/agentd/src/exec_start.rs,crates/agentd/src/lib.rs,crates/agentd/src/main.rs - live:
conformance/lanes/exec.py
AGENTD-13
Section titled “AGENTD-13”The agentd shall report on /v1/health whether an image environment snapshot exists and its key count, without its values.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
bindings/microvms-js/__test__/exec_start.mjs,bindings/microvms-py/tests/test_exec_start.py,crates/protocol/src/health.rs - impl:
crates/agentd/src/routes.rs - live:
conformance/lanes/exec.py
AGENTD-14
Section titled “AGENTD-14”When a start request names a shell, the agentd shall resolve the shell name on the child PATH, the image PATH, /bin and /usr/bin and run the command as the -c script of the resolved shell.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
bindings/microvms-js/__test__/exec_start.mjs,bindings/microvms-py/tests/test_exec_start.py,crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
bindings/microvms-py/src/session.rs,crates/agentd/src/exec_start.rs,crates/microvms-cli/src/cli.rs - live:
conformance/lanes/exec.py
AGENTD-15
Section titled “AGENTD-15”If a start request names a shell that no searched directory holds as an executable file, then the agentd shall answer Bad Request with the unknown_shell error naming the shell and spawn no child.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - live:
conformance/lanes/exec.py
AGENTD-16
Section titled “AGENTD-16”When a start request carries its user and group as integers and its shell as a boolean, the agentd shall demote the child to exactly those ids and run a true shell as /bin/sh -c.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
bindings/microvms-js/__test__/exec_start.mjs,bindings/microvms-py/tests/test_exec_start.py,crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
bindings/microvms-js/src/session.rs,bindings/microvms-py/src/session.rs,crates/agentd/src/exec_start.rs,crates/microvms-cli/src/cli.rs - live:
conformance/lanes/exec.py
AGENTD-17
Section titled “AGENTD-17”If the handshake of an identity-verified tunnel is not made with the host key the run hook pinned, then the agentd shall close the tunnel with close code 4403.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz:
crates/agentd/src/tunnel_fuzz.rs - test:
crates/agentd/src/tunnel_identity.rs,crates/agentd/tests/tunnel_relay.rs - impl:
crates/agentd/src/tunnel_identity.rs - live: waived: no live check presents another host key: that needs a second host identity for one VM, and the relay tests drive the daemon’s real route with one
AGENTD-18
Section titled “AGENTD-18”While the handshake of an identity-verified tunnel has not completed, the agentd shall not dial the guest port or relay any byte between the caller and the guest.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz: waived: when the daemon dials is an order of steps, not a function of bytes; the tunnel model checks it over every interleaving and the relay tests against the daemon’s real route
- test:
crates/agentd/tests/tunnel_relay.rs,crates/model-conformance/tests/tunnel_confirmation.rs,crates/model-conformance/tests/tunnel_end_of_stream.rs - impl:
crates/agentd/src/tunnel.rs - live:
conformance/lanes/tunnel.py
AGENTD-19
Section titled “AGENTD-19”When the guest side of an identity-verified tunnel reaches the end of the guest stream, the agentd shall send the end of stream inside the Noise session before the agentd closes the tunnel.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz: waived: what the daemon sends at a guest EOF doesn’t depend on any byte it read; the tunnel model checks that the end precedes the close, and the client’s frame harness that it opens only after every chunk
- test:
crates/agentd/tests/tunnel_relay.rs - impl:
crates/agentd/src/tunnel.rs - live: waived: the live suite’s BIND-23 check observes it: the client reads Closed through the real proxy only when this end of stream crossed it
AGENTD-20
Section titled “AGENTD-20”If an identity-verified tunnel whose caller offered the end of stream ends without the caller’s end of stream, then the agentd shall reset the guest connection rather than close the guest connection.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz:
crates/agentd/src/tunnel_fuzz.rs - test:
crates/agentd/tests/tunnel_relay.rs,crates/microvms-edges/tests/tunnel_end_of_stream.rs,crates/model-conformance/tests/tunnel_end_of_stream.rs - impl:
crates/agentd/src/tunnel.rs - live: waived: a live run can’t cut the endpoint proxy’s connection mid-stream or withhold one frame, so no live check presents a caller end without its end of stream; the relay tests drive the daemon’s real route
AGENTD-21
Section titled “AGENTD-21”If a frame of an identity-verified tunnel does not authenticate at the frame’s position in the caller’s stream, then the agentd shall end the tunnel without relaying the frame to the guest.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz:
crates/agentd/src/tunnel_fuzz.rs - test:
crates/agentd/tests/tunnel_relay.rs - impl:
crates/agentd/src/tunnel.rs - live: waived: a live daemon and the endpoint proxy neither replay nor forge a frame, so a live run can’t present one; the relay tests send both to the daemon’s real route
AGENTD-22
Section titled “AGENTD-22”Where the image environment sets the default user, the agentd shall resolve the default user against the guest’s /etc/passwd as the user of each start request that names no user.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
crates/agentd/src/config.rs,crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs,crates/agentd/src/routes.rs - impl:
crates/agentd/src/config.rs,crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - live:
conformance/lanes/default_user.py,conformance/lanes/wrapped_user.py
AGENTD-23
Section titled “AGENTD-23”Where the image environment sets the default user, the agentd shall demote the child of a start request that names its user to the named user rather than the default user.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
crates/agentd/src/config.rs,crates/agentd/src/exec_start.rs - live:
conformance/lanes/default_user.py,conformance/lanes/wrapped_user.py
AGENTD-24
Section titled “AGENTD-24”If a start request names no user and the guest’s /etc/passwd does not contain the default user, then the agentd shall answer Bad Request with the unknown_user error naming the default user setting and spawn no child.
- model:
crates/model/src/exec_start.rs - gherkin:
crates/agentd/tests/features/exec_start.feature - fuzz:
crates/agentd/src/exec_start_fuzz.rs - test:
crates/agentd/src/exec.rs,crates/agentd/src/exec_start.rs - impl:
crates/agentd/src/exec_start.rs - live:
conformance/lanes/default_user.py
AGENTD-25
Section titled “AGENTD-25”When an accepted start request sets poweroff_on_exit to true, the agentd shall request guest power-off only after observing that the execution’s original process group has no live members.
- model: waived: the process identities and liveness are Linux procfs observations; fixture snapshots and a real child group test the observer, while the live lane checks the guest shutdown path
- gherkin: waived: the route test starts a real shell and holds its background group member until after result publication; another textual scenario would restate that sequence
- fuzz: waived: the observer rejects malformed procfs records and tests PID reuse, disappearing entries, and zombie liveness directly; the shutdown action is injected so no fuzz input can power off the host
- test:
crates/agentd/src/exec.rs,crates/agentd/src/poweroff.rs - impl:
crates/agentd/src/poweroff.rs - live:
conformance/lanes/poweroff.py
AGENTD-26
Section titled “AGENTD-26”When the image enables AGENTD_DROP_EXEC_CAPABILITIES, the agentd shall verify that inheritable and ambient capabilities are empty and bounding capabilities SYS_MODULE, SYS_RAWIO, SYS_PTRACE, SYS_ADMIN, SYS_BOOT, PERFMON, and BPF are absent while its permitted and effective capabilities remain unchanged before creating threads or serving requests.
- model: waived: the policy uses Linux thread capabilities; injected syscall failures and an isolated real capability subprocess test its state transitions
- gherkin: waived: the isolated subprocess exercises nonempty inheritable and ambient sets, thread creation, and exec directly; a textual scenario would repeat it
- fuzz: waived: strict boolean parsing and syscall postconditions are finite inputs exercised directly, and capability mutations belong only in isolated subprocesses
- test:
crates/agentd/src/exec_capabilities.rs - impl:
crates/agentd/src/exec_capabilities.rs - live:
conformance/lanes/capability_policy.py
ARCH-1
Section titled “ARCH-1”The microvms-core shall be the single library crate the CLI crate and the language bindings depend on, composing microvms-app with microvms-edges and re-exporting microvms-domain.
- model: waived: a property of the workspace’s dependency graph, not of a state
- gherkin: waived: no behavior to script: cargo metadata’s resolved graph is the evidence, and dependency_direction.rs reads it
- fuzz: waived: there is no input stream; the rule is over manifests and re-exports
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/microvms-core/src/lib.rs,crates/microvms-domain/src/lib.rs - live: waived: composition makes no AWS call of its own
ARCH-2
Section titled “ARCH-2”The microvms-core shall share protocol types with the agentd crate through a common dependency so that protocol drift fails compilation.
- model: waived: a property of the workspace’s dependency graph, not of a state
- gherkin: waived: no behavior to script: the shared crate makes a wire-type mismatch a compile error, before anything runs
- fuzz: waived: there is no input stream; the rule is over manifests
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/agentd/src/tunnel.rs,crates/microvms-app/src/session/mod.rs,crates/protocol/src/identity.rs,crates/protocol/src/tunnel.rs - live: waived: a build-time property; the live tier runs a client and a daemon built from the one protocol crate, which is its premise, not a check of it
ARCH-3
Section titled “ARCH-3”The CLI crate shall depend on microvms-core for each control-plane and endpoint-proxy operation.
- model: waived: a property of the workspace’s dependency graph, not of a state
- gherkin: waived: no behavior to script: cargo metadata’s resolved graph is the evidence, and dependency_direction.rs reads it
- fuzz: waived: there is no input stream; the rule is over manifests
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/microvms-cli/src/main.rs - live: waived: a dependency edge makes no AWS call
ARCH-4
Section titled “ARCH-4”The microvms-core shall not depend on the CLI crate.
- model: waived: a property of the workspace’s dependency graph, not of a state
- gherkin: waived: no behavior to script: cargo metadata’s resolved graph is the evidence, and dependency_direction.rs reads it
- fuzz: waived: there is no input stream; the rule is over manifests
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/microvms-core/src/lib.rs - live: waived: a dependency edge makes no AWS call
ARCH-5
Section titled “ARCH-5”The CLI crate shall not carry any type or function a language binding needs.
- model: waived: a property of the CLI crate’s targets and of the capability table, not of a state
- gherkin: waived: no behavior to script: cargo metadata and the capability table are the evidence, and dependency_direction.rs reads both
- fuzz: waived: there is no input stream; the rule is over the crate’s targets and the table
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/microvms-cli/src/main.rs - live: waived: a crate’s targets and the table’s cells make no AWS call
ARCH-6
Section titled “ARCH-6”The microvms-domain shall not perform network, filesystem, subprocess, environment, clock, or entropy access.
- model: waived: a property of a crate’s code and dependencies, not of a state
- gherkin: waived: no behavior to script: clippy and the dependency set enforce it at build time
- fuzz: waived: there is no input stream; the rule is over source and manifests
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/microvms-core/src/lib.rs,crates/microvms-core/src/prelude.rs,crates/microvms-domain/src/cost.rs,crates/microvms-domain/src/identity.rs,crates/microvms-domain/src/lib.rs,crates/microvms-domain/src/names.rs - live: waived: the domain makes no AWS call by construction
ARCH-7
Section titled “ARCH-7”The microvms-app shall not depend directly on a crate or a tokio feature that performs network, AWS, filesystem, subprocess, or entropy I/O.
- model: waived: a property of a crate’s code and dependencies, not of a state
- gherkin: waived: no behavior to script: clippy and the dependency set enforce it at build time
- fuzz: waived: there is no input stream; the rule is over source and manifests
- test:
crates/microvms-app/src/sandbox.rs,crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/microvms-app/src/lib.rs,crates/microvms-app/src/workspace.rs,crates/microvms-core/src/lib.rs,crates/microvms-edges/src/lib.rs - live: waived: the app’s AWS calls all go through ports, so the live tier exercises the edges’ implementations, not this rule
ARCH-8
Section titled “ARCH-8”The microvms-core shall not contain logic beyond composition and re-exports.
- model: waived: a property of a crate’s code and dependencies, not of a state
- gherkin: waived: no behavior to script: the dependency set and the ratchet check it over source and manifests
- fuzz: waived: there is no input stream; the rule is over source and manifests
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
crates/microvms-core/src/lib.rs - live: waived: composition makes no AWS call of its own
BIND-1
Section titled “BIND-1”The language bindings layer shall depend on microvms-core and, among the crates below it, only on microvms-protocol, with no dependency edge to the CLI crate.
- model: waived: a property of the workspace’s dependency graph, not of a state
- gherkin: waived: no behavior to script: cargo metadata’s resolved graph is the evidence, and dependency_direction.rs reads it
- fuzz: waived: there is no input stream; the rule is over manifests
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
bindings/microvms-js/src/lib.rs,bindings/microvms-py/src/lib.rs - live: waived: a dependency edge makes no AWS call
BIND-2
Section titled “BIND-2”The language bindings layer shall not expose a parameter that bypasses a trap closure enforced in microvms-core.
- model: waived: a property of each binding’s parameter surface, not of a state
- gherkin: waived: no Gherkin tier drives the bindings; their own suites call each surface and assert the refusal comes from core
- fuzz: waived: the surface is a fixed set of signatures, not an input stream; the closures it must not reopen live in core, whose tests and harnesses exercise them
- test:
bindings/microvms-py/tests/test_exec.py,bindings/microvms-py/tests/test_session.py,bindings/microvms-py/tests/test_smoke.py - impl:
bindings/microvms-js/src/errors.rs,bindings/microvms-js/src/exec.rs,bindings/microvms-js/src/hooks.rs,bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/exec.rs,bindings/microvms-py/src/hooks.rs,bindings/microvms-py/src/sandbox.rs - live: waived: the live suite drives the CLI, and a binding makes no AWS call core doesn’t make; the closures it must not bypass are core’s, checked offline
BIND-3
Section titled “BIND-3”The Python binding shall deposit a thin idiomatic wrapper over microvms-core via PyO3.
- model: waived: a property of the crate’s dependencies and surface, not of a state
- gherkin: waived: no behavior to script: the dependency set and the adapter-logic ratchet check it over manifests and source
- fuzz: waived: there is no input stream; the rule is over manifests and source
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
bindings/microvms-py/src/lib.rs - live:
conformance/lanes/bindings.py
BIND-4
Section titled “BIND-4”The JavaScript binding shall deposit a thin idiomatic wrapper over microvms-core via napi-rs.
- model: waived: a property of the crate’s dependencies and surface, not of a state
- gherkin: waived: no behavior to script: the dependency set and the adapter-logic ratchet check it over manifests and source
- fuzz: waived: there is no input stream; the rule is over manifests and source
- test:
crates/microvms-cli/tests/dependency_direction.rs - impl:
bindings/microvms-js/src/lib.rs - live:
conformance/lanes/bindings.py
BIND-5
Section titled “BIND-5”The language bindings layer shall preserve the cost honesty rules, exposing provenance-labelled durations, estimate-typed dollars, and the distinct Unpriced value.
- model: waived: a property of the bindings’ cost types, which have no states to explore
- gherkin: waived: no behavior to script: each binding’s suite asserts the shut doors directly, the coercions, the missing constructor and the absent usd key
- fuzz: waived: there is no input stream; the rule is over each binding’s type surface, which the suites enumerate spelling by spelling
- test:
bindings/microvms-js/__test__/smoke.mjs,bindings/microvms-py/tests/test_smoke.py - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs - live: waived: the bindings’ cost types are local values and make no AWS call; the live suite holds core’s report through the CLI (COST-1, COST-3, COST-4, COST-10)
BIND-6
Section titled “BIND-6”The microvms-core shall report a finished exec’s POSIX exit code as 124 when a deadline ended the command, as 128 plus the signal number for any other signal death, and otherwise as the exit code.
- model:
crates/model/src/run.rs - gherkin:
crates/microvms-core/tests/features/run_to_completion.feature - fuzz:
crates/microvms-core/tests/run_to_completion_fuzz.rs - test:
bindings/microvms-js/__test__/run_to_completion.mjs,bindings/microvms-py/tests/test_run_to_completion.py,crates/microvms-app/src/session/exec.rs,crates/microvms-core/tests/live_run_to_completion.rs,crates/model-conformance/tests/tables.rs - impl:
bindings/microvms-js/src/exec.rs,bindings/microvms-js/src/session.rs,bindings/microvms-py/src/exec.rs,bindings/microvms-py/src/session.rs,crates/microvms-app/src/session/complete.rs,crates/microvms-app/src/session/exec.rs,crates/microvms-cli/src/commands/attached.rs - live:
conformance/lanes/sessions.py
BIND-7
Section titled “BIND-7”The microvms-core shall annotate an exec result with one human-readable note for each of truncated output, an expired daemon deadline, writers left alive past the linger deadline, an expired client deadline, and a synthesized result.
- model:
crates/model/src/run.rs - gherkin:
crates/microvms-core/tests/features/run_to_completion.feature - fuzz:
crates/microvms-core/tests/run_to_completion_fuzz.rs - test:
bindings/microvms-js/__test__/run_to_completion.mjs,bindings/microvms-py/tests/test_run_to_completion.py,crates/microvms-app/src/session/exec.rs,crates/microvms-core/tests/live_run_to_completion.rs - impl:
bindings/microvms-js/src/exec.rs,bindings/microvms-py/src/exec.rs,crates/microvms-app/src/session/exec.rs,crates/microvms-cli/src/commands/attached.rs - live:
conformance/lanes/sessions.py
BIND-8
Section titled “BIND-8”If the output stream of a run-to-completion call ends without the terminal exit event, then the microvms-core shall fall back to waiting for and acknowledging the exec and return exactly one result.
- model:
crates/model/src/run.rs - gherkin:
crates/microvms-core/tests/features/run_to_completion.feature - fuzz:
crates/microvms-core/tests/run_to_completion_fuzz.rs - test:
bindings/microvms-js/__test__/run_to_completion.mjs,bindings/microvms-py/tests/test_run_to_completion.py,crates/microvms-app/src/session/complete.rs,crates/microvms-core/tests/live_run_to_completion.rs - impl:
crates/microvms-app/src/session/complete.rs,crates/microvms-cli/src/cli.rs - live:
conformance/lanes/sessions.py
BIND-9
Section titled “BIND-9”If the client deadline of a run-to-completion call expires before the exec’s result is acknowledged, then the microvms-core shall signal the exec’s process group before acknowledging the exec within the client grace period.
- model:
crates/model/src/run.rs - gherkin:
crates/microvms-core/tests/features/run_to_completion.feature - fuzz:
crates/microvms-core/tests/run_to_completion_fuzz.rs - test:
bindings/microvms-js/__test__/run_to_completion.mjs,bindings/microvms-py/tests/test_run_to_completion.py,crates/microvms-app/src/session/complete.rs,crates/microvms-core/tests/live_run_to_completion.rs - impl:
crates/microvms-app/src/session/complete.rs,crates/microvms-app/src/session/exec.rs - live:
conformance/lanes/sessions.py
BIND-10
Section titled “BIND-10”If the acknowledgement that follows a client-deadline kill fails, then the microvms-core shall return a synthesized result whose POSIX exit code is 124 and whose notes name the failure.
- model:
crates/model/src/run.rs - gherkin:
crates/microvms-core/tests/features/run_to_completion.feature - fuzz:
crates/microvms-core/tests/run_to_completion_fuzz.rs - test:
bindings/microvms-js/__test__/run_to_completion.mjs,bindings/microvms-py/tests/test_run_to_completion.py,crates/microvms-app/src/session/complete.rs,crates/microvms-cli/src/guards/exec.rs,crates/microvms-core/tests/live_run_to_completion.rs - impl:
bindings/microvms-js/src/exec.rs,bindings/microvms-py/src/exec.rs,crates/microvms-app/src/session/complete.rs,crates/microvms-app/src/session/exec.rs,crates/microvms-cli/src/cli.rs,crates/microvms-cli/src/commands/attached.rs - live:
conformance/lanes/sessions.py
BIND-11
Section titled “BIND-11”The microvms-core shall derive a launch’s egress posture from its launch options alone, as open when managed internet egress is requested, best-effort when the advisory deny is requested, and unsealed otherwise, and never as sealed.
- model:
crates/model/src/posture.rs - gherkin:
crates/microvms-core/tests/features/egress_posture.feature - fuzz:
crates/microvms-app/src/control/posture_fuzz.rs - test:
bindings/microvms-js/__test__/egress_posture.mjs,bindings/microvms-py/tests/test_egress_posture.py,crates/microvms-app/src/control/connector.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/control/connector.rs - live:
conformance/lanes/posture.py
BIND-12
Section titled “BIND-12”The language bindings layer shall expose on each session the egress posture the CLI envelope reports for the same launch options, and unsealed for a session whose launch options the session does not hold.
- model:
crates/model/src/posture.rs - gherkin:
crates/microvms-core/tests/features/egress_posture.feature - fuzz:
crates/microvms-app/src/control/posture_fuzz.rs - test:
bindings/microvms-js/__test__/egress_posture.mjs,bindings/microvms-py/tests/test_egress_posture.py,crates/microvms-app/src/sandbox.rs,crates/microvms-cli/src/guards/run.rs,crates/microvms-core/tests/live_posture.rs - impl:
crates/microvms-app/src/sandbox.rs,crates/microvms-app/src/session/mod.rs,crates/microvms-cli/src/commands/lifecycle.rs - live:
conformance/lanes/posture.py
BIND-13
Section titled “BIND-13”When a caller asks for the egress posture of a set of launch options, the microvms-core shall answer with the posture a launch with those options would report, or with the invalid-argument refusal the launch would raise, without any AWS call.
- model:
crates/model/src/posture.rs - gherkin:
crates/microvms-core/tests/features/egress_posture.feature - fuzz:
crates/microvms-app/src/control/posture_fuzz.rs - test:
bindings/microvms-js/__test__/egress_posture.mjs,bindings/microvms-py/tests/test_egress_posture.py,crates/microvms-app/src/control/connector.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/control/connector.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-cli/src/commands/lifecycle.rs - live: waived: a pure function that makes no AWS call; its refusals precede any call, so the service never sees them (zero calls asserted by the Gherkin scenarios and the fuzz harness)
BIND-14
Section titled “BIND-14”The sizing model shall select for a resource request the smallest size class whose baseline memory and baseline vCPU both cover the request, the default class when the request names neither, and an invalid-argument refusal naming the largest class when no class covers the request.
- model: waived: a stateless selection over the five-row size table; the bolero harness checks minimality and coverage over arbitrary requests instead
- gherkin:
crates/microvms-core/tests/features/request_and_preflight.feature - fuzz:
crates/microvms-domain/src/sizing_fuzz.rs - test:
bindings/microvms-js/__test__/request_and_preflight.mjs,bindings/microvms-py/tests/test_request_and_preflight.py,crates/microvms-domain/src/sizing.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs,crates/microvms-domain/src/sizing.rs - live: waived: a pure function of the request and the documented table; it makes no AWS call
BIND-15
Section titled “BIND-15”When a caller asks for a preflight, the microvms-core shall report whether the region resolves to a supported region, whether the credential chain resolves credentials, and whether the MicroVMs service answers a free read-only listing in that region, as one report whose ok is true only when every fatal check passed.
- model:
crates/model/src/preflight.rs - gherkin:
crates/microvms-core/tests/features/request_and_preflight.feature - fuzz: waived: the outcome space (3 region x 2 credential x 3 service worlds) is enumerated exhaustively by the Stateright model; there is no input stream to fuzz
- test:
bindings/microvms-js/__test__/request_and_preflight.mjs,bindings/microvms-py/tests/test_request_and_preflight.py,crates/microvms-app/src/preflight.rs,crates/microvms-cli/src/guards/doctor.rs,crates/microvms-core/tests/live_preflight.rs,crates/model-conformance/tests/tables.rs - impl:
bindings/microvms-js/src/preflight.rs,bindings/microvms-py/src/preflight.rs,crates/microvms-app/src/control/image.rs,crates/microvms-app/src/control/transport.rs,crates/microvms-app/src/preflight.rs,crates/microvms-domain/src/preflight.rs - live:
conformance/lanes/local.py
BIND-16
Section titled “BIND-16”The microvms-core shall not make a billable or mutating AWS call during a preflight, nor any AWS call after the region or the credentials failed to resolve.
- model:
crates/model/src/preflight.rs - gherkin:
crates/microvms-core/tests/features/request_and_preflight.feature - fuzz: waived: the outcome space (3 region x 2 credential x 3 service worlds) is enumerated exhaustively by the Stateright model; there is no input stream to fuzz
- test:
bindings/microvms-js/__test__/request_and_preflight.mjs,bindings/microvms-py/tests/test_request_and_preflight.py,crates/microvms-app/src/preflight.rs,crates/microvms-core/tests/live_preflight.rs,crates/model-conformance/tests/tables.rs - impl:
bindings/microvms-js/src/preflight.rs,bindings/microvms-py/src/preflight.rs,crates/microvms-app/src/control/image.rs,crates/microvms-app/src/preflight.rs,crates/microvms-domain/src/preflight.rs - live:
conformance/lanes/local.py
BIND-17
Section titled “BIND-17”When a caller requests the agentd daemon binary, the language bindings layer shall return the agentd binary that microvms-core resolves from a caller-supplied path, then the cache entry for the requested version, then the release asset for that version, with the version defaulting to the core version.
- model:
crates/model/src/provision.rs - gherkin:
crates/microvms-core/tests/features/provision.feature - fuzz:
crates/microvms-edges/src/provision_fuzz.rs - test:
bindings/microvms-js/__test__/provision.mjs,crates/microvms-edges/src/provision.rs - impl:
bindings/microvms-js/src/provision.rs,bindings/microvms-py/src/provision.rs,crates/microvms-edges/src/lib.rs,crates/microvms-edges/src/provision.rs - live:
conformance/lanes/quickstart.py
BIND-18
Section titled “BIND-18”If a fetched agentd release asset fails its attestation or SHA256SUMS verification, or neither verification can run, then the microvms-core shall fail with ERR_PRECONDITION without returning or caching the bytes.
- model:
crates/model/src/provision.rs - gherkin:
crates/microvms-core/tests/features/provision.feature - fuzz:
crates/microvms-edges/src/provision_fuzz.rs - test:
bindings/microvms-js/__test__/provision.mjs,crates/microvms-app/src/provision.rs,crates/microvms-edges/src/provision.rs,crates/microvms-edges/src/provision/release.rs,crates/microvms-edges/tests/provision_concurrent.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/provision.rs,crates/microvms-edges/src/provision.rs,crates/microvms-edges/src/provision/release.rs - live:
conformance/lanes/quickstart.py
BIND-19
Section titled “BIND-19”If a cached agentd binary does not match the digest recorded when its release asset was verified, then the microvms-core shall discard the entry and fetch the release asset again.
- model:
crates/model/src/provision.rs - gherkin:
crates/microvms-core/tests/features/provision.feature - fuzz:
crates/microvms-edges/src/provision_fuzz.rs - test:
bindings/microvms-js/__test__/provision.mjs,crates/microvms-edges/src/provision.rs,crates/microvms-edges/tests/provision_concurrent.rs - impl:
crates/microvms-edges/src/provision.rs - live:
conformance/lanes/quickstart.py
BIND-20
Section titled “BIND-20”If a caller-supplied or fetched agentd binary is not an aarch64 ELF executable, then the microvms-core shall refuse it with ERR_PRECONDITION.
- model:
crates/model/src/provision.rs - gherkin:
crates/microvms-core/tests/features/provision.feature - fuzz:
crates/microvms-edges/src/provision_fuzz.rs - test:
bindings/microvms-js/__test__/image_daemon.mjs,bindings/microvms-js/__test__/provision.mjs,crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/image.rs,crates/microvms-cli/src/guards/build.rs,crates/microvms-edges/src/provision.rs - impl:
bindings/microvms-js/src/provision.rs,bindings/microvms-py/src/provision.rs,crates/microvms-domain/src/provision.rs,crates/microvms-edges/src/provision.rs - live:
conformance/lanes/quickstart.py
BIND-21
Section titled “BIND-21”If the far end of an identity-verified tunnel does not complete the handshake against the VM public key pinned in the name record, then the microvms-core shall fail the tunnel rather than relay the local connection through the tunnel.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz:
crates/microvms-edges/src/session/tunnel_fuzz.rs - test:
crates/microvms-core/tests/tunnel_end_to_end.rs - impl:
crates/microvms-edges/src/session/tunnel.rs - live:
conformance/lanes/tunnel.py
BIND-22
Section titled “BIND-22”If a daemon event stream carries bytes that are not well-formed server-sent events, then the microvms-core shall drop the frame or end the stream with an error, without a panic and without holding more than 4 MiB of bytes that no frame terminator ends between reads.
- model: waived: one stream read by one parser has no interleavings to explore; its input space is bytes
- gherkin: waived: hostile bytes aren’t a scenario a caller drives; the parser’s tests feed it directly
- fuzz:
crates/microvms-app/src/session/sse_fuzz.rs - test:
crates/microvms-app/src/session/sse.rs - impl:
crates/microvms-app/src/session/sse.rs - live: waived: a live daemon sends well-formed events, so a live run can’t present hostile bytes
BIND-23
Section titled “BIND-23”If the far end of an identity-verified tunnel whose daemon offered the end of stream closes the tunnel without the daemon’s end of stream, then the microvms-core shall report the tunnel as truncated rather than closed.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz:
crates/microvms-edges/src/session/tunnel_fuzz.rs - test:
crates/microvms-edges/tests/tunnel_end_of_stream.rs,crates/model-conformance/tests/tunnel_end_of_stream.rs - impl:
crates/microvms-edges/src/session/tunnel.rs - live:
conformance/lanes/tunnel.py
BIND-24
Section titled “BIND-24”If a frame of an identity-verified tunnel does not authenticate at the frame’s position in the daemon’s stream, then the microvms-core shall fail the tunnel without writing the frame to the local connection.
- model:
crates/model/src/tunnel.rs - gherkin: waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
- fuzz:
crates/microvms-edges/src/session/tunnel_fuzz.rs - test:
crates/microvms-edges/tests/tunnel_end_of_stream.rs - impl:
crates/microvms-edges/src/session/tunnel.rs - live: waived: a live daemon and the endpoint proxy neither replay nor forge a frame, so a live run can’t present one; the stand-in tests send both to the client’s real relay
BIND-25
Section titled “BIND-25”When a caller awaits the awaitable twin of a Python binding method that calls AWS or the daemon, the Python binding shall run the future that the method’s blocking spelling runs, with the same arguments, as a task on the binding’s shared runtime, and answer that future’s result or its error class.
- model: waived: one future behind two spellings has no state of its own to explore; the future’s states are core’s, which its models hold
- gherkin: waived: no Gherkin tier drives the bindings; the Python suite calls each twin beside its blocking spelling and compares the answers
- fuzz: waived: the surface is a fixed set of signatures, not an input stream; the census test enumerates it twin by twin
- test:
bindings/microvms-py/tests/test_async.py - impl:
bindings/microvms-py/src/runtime.rs - live: waived: a twin makes the AWS calls its blocking spelling makes and no other; the live suite drives those through the CLI and core
BIND-26
Section titled “BIND-26”If a caller cancels the awaitable twin of a Python binding call that is not a lifecycle transition, then the Python binding shall abort the call’s task at its next await.
- model: waived: cancellation is the runtime’s abort of one task, not a protocol state; the core’s own models hold the states a dropped request leaves
- gherkin: waived: no Gherkin tier drives the bindings; the Python suite cancels a twin against a loopback daemon and a stalling proxy
- fuzz: waived: there is no input stream; the rule is over which spawn a twin calls
- test:
bindings/microvms-py/tests/test_async.py - impl:
bindings/microvms-py/src/runtime.rs - live: waived: a cancelled read makes no AWS call a live run could observe that the loopback tests don’t; the proxy test watches the connection itself
BIND-27
Section titled “BIND-27”If a caller cancels the awaitable twin of a lifecycle transition (a launch, a non-content-addressed image build, a suspend, a resume or a teardown), then the Python binding shall run the transition to completion on the object that started it.
- model: waived: cancellation is the runtime’s choice not to abort one task; the transitions it lets finish are core’s, which its models hold
- gherkin: waived: no Gherkin tier drives the bindings; the Python suite cancels a lifecycle twin through a stalling proxy
- fuzz: waived: there is no input stream; the rule is over which spawn a twin calls
- test:
bindings/microvms-py/tests/test_async.py - impl:
bindings/microvms-py/src/runtime.rs - live: waived: launching a VM to cancel its launch costs a billable VM per run for what the proxy test shows offline: the request stays open after the awaitable is gone
The CLI crate shall render its interactive surface with ratatui.
- model: waived: a rendering choice, not a state
- gherkin: waived: the TUI draws only when stdout is a terminal, and the Gherkin tier runs the binary on pipes
- fuzz: waived: a frame is drawn from rows the command has already rendered as text; there is no input stream
- test:
crates/microvms-cli/src/tui.rs - impl:
crates/microvms-cli/src/envelope.rs,crates/microvms-cli/src/tui.rs - live: waived: the live suite runs the CLI with –json on a pipe, where the TUI never draws
The CLI crate shall reach the control plane and the endpoint proxy only through microvms-core.
- model: waived: a property of the crate’s dependencies and of its one door to core, not of a state
- gherkin: waived: the behavioral guard already drives every AWS-touching command through a seam that refuses, which a scenario would restate
- fuzz: waived: there is no input stream; the rule is over the dependency set and the source
- test:
crates/microvms-cli/src/guards/thinness.rs - impl:
crates/microvms-app/src/session/exec.rs,crates/microvms-cli/src/commands/attached.rs,crates/microvms-cli/src/commands/local.rs,crates/microvms-cli/src/provision.rs,crates/microvms-cli/src/seam.rs - live: waived: a live run can’t show that a call didn’t bypass core; the dependency denylist, the clippy bans and the refusing seam can
The CLI crate shall emit a stable exit code per documented failure class, distinct from the code for an unexpected error.
- model: waived: a fixed table from failure class to code, not a state machine
- gherkin: waived: the table-driven test asserts every row, and tests/exit_codes.rs reads each class’s code at the process boundary; a scenario per row would restate the table
- fuzz: waived: the input is a closed enum of failure kinds, which the table-driven test walks exhaustively
- test:
crates/microvms-cli/src/exit.rs,crates/microvms-cli/src/guards/exit_codes.rs - impl:
crates/microvms-cli/src/exit.rs - live:
conformance/lanes/local.py,conformance/selftest/suite.py
Where JSON output is requested, the CLI crate shall emit exactly one envelope object per invocation on stdout, carrying an outcome discriminant and on failure a machine-readable code.
- model: waived: one envelope per invocation follows from main’s single write, not from a state; crates/model/src/output.rs models the closed-pipe rules, CLI-7 to CLI-9
- gherkin: waived: tests/exit_codes.rs parses stdout as one document at the process boundary, and the live harness does on every call
- fuzz: waived: the envelope’s count isn’t input-driven: one call in main writes it, and the closed-output harness fuzzes what happens around it (CLI-9)
- test:
crates/microvms-cli/src/envelope.rs,crates/microvms-cli/tests/exit_codes.rs,crates/microvms-cli/tests/thinness.rs - impl:
crates/microvms-cli/src/commands/attached.rs,crates/microvms-cli/src/commands/local.rs,crates/microvms-cli/src/commands/mod.rs,crates/microvms-cli/src/envelope.rs,crates/microvms-cli/src/main.rs - live:
conformance/lanes/local.py,conformance/selftest/suite.py
The CLI crate shall not expose an option that permits a value microvms-core rejects.
- model: waived: a property of the parser’s closed domains, not of a state
- gherkin: waived: the parser tests enumerate each closed domain and round-trip the manifest’s published values; a scenario per value would restate them
- fuzz: waived: the domains are closed sets the tests enumerate exactly, so there is no open input space to search
- test:
crates/microvms-cli/src/cli.rs,crates/microvms-cli/src/config.rs,crates/microvms-cli/src/manifest.rs,crates/microvms-cli/tests/manifest.rs - impl:
crates/microvms-cli/src/cli.rs,crates/microvms-cli/src/commands/local.rs,crates/microvms-cli/src/config.rs,crates/microvms-cli/src/manifest.rs - live: waived: a value the parser refuses never leaves the process, so the service never sees it
If a command is interrupted after a MicroVM has launched, then the CLI crate shall tear down the MicroVM and emit the identifiers of every resource it could not delete.
- model: waived: one interrupt in one window of one launch; the guard places it there against a scripted control plane
- gherkin: waived: the guard is the scenario: it scripts the control plane, interrupts at RunMicrovm and asserts the exit code, the terminate call, the envelope and the ledger
- fuzz: waived: there is no input stream; the window that matters is the one between the launch and RUNNING
- test:
crates/microvms-app/src/sandbox.rs,crates/microvms-cli/src/envelope.rs,crates/microvms-cli/src/guards/closed_output.rs,crates/microvms-cli/src/guards/interrupt.rs,crates/microvms-cli/src/ledger.rs - impl:
crates/microvms-app/src/sandbox.rs,crates/microvms-cli/src/commands/agent.rs,crates/microvms-cli/src/commands/attached.rs,crates/microvms-cli/src/commands/lifecycle.rs,crates/microvms-cli/src/exit.rs,crates/microvms-cli/src/main.rs - live: waived: an interrupt has to land between a billable launch and RUNNING, which a live run can’t place deterministically; the guard places it at RunMicrovm
If a reader closes the CLI’s stdout or stderr, then the CLI crate shall exit with a status from its exit table and neither panic nor terminate by signal.
- model:
crates/model/src/output.rs - gherkin:
crates/microvms-cli/tests/features/closed_output.feature - fuzz:
crates/microvms-cli/src/closed_output_fuzz.rs - test:
crates/microvms-cli/src/closed_output.rs,crates/microvms-cli/src/closed_output_fuzz.rs,crates/microvms-cli/tests/thinness.rs - impl:
crates/microvms-app/src/lib.rs,crates/microvms-cli/src/closed_output.rs,crates/microvms-cli/src/envelope.rs,crates/microvms-cli/src/main.rs,crates/microvms-core/src/lib.rs,crates/microvms-domain/src/lib.rs,crates/microvms-edges/src/adapters.rs,crates/microvms-edges/src/lib.rs - live:
conformance/lanes/closed_output.py
If the reader of stdout or stderr closes after a command has started, then the CLI crate shall perform every teardown and ledger write that command owes and exit with the code of the command’s own outcome, except for a streaming command whose stdout reader closes.
- model:
crates/model/src/output.rs - gherkin:
crates/microvms-cli/tests/features/closed_output.feature - fuzz:
crates/microvms-cli/src/closed_output_fuzz.rs - test:
crates/microvms-cli/src/closed_output_fuzz.rs,crates/microvms-cli/src/guards/closed_output.rs - impl:
crates/microvms-cli/src/closed_output.rs,crates/microvms-cli/src/envelope.rs,crates/microvms-cli/src/main.rs - live:
conformance/lanes/closed_output.py,conformance/selftest/closed_output.py
If the stdout reader of a streaming command closes, then the CLI crate shall stop streaming within one further event, leave the remote exec running, and exit with ERR_INTERRUPTED naming the exec id on stderr.
- model:
crates/model/src/output.rs - gherkin:
crates/microvms-cli/tests/features/closed_output.feature - fuzz:
crates/microvms-cli/src/closed_output_fuzz.rs - test:
crates/microvms-cli/src/closed_output_fuzz.rs,crates/microvms-cli/src/guards/closed_output.rs - impl:
crates/microvms-cli/src/closed_output.rs,crates/microvms-cli/src/commands/attached.rs,crates/microvms-cli/src/envelope.rs - live:
conformance/lanes/closed_output.py
COST-1
Section titled “COST-1”The cost engine shall carry a provenance label of measured or projected on each duration, with no unlabelled constructor.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: a duration has no unlabelled constructor, and the tests build each label
- fuzz: waived: the input is a choice of two labels and a number, which the tests enumerate at the boundaries
- test:
crates/microvms-domain/src/cost.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs,crates/microvms-domain/src/cost.rs - live:
conformance/lanes/lifecycle.py
COST-2
Section titled “COST-2”The cost engine shall not expose an implicit coercion from an estimated dollar amount to a bare float.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: a property of the types’ constructors and trait impls, which the compiler holds and a doctest shows failing to compile
- fuzz: waived: there is no input stream; the rule is over the type’s impls
- test:
bindings/microvms-py/tests/test_smoke.py,crates/microvms-domain/src/cost.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs,crates/microvms-domain/src/cost.rs - live: waived: a coercion that doesn’t compile can’t show up at runtime; the live suite reads dollar figures only as strings
COST-3
Section titled “COST-3”The cost engine shall represent an unpriced quantity as a distinct Unpriced variant carrying the reason, rather than as zero dollars.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: the tests build every unpriced line and assert it carries its reason and no figure
- fuzz: waived: the unpriced lines are a fixed set the tests enumerate, and the COST-4 property test mixes them with priced ones
- test:
crates/microvms-domain/src/cost.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs,crates/microvms-domain/src/cost.rs - live:
conformance/lanes/lifecycle.py
COST-4
Section titled “COST-4”If an Unpriced amount is summed with an estimated amount, then the cost engine shall produce a lower-bound total that names its unpriced line items rather than a plain sum.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: the proptest over every mix of priced and unpriced lines is the specification
- fuzz: waived: the proptest
a_total_is_a_lower_bound_exactly_when_something_is_unpricedsearches that space; a coverage-guided harness would search the same one - test:
bindings/microvms-py/tests/test_cost.py,bindings/microvms-py/tests/test_smoke.py,crates/microvms-domain/src/cost.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs,crates/microvms-cli/src/cli.rs,crates/microvms-cli/src/commands/cost.rs,crates/microvms-domain/src/cost.rs - live:
conformance/lanes/lifecycle.py
COST-5
Section titled “COST-5”The cost engine shall compute each compute line item from the size class baseline rather than from the peak the guest reports.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: the tests price every size class from its baseline and compare with the peak
- fuzz: waived: the size classes are a closed table the tests walk row by row
- test:
bindings/microvms-py/tests/test_cost.py,bindings/microvms-py/tests/test_smoke.py,crates/microvms-domain/src/cost.rs - impl:
crates/microvms-domain/src/cost.rs,crates/microvms-domain/src/sizing.rs - live: waived: a pure function of the usage and the pinned rate table; it makes no AWS call, and the unit tests cover it
COST-6
Section titled “COST-6”The cost engine shall perform money arithmetic in decimal representation, converting each float exactly once at the boundary.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: the float boundaries are two functions the tests call directly
- fuzz: waived: the proptest
compute_figures_are_exactly_the_decimal_referencedrives the whole arithmetic over generated quantities and checks every figure exactly - test:
crates/microvms-domain/src/cost.rs - impl:
crates/microvms-domain/src/cost.rs - live: waived: a pure function of the usage and the pinned rate table; it makes no AWS call, and the unit tests cover it
COST-7
Section titled “COST-7”While the pinned rate table is older than the staleness window, the cost engine shall attach a staleness warning to each report computed from the stale table.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: staleness is a date comparison the tests make on each side of the window
- fuzz: waived: the proptest
staleness_is_the_ninety_day_verdict_and_carries_the_agecovers every age; the window is one threshold - test:
crates/microvms-domain/src/cost.rs - impl:
crates/microvms-domain/src/cost.rs - live: waived: the pinned table’s age is today minus a committed date, which a live run can’t move; the tests pass
todayin
COST-8
Section titled “COST-8”The cost engine shall apply the one-week minimum retention floor to each snapshot storage line item.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: the tests price snapshot storage below, at and above the one-week floor
- fuzz: waived: the proptest
storage_bills_the_greater_of_the_hold_and_the_retention_floorcovers every hold; the floor is one threshold - test:
crates/microvms-domain/src/cost.rs - impl:
crates/microvms-domain/src/cost.rs - live: waived: a pure function of the usage and the pinned rate table; it makes no AWS call, and the unit tests cover it
COST-9
Section titled “COST-9”The cost engine shall price compute from the ARM rate only, rejecting a catalog whose ARM line is missing rather than substituting the x86 rate.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: the tests parse catalogs with and without the ARM line and assert the refusal
- fuzz: waived: a catalog is a fixed set of named lines, and the tests drop each one the parser needs
- test:
bindings/microvms-py/tests/test_cost.py,bindings/microvms-py/tests/test_smoke.py,crates/microvms-domain/src/cost.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs,crates/microvms-domain/src/constants.rs,crates/microvms-domain/src/cost.rs - live: waived: the rate table is pinned and parsed offline; the Pricing API is never called at runtime
COST-10
Section titled “COST-10”The cost engine shall mark each duration in a plan estimate as projected, so that the resulting report is distinguishable from a measured report.
- model: waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
- gherkin: waived: no behavior to script: the tests build a plan and assert every duration on its report is projected
- fuzz: waived: the proptest
every_duration_in_a_plan_is_projectedgenerates the plans; a coverage-guided harness would search the same space - test:
bindings/microvms-py/tests/test_cost.py,bindings/microvms-py/tests/test_smoke.py,crates/microvms-cli/src/commands/cost.rs,crates/microvms-domain/src/cost.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-py/src/cost.rs,crates/microvms-domain/src/cost.rs - live:
conformance/lanes/local.py
IMAGE-1
Section titled “IMAGE-1”The microvms-core shall emit the agentd stanza of a wrapped task Dockerfile and of the default Dockerfile from one source.
- model:
crates/model/src/wrap.rs - gherkin:
crates/microvms-core/tests/features/wrap_task_image.feature - fuzz:
crates/microvms-core/tests/wrap_fuzz.rs - test:
crates/microvms-app/src/control/artifact.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/control/artifact.rs - live: waived: a pure function of Dockerfile text; it makes no AWS call
IMAGE-2
Section titled “IMAGE-2”When a caller wraps a task Dockerfile, the microvms-core shall end the result with the agentd stanza carrying the client’s AGENTD_PORT, preceded by USER root when the task sets another user.
- model:
crates/model/src/wrap.rs - gherkin:
crates/microvms-core/tests/features/wrap_task_image.feature - fuzz:
crates/microvms-core/tests/wrap_fuzz.rs - test:
crates/microvms-app/src/control/artifact.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/control/artifact.rs,crates/microvms-cli/src/commands/local.rs - live:
conformance/lanes/ensure_image.py,conformance/lanes/wrapped_user.py
IMAGE-3
Section titled “IMAGE-3”If a task Dockerfile has no FROM, ends inside an unfinished instruction, or sets a keepalive not under the stream idle timeout, or the wrap options name an invalid port or workdir or ask to inherit a workdir that nothing declares, then the microvms-core shall refuse to wrap the task Dockerfile with an invalid-argument error naming the cause.
- model:
crates/model/src/wrap.rs - gherkin:
crates/microvms-core/tests/features/wrap_task_image.feature - fuzz:
crates/microvms-core/tests/wrap_fuzz.rs - test:
crates/microvms-app/src/control/artifact.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/control/artifact.rs,crates/microvms-cli/src/commands/local.rs - live: waived: a pure function of Dockerfile text; it makes no AWS call
IMAGE-4
Section titled “IMAGE-4”When a caller derives a base image from a Dockerfile, the microvms-core shall take the docker_ref from the first FROM, keep the managed base image name, and refuse a Dockerfile with no FROM.
- model:
crates/model/src/wrap.rs - gherkin:
crates/microvms-core/tests/features/wrap_task_image.feature - fuzz:
crates/microvms-core/tests/wrap_fuzz.rs - test:
crates/microvms-app/src/control/artifact.rs - impl:
crates/microvms-app/src/control/artifact.rs,crates/microvms-cli/src/commands/local.rs - live:
conformance/lanes/ensure_image.py
IMAGE-5
Section titled “IMAGE-5”The language bindings layer shall expose wrap_dockerfile and the from-Dockerfile base image as thin wrappers that raise the refusals of microvms-core as invalid-argument errors.
- model: waived: a binding pass-through has no states; core’s are modeled as IMAGE-1..4
- gherkin: waived: the scenarios are core’s (IMAGE-1..4); each binding’s tests check the pass-through
- fuzz: waived: the binding hands the text unchanged to core’s fuzzed function
- test:
bindings/microvms-js/__test__/wrap.mjs,bindings/microvms-py/tests/test_wrap_dockerfile.py - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs - live: waived: a pure function of Dockerfile text; it makes no AWS call
IMAGE-6
Section titled “IMAGE-6”The microvms-core shall name an ensured image by its prefix and twelve hex characters of a hash over the daemon bytes, the Dockerfile, the build context entries, the base image, and the size class, keeping the artifact content hash of a request without a build context unchanged.
- model: waived: a pure function of the build inputs; the name has no states to explore
- gherkin:
crates/microvms-core/tests/features/ensure_image.feature - fuzz:
crates/microvms-core/tests/context_fuzz.rs - test:
crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/ensure.rs - impl:
crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/ensure.rs - live:
conformance/lanes/ensure_image.py
IMAGE-7
Section titled “IMAGE-7”When a caller supplies a build context directory, the microvms-core shall add each regular file that Dockerfile.dockerignore, or else .dockerignore, does not exclude to an artifact zip with fixed entry dates and modes, skipping each symlink with a warning.
- model: waived: reading a directory has no states; the ignore rules are fuzzed against moby’s own regex translation instead
- gherkin:
crates/microvms-core/tests/features/ensure_image.feature - fuzz:
crates/microvms-core/tests/context_fuzz.rs - test:
crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/context.rs,crates/microvms-edges/src/control/context.rs - impl:
crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/context.rs,crates/microvms-app/src/control/ensure.rs,crates/microvms-core/src/lib.rs,crates/microvms-edges/src/control/context.rs - live:
conformance/lanes/ensure_image.py
IMAGE-8
Section titled “IMAGE-8”When the microvms-core ensures an image, the microvms-core shall resolve the image ARN from one caller-identity call per sandbox and upload the artifact to the content-addressed key under the caller’s bucket and key prefix.
- model:
crates/model/src/image.rs - gherkin:
crates/microvms-core/tests/features/ensure_image.feature - fuzz:
crates/microvms-core/tests/context_fuzz.rs - test:
crates/microvms-app/src/control/ensure.rs,crates/microvms-edges/src/control/services.rs - impl:
crates/microvms-app/src/control/ensure.rs,crates/microvms-app/src/control/services.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-edges/src/control/services.rs - live:
conformance/lanes/ensure_image.py
IMAGE-9
Section titled “IMAGE-9”When a describe finds the ensured image ready or building and the caller has not forced a rebuild, the microvms-core shall return the image once it is ready, marked reused, with no upload and no create.
- model:
crates/model/src/image.rs - gherkin:
crates/microvms-core/tests/features/ensure_image.feature - fuzz: waived: the input space is two callers interleaved against the platform, which crates/model/src/image.rs checks exhaustively; the decision table is ten rows, all pinned by the_plan_table
- test:
crates/microvms-app/src/control/ensure.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/control/ensure.rs - live:
conformance/lanes/ensure_image.py
IMAGE-10
Section titled “IMAGE-10”If the ensured image has failed or the caller forces a rebuild, then the microvms-core shall delete the image and wait for the name to be free before building, deleting a ready image only under a forced rebuild.
- model:
crates/model/src/image.rs - gherkin:
crates/microvms-core/tests/features/ensure_image.feature - fuzz: waived: the input space is two callers interleaved against the platform, which crates/model/src/image.rs checks exhaustively; the decision table is ten rows, all pinned by the_plan_table
- test:
crates/microvms-app/src/control/ensure.rs,crates/model-conformance/tests/tables.rs - impl:
crates/microvms-app/src/control/ensure.rs - live:
conformance/lanes/ensure_image.py
IMAGE-11
Section titled “IMAGE-11”If the create of an ensured image is refused because another caller created the name, then the microvms-core shall describe the image again and wait for that build, returning only a ready image, marked reused.
- model:
crates/model/src/image.rs - gherkin:
crates/microvms-core/tests/features/ensure_image.feature - fuzz: waived: the input space is two callers interleaved against the platform, which crates/model/src/image.rs checks exhaustively; the decision table is ten rows, all pinned by the_plan_table
- test:
crates/microvms-app/src/control/ensure.rs - impl:
crates/microvms-app/src/control/ensure.rs - live:
conformance/lanes/ensure_image.py
IMAGE-12
Section titled “IMAGE-12”The language bindings layer shall expose ensure_image as a thin wrapper that returns the image with the reused flag and the context warnings of microvms-core.
- model: waived: a binding pass-through has no states; core’s are modeled as IMAGE-8..11
- gherkin: waived: the scenarios are core’s (IMAGE-6..11); each binding’s tests check the pass-through
- fuzz: waived: the binding hands its arguments unchanged to core’s fuzzed functions
- test:
bindings/microvms-js/__test__/ensure.mjs,bindings/microvms-py/tests/test_ensure_image.py - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs - live: waived: the conformance section drives core’s ensure_image, which each binding forwards unchanged
STATE-1
Section titled “STATE-1”When a launch request is accepted, the microvms-core shall transition the lifecycle to PENDING and record the image as existing.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/sandbox.rs - live: waived: PENDING between an accepted launch and the hook’s report is the client’s own record, which a live run sees only as
runreturning; the replay checks it after every call
STATE-2
Section titled “STATE-2”When the platform reports that the run hook answered with a success status, the microvms-core shall mark the lifecycle RUNNING and the agent token installed.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-cli/src/commands/lifecycle.rs - live: waived: a live run sees the hook’s report only as
runreturning with a daemon that answers (AGENTD-2’s live check); the client’s RUNNING-and-installed record is checked by the replay after every call
STATE-3
Section titled “STATE-3”The microvms-core shall install the agent token at most once per VM lifetime.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/sandbox.rs - live: waived: the client offers one launch per
Sandbox; a second install is the daemon’s refusal, which AGENTD-3’s live check asserts
STATE-4
Section titled “STATE-4”While the lifecycle is RUNNING, the microvms-core shall accept a suspend request and transition the lifecycle to SUSPENDING.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
crates/microvms-app/src/sandbox.rs - live: waived: SUSPENDING is the client’s record while the platform suspends, and
suspendreturns only once it reads SUSPENDED (STATE-6’s live check); the replay checks the transition after every call
STATE-5
Section titled “STATE-5”The microvms-core shall not issue a suspend call while the lifecycle is not RUNNING.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/control.rs,bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/control.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-cli/src/commands/lifecycle.rs - live: waived: a refusal before any call never reaches the service; the model and its replay against
Sandboxhold it, and the app’s tests drive it
STATE-6
Section titled “STATE-6”When the platform reports suspension complete, the microvms-core shall mark the lifecycle SUSPENDED.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
crates/microvms-app/src/sandbox.rs - live:
conformance/lanes/suspend.py
STATE-7
Section titled “STATE-7”While the lifecycle is SUSPENDED, the microvms-core shall accept a resume request, reuse the installed agent token, and transition the lifecycle to RUNNING without re-delivering a run-hook payload.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/control.rs,bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/control.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/sandbox.rs - live:
conformance/lanes/suspend.py
STATE-8
Section titled “STATE-8”When a resume completes, the microvms-core shall invalidate the cached proxy token.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
bindings/microvms-py/tests/test_session.py,crates/microvms-app/src/sandbox.rs,crates/microvms-app/src/session/mod.rs,crates/microvms-app/src/session/proxy.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/session.rs,bindings/microvms-py/src/session.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-app/src/session/mod.rs,crates/microvms-app/src/session/proxy.rs - live: waived: the proxy token cache is client state no live response shows; the replay checks it after every call, and the app’s tests check the next request mints
STATE-9
Section titled “STATE-9”When a terminate request is accepted, the microvms-core shall transition the lifecycle to TERMINATING and record the VM as terminated.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
crates/microvms-app/src/sandbox.rs - live: waived: TERMINATING is the client’s record while the platform terminates, and the live terminate checks read TERMINATED (STATE-10’s); the replay checks the transition after every call
STATE-10
Section titled “STATE-10”When the platform reports termination complete, the microvms-core shall mark the lifecycle TERMINATED.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
crates/microvms-app/src/sandbox.rs - live:
conformance/lanes/sessions.py
STATE-11
Section titled “STATE-11”The microvms-core shall not return a terminated VM to RUNNING.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/sandbox.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/sandbox.rs - live: waived: a refusal before any call never reaches the service; the model and its replay against
Sandboxhold it, and the app’s tests drive it
STATE-12
Section titled “STATE-12”If a resume is requested for a suspended MicroVM that the service terminated while it was suspended, then the microvms-core shall issue the resume to the service and report its refusal as a window-closed error naming the state and stateReason that GetMicrovm reports.
- model:
crates/model/src/client.rs - gherkin: waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance’s replay drives each path against
Sandbox; a scenario would restate one of those paths - fuzz: waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
- test:
crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-cli/src/guards/history.rs,crates/model-conformance/tests/client_lifecycle.rs - impl:
bindings/microvms-js/src/control.rs,bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/control.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/sandbox.rs - live:
conformance/lanes/state12.py,conformance/selftest/state12.py
TRAP-1
Section titled “TRAP-1”The microvms-core shall derive each image create token from a value unique per build attempt, with no caller-supplied token override.
- model: waived: a fresh value per build attempt, drawn from the entropy port, not a state
- gherkin: waived: no scenario can show a token is unique: the tests draw two hundred and find no repeat, and recreating one name sends two distinct tokens
- fuzz: waived: the token has no caller input to fuzz: there’s no override to feed
- test:
bindings/microvms-py/tests/test_smoke.py,crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/image.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/token.rs,crates/microvms-cli/src/cli.rs,crates/microvms-core/src/lib.rs,crates/microvms-core/src/prelude.rs,crates/microvms-edges/src/entropy.rs - impl:
bindings/microvms-js/src/lib.rs,bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/control/fake.rs,crates/microvms-app/src/control/image.rs,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/control/token.rs,crates/microvms-app/src/control/transport.rs,crates/microvms-app/src/entropy.rs,crates/microvms-app/src/ledger.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-app/src/testing.rs,crates/microvms-cli/src/cli.rs,crates/microvms-cli/src/commands/lifecycle.rs,crates/microvms-core/src/lib.rs,crates/microvms-core/src/prelude.rs,crates/microvms-domain/src/constants.rs - live: waived: a replayed token wedges an image in CREATING for about fifteen hours (docs/PLATFORM.md), so a live run can’t show the failure it closes; every live build sends a fresh one
TRAP-2
Section titled “TRAP-2”If an image build remains in CREATING past the stall grace period with every build still PENDING, then the microvms-core shall reject the build wait with an error naming the client-token replay signature.
- model: waived: one wait’s verdict over a sequence of describe answers, which the tests script
- gherkin: waived: the stall is a timed sequence of describe answers, which the tests script against a fake clock; a scenario would restate them
- fuzz: waived: the verdict turns on elapsed time and the builds’ statuses, which the tests enumerate
- test:
crates/microvms-app/src/control/image.rs - impl:
crates/microvms-app/src/clock.rs,crates/microvms-app/src/control/image.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-domain/src/constants.rs - live: waived: a stall needs a replayed token’s wedged image, about fifteen hours in CREATING (docs/PLATFORM.md)
TRAP-3
Section titled “TRAP-3”Where guest identity repair is requested, the microvms-core shall set the additional OS capabilities field to the single enum value the pinned service model accepts, via a typed intent flag rather than a free-form capability list.
- model: waived: a bool mapped to the one enum value the model accepts, not a state
- gherkin: waived: no behavior to script: a typed flag and the request it writes, which the tests assert
- fuzz: waived: the input is one bool; there is no input space
- test:
crates/microvms-app/src/control/image.rs - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/control/image.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-cli/src/cli.rs,crates/microvms-domain/src/constants.rs - live:
conformance/lanes/lifecycle.py
TRAP-4
Section titled “TRAP-4”The microvms-core shall derive each platform network connector value as a fully-qualified connector ARN for the request region from an enumerated ingress or egress intent, and accept a caller-supplied connector ARN only as a customer-managed egress connector in the request region when the platform egress intent is absent.
- model: waived: a derivation from a closed enum and a shape check on caller ARNs, not a state
- gherkin:
crates/microvms-core/tests/features/egress_posture.feature - fuzz:
crates/microvms-app/src/control/posture_fuzz.rs - test:
crates/microvms-app/src/control/connector.rs,crates/microvms-app/src/control/microvm.rs - impl:
crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-cli/src/cli.rs - live: waived: every live launch sends connectors derived this way, but no named check reads them back; the offline tests assert the recorded requests
TRAP-5
Section titled “TRAP-5”If a run-hook payload exceeds the ceiling of 4096 bytes that the service model declares, then the microvms-core shall reject the launch locally before any control-plane call, naming the service-model ceiling.
- model: waived: a length check against one constant, not a state
- gherkin: waived: no behavior to script: the tests cover both sides of the 4096-byte boundary
- fuzz: waived: a length against one ceiling, which the boundary tests cover on both sides
- test:
crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/microvm.rs - impl:
crates/microvms-app/src/control/artifact.rs,crates/microvms-app/src/control/context.rs,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/sandbox.rs - live: waived: refused before the first control-plane call, so the service never sees it
TRAP-6
Section titled “TRAP-6”If the control-plane call in the requested region fails with the null-message AccessDeniedException and the requested region is outside the measured MicroVMs regions, then the microvms-core shall report the error naming the region’s service availability and the access policy, the two causes to verify.
- model: waived: one branch on a membership test in an error’s text, not a state
- gherkin:
crates/microvms-core/tests/features/request_and_preflight.feature - fuzz: waived: the classifier’s inputs are a status, an empty message and a region, which the tests enumerate on both sides of the membership test
- test:
bindings/microvms-py/tests/test_smoke.py,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/control/transport.rs - impl:
bindings/microvms-js/src/lib.rs,bindings/microvms-js/src/region.rs,bindings/microvms-py/src/lib.rs,bindings/microvms-py/src/region.rs,crates/microvms-app/src/control/image.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/control/transport.rs,crates/microvms-app/src/preflight.rs,crates/microvms-core/src/lib.rs,crates/microvms-core/src/prelude.rs,crates/microvms-domain/src/region.rs - live: waived: the live suite runs in a region AWS was measured running MicroVMs in, so its calls can’t produce the response; docs/PLATFORM.md records the response in us-west-1
TRAP-7
Section titled “TRAP-7”The microvms-core shall read the minted proxy token from the auth-token header map and send the proxy auth header and the proxy port header on each endpoint request.
- model: waived: a header read and two headers sent on each request, not a state
- gherkin: waived: no behavior to script: the tests assert the headers on the recorded endpoint requests
- fuzz: waived: the headers carry a minted token and a port, with no caller input to fuzz
- test:
bindings/microvms-py/tests/test_session.py,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/session/mod.rs,crates/microvms-app/src/session/proxy.rs - impl:
bindings/microvms-js/src/session.rs,bindings/microvms-py/src/session.rs,crates/microvms-app/src/control/fake.rs,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/session/mod.rs,crates/microvms-app/src/session/proxy.rs - live:
conformance/lanes/lifecycle.py
TRAP-8
Section titled “TRAP-8”If a MicroVM reaches a terminal state before RUNNING, then the microvms-core shall reject the launch with the state and stateReason attached.
- model: waived: the rule is what a refusal carries, the state and its reason, which the tests assert on scripted terminal states
- gherkin: waived: the tests drive every terminal state before RUNNING against a scripted control plane; a scenario per state would restate them
- fuzz: waived: the input is a closed set of terminal states, which the tests enumerate
- test:
crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/sandbox.rs - impl:
bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/sandbox.rs,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-domain/src/constants.rs - live: waived: a VM can’t be made to reach a terminal state before RUNNING on demand against the live service
TRAP-9
Section titled “TRAP-9”The microvms-core shall mint the endpoint proxy token inside the request retry path at an interval strictly below the sixty-minute service ceiling.
- model: waived: an interval against a ceiling on the clock port, not a state
- gherkin: waived: the refresh is asserted against a fake clock in the tests; a scenario would restate them
- fuzz: waived: the interval is a constant against a sixty-minute ceiling, with no input space
- test:
bindings/microvms-py/tests/test_session.py,crates/microvms-app/src/session/exec.rs,crates/microvms-app/src/session/mod.rs,crates/microvms-app/src/session/proxy.rs,crates/microvms-core/tests/turmoil_client.rs - impl:
bindings/microvms-js/src/session.rs,bindings/microvms-py/src/session.rs,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-app/src/sandbox.rs,crates/microvms-app/src/session/mod.rs,crates/microvms-app/src/session/proxy.rs,crates/microvms-cli/src/commands/attached.rs,crates/microvms-cli/src/seam.rs,crates/microvms-edges/src/session/forward.rs - live: waived: the ceiling is sixty minutes, so a live check would hold a billable session past it to see one re-mint; the tests expire the token on a fake clock instead
TRAP-10
Section titled “TRAP-10”If a requested minimumMemoryInMiB is not one of the five documented size-class baselines, then the microvms-core shall reject the request locally rather than forwarding an off-table value.
- model: waived: a membership check over the five documented baselines, not a state
- gherkin: waived: no behavior to script: the tests accept each of the five baselines and refuse the values beside them
- fuzz: waived: the baselines are a closed table the tests enumerate, with nothing between rows to search
- test:
bindings/microvms-py/tests/test_cost.py,bindings/microvms-py/tests/test_smoke.py,crates/microvms-cli/src/cli.rs,crates/microvms-domain/src/cost.rs,crates/microvms-domain/src/sizing.rs - impl:
bindings/microvms-js/src/cost.rs,bindings/microvms-js/src/sandbox.rs,bindings/microvms-py/src/cost.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-cli/src/cli.rs,crates/microvms-domain/src/sizing.rs - live: waived: refused before the first control-plane call, so the service never sees it
TRAP-11
Section titled “TRAP-11”The microvms-core shall not request a SHELL_INGRESS connector unless the launch asks for shell access, nor call CreateMicrovmShellAuthToken except to open an interactive shell session.
- model: waived: a rule over which operations a lifecycle calls, not over its states
- gherkin: waived: no behavior to script: the full-lifecycle test counts every operation and connector a lifecycle sends
- fuzz: waived: there is no input stream; the rule is over the calls a lifecycle makes
- test:
crates/microvms-app/src/control/connector.rs,crates/microvms-app/src/control/microvm.rs - impl:
crates/microvms-app/src/control/connector.rs,crates/microvms-app/src/control/fake.rs,crates/microvms-app/src/control/microvm.rs,crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/transport.rs,crates/microvms-edges/src/session/shell.rs - live: waived: a live run can’t see an operation the client didn’t call; the recorded lifecycle can, and counts none
TRAP-12
Section titled “TRAP-12”The microvms-core shall verify each hardcoded service constraint against the pinned botocore service model in the build gate.
- model: waived: a comparison of constants with the pinned service model, not a state
- gherkin: waived: no behavior to script: the gate compares two JSON documents
- fuzz: waived: the inputs are the pinned model and the emitted constants, both fixed
- test:
crates/microvms-domain/src/constants.rs - impl:
crates/microvms-app/src/control/mod.rs,crates/microvms-app/src/control/ops.rs,crates/microvms-cli/src/cli.rs,crates/microvms-cli/src/commands/local.rs,crates/microvms-domain/src/constants.rs,crates/microvms-domain/src/hooks.rs - live: waived: the gate reads the pinned model offline and makes no AWS call
TRAP-13
Section titled “TRAP-13”The sizing model shall read baseline and peak from the documented five-row table rather than computing the peak as four times the baseline.
- model: waived: a table lookup, not a state
- gherkin: waived: no behavior to script: the tests read each of the five rows
- fuzz: waived: the table has five rows, which the tests read exhaustively
- test:
crates/microvms-domain/src/sizing.rs - impl:
crates/microvms-core/src/lib.rs,crates/microvms-domain/src/cost.rs,crates/microvms-domain/src/sizing.rs - live:
conformance/lanes/local.py
Threats
Section titled “Threats”The threat table in docs/TRUST.md, each key marked when this matrix doesn’t
trace it.
| Threat | Requirement | Guard | Status |
|---|---|---|---|
| An in-VM process races the platform to the bootstrap hook | AGENTD-1, AGENTD-3 | crates/agentd/tests/model_conformance.rs::slice_0_of_the_walk_replays_against_the_daemon, crates/agentd/src/state.rs::identical_replay_succeeds_and_a_different_token_conflicts |
guarded; a process that starts before the daemon still wins, which is the unenforced invariant below |
| An ordinary exec inherits image privileges its workload does not need | AGENTD-26 | crates/agentd/src/exec_capabilities.rs::reduction_clears_i_a_and_only_the_seven_bounding_bits |
guarded when the image enables AGENTD_DROP_EXEC_CAPABILITIES. It defaults off, and root workloads remain in the daemon’s trust boundary |
| A caller holding the agent token but not the host key opens a verified tunnel | AGENTD-17 | crates/agentd/src/tunnel_identity.rs::only_the_pinned_host_key_completes_a_handshake, crates/agentd/tests/tunnel_relay.rs::a_valid_token_with_the_wrong_host_key_is_refused, crates/model/src/tunnel.rs::agentd_17_a_token_holder_without_the_host_key_is_refused_before_any_dial |
guarded; under KK no one-sided change turns the pin off, so its seeded fault turns it off in the tunnel model |
| A verified tunnel’s handshake fails, or the VM has no key, and the guest service is reached anyway | AGENTD-18 | crates/agentd/tests/tunnel_relay.rs::a_refused_caller_never_causes_a_guest_connection, crates/agentd/tests/tunnel_relay.rs::identity_against_a_seedless_vm_is_refused_not_downgraded, crates/model-conformance/tests/tunnel_confirmation.rs::a_handshake_without_confirmation_leaves_the_guest_listener_idle, crates/model-conformance/tests/tunnel_end_of_stream.rs::a_verified_tunnel_requires_the_requested_guest_port |
guarded |
| A guest answers a verified tunnel’s handshake with a key other than the pinned VM key | BIND-21 | crates/microvms-core/tests/tunnel_end_to_end.rs::a_wrong_pin_fails_closed_with_a_diagnosis, crates/microvms-core/tests/tunnel_end_to_end.rs::a_reply_that_does_not_verify_against_the_pin_fails_the_tunnel |
guarded |
| A guest or the path replays, reorders or forges tunnel frames after the handshake | AGENTD-21, BIND-24 | crates/agentd/tests/tunnel_relay.rs::agentd_21_a_replayed_frame_ends_the_tunnel_unrelayed, crates/agentd/tests/tunnel_relay.rs::agentd_21_a_forged_frame_ends_the_tunnel_unrelayed, crates/microvms-edges/tests/tunnel_end_of_stream.rs::bind_24_a_replayed_frame_fails_the_tunnel_unwritten, crates/microvms-edges/tests/tunnel_end_of_stream.rs::bind_24_a_forged_frame_fails_the_tunnel_unwritten, crates/model/src/tunnel.rs::bind_24_the_model_finds_a_replay_when_frames_carry_no_position, crates/agentd/src/tunnel_fuzz.rs::frames_open_in_order_and_the_callers_end_only_after_every_chunk, crates/microvms-edges/src/session/tunnel_fuzz.rs::frames_open_in_order_and_the_daemons_end_only_after_every_chunk |
guarded |
| A guest streams hostile server-sent events to the client | BIND-22 | crates/microvms-app/src/session/sse.rs::an_unterminated_stream_is_refused_at_the_pending_ceiling, crates/microvms-app/src/session/sse.rs::an_unrecognized_or_unparseable_frame_is_dropped_rather_than_raised, crates/microvms-app/src/session/sse_fuzz.rs::hostile_stream_bytes_stay_bounded_and_every_event_round_trips |
guarded |
A workload whose caller omits user runs as guest root |
AGENTD-22, AGENTD-24 | crates/agentd/src/exec.rs::a_start_that_names_no_user_runs_as_the_default_resolved_per_request, crates/agentd/src/exec.rs::a_numeric_default_runs_as_its_row_and_one_with_no_row_is_refused, crates/agentd/src/exec_start.rs::a_default_that_names_nobody_is_refused_naming_the_variable, crates/model/src/exec_start.rs::an_unknown_default_falling_back_to_the_daemon_starts_as_root, crates/model/src/exec_start.rs::a_default_read_as_a_request_string_keeps_the_daemons_group, crates/agentd/src/exec_start.rs::captured_numeric_identity_preserves_the_primary_gid_and_explicit_precedence |
guarded when the image sets a non-root AGENTD_DEFAULT_USER or preserves a non-root Dockerfile user. An authorized caller can still ask for root |
| A replaced or tampered daemon release asset | BIND-18 | crates/microvms-edges/src/provision/release.rs::another_signer_identity_is_refused, crates/microvms-edges/src/provision/release.rs::one_flipped_byte_in_the_asset_is_refused |
guarded |
A release directory ($MICROVM_RELEASE_DIR) holding an asset and a matching SHA256SUMS but no bundle, or another release’s files under the requested tag |
BIND-18 | crates/microvms-edges/src/provision/release.rs::a_release_directory_without_its_bundle_is_refused_despite_a_matching_checksum, crates/microvms-edges/src/provision/release.rs::another_releases_files_under_the_requested_tag_are_refused |
guarded |
| An on-path party ends a verified tunnel early, with a plaintext close frame or by dropping the connection | BIND-23, AGENTD-19, AGENTD-20 | crates/microvms-edges/tests/tunnel_end_of_stream.rs::a_verified_tcp_consumer_observes_the_stream_verdict, crates/model-conformance/tests/tunnel_end_of_stream.rs::bind_23_a_close_frame_forged_mid_stream_ends_truncated, crates/model-conformance/tests/tunnel_end_of_stream.rs::bind_23_a_connection_dropped_mid_stream_ends_truncated, crates/model-conformance/tests/tunnel_end_of_stream.rs::bind_23_the_daemons_end_of_stream_withheld_ends_truncated, crates/model-conformance/tests/tunnel_end_of_stream.rs::agentd_20_the_clients_end_of_stream_withheld_resets_the_guest, crates/agentd/tests/tunnel_relay.rs::agentd_19_a_guest_eof_reaches_the_caller_as_the_end_of_stream |
guarded. A protocol 2 peer that omits the end-of-stream offer ends ClosedUnproven. Each side refuses a protocol 1 handshake |