El mejor lenguaje para un TEE

Un TEE — AWS Nitro Enclaves, Intel TDX, AMD SEV-SNP, dstack — te da una sola cosa: una caja cuya memoria el anfitrión no puede leer. Es una propiedad del hardware, y es genuinamente difícil de conseguir de otra manera.

También es apenas un tercio del problema. Quedan dos trabajos, y los dos son tuyos:

1. El código de adentro no debe filtrar los datos. Al enclave no le importa. Si tu programa escribe el saldo de un cliente en stdout, en una línea de log o en una respuesta HTTP, el hardware lo entrega con toda amabilidad. 2. El cliente tiene que poder saber qué hay en la caja antes de mandar nada. Si no, moviste la confianza de "confío el dato al operador" a "confío en lo que el operador dice del binario", que es la misma confianza con pasos de más.

En C, en Rust o en Go, las dos son proyectos de ingeniería. La primera es una revisión de código que repetís para siempre; la segunda, unos cientos de líneas de CBOR, COSE y X.509 por plataforma, de los dos lados del cable. En Synsema son funciones del lenguaje, y ese es todo el argumento de esta entrada.

La primera muralla: los datos no pueden salir por accidente§

Las capacidades ya responden ¿puede este programa tocar la red, siquiera? — deny-by-default, declarado en el código. Las etiquetas responden la pregunta siguiente: ¿puede salir este valor?

let score be private(payload["score"], "applicant")
let approved be score >= CUTOFF
give {"approved": approved}

Ese programa no corre. El motor sigue la etiqueta a través de la comparación y rechaza la respuesta:

label_violation: response.approved is private to applicant, the sink accepts (public);
declassify(<that value>, "<why it may be published>") the scalar you want to publish

El arreglo es decir qué estás publicando y por qué — en el código, sobre el registro:

give declassify(approved, "the yes/no is what the lender asked for; the score stays inside")

Cada operación propaga la unión de las etiquetas de sus operandos: aritmética, texto, lecturas de campo, json_encode, hashes, y las ramas tomadas a causa de un valor privado. Los sumideros públicos — la respuesta HTTP, stdout, los archivos, la red, las bases de datos, los procesos — rechazan dos cosas antes de que ocurra el efecto: un valor etiquetado en cualquier argumento a cualquier profundidad, y la llamada misma cuando está bajo una rama que dependió de datos privados. Esa segunda regla es la que se subestima: la cantidad de líneas que imprimís no es redactable, así que un print por iteración de un bucle sobre un secreto deletrea el secreto por conteo de líneas a quien lea la consola — y en un enclave, ese lector es el operador, parado afuera.

Revisar esto tampoco es un ejercicio de lectura. Cada declassify queda listado, con su línea y su motivo, antes de que corra nada:

$ synsema code check score.syn --json
{
  "ok": true,
  "declassify": [
    {"file": "score.syn", "line": 11, "column": 20,
     "reason": "the yes/no is what the lender asked for; the score stays inside",
     "to": null, "constant": false}
  ]
}

Esa lista es la revisión. Si tiene una entrada y estás de acuerdo con la oración que hay en ella, el programa publica una sola cosa.

La segunda muralla: el cliente revisa el código antes de mandar nada§

La atestación son cinco builtins. attest(opts) le pide a la plataforma un documento que ata una medición del código que corre a 64 bytes que elegís vos. attest_key(purpose) deriva una clave de esa medición, así que otra construcción no puede leer lo que selló esta. attestation_document() y attestation_key() son la identidad del servidor dentro del cual estás corriendo — y esa clave está sellada: reveal() la rechaza incluso cuando el programa tiene la capacidad reveal, porque exportar la clave que ancla a la vez el canal TLS y el documento anularía la atestación.

El quinto es el lado del cliente, y es puro — sin capacidad, sin red:

let v be attestation_verify(bytes(seen["document"], "base64"),
    {"format": seen["format"], "now": floor(now()), "expect": {"measurements": {"pcr0": PINNED}}})

opts.now es obligatorio. Dentro de un enclave no hay reloj confiable, y un veredicto tiene que ser reproducible, así que la ventana de validez de los certificados se verifica contra la marca de tiempo que pasás vos — nunca contra lo que el anfitrión diga que es la hora. Es el tipo de decisión que te dice si una función de computación confidencial fue diseñada o atornillada.

Qué verifica, fallando cerrado en la primera duda: la estructura y los tipos exactos del payload; que la raíz del bundle sea, por SHA-256 de su DER, la raíz de la PKI de AWS Nitro fijada dentro del motor; la cadena X.509 completa (ECDSA-SHA384 sobre P-384, emisor y sujeto byte por byte, validez en cada certificado); y por último la firma COSE con la clave de la hoja. Los documentos tdx, sgx y sev-snp vuelven como un error explícito en vez de un true optimista — attest sigue produciendo esos formatos, así que un enclave emite lo que su plataforma le da, pero esta versión no va a fingir que verificó una cadena para la que no tiene el material.

serve --attested: una identidad, no una bandera§

synsema serve --attested app.syn

