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 opts be {"format": doc["format"], "now": floor(now())}
when get(doc, "aux") != nothing
    set opts["aux"] to doc["aux"]       -- sev-snp: the host's table, with the key that signed
when get(doc, "root") != nothing
    set opts["root"] to doc["root"]     -- mock only: its own root
let seen be attestation_verify(doc["document"], opts)
print(seen["measurements"])

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. In the document it lands in user_data (nitro, nitro-tpm, mock) or in the report's REPORT_DATA, zero-padded to 64 bytes (sev-snp); the engine checks that the document carries it before handing it over. aux is SEV-SNP's certificate table (pass it to attestation_verify), event_log comes only from dstack, and root only from mock.

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>). Only dstack (and mock) derive it; with nitro, nitro-tpm and tsm it is an error that points at the KMS recipe. Nitro and TDX have no such key. SEV-SNP does have one (SNP_GET_DERIVED_KEY), but on EC2 the measurement it is bound to is the firmware's, not your program's, so it would not seal anything to this code — the engine does not offer it.

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.format is one of nitro, nitro-tpm, sev-snp or mock. opts.expect compares and fails closed on a mismatch:

• "measurements": {"pcr0": "<hex>", …} — the names of the format (pcrN for nitro/nitro-tpm/mock, measurement and host_data for sev-snp; an unknown name is an error).
• "report_data": <bytes or hex> — the whole report_data. In sev-snp, whose report_data is 64 bytes, a shorter value is padded with zeros, so you write sha256(spki ‖ program_sha ‖ config_sha) without thinking about the padding. In nitro, nitro-tpm and mock it is the user_data as is, and the match is exact. A mismatch says how many bytes match, never the values.

It returns {format, measurements, report_data, user_data, public_key, nonce, timestamp, module_id, digest, chain, tcb} (chain leaf first). What it checks depends on the format, always in order and failing closed at the first doubt:

nitro (AWS Nitro Enclaves) and mock: the payload's structure and types; that the cabundle root is by SHA-256 of its DER the pinned AWS Nitro root (mock: the opts.root you pass — it is the only format that takes one); 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.

nitro-tpm (EC2 instance attestation: NitroTPM inside a VM): the same envelope, the same pinned AWS root and the same chain checks. The payload is an indefinite-length CBOR map and the measurements come in nitrotpm_pcrs — pcr0…pcr23, SHA-384. It is a different format on purpose: a VM's document never verifies as nitro (an enclave) and an enclave's never as nitro-tpm; each names the key that gives it away. The leaf lives about three hours, so now matters.

sev-snp (AMD SEV-SNP): doc is the 1184-byte report (attest()["document"]). The key that signed it — the VLEK on AWS, a VCEK elsewhere — comes from opts.aux (the host's certificate table, attest()["aux"] or the identity's aux in base64) or from opts.vek (DER or PEM, e.g. a VCEK you fetched yourself from AMD); if both are given they must be the same certificate. In order:

1. size 0x4A0 and VERSION 2–5; SIGNATURE_ALGO = ECDSA P-384/SHA-384; 2. KEY_INFO says which key signed: VCEK or VLEK; "none" is the report is not signed; 3. the product (Milan, Genoa, Turin) from the VEK's productName, cross-checked with the CPUID in the report (reports of VERSION 3 and later carry it; a VERSION 2 report cannot be Turin); 4. the chain VEK ← ASK (VCEK) or ASVK (VLEK) ← ARK with AMD's roots embedded in the engine and pinned by SHA-256 — the ARK/ASK the host puts in aux are ignored; RSASSA-PSS with SHA-384 and a 48-byte salt and nothing else; validity of each certificate against now (an AWS VLEK lives one year); 5. the report's ECDSA P-384 signature over its first 0x2A0 bytes; 6. the VEK's TCB (boot loader, TEE, SNP, microcode, and FMC on Turin) equal to the report's REPORTED_TCB; for a VCEK, its hwID equal to CHIP_ID; 7. POLICY.DEBUG set is an error (the guest allows debug: the host can read its memory), with no option to skip it.

measurements is {measurement, host_data}; tcb is {product, signing_key ("vlek"|"vcek"), csp_id (VLEK), chip_id, vmpl, reported, current, committed, launch}; policy lists the guest policy bits with raw; version is the report's. timestamp, module_id, user_data, public_key and nonce are nothing — the report carries no time, and the verifier does not invent one. opts.root is refused with nitro, nitro-tpm and sev-snp alike: they trust only their pinned roots.

