Capacidades y seguridad

Attestation

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

Los 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: la tabla del host, con la clave que firmó
when get(doc, "root") != nothing
    set opts["root"] to doc["root"]     -- sólo mock: su propia raíz
let seen be attestation_verify(doc["document"], opts)
print(seen["measurements"])

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. En el documento cae en user_data (nitro, nitro-tpm, mock) o en el REPORT_DATA del reporte, rellenado con ceros a 64 bytes (sev-snp); el motor comprueba que el documento lo lleve antes de entregarlo. aux es la tabla de certificados de SEV-SNP (pasásela a attestation_verify), event_log sólo lo da dstack, y root sólo mock.

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:<propósito>). Sólo dstack (y mock) la derivan; con nitro, nitro-tpm y tsm es un error que apunta a la receta del KMS. Nitro y TDX no tienen esa clave. SEV-SNP sí tiene una (SNP_GET_DERIVED_KEY), pero en EC2 la medida a la que se ata es la del firmware, no la de tu programa, así que no sellaría nada a este código — el motor no la ofrece.

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.format es nitro, nitro-tpm, sev-snp o mock. opts.expect compara y falla cerrado ante una diferencia:

• "measurements": {"pcr0": "<hex>", …} — los nombres del formato (pcrN en nitro/nitro-tpm/mock, measurement y host_data en sev-snp; un nombre desconocido es error).
• "report_data": <bytes o hex> — el report_data entero. En sev-snp, cuyo report_data mide 64 bytes, un valor más corto se rellena con ceros, así que escribís sha256(spki ‖ program_sha ‖ config_sha) sin pensar en el relleno. En nitro, nitro-tpm y mock es el user_data tal cual y la igualdad es exacta. Un mismatch dice cuántos bytes coinciden, nunca los valores.

Devuelve {format, measurements, report_data, user_data, public_key, nonce, timestamp, module_id, digest, chain, tcb} (chain con la hoja primero). Qué verifica depende del formato, siempre en orden y fallando cerrado ante la primera duda:

nitro (AWS Nitro Enclaves) y mock: 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 (mock: el opts.root que pasás — es el único formato que lo acepta); 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.

nitro-tpm (EC2 instance attestation: NitroTPM adentro de una VM): el mismo sobre, la misma raíz pineada de AWS y los mismos chequeos de cadena. El payload es un mapa CBOR de longitud indefinida y las medidas vienen en nitrotpm_pcrs — pcr0…pcr23, SHA-384. Es un formato distinto a propósito: un documento de una VM nunca verifica como nitro (un enclave) y el de un enclave nunca como nitro-tpm; cada uno nombra la clave que lo delata. La hoja vive unas tres horas, así que now importa.

sev-snp (AMD SEV-SNP): doc es el reporte de 1184 bytes (attest()["document"]). La clave que lo firmó — la VLEK en AWS, una VCEK en otros lados — sale de opts.aux (la tabla de certificados del host, attest()["aux"] o el aux de la identidad en base64) o de opts.vek (DER o PEM, p. ej. una VCEK que bajaste vos de AMD); si vienen las dos, tienen que ser el mismo certificado. En orden:

1. tamaño 0x4A0 y VERSION 2–5; SIGNATURE_ALGO = ECDSA P-384/SHA-384; 2. KEY_INFO dice qué clave firmó: VCEK o VLEK; "ninguna" es the report is not signed; 3. el producto (Milan, Genoa, Turin) por el productName de la VEK, cruzado con el CPUID del reporte (lo traen los reportes de VERSION 3 en adelante; un reporte VERSION 2 no puede ser de Turin); 4. la cadena VEK ← ASK (VCEK) o ASVK (VLEK) ← ARK con las raíces de AMD embebidas en el motor y pineadas por SHA-256 — las ARK/ASK que el host pone en aux se ignoran; RSASSA-PSS con SHA-384 y sal de 48 bytes y nada más; validez de cada certificado contra now (una VLEK de AWS vive un año); 5. la firma ECDSA P-384 del reporte sobre sus primeros 0x2A0 bytes; 6. la TCB de la VEK (boot loader, TEE, SNP, microcódigo, y FMC en Turin) igual al REPORTED_TCB del reporte; en una VCEK, su hwID igual a CHIP_ID; 7. POLICY.DEBUG prendido es error (the guest allows debug: the host can read its memory), sin opción para saltearlo.

