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?

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(<that value>, "<why it may be published>") the scalar you want to publish

The fix is to say what you are publishing and why — in the source, on the record:

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:

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§

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:

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:

synsema run --attest report.syn

The program prints what it prints, then one JSON line tying program, input, output and configuration together:

{"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§

Chain-anchored deployments are one instance of this, not the whole story: the 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 and Information-flow labels — and the next post walks through building one of these end to end.