Al arrancar, el servidor genera un par de claves 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, porque un servicio confidencial que en silencio se cae a uno común es peor que no tener atestación.

Tres consecuencias que conviene saber antes de escribir las rutas:

• Las etiquetas están prendidas, siempre. --attested las prende para todos los intérpretes del

proceso y no se pueden apagar. Un despliegue atestiguado que pudiera publicar sus entradas estaría atestiguando la propiedad equivocada.

• TLS es la misma clave. Sin un certificado de operador, el canal se sirve con la clave del

documento, así que un cliente que la fija sabe que el par TLS es el código atestiguado. Con tu propio certificado, la identidad publicada dice tls_key: "operator" y el cliente no debe fijarla — el documento dice cuál de los dos casos es, así que el cliente nunca tiene que adivinar.

• La configuración también va firmada. config lleva el techo, si las etiquetas estaban

prendidas, el perfil y de dónde salió la clave TLS; su hash está dentro del user_data firmado. Un operador no puede atestiguar una configuración endurecida y después servir una floja.

Esto es lo que hace un cliente con eso — este es el programa, y esta es su salida contra un servidor corriendo con el driver de desarrollo:

let bound be sha256(bytes(seen["public_key_hex"], "hex")
    + bytes(seen["program_sha"], "hex")
    + bytes(seen["config_sha"], "hex"))

print("it is the code it says it is: " + text(v["user_data"] == bound))
print("labels on: " + text(seen["config"]["labels"]))

user_data  f269f90cd8922005db59c98d20cc0de0331fee956da2f2f222fc0b58b6609617
recomputed f269f90cd8922005db59c98d20cc0de0331fee956da2f2f222fc0b58b6609617
it is the code it says it is: true
labels on: true

Los dos lados de ese intercambio son un lenguaje y un binario. Sin SDK en el servidor, sin biblioteca de verificación en el cliente, sin una segunda cadena de herramientas para el enclave.

Cuando el verificador no está en línea: run --attest§

A veces la contraparte no habla con tu servicio; lee un artefacto, más tarde, y tiene que poder comprobarlo sin conexión. Ese es otro trabajo y tiene su propia forma:

synsema run --attest report.syn

El programa imprime lo que imprime, y después una línea JSON que ata programa, entrada, salida y configuración:

{"output_sha":"c8edaa79…","state_root":"fa286852…","program_sha":"d58fac9d…",
 "input_sha":"e3b0c442…","config":{"ceiling":["stdout"],"labels":false,"profile":"pure"},
 "config_sha":"a3e2b58c…","attestation":{"format":"…","document":"…"}}

--attest implica --deterministic: el perfil puro y un techo de solo stdout, así que el mismo programa con la misma entrada da los mismos bytes, y dos enclaves — o un contrato — pueden comparar un state_root. Combinarlo con banderas que romperían esa promesa es un error de uso con el motivo, no una degradación silenciosa. Y steps deliberadamente no forma parte de lo que se firma, y es null cada vez que la corrida tocó un valor privado: el contador de pasos del intérprete es lineal en lo que el programa recorrió, así que después de un bucle cuya condición dependió de un secreto es el secreto con aritmética encima.

El resto de lo que un enclave necesita, ya adentro§

• groth16_verify(vk, proof, public_inputs) — Groth16 sobre BN254, tomando los archivos de

snarkjs tal como vienen. Un enclave puede aceptar entrada no confiable con una prueba adosada en vez de confiar en un oráculo. Puro, sin capacidad. Una prueba inválida pero bien formada devuelve false; un formato dudoso es un error.

• laplace_noise / gaussian_noise — ruido de privacidad diferencial determinista en su

semilla. Es el diseño: un enclave no tiene entropía confiable, y que la misma consulta sobre el mismo estado devuelva el mismo ruido es lo que impide que quien pregunta lo promedie hasta anularlo.

• Parsers totales. json_decode(text, default), number(value, default),

aes_gcm_decrypt(key, nonce, ct, aad, default) y compañía devuelven un valor de reserva en vez de levantar error — porque un error causado por datos privados no se puede atrapar (si la operación falló es justamente el bit que la regla existe para esconder), y validar entrada no confiable es precisamente el trabajo de un enclave.

• Secretos sellados. Un valor que viene de secret("KEY") no es un string: puede autenticar un

pedido o firmar, y todo lo demás se rechaza o se redacta. La clave que el modelo o el prompt no pueden leer es la clave que el prompt no puede filtrar.

• invariant, condiciones evaluadas por transición de estado, que los adaptadores guest corren

en cada punto de entrada.

Lo que escribirías a mano§

Los despliegues anclados a una cadena son un caso de esto, no toda la historia: el guest de Vela corre con las etiquetas siempre prendidas y la cadena como sumidero público, y el mismo programa, sin cambios, es una sala limpia frente a dos bancos, un servicio de scoring que el prestamista no puede leer o un motor de matching privado. El lenguaje no sabe cuál de esos estás construyendo.

Un binario, Apache 2.0: curl -fsSL https://synsema.org/install.sh | sh. El manual está en Atestación y Etiquetas de flujo de información — y la próxima entrada recorre la construcción de uno de estos de punta a punta.