measurements es {measurement, host_data}; tcb es {product, signing_key ("vlek"|"vcek"), csp_id (VLEK), chip_id, vmpl, reported, current, committed, launch}; policy lista los bits de la política del guest con raw; version es la del reporte. timestamp, module_id, user_data, public_key y nonce son nothing — el reporte no trae hora y el verificador no la inventa. opts.root se rechaza igual con nitro, nitro-tpm y sev-snp: confían sólo en sus raíces pineadas.

Qué pasó por hardware real. El verificador sev-snp comprobó un reporte real sólo de Milan (AWS c6a, firmado por una VLEK). Genoa y Turin, el camino de la VCEK, y los rechazos de política, TCB y campos reservados están probados con cadenas sintéticas construidas según las especificaciones de AMD (el ABI de SEV-SNP y la spec de certificados VCEK); la disposición de la TCB de Turin sale de esos documentos, no de un reporte de Turin. Turin con VCEK no está soportado en esta release: su hwID puede no medir los 64 bytes que exige el verificador, y un reporte así se rechaza en vez de adivinarse. No se consultan las listas de revocación de AMD (CRL) — no se descarga nada.

tdx y sgx no se verifican en esta release — error explícito, nunca un true optimista. attest igual produce tdx, así que un enclave puede emitir lo que su plataforma le da.

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

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. Una vez levantado imprime todos los drivers y formatos con los que atesta, en orden, por ejemplo Attested: drivers=tsm,nitro-tpm formats=sev-snp,nitro-tpm program_sha=95cb… — GET /.well-known/attestation (motor v0.6.44+; antes nombraba sólo el primer driver).

Los documentos se renuevan con la misma clave y el mismo binding. La hoja de NitroTPM o de Nitro vive unas tres horas, así que el servidor les pide documentos nuevos a todos los drivers a la mitad de la vida del más corto, y por lo menos una vez por día, y los reemplaza todos de una vez. Un reporte SEV-SNP no tiene vida propia, pero la VLEK (o VCEK) de su aux sí — alrededor de un año en AWS — y ahí vence; renovar no trae una VLEK nueva, así que pasada la mitad de su vida el servidor renueva a la mitad de lo que queda (una vez por día mientras queden meses). /.well-known/attestation y attestation_document() dan siempre los vigentes; /.well-known/attestation responde 503 antes que servir uno vencido. Si una renovación falla, reintenta con backoff y lo anota en stderr; si los documentos vigentes vencen sin renovación, el servidor se cierra con error — nunca sirve un documento vencido ni saca el driver que falló.

Con más de un driver (SYNSEMA_ATTEST=tsm,nitro-tpm, o autodetectados — ver Qué mide cada documento más abajo) cada driver firma el mismo binding, y si cualquiera falla el servidor no arranca. program_sha es sha256(fuente ‖ 0x00 ‖ sha256(módulo_1) ‖ … ‖ sha256(módulo_n)), cada módulo de use una vez (por ruta resuelta), en profundidad y en el orden en que aparecen los use en el fuente — cuenta también un use adentro de una task que nunca corre. synsema code sha app.syn lo imprime, así quien verifica calcula el valor esperado sin reimplementar la resolución de módulos; corre antes el chequeo estático (cada use tiene que resolver), y --json lista los módulos con rutas relativas a la carpeta del programa, escritas con /. Cambió en v0.6.43: antes, un módulo importado desde dos lugares se hasheaba dos veces, así que para esos programas el program_sha difiere del de v0.6.42.

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 antes de escribir rutas.
• --attested y --watch son mutuamente excluyentes: un reinicio cambiaría la identidad debajo de los clientes vivos.
• Con --auditor (engine v0.6.46+), los recibos sellados del server — uno por request — se firman con esta clave atestada: su header dice "run_key": {"alg": "P-256", "public": "<el punto comprimido, en base64url>", "identity": "attested"}, la misma clave que public_key_hex (ahí en forma SPKI), y config_sha es el que se publica acá. La clave del auditor no forma parte de config, así que no cambia config_sha. Recibos, claves y replay: Observabilidad § Recibos sellados.
• 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:

{"format": "sev-snp", "driver": "tsm", "engine": "v0.6.43",
 "public_key": "-----BEGIN PUBLIC KEY-----…", "public_key_hex": "<SPKI en 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>"}]}

