Capabilities & Security

Information-flow labels

Capabilities answer may this program touch the network at all? Labels answer may this value leave? You mark a value as belonging to a principal, and the engine carries that mark through every operation — arithmetic, text, field reads, json_encode, hashes, and the branches taken because of it — and refuses to let it reach a public sink unless you say, in writing and on the record, why it may be published.

You want this when the operator runs the code but must not read the data: a confidential deployment (TEE/enclave), a multi-tenant service that must not cross tenants, anything where "we are careful" is not an acceptable answer.

Turning it on§

Off by default. synsema run app.syn behaves exactly as it always has, down to the step counter.

synsema run  --labels app.syn
synsema test --labels app.test.syn
synsema serve --labels app.syn
synsema serve --attested app.syn    # labels are ALWAYS on here

With labels off, private(…) raises the moment it is called — private: labels are off; run with --labels or serve --attested. Note called, not loaded: synsema check passes, and a private(…) inside a branch that never runs never fires. If the program must refuse to start without labels, call one at the top.

Inside a guest adapter (Vela) labels are always on too — see Vela.

The four builtins§

let balance be private(1200, "app")        -- this belongs to the principal "app"
let doubled be balance * 2                 -- private(app) — every operation propagates
print(label_of(doubled))                   -- private(app)  ← redacted, see below
print(is_private(doubled))                 -- private(app)  ← redacted too
let code be declassify("insufficient", "the outcome code is public on-chain")
print(code)                                -- insufficient

private(value, "principal") — mark a value. The principal is a text literal written at the call: a computed principal is refused, because choosing the principal from private data would be a channel of its own. Over a list or map it makes a private copy, so a public alias someone already holds keeps seeing the public original.
declassify(value, "reason") — publish it, on the record. The reason is mandatory and public. Every declassify is logged with its source line and listed by synsema code check --json before anything runs, which is what an auditor reads.
declassify(value, "reason", [...]) — narrow instead of publishing. The third argument must be a subset of what the value is already private to, because declassify may only narrow. A value private to ["app", "bank"] can come out private to ["bank"] alone; asking a value private to "app" for ["bank"] is widening, and the engine refuses it by name (cannot widen a label — [bank] is not a subset of what this value is private to).
label_of(v) → the principals; is_private(v) → bool. Both answers are as private as what you asked about. If they came back public they would be an oracle: one bit per question, and the branch you take on the answer would be a public branch on private data. Use them to decide inside the program, not to report.

Narrowing, in one example:

let joint be private(private(500, "app"), "bank")   -- private to both
let only_bank be declassify(joint, "the bank settles it", ["bank"])
print(declassify(text(label_of(only_bank)), "probe"))   -- [bank]

These names, plus print, are protected: a program cannot bind them to something callable. Redefining one would silently un-label its own sources and mislead the audit listing.

labels.syn

-- Doc example: information-flow labels. Runs under `synsema test --labels` ONLY —
-- with labels off `private(...)` is a load error, which is the point: a program that
-- needs the second wall says so, instead of silently running without it.
intent: "doc example: information-flow labels"

let BALANCE be private(1200, "app")

task doubled()
    -- Every operation carries the union of its operands' labels.
    give BALANCE * 2

task marking_a_list_copies_it()
    -- `private` over a container gives a PRIVATE COPY: the public alias keeps
    -- seeing the public original, so marking cannot retroactively hide what
    -- someone else already holds.
    let public_rows be [1, 2, 3]
    let secret_rows be private(public_rows, "app")
    give public_rows[0]

task parse_untrusted(payload)
    -- An error CAUSED by private data is not catchable (whether an operation
    -- failed is exactly the bit labels exist to hide), so `try`/`recover` is not
    -- the answer for input an enclave receives from anyone. The total variant is:
    -- no error, so no bit.
    let d be json_decode(payload, nothing)
    when d == nothing
        give "malformed"
    give "ok"

task published()
    -- The only way out is on the record: the reason is mandatory and public, and
    -- `synsema code check --json` lists every declassify before anything runs.
    give declassify(BALANCE > 0, "whether the account is open is public")

test "labels propagate through arithmetic"
    assert(is_private(doubled()))
    assert_eq(text(declassify(doubled(), "doc example")), "2400")

test "the answer about a private value is as private as the value"
    -- `is_private`/`label_of` are NOT public oracles: one bit per question would
    -- be a channel of its own.
    assert(is_private(is_private(BALANCE)))
    assert(is_private(label_of(BALANCE)))

test "marking a container copies it"
    assert_eq(marking_a_list_copies_it(), 1)