What has met real hardware. The sev-snp verifier has checked a real report only from Milan (AWS c6a, signed by a VLEK). Genoa and Turin, the VCEK path, and the policy, TCB and reserved-field rejections are tested with synthetic chains built to AMD's specifications (the SEV-SNP ABI and the VCEK certificate spec); Turin's TCB layout comes from those documents, not from a Turin report. Turin with a VCEK is not supported in this release: its hwID may not be the 64 bytes the verifier requires, and such a report is refused rather than guessed. AMD's revocation lists (CRLs) are not consulted — nothing is downloaded.

tdx and sgx are not verified by this release — an explicit error, never an optimistic true. attest still produces tdx, 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)")

test "expect.report_data compares the bound value, and another one fails closed"
    let bound be attestation_verify(DOC["document"], {"format": "mock", "now": 1789000000, "root": DOC["root"], "expect": {"report_data": sha256(bytes(answer()))}})
    assert_eq(bound["report_data"], sha256(bytes(answer())))
    assert_error(() => attestation_verify(DOC["document"], {"format": "mock", "now": 1789000000, "root": DOC["root"], "expect": {"report_data": sha256(bytes("another answer"))}}))

test "a platform format trusts only its pinned roots: a root of your own is refused"
    assert_error(() => attestation_verify(DOC["document"], {"format": "nitro", "now": 1789000000, "root": DOC["root"]}))
    assert_error(() => attestation_verify(DOC["document"], {"format": "sev-snp", "now": 1789000000, "root": DOC["root"]}))

test "an enclave-shaped document is not a VM document"
    -- Refused for the right reason: the payload says which format it is, before any root.
    let why be ""
    try
        attestation_verify(DOC["document"], {"format": "nitro-tpm", "now": 1789000000})
    recover err
        set why to err
    assert(contains(why, "payload has the key \"pcrs\""), why)

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. Once it is up it prints every driver and format it attests with, in order, for example Attested: drivers=tsm,nitro-tpm formats=sev-snp,nitro-tpm program_sha=95cb… — GET /.well-known/attestation (engine v0.6.44+; before, only the first driver was named).

The documents are renewed with the same key and the same binding. A NitroTPM or Nitro leaf certificate lives about three hours, so the server asks every driver for fresh documents at half the life of the shortest one, and at least once a day, and replaces them all at once. A SEV-SNP report has no lifetime of its own, but the VLEK (or VCEK) in its aux does — about a year on AWS — and that is when it expires; renewing does not bring a new VLEK, so past half of its life the server renews at half of what is left (once a day while months remain). /.well-known/attestation and attestation_document() always give the current ones; /.well-known/attestation answers 503 rather than serve an expired one. If a renewal fails it retries with backoff and logs to stderr; if the current documents expire without a renewal, the server shuts down with an error — it never serves an expired document and never drops the driver that failed.

With more than one driver (SYNSEMA_ATTEST=tsm,nitro-tpm, or auto-detected — see What each document measures below) every driver signs the same binding, and if any of them fails the server does not start. program_sha is sha256(source ‖ 0x00 ‖ sha256(module_1) ‖ … ‖ sha256(module_n)), each used module once (by resolved path), depth first in the order the use lines appear in the source — a use inside a task that never runs counts too. synsema code sha app.syn prints it, so whoever verifies computes the expected value without reimplementing module resolution; it runs the static check first (every use must resolve), and --json lists the modules with paths relative to the program's folder, written with /. Changed in v0.6.43: before, a module imported from two places was hashed twice, so for such programs program_sha differs from v0.6.42's.

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.
• With --auditor (engine v0.6.46+), the server's sealed receipts — one per request — are signed with this attested key: their header says "run_key": {"alg": "P-256", "public": "<the compressed point, base64url>", "identity": "attested"}, the same key as public_key_hex (there in SPKI form), and config_sha is the one published here. The auditor key is not part of config, so it does not change config_sha. Receipts, keys and replay: Observability § Sealed receipts.
• 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": "sev-snp", "driver": "tsm", "engine": "v0.6.43",
 "public_key": "-----BEGIN PUBLIC KEY-----…", "public_key_hex": "<SPKI hex>",
 "program_sha": "<hex>", "config_sha": "<hex>",
 "config": {"ceiling": "unbounded", "drivers": ["tsm", "nitro-tpm"], "engine": "v0.6.43",
            "labels": true, "profile": "native", "tls_key": "attested"},
 "document": "<base64>", "aux": "<base64>", "tls_key": "attested",
 "documents": [
   {"format": "sev-snp", "driver": "tsm", "document": "<base64>", "aux": "<base64>"},
   {"format": "nitro-tpm", "driver": "nitro-tpm", "document": "<base64>"}]}

