Construí una app que corre dentro de un TEE

El ejemplo es deliberadamente chico y completamente real: un prestamista manda el score de un solicitante, el servicio responde sí o no, y nadie de afuera — incluido quien corre la máquina — llega a ver el score. Todos los comandos y todas las salidas de acá abajo salieron de una corrida en una laptop común.

Necesitás el binario y nada más:

curl -fsSL https://synsema.org/install.sh | sh

1. La forma de un servicio confidencial§

Antes de la sintaxis, la forma, porque es la parte que se suele errar. Un servicio confidencial tiene tres momentos:

1. Ingesta — llegan datos que, como operador, no tenés permitido leer. 2. Decisión — el programa calcula con ellos, dentro de la caja. 3. Publicación — sale un valor chico y deliberado, y podés decir en una oración por qué puede salir.

Si el paso 3 es difícil de decir en una oración, el diseño no está listo. El lenguaje te va a exigir esa oración.

2. Escribilo, con los datos marcados§

intent: "score one applicant inside the enclave and publish only the decision"

require serve(8080)
require attest

let CUTOFF be 620

task verdict(payload)
    let score be private(payload["score"], "applicant")
    let approved be score >= CUTOFF
    give declassify(approved, "the yes/no is what the lender asked for; the score stays inside")

serve on 8080
    route "GET /identity"
        give attestation_document()

    route "POST /decide"
        expect body {score: number}
        give {"approved": verdict(json of request)}

Dos líneas llevan toda la política. private(…, "applicant") dice de quién es el valor; declassify(…, "…") dice qué sale y por qué. attestation_document() no necesita capacidad y, corrido fuera de un servidor atestiguado, falla con un error claro — así que una ruta que sirve la identidad es honesta por construcción.

3. Correlo con la muralla levantada§

synsema serve app.syn --port 8080 --labels

Las etiquetas están apagadas en un synsema run normal, y siempre prendidas bajo serve --attested. Prenderlas explícitamente mientras desarrollás es la forma de enterarte temprano. Probá publicar el score en vez de la decisión y la respuesta nunca sale de la máquina:

{"error": "label_violation: response.score is private to applicant, the sink accepts (public);
declassify(<that value>, \"<why it may be published>\") the scalar you want to publish and build
the container outside the private branch", "status": 500}

El mensaje nombra el valor, el sumidero y los dos arreglos. Nueve de cada diez veces el correcto es el primero: el destino también tendría que haber sido privado.

Antes de distribuir, leé qué publica el programa — la lista se produce antes de que corra nada:

synsema code check app.syn --json

"declassify": [
  {"file": "app.syn", "line": 11, "column": 20,
   "reason": "the yes/no is what the lender asked for; the score stays inside"}
]

Una entrada, una oración. Esa es la revisión de seguridad de este servicio.

4. Dale una identidad§

synsema serve --attested app.syn --port 8443

Serving HTTPS on port 8443 (2 route(s))
Attested: driver=mock format=mock program_sha=d0e0701a3a80627ff0fa867ff2bf57b1d8367c5a68bc89448079b5e777ff3bc7
 — GET /.well-known/attestation

El servidor generó un par de claves P-256, le pidió a la plataforma un documento que ata sha256(spki ‖ program_sha ‖ config_sha), terminó TLS con esa misma clave y publicó el documento. Si la plataforma no hubiera respondido, no habría arrancado: no hay modo degradado al que caerse.

Lo que publica:

{"format": "…", "driver": "…", "engine": "v0.6.24",
 "public_key": "-----BEGIN PUBLIC KEY-----…", "public_key_hex": "3059301306072a8648…",
 "program_sha": "d0e0701a…", "config_sha": "c684dde2…",
 "config": {"ceiling": "unbounded", "engine": "v0.6.24", "labels": true,
            "profile": "native", "tls_key": "attested"},
 "document": "hEShATgioFkGwqlpbW9kdWxlX2lka2ktbW9jay1l…"}

Fijate en config. Es el modo, no solo el programa: el techo, que las etiquetas estaban prendidas, el perfil, y que la clave TLS es la atestiguada y no un certificado de operador. Su hash está dentro del payload firmado, así que la configuración no se puede atestiguar dura y servir blanda.

Dos reglas para tener en cuenta acá: --attested y --watch son mutuamente excluyentes (un reinicio cambiaría la identidad debajo de clientes vivos), y el programa no puede declarar /.well-known/attestation, /openapi.json, /docs, /llms.txt, /sitemap.xml ni /robots.txt — el servidor se niega a arrancar en vez de dejar que una quede tapada en silencio.

5. El cliente, que es de lo que se trata§

Un servicio confidencial que nadie verifica es un servicio confidencial de nombre. El verificador es un programa en el mismo lenguaje, y no necesita capacidad ni red más allá de traer el documento:

let seen be json_decode(read_file("identity.json"))

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

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

print("pcr0       " + v["measurements"]["pcr0"])
print("user_data  " + decode(v["user_data"], "hex"))
print("recomputed " + decode(bound, "hex"))
print("it is the code it says it is: " + text(v["user_data"] == bound))
print("labels on: " + text(seen["config"]["labels"]))

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

En producción agregá "expect": {"measurements": {"pcr0": "<el hex que publicaste>"}}, que compara y falla cerrado ante una diferencia, y fijá la clave pública después del veredicto. opts.now es obligatorio a propósito: la ventana de validez se verifica contra una marca de tiempo que elige el verificador, no contra un reloj que controla el anfitrión.

Recién entonces, mandá los datos:

curl -X POST https://your-enclave/decide -d '{"score": 710}'
{"approved": true}

curl -X POST https://your-enclave/decide -d '{"score": 480}'
{"approved": false}

Dos pedidos, dos bits afuera. El score nunca apareció en una respuesta, en una línea de log ni en una consola.

6. Mantenelo honesto en CI§

Todo el camino — documento, clave TLS, verificación, el recálculo del cliente — corre en cualquier máquina con el driver de desarrollo:

SYNSEMA_ATTEST=mock SYNSEMA_ATTEST_MOCK_SEED=ci synsema serve --attested app.syn --port 8443

synsema: warning: SYNSEMA_ATTEST=mock: documents are FORGEABLE (deterministic test key),
never trust them outside CI

Lo dice por stderr, anuncia format: "mock" y cada documento que produce lleva "mock": true — así que un documento de desarrollo no se puede confundir con el de una plataforma en un log, en un cliente ni en una captura de pantalla. Nunca se elige solo: en Linux el driver se detecta de la máquina, y el de desarrollo aparece únicamente cuando lo pedís por nombre.

7. Antes de llamarlo confidencial§

1. Revisá el motor que estás distribuyendo. gh attestation verify synsema-linux-x86_64 --repo kitecosmic/synsema responde con el workflow, el commit y el tag que produjeron esos bytes exactos. Atestiguar un programa construido por un motor de origen desconocido atestigua la mitad equivocada. 2. Corré con las etiquetas prendidas y leé la lista de declassify; asegurate de que cada oración sea una que le mandarías a un cliente, porque en efecto se la estás mandando. 3. serve --attested, sin --watch. Decidí el TLS: la clave atestiguada (el cliente la fija) o tu propio certificado (no debe fijarla). 4. Publicá el program_sha y las mediciones esperadas donde tus usuarios las van a buscar — una página de estado, un repositorio, el contrato. 5. Dale a la contraparte las veinte líneas del verificador de arriba. Si no las va a correr, la propiedad que construiste no es la que está comprando.

La parte del lenguaje termina acá: lo que queda es elegir el hardware donde corre la caja, y esa elección es otra conversación, sobre precio, región y operación. El manual tiene los detalles — Atestación, Etiquetas, Capacidades — y cada página también es Markdown: agregale .md a la URL.