# El mejor lenguaje para un TEE

> Un entorno de ejecución confiable esconde tus datos del operador. No evita que tu propio código los filtre, ni le dice al cliente qué está corriendo adentro. Synsema hace las dos cosas — las etiquetas de flujo de información y la atestación son parte del lenguaje, no una biblioteca.

Published 2026-09-20 · https://synsema.org/es/blog/the-best-language-for-a-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**?*

```synsema
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:

```synsema
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:

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

```sh
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:

```synsema
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:

```sh
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:

```json
{"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

| El trabajo | En otro lado | Synsema |
|---|---|---|
| Que el código no filtre los datos | revisión de código, para siempre | `private` / `declassify`, aplicado |
| Listar qué publica el programa | grep, y fe | `synsema code check --json` |
| Conseguir un documento de la plataforma | un SDK por plataforma | `attest()` |
| Servirlo con la clave del canal | cablear NSM + TLS a mano | `serve --attested` |
| Verificarlo como cliente | CBOR + COSE + X.509 | `attestation_verify()` |
| Un resultado reproducible para comparar | un sistema de build | `run --attest` |
| Claves que otra construcción no puede leer | una integración con un KMS | `attest_key(purpose)` |

Los despliegues anclados a una cadena son un caso de esto, no toda la historia: el guest de
[Vela](https://synsema.dev/es/0.6.x/73-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](https://synsema.dev/es/0.6.x/24-attestation) y
[Etiquetas de flujo de información](https://synsema.dev/es/0.6.x/23-labels) — y la próxima entrada
recorre la construcción de uno de estos de punta a punta.