The top-level format/driver/document/aux are the first driver's, as before; documents has one entry per driver, in order. config is the mode, not just the program: the ceiling, the drivers, whether labels were on, the profile, where the TLS key came from. Its SHA-256 (canonical JSON, sorted keys: sha256(canonical_json(config))) is inside every signed document, 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"], "drivers": ["nitro"], "engine": "v0.6.43", "labels": false,
            "profile": "pure", "tls_key": "none"},
 "config_sha": "<hex>",
 "attestation": {"format": "nitro", "document": "<base64>", "driver": "nitro"},
 "attestations": [{"format": "nitro", "driver": "nitro", "document": "<base64>"}]}

attestation is the first driver's document; attestations has one per driver, all binding the same report_data. If any driver fails there is no artefact. The drivers are chosen and checked before the program runs, so a missing platform stops it from running at all; a driver that fails when asked for the document fails after: the program's output is already printed, the JSON line is missing and the exit code is 1.

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

config names the engine too, so the same program attested by two engine versions gives two config_sha. 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.

run --attest with an auditor — the receipt's key is bound (engine v0.6.46+)§

With --auditor (see Observability § Sealed receipts), the run's sealed receipt is signed with a key made for the run ("identity": "ephemeral"). On its own, such a key only detects accidental damage. run --attest binds it: the JSON line gains "run_key": "<base64url of the 32-byte Ed25519 public key>", the same as the receipt's header.run_key.public, and

report_data = sha256(program_sha ‖ input_sha ‖ output_sha ‖ config_sha ‖ sha256(run_key))

where every field is the raw 32 bytes (hex or base64url decoded) and sha256(run_key) hashes the 32 bytes of the key. A document that verifies with this report_data says that this receipt was signed inside the measured code. The receipt's header carries the same config_sha.

• Without an auditor report_data does not change (four fields, no run_key in the line). A verifier of run --attest documents has to add the fifth field when run_key is present, or every audited document fails to verify.
• --attest and --auditor go together with --receipt <path>; --replay and --explain do not combine with either.

require file.read("attest.json")
require time

-- the JSON line that `SYNSEMA_ATTEST=mock synsema run --attest --auditor <public> p.syn` printed last
let art be json_decode(read_file("attest.json"))
let a be art["attestation"]
let seen be attestation_verify(bytes(a["document"], "base64"), {"now": floor(now()), "format": a["format"], "root": bytes(a["root"], "base64")})
let base be bytes(art["program_sha"], "hex") + bytes(art["input_sha"], "hex") + bytes(art["output_sha"], "hex") + bytes(art["config_sha"], "hex")
let expected be sha256(base)
when get(art, "run_key") != nothing
    set expected to sha256(base + sha256(bytes(art["run_key"], "base64url")))
print(seen["report_data"] == expected)    -- true

(root is passed only for the mock driver; with a real platform the root is pinned.)

Which data went in — lineage in the receipt§

Attestation proves which code ran. Since engine v0.6.29 the engine also records which data it read: every file, HTTP answer, database or chain read, model answer, stdin line and child program result goes into lineage(), each with the sha256 of the bytes the program received and the encoding that says which bytes those were — so a verifier who holds the input recomputes the hash. receipt() publishes the same list as credentialSubject.inputs, next to program_sha, engine and the capability audit; and, since engine v0.6.46, credentialSubject.outputs: every file the run wrote (write_file, append_file, edit_file, zip_extract, tar_extract) with its path and sha256 — Observability § Outputs. Signed, one document says this code read these inputs, wrote these files and declared this output. A query or a prompt is published only as a salted commitment, and a host without credentials, path or query: the receipt never carries data. The fields and a worked example are in Agent identity.

To fix a signed receipt in time, anchor sha256(canonical_json(receipt)) on a chain (calldata or an event of your own contract). What lineage does not cover: values that are not reads (env/secret, the blackboard) and completeness across units of work.

Drivers§

Chosen by SYNSEMA_ATTEST — one driver or a comma-separated list, such as tsm,nitro-tpm — or auto-detected on Linux. mock is never auto-selected, and it cannot be mixed with other drivers. With a list, serve --attested and run --attest get one document per driver; attest() and attest_key() use the first.

Auto-detection: /dev/nsm → nitro; otherwise configfs-tsm → tsm, and a TPM that answers AWS's NitroTPM command → nitro-tpm (both when both are there, tsm first); otherwise a dstack socket. A TPM is not enough on its own: the engine asks it the NitroTPM question and a plain TPM says it does not know the command. Forcing nitro-tpm on a machine with no TPM device fails with NitroTPM is not available: the AMI needs TpmSupport=v2.0 and UEFI; on a TPM that is not a NitroTPM it fails when the TPM refuses AWS's command (NitroTPM NSM request failed: TPM response code 0x143).

