# Construí una app que corre dentro de un TEE

> Un recorrido, del archivo vacío a un servicio cuyo cliente verifica el código antes de mandar nada — etiquetas prendidas, una identidad atestiguada y las mismas comprobaciones corriendo en CI con el driver de desarrollo.

Published 2026-09-20 · https://synsema.org/es/blog/build-an-app-that-runs-inside-a-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:

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

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

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

```sh
synsema code check app.syn --json
```

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

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

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

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

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

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

```sh
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](https://synsema.dev/es/0.6.x/24-attestation),
[Etiquetas](https://synsema.dev/es/0.6.x/23-labels),
[Capacidades](https://synsema.dev/es/0.6.x/20-capabilities) — y cada página también es Markdown:
agregale `.md` a la URL.