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

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.