How the nitro-tpm driver uses the TPM, and what it means for other TPM users on the same VM. One request at a time per process. It opens /dev/tpm0, which Linux gives to one process at a time; if another holds it, it waits up to 10 seconds and only then uses /dev/tpmrm0. With /dev/tpm0 it first releases what a process killed in the middle of a request left behind (a SIGKILL or the OOM killer can strike between steps): the objects and sessions loaded in the TPM, and the 8 KiB message buffers with exactly the shape this driver creates — other owners' NV indices are never touched. Without that, a few such kills fill the TPM and the driver stops working until someone cleans it by hand. Two consequences, both rare and both failing closed:

• if two Synsema processes on the same VM attest at once and one had to fall back to /dev/tpmrm0, the other's cleanup can remove its buffer mid-request: that request fails with an error and serve --attested retries it;
• objects and sessions that another application loaded through /dev/tpm0 and expects to survive between openings are released. Applications that use /dev/tpmrm0 (the kernel resource manager, what most TPM tools use today) are not affected. If something else on the VM uses /dev/tpm0 directly, do not run it alongside the nitro-tpm driver.

This driver has been tested against a simulated TPM, not yet on a NitroTPM.

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, a driver listed twice, an odd provider, a response that does not parse, report_data over 64 bytes — is an explicit error. There is no "probably fine" document.

What each document measures§

Read this before deciding what a client must check, because on a cloud VM the answer is not what the word "attestation" suggests.

