--- slug: 24-attestation title: Attestation (probar qué código respondió) description: Pedile a la plataforma un documento que ate lo que corre al código que corre — AWS Nitro, TDX, SEV-SNP, dstack — servilo por TLS con la clave atestada, y verificalo como cliente con attestation_verify. example_ids: [attestation] --- # Attestation Las [etiquetas](23-labels) evitan que el dato se vaya. La attestation le permite a un tercero remoto comprobar **qué está corriendo antes de mandar el dato**. La plataforma — un TEE: AWS Nitro, Intel TDX, AMD SEV-SNP, dstack — firma un documento que ata una medida del código a un valor que vos elegís, y un cliente verifica ese documento contra una raíz pineada. No hace falta confiar en el operador, que es todo el punto. Dos formas, y son trabajos distintos: | | atesta | el verificador | |---|---|---| | `serve --attested` | un **servicio**: una identidad de larga vida cuya clave pública termina el TLS | te habla | | `run --attest` | un **resultado**: un programa, una entrada, una salida | lee un artefacto, offline | ## Los builtins ```synsema require attest let doc be attest({"report_data": sha256(bytes("el saldo está saldado"))}) let seen be attestation_verify(doc["document"], {"format": doc["format"], "now": now()}) print(seen["measurements"]["pcr0"]) ``` | builtin | capacidad | qué da | |---|---|---| | `attest(opts?)` → map | `require attest` | un documento fresco de la plataforma | | `attest_key(propósito)` → secret | `require attest` | una clave que la plataforma deriva de la medida | | `attestation_document()` → map | ninguna | la identidad del `serve --attested` en el que estás adentro | | `attestation_key()` → secret | `require attest` | la clave privada de esa identidad, **sellada** | | `attestation_verify(doc, opts)` → map | ninguna (puro) | el veredicto, normalizado entre plataformas | **`attest(opts?)`** toma `{"report_data"?: bytes (≤ 64), "nonce"?: bytes, "public_key"?: bytes}` y devuelve `{"format", "document": bytes, "driver", "report_data", "aux"?, "event_log"?, "root"?}`. `report_data` son los 64 bytes que **vos** elegís: es lo que convierte "existe algún enclave" en "*este* enclave calculó *eso*". Hasheá tu respuesta ahí adentro. **`attest_key(propósito)`** la deriva la plataforma para esta medida, así que otra build no puede leer lo que ésta selló. La etiqueta del secret lleva el propósito — `secret(attest_key:)`. Nitro/TDX/SEV-SNP crudos **no sellan claves**; el error lo dice y apunta a la receta del KMS. Es un hecho de la plataforma, no una función que falta. **`attestation_key()`** es un secret **sellado**: `reveal()` lo rechaza *aun con la capacidad `reveal`* (`reveal: secret(attestation_key) is sealed`). Sólo el ECDH con la propia clave y el MAC/hash de una vía pueden consumirlo. Exportar la clave que ancla el TLS y el documento anularía la attestation. **`attestation_verify(doc, opts)`** es puro — sin capacidad, sin red — y **`opts.now` (segundos unix) es obligatorio**: adentro de un enclave no hay reloj confiable y el veredicto tiene que ser reproducible, así que el verificador jamás lee el reloj de pared. `opts.expect = {"measurements": {"pcr0": ""}}` compara y falla cerrado ante una diferencia. Devuelve `{format, measurements, report_data, user_data, public_key, nonce, timestamp, module_id, digest, chain, tcb}`, y verifica, en este orden y fallando cerrado ante la primera duda: la estructura y los tipos exactos del payload; que la raíz del `cabundle` sea **por SHA-256 de su DER** la raíz pineada de AWS Nitro; la cadena X.509 completa (ECDSA-SHA384 sobre P-384, issuer/subject byte a byte, validez contra `opts.now` en **todos** los certificados); y por último la firma COSE ES384 con la clave de la hoja. > `tdx`, `sgx` y `sev-snp` **no se verifican** en esta release — error explícito, nunca un `true` optimista. `attest` igual *produce* esos formatos, así que un enclave puede emitir lo que su plataforma le da. ```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 ``` Al arrancar, el servidor genera un par P-256, le pide a la plataforma un documento que ate `sha256(spki ‖ program_sha ‖ config_sha)`, y lo publica en `GET /.well-known/attestation`. **Si la plataforma no responde, el servidor no arranca** — no hay modo degradado. ```synsema require serve(8080) require attest serve on 8080 route "GET /identity" give attestation_document() ``` - **TLS.** Sin `--tls-cert`/`--tls-auto` el canal usa un certificado autofirmado emitido con **esa misma clave**, así que el cliente pinea la clave del documento y sabe que el par TLS es el código atestado. Con un certificado del operador, el `tls_key` publicado dice `"operator"`: la clave anunciada **no** es la del canal, y el cliente no debe pinearla. - **Las etiquetas están siempre encendidas** — la respuesta HTTP y todo stream son sumideros públicos. Un despliegue atestado que pudiera publicar sus entradas estaría atestando la propiedad equivocada. Leé [etiquetas](23-labels) antes de escribir rutas. - **`--attested` y `--watch` son mutuamente excluyentes**: un reinicio cambiaría la identidad debajo de los clientes vivos. - El programa no puede declarar `/.well-known/attestation`, `/openapi.json`, `/docs`, `/llms.txt`, `/sitemap.xml` ni `/robots.txt`; el servidor se niega a arrancar nombrando la colisión, en vez de sombrearla en silencio. La identidad publicada: ```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` es el **modo**, no sólo el programa: el techo, si las etiquetas estaban encendidas, el perfil, de dónde salió la clave TLS. Su SHA-256 va adentro del `user_data` firmado, así que un operador no puede atestar una configuración endurecida y servir una floja. El driver `mock` agrega `"mock": true` y su `"root"`; una plataforma real no manda ninguno de los dos. ## `run --attest` ```sh synsema run --attest reporte.syn -- 2026-09 ``` La salida del programa se imprime como siempre, y después **una línea JSON**: ```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` implica `--deterministic` (perfil puro, techo sólo `stdout`), así que el mismo programa con la misma entrada da la misma salida; combinarlo con `--explain`, `--sandbox`, `--cap-set` o `--profile native` es error de uso (exit 2) con el motivo. `report_data = sha256(program_sha ‖ input_sha ‖ output_sha ‖ config_sha)`, donde la salida es todo lo que el programa juntó — `print` **y `log` y `show`** — unido con `\n`. `state_root` es el keccak256 de esa misma salida: el valor que comparan dos enclaves (o un contrato). `steps` es informativo y **no** entra en `report_data`, y es `null` si la corrida tocó un valor privado — si no, dos corridas con secretos distintos podían compartir `output_sha` y diferir en `steps`, un canal adentro del artefacto cuyo propósito es publicarse. ## Drivers Los elige `SYNSEMA_ATTEST`, o se autodetectan en Linux. **`mock` jamás se elige solo.** | driver | dónde | estado | |---|---|---| | `nitro` | Linux, AWS Nitro Enclaves por `/dev/nsm` | escrito contra el SDK de AWS, **sin probar todavía en hardware** | | `tsm` | Linux ≥ 6.7, configfs-tsm (el `provider` decide `tdx` o `sev-snp`) | **sin probar todavía en hardware** | | `dstack` | Unix, el socket del guest agent | **sin probar todavía contra una VM real** | | `mock` | cualquier SO, para CI y desarrollo local | probado; avisa por stderr y marca todo documento que hace | Perillas del host, del entorno del proceso (Docker `-e`, systemd) y no del `.env`: `SYNSEMA_ATTEST`, `SYNSEMA_ATTEST_MOCK_SEED`, `SYNSEMA_ATTEST_MOCK_PCRS`, `SYNSEMA_ATTEST_MOCK_TIMESTAMP`, y `DSTACK_SIMULATOR_ENDPOINT` — honrada sólo con un `SYNSEMA_ATTEST=dstack` explícito, así que el simulador nunca puede elegir el driver por sí solo. Cualquier cosa dudosa — un driver desconocido, un provider raro, una respuesta que no parsea, un `report_data` de más de 64 bytes — es un error explícito. No hay documento "probablemente bien". ## Verificar lo que bajaste La attestation responde *qué código corre adentro del enclave*. La pregunta anterior es *qué código instalé* — y la release también la responde, en tres niveles de fuerza. Vale conocerlos, porque `serve --attested` ata el `program_sha` y `measurements.json` pinea una imagen construida con estos mismos bytes: si no podés decir de dónde salió el binario, el resto de la cadena no se apoya en nada. **1. El checksum — integridad de la descarga.** Cada asset trae su `.sha256` al lado, y `install.sh` lo verifica antes de instalar; si no encuentra `sha256sum`/`shasum` en la máquina **aborta** en vez de instalar sin verificar. Eso atrapa una descarga cortada o un mirror alterado. No te dice quién construyó el archivo. **2. La procedencia del build — quién lo construyó y desde qué.** Los ocho artefactos de una release (los cuatro binarios de plataforma, los tres `.wasm` y `measurements.json`) están firmados con la build provenance de GitHub. Cualquiera puede comprobarla, sin confiar en el proyecto: ```sh gh attestation verify synsema-linux-x86_64 --repo kitecosmic/synsema ``` Responde con el workflow, el commit y el tag que produjeron *esos bytes exactos* — para v0.6.24, `release.yml@refs/tags/v0.6.24` en el commit `8284861`. Ésta es la comprobación a correr, y es la que la propia release corre sobre el binario de Linux antes de que ese binario entre a la imagen cuyo digest publica `measurements.json`. **3. Reproducibilidad — ¿otro llega a los mismos bytes?** Para el **guest de Vela** la release reconstruye `synsema-vela-guest.wasm` en dos versiones distintas de Ubuntu con el toolchain pineado y compara las dos contra el asset que publicó. En v0.6.24 los tres coincidieron: `87bad7b8d20c1d249fbfd06a9cf48c73e51af533bfd87754351922ee587d0325`. Ahí importa porque la cadena verifica un `wasmSha256`, así que "reconstruilo vos y compará" es una comprobación que una contraparte puede correr de verdad — ver [Vela](73-vela). **Lo que NO se promete, dicho de frente.** Esa comparación **avisa, no rompe** la release: la reproducibilidad se *reporta*, no se garantiza. Y los cuatro binarios nativos **no tienen ninguna comprobación de reproducibilidad** — lo que sí está garantizado para ellos es la procedencia del nivel 2. Empíricamente el binario de Linux de v0.6.24 salió byte a byte igual en dos corridas independientes de la release (`b57a7f63…`); el de Windows no. No leas ahí "el build de Linux es reproducible": es una observación sobre una imagen de runner, no una propiedad que el proyecto imponga. ## Checklist para un despliegue confidencial 1. **Comprobá el motor que vas a desplegar** — `gh attestation verify --repo kitecosmic/synsema` antes de que entre a una imagen o a un enclave (arriba). Atestar un programa construido por un motor de procedencia desconocida atesta la mitad equivocada. 2. Escribí el programa para que funcione con las etiquetas encendidas. `synsema run --labels` localmente; `synsema code check --json` para leer la lista de declassify antes de shippear. 3. `serve --attested`, sin `--watch`. Decidí el TLS: clave atestada (el cliente pinea) o certificado del operador (no pinea). 4. Publicá el `program_sha` y las medidas esperadas donde tus usuarios las vayan a buscar. 5. El cliente pide `/.well-known/attestation`, verifica con `attestation_verify` pasando `now` y `expect.measurements`, recomputa `sha256(spki ‖ program_sha ‖ config_sha)` contra `user_data`, chequea `config`, y **recién ahí** pinea la clave y manda el dato. 6. En CI, `SYNSEMA_ATTEST=mock` con una semilla fija ejercita todo el camino, y la marca `mock` hace imposible confundirlo con lo real.