Synsemadocsv0.6.xENES

Capacidades y seguridad

Etiquetas de flujo de información

Las capacidades responden ¿este programa puede tocar la red?. Las etiquetas responden ¿puede salir este valor? Marcás un valor como perteneciente a un principal, y el motor arrastra esa marca por cada operación — aritmética, texto, lectura de campos, json_encode, hashes, y las ramas que se tomaron por su causa — y se niega a dejarla llegar a un sumidero público hasta que digas, por escrito y en el registro, por qué puede publicarse.

Esto lo querés cuando el operador corre el código pero no debe leer el dato: un despliegue confidencial (TEE/enclave), un servicio multi-inquilino que no debe cruzar inquilinos, cualquier cosa donde "somos cuidadosos" no sea una respuesta aceptable.

Cómo se enciende§

Apagado por defecto. synsema run app.syn se comporta exactamente como siempre, hasta en el contador de pasos.

synsema run  --labels app.syn
synsema test --labels app.test.syn
synsema serve --labels app.syn
synsema serve --attested app.syn    # acá las etiquetas están SIEMPRE encendidas

Con las etiquetas apagadas, private(…) falla en el momento en que se lo llama — private: labels are off; run with --labels or serve --attested. Ojo: llamado, no cargado: synsema check pasa, y un private(…) dentro de una rama que nunca corre nunca dispara. Si el programa tiene que negarse a arrancar sin etiquetas, llamá una arriba de todo.

Dentro de un adaptador guest (Vela) también están siempre encendidas — ver Vela.

Los cuatro builtins§

let balance be private(1200, "app")        -- esto pertenece al principal "app"
let doubled be balance * 2                 -- private(app) — toda operación propaga
print(label_of(doubled))                   -- private(app)  ← redactado, ver abajo
print(is_private(doubled))                 -- private(app)  ← redactado también
let code be declassify("insufficient", "el código de resultado es público en la cadena")
print(code)                                -- insufficient

Acotar, en un ejemplo:

let joint be private(private(500, "app"), "bank")   -- privado a los dos
let only_bank be declassify(joint, "lo liquida el banco", ["bank"])
print(declassify(text(label_of(only_bank)), "sonda"))   -- [bank]

Estos nombres, más print, están protegidos: un programa no puede ligarlos a algo invocable. Redefinir uno desetiquetaría en silencio sus propias fuentes y engañaría al listado de auditoría.

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]")

Qué es un sumidero§

Cada operación lleva la unión de las etiquetas de sus operandos. Un sumidero público es cualquier lugar donde un valor sale de la memoria del propio programa: la respuesta HTTP y todo stream, el resultado on-chain de un guest, un archivo, una petición saliente, otro intérprete (parallel_map, run_program, cron, el bus, el enjambre). Un valor privado en un sumidero es un label_violation — el request falla, y el mensaje nombra el camino que recorrió el valor, jamás el valor.

Dos que sorprenden:

Errores que no se pueden atrapar§

Un error nacido bajo una rama privada, o causado por un dato privado, no es atrapable: try/recover lo re-propaga y assert_error no lo absorbe. Que una operación haya fallado es exactamente el bit que las etiquetas existen para esconder — xs[indice_privado], 1 / (secreto - i) — y un recover que se lo tragara dejaría que el bucle anterior deje el secreto en una variable pública.

¿Entonces cómo validás input no confiable, que es lo que un enclave recibe de cualquiera? No fallando. Las operaciones que parsean entrada externa tienen una forma total que devuelve un reemplazo:

let d be json_decode(payload, nothing)              -- sin error, así que sin bit
let n be number(field, nothing)
let claro be aes_gcm_decrypt(k, nonce, ct, aad, nothing)

También decimal, float, toml_parse, abi_decode, bech32_decode, rlp_decode. El reemplazo se evalúa siempre (un efecto adentro dispara también en el camino feliz) y nunca se traga una violación de etiquetas — eso sería un try/recover encubierto.

Qué sale del proceso§

Un error redactado dice private(app) y nada más — ni archivo:línea:columna. Si el secreto elige cuál de N sitios falla, la ubicación vale log₂(N) bits. Los principales que nombra son los que el programa declara, jamás los de ese valor en particular: nombrar los propios era un canal, porque en un despliegue multi-inquilino el principal es el inquilino.

Una violación de etiquetas además termina toda la corrida de synsema test --labels, con un solo veredicto que la nombra, en vez de un ✗ en ese bloque y la suite siguiendo — ocho bloques sondeando un bit cada uno y la columna de ✓/✗ deletrea el byte. Una falla ordinaria sigue siendo veredicto por bloque.

Límites, dichos§

Sigue§

Las etiquetas mantienen el dato adentro. La attestation es la otra mitad: probarle a un tercero remoto qué código lo está sosteniendo.