• SEV-SNP on EC2 proves the VM's memory is encrypted with a key AWS does not hold. Its measurement covers only the firmware (OVMF) and the initial vCPU state — not the kernel, not the disk, not the Synsema binary. So the program_sha inside its report_data is declared by a binary nobody measured: whoever operates the image could change it.
• NitroTPM with an Attestable AMI measures the boot: PCR4 is the boot binary (a UKI) and PCR12 its command line, which carries the dm-verity hash of a read-only root. That is what ties the disk, and the engine on it, to the document. Do not use PCR16 or PCR23 as measurements: root inside the VM can reset them.
• That is why one server publishes both (SYNSEMA_ATTEST=tsm,nitro-tpm, or auto-detected), bound to the same key: SEV-SNP for "the memory is private", NitroTPM for "this is the code". A client checks both — the expected PCRs come from whoever built the AMI, the expected SEV-SNP measurement from whoever knows the firmware; the engine provides neither.

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; since v0.6.48 one of the two builds from another folder with another CARGO_HOME. On v0.6.57 all three agreed: 56186763d1057f64dd1df721c19541112fc06fc662a81858a70e60b87f3500af. It matters there because the chain verifies a wasmSha256, so "rebuild it yourself and compare" is a check a counterparty can actually run: from a checkout of the tag, on Linux or WSL, SYNSEMA_VERSION=<the tag> bash packages/guests/vela/tools/build.sh out.wasm gives the published hash in any folder (before v0.6.48 only in the runner's own path; native Windows does not reproduce it) — 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 checks the server before sending it anything. From Synsema it is one option of fetch (and of ws_connect):

require net("203.0.113.7")

let PROGRAM be args()[0]     -- `synsema code sha app.syn` of the source you audited
let PCR4 be args()[1]        -- these two come from whoever built the AMI
let PCR12 be args()[2]
let OVMF be args()[3]        -- the SEV-SNP `measurement` of the firmware, from whoever knows it

let r be fetch("https://203.0.113.7:8443/hola", {"attested": {
    "program_sha": PROGRAM,
    "formats": ["sev-snp", "nitro-tpm"],
    "measurements": {"sev-snp": {"measurement": OVMF},
                     "nitro-tpm": {"pcr4": PCR4, "pcr12": PCR12}}
}})
print(r["attested"]["formats"])

On one TLS connection, failing closed at the first doubt: the handshake records the server's key without trusting any certificate authority (the handshake signature is still verified with that key); GET /.well-known/attestation goes over that same connection; its public_key_hex must be that key; config_sha must match config and program_sha must be yours (mandatory); every document must verify with expect.report_data = sha256(spki ‖ program_sha ‖ config_sha) and its measurements, every format in formats (mandatory) must be there, and an extra document that does not verify is an error too; a mock document is accepted only if formats names "mock". Only then does your request leave, on the same connection. If anything fails the request is never sent and error of r says why. now (unix seconds) is optional and defaults to the system clock, as for any TLS check. The answer carries attested: {program_sha, public_key_hex, formats, config}. In ws_connect(url, headers, {"attested": …}) the upgrade leaves after the checks, on every reconnect too (an explicit now advances with the time elapsed since the first connection), and ws_stats(c)["attested"] says what the last one verified. attested and tls_pin are two ways of fixing the key: pass one, and pass a value — nothing is an error (leave the key out for the usual certificate check). A man in the middle cannot pass: it cannot finish a handshake with the attested key.

measurements is what proves the code, so every format but mock needs its entry. program_sha alone is declared: the binary that publishes it is the one being checked. A document without expected measurements proves only that some machine of that platform answered — anyone who rents one can bind the program_sha you expect to their own key and pass every other check. So attested.measurements must name every format in formats except mock, each with a non-empty map ({"nitro-tpm": {"pcr4": …, "pcr12": …}}); otherwise the call is an error before anything connects. To accept any measurement of a format on purpose — say SEV-SNP only for "the memory is encrypted", with NitroTPM pinning the code — write "sev-snp": "any". On EC2 the SEV-SNP measurement covers only the firmware (see What each document measures), so it is the NitroTPM PCRs that tie the document to the code.

Against a server with an operator certificate (tls_key: "operator") attested fails by design: the channel's key is not the attested one. There, verify the identity by hand (below) and trust the operator's certificate as usual. In the WebAssembly embedding (synsema-wasm-web, where the host does the HTTP) tls_pin and attested fail closed: the host's transport cannot pin a key or read the identity over the handshake's connection.

The errors say which check failed, for example the server runs program_sha …, not the expected …, attested.formats asks for "sev-snp" but the server published no such document, the identity's public_key_hex is not the key of this TLS connection, the identity has two nitro-tpm documents, the server is attested by the mock driver … and attested.formats does not name "mock", the <format> document does not verify: <the verifier's reason>, and the identity response must carry Content-Length (the identity must come with its exact length so the same connection can carry your request).

The same by hand, for an identity you already hold (a copy the operator published, an artefact), with attestation_verify and then tls_pin:

require net("203.0.113.7")
require file.read("identity.json")

let BASE be "https://203.0.113.7:8443"
let EXPECTED_PROGRAM be args()[0]     -- `synsema code sha app.syn` of the source you audited
let NOW be int(args()[1])             -- the time you trust, unix seconds

-- The identity proves itself, so it can come from any channel: here, a copy the operator
-- published. (Read straight from the server it needs the pin you do not have yet.)
let id be json_decode(read_file("identity.json"))

when decode(sha256(canonical_json(id["config"])), "hex") != id["config_sha"]
    raise "config_sha does not match the published config"
when id["program_sha"] != EXPECTED_PROGRAM
    raise "this server runs another program"
let binding be sha256(bytes(id["public_key_hex"], "hex") + bytes(id["program_sha"], "hex") + bytes(id["config_sha"], "hex"))

each d in id["documents"]
    let opts be {"format": d["format"], "now": NOW, "expect": {"report_data": binding}}
    when get(d, "aux") != nothing
        set opts["aux"] to bytes(d["aux"], "base64")
    let seen be attestation_verify(bytes(d["document"], "base64"), opts)
    print(d["driver"] + ": " + seen["format"] + " verified")

-- Only now: the TLS peer must present exactly that key.
let r be fetch(BASE + "/hola", {"tls_pin": id["public_key_hex"]})
print(r["json"])

tls_pin (in fetch's options, and in ws_connect's) takes the server's SubjectPublicKeyInfo as hex, bytes or a PUBLIC KEY PEM. It replaces the check against the system roots and the host name with byte equality of the presented key; the handshake signature is still verified with that key. Another key fails the handshake (tls_pin: the server public key (SPKI) does not match the pinned key); without tls_pin nothing changes — a self-signed certificate is refused as unknown, as always. It needs https:///wss:// and require net for the host. With an operator certificate (tls_key: "operator") do not pin the announced key: it is not the channel's.

From a client that is not Synsema (curl, Python, Go), do the same steps yourself: open the TLS connection without certificate validation but keep the server's certificate (Python: ssl.CERT_NONE and getpeercert(binary_form=True)); send GET /.well-known/attestation over that same connection with Connection: keep-alive; require its public_key_hex to equal the SubjectPublicKeyInfo of that certificate; check config_sha and program_sha; verify every document (with synsema run and attestation_verify, or your platform's verifier) against sha256(spki ‖ program_sha ‖ config_sha); and only then send your request on that connection. Opening a second connection for the request undoes the whole point, unless you pin the key there. 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.