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("el saldo está saldado"))})
let seen be attestation_verify(doc["document"], {"format": doc["format"], "now": now()})
print(seen["measurements"]["pcr0"])

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:<propósito>). 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": "<hex>"}} 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.

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

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.

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.
• 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": "nitro", "driver": "nitro", "engine": "0.6.24",
 "public_key": "-----BEGIN PUBLIC KEY-----…", "public_key_hex": "<SPKI en 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 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§

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", "labels": false, "profile": "pure", "tls_key": "none"},
 "config_sha": "<hex>",
 "attestation": {"format": "nitro", "document": "<base64>", "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.

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:

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.

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