# The best language for a TEE > A trusted execution environment hides your data from the operator. It does not stop your own code from leaking it, and it does not tell the client what is running inside. Synsema does both — information-flow labels and attestation are part of the language, not a library. Published 2026-09-20 · https://synsema.org/blog/the-best-language-for-a-tee A TEE — AWS Nitro Enclaves, Intel TDX, AMD SEV-SNP, dstack — gives you one thing: a box whose memory the host cannot read. That is a hardware property, and it is genuinely hard to get any other way. It is also only a third of the problem. Two jobs are left, and both are yours: 1. **The code inside the box must not leak the data.** The enclave does not care. If your program writes a customer's balance to stdout, into a log line, or into an HTTP response, the hardware hands it over politely. 2. **The client must be able to tell what is in the box before sending anything.** Otherwise you have moved the trust from "trust the operator with the data" to "trust the operator's claim about the binary", which is the same trust with extra steps. In C, Rust or Go, both are engineering projects. The first is a code review you repeat forever; the second is a few hundred lines of CBOR, COSE and X.509 per platform, on both sides of the wire. In Synsema they are language features, and that is the whole argument of this post. ## The first wall: the data cannot leave by accident Capabilities already answer *may this program touch the network at all?* — deny by default, declared in the source. Labels answer the next question: *may **this value** leave?* ```synsema let score be private(payload["score"], "applicant") let approved be score >= CUTOFF give {"approved": approved} ``` That program does not run. The engine tracks the label through the comparison and refuses the response: ``` label_violation: response.approved is private to applicant, the sink accepts (public); declassify(, "") the scalar you want to publish ``` The fix is to say what you are publishing and why — in the source, on the record: ```synsema give declassify(approved, "the yes/no is what the lender asked for; the score stays inside") ``` Every operation propagates the union of its operands' labels: arithmetic, text, field reads, `json_encode`, hashes, and the branches taken *because* of a private value. Public sinks — the HTTP response, stdout, files, the network, databases, processes — refuse two things before the effect happens: a labelled value in any argument at any depth, and **the call itself** when it sits under a branch that depended on private data. That second rule is the one people underestimate: the number of lines you print is not redactable, so one `print` per iteration of a loop over a secret spells the secret out by line count to whoever reads the console — and in an enclave, that reader is the operator, standing outside. Reviewing this is not a reading exercise either. Every `declassify` is listed, with its line and its reason, before anything runs: ``` $ 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} ] } ``` That list *is* the review. If it has one entry and you agree with the sentence in it, the program publishes one thing. ## The second wall: the client checks the code before it sends anything Attestation is five builtins. `attest(opts)` asks the platform for a document binding a measurement of the running code to 64 bytes you choose. `attest_key(purpose)` derives a key from that measurement, so another build cannot read what this one sealed. `attestation_document()` and `attestation_key()` are the identity of the server you are inside — and that key is **sealed**: `reveal()` refuses it even when the program holds the `reveal` capability, because exporting the key that anchors both the TLS channel and the document would void the attestation. The fifth is the client side, and it is pure — no capability, no network: ```synsema let v be attestation_verify(bytes(seen["document"], "base64"), {"format": seen["format"], "now": floor(now()), "expect": {"measurements": {"pcr0": PINNED}}}) ``` `opts.now` is **mandatory**. Inside an enclave there is no trustworthy clock, and a verdict has to be reproducible, so the certificate-validity window is checked against the timestamp you pass — never against whatever the host says the time is. That is the kind of decision that tells you whether a confidential-computing feature was designed or bolted on. What it checks, failing closed at the first doubt: the payload's exact structure and types; that the bundle's root is, by SHA-256 of its DER, the AWS Nitro PKI root pinned inside the engine; the full X.509 chain (ECDSA-SHA384 over P-384, issuer and subject byte for byte, validity on *every* certificate); and last the COSE signature with the leaf's key. `tdx`, `sgx` and `sev-snp` documents come back as an explicit error rather than an optimistic `true` — `attest` still *produces* those formats, so an enclave emits what its platform gives it, but this release will not pretend to have verified a chain it does not have collateral for. ## `serve --attested`: an identity, not a flag ```sh synsema serve --attested app.syn ``` At startup the server generates a P-256 keypair, asks the platform for a document binding `sha256(spki ‖ program_sha ‖ config_sha)`, and publishes it at `GET /.well-known/attestation`. **If the platform does not answer, the server does not start.** There is no degraded mode, because a confidential service that silently falls back to an ordinary one is worse than no attestation at all. Three consequences worth knowing before you write the routes: - **Labels are on, always.** `--attested` turns them on for every interpreter in the process and it cannot be switched off. An attested deployment that could publish its inputs would be attesting the wrong property. - **TLS is the same key.** Without an operator certificate, the channel is served with the key from the document, so a client that pins it knows the TLS peer *is* the attested code. With your own certificate the published identity says `tls_key: "operator"` and the client must not pin it — the document says which case it is, so the client never has to guess. - **The configuration is signed too.** `config` carries the ceiling, whether labels were on, the profile and where the TLS key came from; its hash is inside the signed `user_data`. An operator cannot attest a hardened configuration and then serve a loose one. Here is what a client actually does with it — this is the program, and this is its output against a server running with the development driver: ```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 ``` Both sides of that exchange are one language and one binary. No SDK on the server, no verification library on the client, no second toolchain for the enclave. ## When the verifier is not online: `run --attest` Sometimes the counterparty does not talk to your service; it reads an artefact, later, and has to be able to check it offline. That is a different job and it has its own shape: ```sh synsema run --attest report.syn ``` The program prints what it prints, then one JSON line tying program, input, output and configuration together: ```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` implies `--deterministic`: the pure profile and a stdout-only ceiling, so the same program and the same input give the same bytes, and two enclaves — or a contract — can compare a `state_root`. Combining it with flags that would break that promise is a usage error with the reason, not a silent downgrade. And `steps` is deliberately **not** part of what gets signed, and is `null` whenever the run touched a private value: the interpreter's step counter is linear in what the program walked, so after a loop whose condition depended on a secret it *is* the secret with arithmetic on top. ## The rest of what an enclave needs, already in the box - **`groth16_verify(vk, proof, public_inputs)`** — Groth16 over BN254, taking snarkjs's files as they come. An enclave can accept untrusted input with a proof attached instead of trusting an oracle. Pure, no capability. An invalid-but-well-formed proof returns `false`; a dubious format is an error. - **`laplace_noise` / `gaussian_noise`** — differential-privacy noise that is deterministic in its seed. That is the design: an enclave has no trustworthy entropy, and the same query over the same state returning the same noise is what stops a caller from averaging the noise away. - **Total parsers.** `json_decode(text, default)`, `number(value, default)`, `aes_gcm_decrypt(key, nonce, ct, aad, default)` and friends return a fallback instead of raising — because an error *caused by* private data cannot be caught (whether the operation failed is exactly the bit the rule exists to hide), and validating untrusted input is precisely an enclave's job. - **Sealed secrets.** A value from `secret("KEY")` is not a string: it can authenticate a request or sign, and everything else refuses or redacts. The key the model or the prompt cannot read is the key the prompt cannot leak. - **`invariant`** conditions evaluated per state transition, run by the guest adapters on every entry point. ## What you would otherwise write by hand | The job | Elsewhere | Synsema | |---|---|---| | Stop the code leaking the data | code review, forever | `private` / `declassify`, enforced | | List what the program publishes | grep, and hope | `synsema code check --json` | | Get a document from the platform | a vendor SDK per platform | `attest()` | | Serve it with the channel's key | wire NSM + TLS yourself | `serve --attested` | | Verify it as a client | CBOR + COSE + X.509 | `attestation_verify()` | | A reproducible result to compare | a build system | `run --attest` | | Keys another build cannot read | a KMS integration | `attest_key(purpose)` | Chain-anchored deployments are one instance of this, not the whole story: the [Vela](https://synsema.dev/en/0.6.x/73-vela) guest runs with labels always on and the chain as the public sink, and the same program, unchanged, is a clean room in front of two banks, a scoring service a lender cannot read, or a private matching engine. The language does not know which one you are building. One binary, Apache 2.0: `curl -fsSL https://synsema.org/install.sh | sh`. The manual is at [Attestation](https://synsema.dev/en/0.6.x/24-attestation) and [Information-flow labels](https://synsema.dev/en/0.6.x/23-labels) — and the next post walks through building one of these end to end.