Specification · raw markdown
Ampoule run predicate, v1
Legacy: v1 is superseded by v2. New receipts use v2.
Predicate type: https://ampoule.dev/attestation/run/v1
The URI is permanent: every signed receipt carries it. A breaking change to
the fields gets a new version (/v2), never an edit to this one.
An in-toto Statement v1 with this predicate records one execution of untrusted code inside a sealed Ampoule micro-VM: which kernel ran it, what went in, what came out, and how much work it took. It is carried in a DSSE envelope signed with Ed25519.
Statement
{
"_type": "https://in-toto.io/Statement/v1",
"subject": [{ "name": "output", "digest": { "sha256": "<output_sha256>" } }],
"predicateType": "https://ampoule.dev/attestation/run/v1",
"predicate": {
"version": 1,
"kernel_sha256": "e028af09…",
"vmm": "firecracker",
"runtime": "js",
"flags": 260,
"deterministic": true,
"seed": 7,
"payload_sha256": "bf75c921…",
"output_sha256": "12cece5a…",
"fuel": 14354058,
"status": 0
}
}
The subject is the output, the artifact the run produced. Its digest must
equal predicate.output_sha256; verifiers reject a statement where they differ.
Predicate fields
| field | meaning |
|---|---|
version |
Receipt format version, 1. |
kernel_sha256 |
SHA-256 of the kernel ELF the VM booted. The language runtimes (QuickJS, CPython) are embedded in the kernel, so this pins them too. |
vmm |
qemu or firecracker. Informational: deterministic runs are designed to give the same output and fuel on both. |
runtime |
rhai, wasm, js or python. |
flags |
Request flags as sent in the mailbox (runtime bit, 0x100 = deterministic). |
deterministic |
Clock and randomness derived from seed, limits fuel-only. Only these runs can be re-executed to the same result. |
seed |
The seed used for clock and randomness. |
payload_sha256 |
SHA-256 of the exact request bytes: the source for rhai/js/python; for wasm, u32le module_len ‖ module ‖ input. Computed by the guest and checked by the host. |
output_sha256 |
SHA-256 of the exact output bytes, computed by the guest and checked by the host. |
fuel |
Work done: wasmi fuel consumed for wasm/js/python, Rhai operations counted by the engine for rhai. For deterministic runs, part of what replay must reproduce. |
status |
0 success, 1 error raised by the code, 2 runtime unavailable, other values are limits or faults. A signed receipt with a nonzero status attests a failed run, not a successful one. |
Envelope and signing
payloadTypeisapplication/vnd.in-toto+json; the signature is Ed25519 over the DSSE pre-authentication encodingDSSEv1 <len(type)> <type> <len(body)> <body>.keyidis the lowercase hex SHA-256 of the raw 32-byte public key.- Ed25519 is deterministic: the same statement and key give byte-identical envelopes, so two deterministic runs can be compared as envelopes.
- The host only signs when it has re-hashed the payload and output and they match what the guest reported.
What a signature does and does not prove
It proves that the holder of the key vouched for this run, and that nothing
in the statement changed afterwards. It does not prove that the key holder
was honest, or what hardware ran the VM. That is tamper evidence, not remote
attestation. For deterministic runs the signer does not need to be trusted at
all: anyone with the kernel image, the payload and the seed can re-execute and
compare output digest and fuel (verify --replay). Replay needs the exact
kernel named by kernel_sha256: receipts produced before Rhai fuel was
recorded (older kernel hash) only replay against their own kernel. Binding the signing key to
a measured kernel through a TEE is future work.
Verifying
ampoule-verify envelope.json --key <pubkey-hex|file> [--output F] [--payload F] [--kernel F]
cargo run -p verify --release -- --replay envelope.json --key <pubkey> --js code.js
The public key is the trust anchor and must reach the verifier by some other
channel than the envelope. ampoule-verify pubkey prints the key a host signs with.