test "untrusted input is parsed without exceptions"
    assert_eq(parse_untrusted("{\"a\": 1}"), "ok")
    assert_eq(parse_untrusted("not json at all"), "malformed")

test "declassify is the only way out, and it is on the record"
    assert_eq(published(), true)

test "text() does not sanitise: it is still the value, and still private"
    -- The redaction happens at the SINK, not in the conversion. Passing a private value through
    -- `text()` does not make it safe to hand around.
    assert_eq(declassify(is_private(text(BALANCE)), "doc example"), true)
    assert_eq(declassify(text(BALANCE), "doc example"), "1200")

test "a private value inside a concatenation takes the WHOLE string with it"
    -- At a public sink the entire line is replaced by `private(app)` — the prefix goes too.
    let line be "balance: " + text(BALANCE)
    assert_eq(declassify(is_private(line), "doc example"), true)
    assert_eq(declassify(line, "doc example"), "balance: 1200")

test "the third argument of declassify narrows WITHIN the value's own principals"
    let joint be private(private(500, "app"), "bank")
    let only_bank be declassify(joint, "the bank settles it", ["bank"])
    assert_eq(declassify(text(label_of(only_bank)), "doc example"), "[bank]")

What a sink is§

Every operation carries the union of its operands' labels. A public sink is anywhere a value leaves the program's own memory: the HTTP response and every stream, the on-chain result of a guest, a file, an outbound request, another interpreter (parallel_map, run_program, cron, the bus, the swarm). A private value at a sink is a label_violation — the request fails, and the message names the path the value took, never the value.

Two that surprise people:

Branching on a private value makes the branch private. Anything the branch does carries the label, because which branch ran is the secret. print/show/log inside a private branch are refused: stdout is public and the number of lines is not redacted, so one line per iteration spells the data out.
Printing a private value is fine — it comes out as private(app). The redaction is the answer; the refusal is for the branch.
text(v) does not sanitise. The redaction happens at the sink, nowhere else: text returns the real content, still private. is_private(text(v)) is true, and declassify(text(v), …) gives the value back in full — passing a value through text does not make it safe to hand around.
A private value inside a concatenation takes the whole string with it. print("balance: " + text(v)) prints private(app), not balance: private(app): the prefix is part of a private text now, and the sink replaces the whole thing.

Errors that cannot be caught§

An error born under a private branch, or caused by private data, is not catchable: try/recover re-propagates it and assert_error does not absorb it. Whether an operation failed is exactly the bit labels exist to hide — xs[private_index], 1 / (secret - i) — and a recover that swallowed it would let the loop before it leave the secret in a public variable.

So how do you validate untrusted input, which an enclave receives from anyone? Not by raising at all. The operations that parse external input have a total form that returns a fallback:

let d be json_decode(payload, nothing)              -- no error, so no bit
let n be number(field, nothing)
let clear be aes_gcm_decrypt(k, nonce, ct, aad, nothing)

Also decimal, float, toml_parse, abi_decode, bech32_decode, rlp_decode. The fallback is evaluated eagerly (an effect inside it fires on the happy path too) and it never swallows a label violation — that would be a try/recover in disguise.

What leaves the process§

A redacted error says private(app) and nothing else — no file:line:column. If the secret chooses which of N sites fails, the location is log₂(N) bits. The principals named are the ones the program declares, never the ones of that particular value: naming the value's own was a channel, since in a multi-tenant deployment the principal is the tenant.

A label violation also ends the whole synsema test --labels run, with one outcome naming the violation, rather than a ✗ on that block with the suite carrying on — eight blocks each probing one bit and the column of ✓/✗ spells the byte. An ordinary failure is still a per-block verdict.

Limits, stated§

Termination is one bit per run, and a server run is one request. A run the checker stopped tells an observer that it stopped. Under serve the caller chooses how many runs to make, so it is one bit per request, without a ceiling: eight public requests recover a value by binary search. If a request's outcome must not depend on private data, do not let a private branch decide whether it fails.
Progress. Effects performed before the stop did happen. The engine withholds buffered output and rolls back what the request wrote to the shared state_* store — both live in its own memory — but a file or an outbound call it cannot undo.
Timing and resource use are not modelled at all.
Crossing into another interpreter refuses, deliberately: the channel does carry labels, but what a worker may do with a private value is not yet specified, and the alternative it replaced was worse (the worker got the value stripped and did the effect in the clear while the result came back labelled, so the leak looked tracked).

Next§

Labels keep the data in. Attestation is the other half: proving to a remote party which code is holding it.