format/driver/document/aux de arriba son los del primer driver, como antes; documents trae uno por driver, en orden. config es el modo, no sólo el programa: el techo, los drivers, si las etiquetas estaban encendidas, el perfil, de dónde salió la clave TLS. Su SHA-256 (JSON canónico, claves ordenadas: sha256(canonical_json(config))) va adentro de cada documento 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§

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

La salida del programa se imprime como siempre, y después una línea JSON:

{"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 es el documento del primer driver; attestations trae uno por driver, todos atando el mismo report_data. Si un driver falla no hay artefacto. Los drivers se eligen y se comprueban antes de correr el programa, así que sin plataforma el programa ni corre; un driver que falla al pedirle el documento falla después: la salida del programa ya se imprimió, falta la línea JSON y el código de salida es 1.

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

config nombra también al motor, así que el mismo programa atestado por dos versiones del motor da dos config_sha. 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.

run --attest con un auditor — la clave del recibo queda atada (engine v0.6.46+)§

Con --auditor (ver Observabilidad § Recibos sellados), el recibo sellado de la corrida se firma con una clave hecha para la corrida ("identity": "ephemeral"). Sola, esa clave solo detecta daño accidental. run --attest la ata: la línea JSON suma "run_key": "<base64url de la pública Ed25519 de 32 bytes>", la misma que header.run_key.public del recibo, y

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

donde cada campo son los 32 bytes crudos (decodificados del hex o del base64url) y sha256(run_key) hashea los 32 bytes de la clave. Un documento que verifica con este report_data dice que este recibo se firmó adentro del código medido. El header del recibo lleva el mismo config_sha.

• Sin auditor report_data no cambia (cuatro campos, sin run_key en la línea). Un verificador de documentos de run --attest tiene que sumar el quinto campo cuando run_key está presente, o todo documento auditado falla al verificar.
• --attest y --auditor van juntos con --receipt <ruta>; --replay y --explain no se combinan con ninguno de los dos.

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 se pasa solo con el driver mock; con una plataforma real la raíz está fijada.)

Qué datos entraron — el linaje en el recibo§

La atestación prueba qué código corrió. Desde el motor v0.6.29 el motor registra además qué datos leyó: cada archivo, respuesta HTTP, lectura de base de datos o de cadena, respuesta de modelo, línea de stdin y resultado de un programa hijo entra en lineage(), cada uno con el sha256 de los bytes que recibió el programa y el encoding que dice qué bytes eran — así un verificador que tiene el input recalcula el hash. receipt() publica la misma lista como credentialSubject.inputs, junto a program_sha, engine y la auditoría de capabilities; y, desde el motor v0.6.46, credentialSubject.outputs: cada archivo que escribió la corrida (write_file, append_file, edit_file, zip_extract, tar_extract) con su ruta y su sha256 — Observabilidad § Salidas. Firmado, un solo documento dice este código leyó estos inputs, escribió estos archivos y declaró esta salida. Una query o un prompt se publican solo como un compromiso salado, y un host sin credenciales, ruta ni query: el recibo nunca lleva datos. Los campos y un ejemplo completo están en Identidad de agentes.

Para fijar en el tiempo un recibo firmado, anclá sha256(canonical_json(receipt)) en una cadena (calldata o un evento de tu propio contrato). Lo que el linaje no cubre: valores que no son lecturas (env/secret, el blackboard) y la completitud entre unidades de trabajo.

Drivers§

Los elige SYNSEMA_ATTEST — un driver o una lista separada por comas, como tsm,nitro-tpm — o se autodetectan en Linux. mock jamás se elige solo, y no se puede mezclar con otros drivers. Con una lista, serve --attested y run --attest sacan un documento por driver; attest() y attest_key() usan el primero.

Autodetección: /dev/nsm → nitro; si no, configfs-tsm → tsm, y un TPM que responde al comando NitroTPM de AWS → nitro-tpm (los dos si están los dos, tsm primero); si no, un socket de dstack. Un TPM solo no alcanza: el motor le hace la pregunta de NitroTPM y un TPM común contesta que no conoce el comando. Forzar nitro-tpm en una máquina sin dispositivo TPM falla con NitroTPM is not available: the AMI needs TpmSupport=v2.0 and UEFI; en un TPM que no es NitroTPM falla cuando el TPM rechaza el comando de AWS (NitroTPM NSM request failed: TPM response code 0x143).

