Capabilities & Security

Attestation

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:

The builtins§

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"])

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:<purpose>). 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": "<hex>"}} 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.

-- 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§

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.

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 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:

{"format": "nitro", "driver": "nitro", "engine": "0.6.24",
 "public_key": "-----BEGIN PUBLIC KEY-----…", "public_key_hex": "<SPKI hex>",
 "program_sha": "<hex>", "config_sha": "<hex>",
 "config": {"ceiling": "unbounded", "engine": "0.6.24", "labels": true,
            "profile": "native", "tls_key": "attested"},
 "document": "<base64>", "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§

synsema run --attest report.syn -- 2026-09

The program's output prints as usual, then one JSON line:

{"output_sha": "<hex>", "steps": 412, "state_root": "<keccak256 hex>",
 "program_sha": "<hex>", "input_sha": "<hex>",
 "config": {"ceiling": "stdout", "labels": false, "profile": "pure", "tls_key": "none"},
 "config_sha": "<hex>",
 "attestation": {"format": "nitro", "document": "<base64>", "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.

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:

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.

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 <the asset> --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.