--- slug: 24-attestation title: Attestation (proving which code answered) description: Ask the platform for a document that binds what is running to the code that is running — AWS Nitro, TDX, SEV-SNP, dstack — serve it over TLS with the attested key, and verify it as a client with attestation_verify. example_ids: [attestation] --- # Attestation [Labels](23-labels) keep the data from leaving. Attestation lets a remote party check **what is running before it sends the data in**. The platform — a TEE: AWS Nitro, Intel TDX, AMD SEV-SNP, dstack — signs a document that binds a measurement of the code to a value you choose, and a client verifies that document against a pinned root. No trust in the operator is required, which is the whole point. Two shapes, and they are different jobs: | | attests | the verifier | |---|---|---| | `serve --attested` | a **service**: a long-lived identity whose public key terminates TLS | talks to you | | `run --attest` | a **result**: one program, one input, one output | reads an artefact, offline | ## The builtins ```synsema require attest let doc be attest({"report_data": sha256(bytes("the answer is 42"))}) let seen be attestation_verify(doc["document"], {"format": doc["format"], "now": now()}) print(seen["measurements"]["pcr0"]) ``` | builtin | capability | what it gives | |---|---|---| | `attest(opts?)` → map | `require attest` | a fresh document from the platform | | `attest_key(purpose)` → secret | `require attest` | a key the platform derives from the measurement | | `attestation_document()` → map | none | the identity of the `serve --attested` you are inside | | `attestation_key()` → secret | `require attest` | that identity's private key, **sealed** | | `attestation_verify(doc, opts)` → map | none (pure) | the verdict, normalised across platforms | **`attest(opts?)`** takes `{"report_data"?: bytes (≤ 64), "nonce"?: bytes, "public_key"?: bytes}` and returns `{"format", "document": bytes, "driver", "report_data", "aux"?, "event_log"?, "root"?}`. `report_data` is the 64 bytes **you** choose: it is what turns "some enclave exists" into "*this* enclave computed *that*". Hash your answer into it. **`attest_key(purpose)`** is derived by the platform for this measurement, so another build cannot read what this one sealed. The secret's label carries the purpose — `secret(attest_key:)`. Raw Nitro/TDX/SEV-SNP **do not seal keys**; the error says so and points at the KMS recipe. That is a platform fact, not a missing feature. **`attestation_key()`** is a **sealed** secret: `reveal()` refuses it *even with the `reveal` capability* (`reveal: secret(attestation_key) is sealed`). Only ECDH with your own key and one-way MAC/hash may consume it. Exporting the key that anchors both TLS and the document would void the attestation. **`attestation_verify(doc, opts)`** is pure — no capability, no network — and **`opts.now` (unix seconds) is mandatory**: inside an enclave there is no trustworthy clock and a verdict has to be reproducible, so the verifier never reads the wall clock. `opts.expect = {"measurements": {"pcr0": ""}}` compares and fails closed on a mismatch. It returns `{format, measurements, report_data, user_data, public_key, nonce, timestamp, module_id, digest, chain, tcb}`, and it verifies, in order, failing closed at the first doubt: the payload's structure and types; that the `cabundle` root is **by SHA-256 of its DER** the pinned AWS Nitro root; the whole X.509 chain (ECDSA-SHA384 over P-384, issuer/subject byte for byte, validity against `opts.now` on **every** certificate); and last the COSE ES384 signature with the leaf's key. > `tdx`, `sgx` and `sev-snp` are **not verified** by this release — an explicit error, never an optimistic `true`. `attest` still *produces* those formats, so an enclave can emit what its platform gives. ```synsema -- Doc example: attestation — proving WHICH code produced an answer. -- Runs under the `mock` driver (SYNSEMA_ATTEST=mock): deterministic, forgeable on -- purpose, and it marks every document it makes so CI can never be mistaken for a -- platform. On real hardware the driver is auto-detected and `root` is pinned, not -- supplied. intent: "doc example: attestation" require attest task answer() give "the balance is settled" task document_for(answer_text) -- `report_data` is the 64 bytes YOU choose: it is what turns "some enclave -- exists" into "THIS enclave computed THAT". Hash your answer into it. give attest({"report_data": sha256(bytes(answer_text))}) task verdict(doc) -- Pure: no capability, no network. `opts.now` is MANDATORY — an enclave has no -- trustworthy clock and a verdict has to be reproducible, so the verifier never -- reads the wall clock. `opts.root` is accepted only for the mock format. give attestation_verify(doc["document"], {"format": doc["format"], "now": 1789000000, "root": doc["root"]}) let DOC be document_for(answer()) let SEEN be verdict(DOC) test "the document is bound to the answer, not to the enclave alone" assert_eq(SEEN["report_data"], sha256(bytes(answer()))) test "the mock driver never claims to be a platform" assert_eq(DOC["driver"], "mock") assert_eq(DOC["format"], "mock") test "verifying without a clock is refused, not guessed" assert_error(() => attestation_verify(DOC["document"], {"format": "mock", "root": DOC["root"]})) test "a mock document without an explicit root has nothing to trust" assert_error(() => attestation_verify(DOC["document"], {"format": "mock", "now": 1789000000})) test "expected measurements are compared, and a mismatch fails closed" let good be attestation_verify(DOC["document"], {"format": "mock", "now": 1789000000, "root": DOC["root"], "expect": {"measurements": {"pcr0": SEEN["measurements"]["pcr0"]}}}) assert_eq(good["format"], "mock") assert_error(() => attestation_verify(DOC["document"], {"format": "mock", "now": 1789000000, "root": DOC["root"], "expect": {"measurements": {"pcr0": "00"}}})) test "a key sealed to the measurement is a secret, and its label carries the purpose" let k be attest_key("doc-example") assert_eq(text(k), "secret(attest_key:doc-example)") ``` ## `serve --attested` ```sh synsema serve --attested app.syn ``` At startup the server generates a P-256 keypair, asks the platform for a document binding `sha256(spki ‖ program_sha ‖ config_sha)`, and publishes it at `GET /.well-known/attestation`. **If the platform does not answer, the server does not start** — there is no degraded mode. ```synsema require serve(8080) require attest serve on 8080 route "GET /identity" give attestation_document() ``` - **TLS.** Without `--tls-cert`/`--tls-auto` the channel uses a self-signed certificate issued with **that same key**, so a client pins the key from the document and knows the TLS peer is the attested code. With an operator certificate the published `tls_key` says `"operator"`: the announced key is *not* the channel's, and the client must not pin it. - **Labels are always on** — the HTTP response and every stream are public sinks. An attested deployment that could publish its inputs would be attesting the wrong property. Read [labels](23-labels) before writing routes. - **`--attested` and `--watch` are mutually exclusive**: a restart would change the identity underneath live clients. - The program cannot declare `/.well-known/attestation`, `/openapi.json`, `/docs`, `/llms.txt`, `/sitemap.xml` or `/robots.txt`; the server refuses to start naming the collision, rather than shadowing it silently. The published identity: ```json {"format": "nitro", "driver": "nitro", "engine": "0.6.24", "public_key": "-----BEGIN PUBLIC KEY-----…", "public_key_hex": "", "program_sha": "", "config_sha": "", "config": {"ceiling": "unbounded", "engine": "0.6.24", "labels": true, "profile": "native", "tls_key": "attested"}, "document": "", "tls_key": "attested"} ``` `config` is the **mode**, not just the program: the ceiling, whether labels were on, the profile, where the TLS key came from. Its SHA-256 is inside the signed `user_data`, so an operator cannot attest a hardened configuration and serve a loose one. The `mock` driver adds `"mock": true` and its `"root"`; a real platform sends neither. ## `run --attest` ```sh synsema run --attest report.syn -- 2026-09 ``` The program's output prints as usual, then **one JSON line**: ```json {"output_sha": "", "steps": 412, "state_root": "", "program_sha": "", "input_sha": "", "config": {"ceiling": "stdout", "labels": false, "profile": "pure", "tls_key": "none"}, "config_sha": "", "attestation": {"format": "nitro", "document": "", "driver": "nitro"}} ``` `--attest` implies `--deterministic` (pure profile, `stdout`-only ceiling), so the same program and input give the same output; combining it with `--explain`, `--sandbox`, `--cap-set` or `--profile native` is a usage error (exit 2) with the reason. `report_data = sha256(program_sha ‖ input_sha ‖ output_sha ‖ config_sha)`, where the output is everything the program collected — `print` **and `log` and `show`** — joined with `\n`. `state_root` is keccak256 of that same output: the value two enclaves (or a contract) compare. `steps` is informative and is **not** in `report_data`, and it is `null` when the run touched a private value — otherwise two runs with different secrets could share an `output_sha` and differ in `steps`, a channel inside the very artefact meant to be published. ## Drivers Chosen by `SYNSEMA_ATTEST`, or auto-detected on Linux. **`mock` is never auto-selected.** | driver | where | status | |---|---|---| | `nitro` | Linux, AWS Nitro Enclaves via `/dev/nsm` | written against the AWS SDK, **not yet exercised on hardware** | | `tsm` | Linux ≥ 6.7, configfs-tsm (`provider` picks `tdx` or `sev-snp`) | **not yet exercised on hardware** | | `dstack` | Unix, the guest agent's socket | **not yet exercised against a real VM** | | `mock` | any OS, for CI and local development | exercised; warns on stderr and marks every document | Host knobs, from the process environment (Docker `-e`, systemd) and not the `.env`: `SYNSEMA_ATTEST`, `SYNSEMA_ATTEST_MOCK_SEED`, `SYNSEMA_ATTEST_MOCK_PCRS`, `SYNSEMA_ATTEST_MOCK_TIMESTAMP`, and `DSTACK_SIMULATOR_ENDPOINT` — honoured only with an explicit `SYNSEMA_ATTEST=dstack`, so the simulator can never pick the driver by itself. Anything unclear — an unknown driver, an odd provider, a response that does not parse, `report_data` over 64 bytes — is an explicit error. There is no "probably fine" document. ## Verifying what you downloaded Attestation answers *which code is running inside the enclave*. The question before it is *which code did I install* — and the release answers that too, at three levels of strength. They are worth knowing, because `serve --attested` binds `program_sha` and `measurements.json` pins an image built from these very bytes: if you cannot tell where the binary came from, the rest of the chain rests on nothing. **1. The checksum — integrity of the download.** Every asset ships a `.sha256` next to it, and `install.sh` verifies it before installing; with no `sha256sum`/`shasum` on the machine it **aborts** rather than installing unverified. That catches a truncated download or a tampered mirror. It does not tell you who built the file. **2. The build provenance — who built it, from what.** All eight artefacts of a release (the four platform binaries, the three `.wasm`, and `measurements.json`) are signed with GitHub's build provenance. Anyone can check it, with no trust in the project: ```sh gh attestation verify synsema-linux-x86_64 --repo kitecosmic/synsema ``` It answers with the workflow, the commit and the tag that produced *those exact bytes* — for v0.6.24, `release.yml@refs/tags/v0.6.24` at commit `8284861`. This is the check to run, and it is the one the release itself runs on the Linux binary before that binary goes into the image whose digest `measurements.json` publishes. **3. Reproducibility — can someone else get the same bytes?** For the **Vela guest** the release rebuilds `synsema-vela-guest.wasm` on two different Ubuntu versions with the pinned toolchain and compares both against the asset it published. On v0.6.24 all three agreed: `87bad7b8d20c1d249fbfd06a9cf48c73e51af533bfd87754351922ee587d0325`. It matters there because the chain verifies a `wasmSha256`, so "rebuild it yourself and compare" is a check a counterparty can actually run — see [Vela](73-vela). **What is not promised, stated plainly.** That comparison **warns, it does not fail** the release: reproducibility is *reported*, not guaranteed. And the four native binaries have **no reproducibility check at all** — what is guaranteed for them is the provenance of level 2. Empirically the Linux binary of v0.6.24 came out byte-identical across two independent release runs (`b57a7f63…`); the Windows one did not. Do not read "the Linux build is reproducible" into that: it is one observation on one runner image, not a property the project enforces. ## Checklist for a confidential deployment 1. **Check the engine you are deploying** — `gh attestation verify --repo kitecosmic/synsema` before it goes into an image or an enclave (above). Attesting a program built by an engine of unknown provenance attests the wrong half. 2. Write the program so it works with labels on. `synsema run --labels` locally; `synsema code check --json` to read the declassify list before shipping. 3. `serve --attested`, no `--watch`. Decide TLS: attested key (client pins) or operator certificate (client does not). 4. Publish `program_sha` and the expected measurements where your users will look for them. 5. The client fetches `/.well-known/attestation`, verifies with `attestation_verify` passing `now` and `expect.measurements`, recomputes `sha256(spki ‖ program_sha ‖ config_sha)` against `user_data`, checks `config`, and **only then** pins the key and sends the data. 6. In CI, `SYNSEMA_ATTEST=mock` with a fixed seed exercises the whole path, and the `mock` marker makes it impossible to confuse with the real thing.