Cómo usa el TPM el driver nitro-tpm, y qué significa para otros usuarios del TPM en la misma VM. Un pedido a la vez por proceso. Abre /dev/tpm0, que Linux da a un proceso por vez; si otro lo tiene, espera hasta 10 segundos y recién ahí usa /dev/tpmrm0. Con /dev/tpm0, primero libera lo que dejó un proceso que murió a mitad de un pedido (un SIGKILL o el OOM killer pueden caer entre pasos): los objetos y sesiones cargados en el TPM, y los buffers de mensaje de 8 KiB con exactamente la forma que crea este driver — los índices NV de otros dueños no se tocan nunca. Sin eso, unos pocos cortes así llenan el TPM y el driver deja de andar hasta que alguien lo limpie a mano. Dos consecuencias, raras y las dos fallando cerrado:

• si dos procesos de Synsema atestan a la vez en la misma VM y uno tuvo que pasar a /dev/tpmrm0, la limpieza del otro puede borrarle el buffer a mitad del pedido: ese pedido falla con error y serve --attested lo reintenta;
• se liberan los objetos y sesiones que otra aplicación cargó por /dev/tpm0 y espera que sobrevivan entre aperturas. Las aplicaciones que usan /dev/tpmrm0 (el gestor de recursos del kernel, lo que usan hoy casi todas las herramientas de TPM) no se ven afectadas. Si algo más en la VM usa /dev/tpm0 directo, no lo corras junto al driver nitro-tpm.

Este driver está probado contra un TPM simulado, todavía no en un NitroTPM.

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 driver repetido, 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".

Qué mide cada documento§

Leé esto antes de decidir qué tiene que comprobar un cliente, porque en una VM de nube la respuesta no es la que sugiere la palabra "attestation".

• SEV-SNP en EC2 prueba que la memoria de la VM está cifrada con una clave que AWS no tiene. Su measurement cubre sólo el firmware (OVMF) y el estado inicial de las vCPUs — no el kernel, no el disco, no el binario de Synsema. Así que el program_sha adentro de su report_data lo declara un binario que nadie midió: quien opera la imagen podría cambiarlo.
• NitroTPM con una Attestable AMI mide el arranque: PCR4 es el binario de arranque (un UKI) y PCR12 su línea de comandos, que lleva el hash dm-verity de un root de sólo lectura. Eso es lo que ata el disco, y el motor que está en él, al documento. No uses PCR16 ni PCR23 como medida: root adentro de la VM puede resetearlos.
• Por eso un mismo servidor publica los dos (SYNSEMA_ATTEST=tsm,nitro-tpm, o autodetectados), atados a la misma clave: SEV-SNP para "la memoria es privada", NitroTPM para "éste es el código". Un cliente comprueba los dos — los PCR esperados los da quien construyó la AMI, el measurement SEV-SNP esperado quien conoce el firmware; el motor no da ninguno.

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:

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ó; desde v0.6.48 una de las dos compila en otra carpeta y con otro CARGO_HOME. En v0.6.57 los tres coincidieron: 56186763d1057f64dd1df721c19541112fc06fc662a81858a70e60b87f3500af. 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: desde un checkout del tag, en Linux o WSL, SYNSEMA_VERSION=<el tag> bash packages/guests/vela/tools/build.sh out.wasm da el hash publicado en cualquier carpeta (antes de v0.6.48, sólo en la ruta del runner; Windows nativo no lo reproduce) — ver 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 <el asset> --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 comprueba el servidor antes de mandarle nada. Desde Synsema es una opción de fetch (y de ws_connect):

require net("203.0.113.7")

let PROGRAM be args()[0]     -- `synsema code sha app.syn` del fuente que auditaste
let PCR4 be args()[1]        -- estos dos los da quien construyó la AMI
let PCR12 be args()[2]
let OVMF be args()[3]        -- el `measurement` SEV-SNP del firmware, de quien lo conoce

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

En una conexión TLS, fallando cerrado ante la primera duda: el handshake registra la clave del servidor sin confiar en ninguna autoridad (la firma del handshake se sigue verificando con esa clave); GET /.well-known/attestation va por esa misma conexión; su public_key_hex tiene que ser esa clave; config_sha tiene que coincidir con config y program_sha tiene que ser el tuyo (obligatorio); cada documento tiene que verificar con expect.report_data = sha256(spki ‖ program_sha ‖ config_sha) y sus measurements, cada formato de formats (obligatorio) tiene que estar, y un documento de más que no verifica también es error; un documento mock sólo se acepta si formats nombra "mock". Recién ahí sale tu request, por la misma conexión. Si algo falla el request no sale nunca y error of r dice por qué. now (segundos unix) es opcional y por defecto es el reloj del sistema, como en cualquier validación TLS. La respuesta trae attested: {program_sha, public_key_hex, formats, config}. En ws_connect(url, headers, {"attested": …}) el upgrade sale después de los chequeos, también en cada reconexión (un now explícito avanza con el tiempo transcurrido desde la primera conexión), y ws_stats(c)["attested"] dice qué verificó la última. attested y tls_pin son dos formas de fijar la clave: pasá una, y pasá un valor — nothing es error (para la validación de siempre se omite la clave). Un intermediario no pasa: no puede completar un handshake con la clave atestada.

measurements es lo que prueba el código, así que todo formato salvo mock necesita su entrada. program_sha solo es declarado: lo publica el mismo binario que se está comprobando. Un documento sin medidas esperadas prueba sólo que contestó alguna máquina de esa plataforma — cualquiera que alquile una puede atar el program_sha que esperás a su propia clave y pasar todos los demás chequeos. Por eso attested.measurements tiene que nombrar cada formato de formats salvo mock, cada uno con un mapa no vacío ({"nitro-tpm": {"pcr4": …, "pcr12": …}}); si no, la llamada es error antes de conectar nada. Para aceptar cualquier medida de un formato a propósito — por ejemplo SEV-SNP sólo para "la memoria está cifrada", con NitroTPM fijando el código — escribí "sev-snp": "any". En EC2 el measurement de SEV-SNP cubre sólo el firmware (ver Qué mide cada documento), así que son los PCR de NitroTPM los que atan el documento al código.

Contra un servidor con certificado del operador (tls_key: "operator") attested falla a propósito: la clave del canal no es la atestada. Ahí verificá la identidad a mano (abajo) y confiá en el certificado del operador como siempre. En el embebido WebAssembly (synsema-wasm-web, donde el HTTP lo hace el host) tls_pin y attested fallan cerrado: el transporte del host no puede fijar una clave ni leer la identidad por la conexión del handshake.

Los errores dicen qué chequeo falló, por ejemplo 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 <formato> document does not verify: <el motivo del verificador>, y the identity response must carry Content-Length (la identidad tiene que venir con su largo exacto para que la misma conexión pueda llevar tu request).

Lo mismo a mano, para una identidad que ya tenés (una copia que publicó el operador, un artefacto), con attestation_verify y después 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` del fuente que auditaste
let NOW be int(args()[1])             -- la hora en la que confiás, segundos unix

-- La identidad se prueba sola, así que puede venir por cualquier canal: acá, una copia que
-- publicó el operador. (Leída del servidor directo necesita el pin que todavía no tenés.)
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")

-- Recién ahora: el par TLS tiene que presentar exactamente esa clave.
let r be fetch(BASE + "/hola", {"tls_pin": id["public_key_hex"]})
print(r["json"])

tls_pin (en las opciones de fetch, y en las de ws_connect) toma la SubjectPublicKeyInfo del servidor en hex, bytes o PEM PUBLIC KEY. Reemplaza la validación contra las raíces del SO y el nombre del host por la igualdad byte a byte de la clave presentada; la firma del handshake se sigue verificando con esa clave. Otra clave rompe el handshake (tls_pin: the server public key (SPKI) does not match the pinned key); sin tls_pin nada cambia — un certificado autofirmado se rechaza por raíz desconocida, como siempre. Necesita https:///wss:// y require net para el host. Con un certificado del operador (tls_key: "operator") no fijes la clave anunciada: no es la del canal.

Desde un cliente que no es Synsema (curl, Python, Go), hacé los mismos pasos: abrí la conexión TLS sin validar el certificado pero guardando el certificado del servidor (Python: ssl.CERT_NONE y getpeercert(binary_form=True)); mandá GET /.well-known/attestation por esa misma conexión con Connection: keep-alive; exigí que su public_key_hex sea la SubjectPublicKeyInfo de ese certificado; chequeá config_sha y program_sha; verificá cada documento (con synsema run y attestation_verify, o el verificador de tu plataforma) contra sha256(spki ‖ program_sha ‖ config_sha); y recién ahí mandá tu request por esa conexión. Abrir una segunda conexión para el request deshace todo, salvo que ahí fijes la clave. 6. En CI, SYNSEMA_ATTEST=mock con una semilla fija ejercita todo el camino, y la marca mock hace imposible confundirlo con lo real.