Sabline 8.6.0

Security policy

Sabline takes "you can trust code you didn't write" seriously - that includes trusting the compiler itself. THREAT_MODEL.md says what is and is not defended against; this file says how to report, what is promised in return, and how to check that what you downloaded is what was released.

Reporting a vulnerability #

Please do NOT open a public issue for security problems. Instead, write to security@sabline.dev, or use GitHub's private reporting: Security tab -> Report a vulnerability on this repository. You will get a response within 48 hours - an acknowledgement that the report arrived and is being looked at, not necessarily a fix. This is a single-maintainer project (SUPPORT.md); the 48-hour promise is for the first reply, and a fix to a soundness or sandbox report is promised within a week (below).

In scope: anything that makes Sabline's guarantees lie - an effect the checker misses, a "proven" promise that can actually break at runtime, a way past --allow, a sandbox escape through the playground, or unsafe behavior in fetch / read_file / write_file. From 3.4 also: a way into the HTTP door without its token, a way past either door's --max-allow, the token appearing in a log, an error message, a process argument or a program's environment, and a changed MCP tool description that sabline mcp-verify passes. From 4.0 also: a run through either door that gets more time or memory than its operator's --max-timeout or --max-memory-mb, and a change to a repository's code that needs more than its sabline.capabilities declares while sabline capabilities check passes it.

The three guarantees, and which findings get a CVE #

Sabline makes three promises a person relies on to run code they have not read. A report that breaks one is a security report.

  • Goal A - Soundness. A promise Sabline reports "proven" never breaks at run time. If check, proofs, explain, audit or the library marks a requires/ensures/invariant proven and a run then violates it, Goal A is broken.
  • Goal B - Honesty. A program's declared effects, and the audit built from them, name everything it can do to the outside world - the transitive effect rule (SPEC.md 7). If a program performs an effect no signature on its call graph declares, Goal B is broken.
  • Goal C - Confinement. No effect outside the operator's budget happens, whatever the source claims. If a program reads a file, reaches a host, reads the environment, calls Python or otherwise acts outside --allow and carries on, Goal C is broken.

A finding against Goal A or Goal C gets a CVE requested. Those are the two guarantees a person leans on when they run unread code: that a proof is not a lie, and that the budget holds. A report that establishes one is treated as a security issue, fixed within a week, credited by name, and a repository security advisory with a CVE is drafted for it (RELEASING.md says how the release workflow prepares the request).

Goal B findings are fixed too, but the audit is documented as reading a program's text, not running it (THREAT_MODEL.md): it describes what a program declares, and the budget - Goal C - is the boundary that holds regardless. A Goal B finding that also lets a program escape its budget is a Goal C finding, and gets the CVE.

What is not a Goal A/B/C finding is anything the "Known open" table in THREAT_MODEL.md lists as a stated limit - a granted ffi module's behaviour, native code inside one, a timing channel, a secret arriving outside the two builtins, the absence of OS confinement. Those are documented as not defended; a report of one is welcome as a documentation or hardening issue, not a broken guarantee.

Soundness reports are security reports #

If the prover claims something is proven and you can make it false at runtime, that is a vulnerability in this language's core promise (Goal A above). These reports get top priority.

Standing challenge #

Anyone who does either of these is credited by name in CHANGELOG.md and in HALL_OF_FAME.md, and the report is treated as a security issue and fixed within a week:

  1. Make Sabline report "proven" (in sabline check, sabline proofs, sabline explain, sabline audit or the library) for a promise that is false at runtime. A requires, ensures or invariant that the compiler marks proven and that a run under --no-native or with native code then violates, or a division or list read the compiler passed that then fails with E403 or E602 without a runtime-check warning having been issued.

  2. Escape io. A program run with sabline program.vel (which grants io and nothing else from 5.0), with --allow io, or with sabline.run(source, allow={"io"}) or allow=None, that reads or writes a file, reaches the network, reads the environment, or calls a Python module - including one outside a named ffi: list - and carries on. args() and read_line() do not count: io is the console, and THREAT_MODEL.md says so. Since 3.0 env is its own effect, so env() under io alone is a refusal like the rest.

There is no money. There is credit, in the file every reader sees, and a fix within the week, recorded in the changelog with what was found and what was wrong. Report through the private channel above so the fix ships before the details do; the credit is public either way.

Resolved advisories #

  • == on two maps, lists or records was a constant to the prover (challenge #1, Goal A), affecting 2.6 through 8.2.1, fixed in 8.3.0: a comparison of two values the prover holds as its own objects - two maps, lists of lists, lists of Bool or Text, a map and put of it, records with a list or Float field - was Python's comparison of those objects, so a branch on it looked unreachable and a promise past it was reported proven, and broke when it ran. The interpreter checks every promise and no such function is native code, so each break stopped with E601; the report and an attestation's proven count were false. Those comparisons are now left to runtime. Found writing a test for a surviving mutant. See advisory-prover-compare.md.
  • Negating the smallest whole number was not range-checked (challenge #1, Goal A), affecting 2.14 through 8.1.1, fixed in 8.2.0: -n of -9223372036854775808 left the 64-bit range without E407, and a function whose ensures about -n was proven ran as native code and returned a value that broke it. Unary minus, and the smallest number divided by -1, now stop with E407 in both engines. Found by the 8.2 corpus of false promises. See advisory-int-negation.md.
  • Words after -- were read as Sabline's own flags (Goal C), affecting 5.0.0 through 8.1.1, fixed in 8.2.0: sabline program.vel -- --allow all granted every effect to a run whose operator named no budget, and -- --receipt x wrote a file. On a run, -- now ends Sabline's flags and everything after it is the program's args(). Found by the 8.2 self-budget suite. See advisory-cli-double-dash.md.
  • A program given to the library as text imported from the temp directory (Goal C), affecting 2.52 through 8.1.1, fixed in 8.2.0: its imports resolved in the system temp directory first, so a std.vel another local user planted in /tmp ran in place of the standard library's, and the audit reported it. The text is now written into a directory of its own. Found by the 8.2 self-budget suite. See advisory-source-temp-import.md.
  • A per-user proof cache entry was believed (challenge #1, Goal A), affecting 7.1.2 through 8.1.0, fixed in 8.1.1: a process running as the same user, or an XDG_CACHE_HOME or LOCALAPPDATA pointed at a directory it chose, could write a cache entry with the real proof key that made a false ensures report "proven" and, compiled to native code, run unchecked. Nothing in the cache is believed now: a promise is proven only when the process reporting on it or running it proved it. Reported by two independent external assessments. See advisory-proof-cache-2.md.
  • Prover names a program could write (challenge #1, Goal A), affecting 0.9 through 8.0.0, fixed in 8.1.0: a parameter named like a name the prover made up for itself - __g_result_1 for the result of a call to g - was the same Z3 value, and a false ensures was reported proven and, compiled to native code, went unenforced. The prover's names now use characters no identifier can. See advisory-prover-names.md.
  • An import that read a file and quoted it (Goal C), affecting 0.16 through 8.0.0, fixed in 8.1.0: a program sent to the HTTP door, the MCP server or a platform's sabline.audit could import any readable file, and the error named its first token. Such an error now shows nothing of the file, and the doors refuse an import outside the directory they serve (E515). See advisory-import-read.md.
  • Proof cache poisoning (challenge #1), affecting 2.29 through 7.1.1, fixed in 7.1.2: a ./.sabline/proofs.json shipped with an untrusted program could make a false ensures report "proven" and go unenforced at run time. The proof cache now lives only in a per-user directory and a project-local ./.sabline/ is ignored. See advisory-proof-cache.md and THREAT_MODEL.md.

What is not in scope of the challenge, because it is documented as not defended: anything a granted ffi module does, resource use below a limit, the meaning of printed text, the memory cap on macOS (where RLIMIT_AS is best-effort; it is enforced on Linux and, since 3.1, on Windows through a job object), and programs not written in Sabline.

Verifying a download #

Every artifact of a release from v2.63 onward is signed keylessly through sigstore by the release workflow itself, so the signature proves the file was built by .github/workflows/release.yml in this repository. Which run of it the certificate names changed at 7.2.0:

  • Up to 7.1.2 pushing a tag started a release, and the identity is the tag's. For a release vX.Y:

    Text
    https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/tags/vX.Y

  • From 7.2.0 no tag starts a release. The workflow runs on main once the tests pass there, tags the commit itself and signs in that same run (RELEASING.md), so the identity names main:

    Text
    https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/heads/main

    That identity says "the release workflow, on main", not which release. The certificate also records the commit the run was on and the event that started it; checking both ties a file to the tagged commit and to a real release (a release is started only by workflow_run; a dry run by hand is workflow_dispatch):

    Text
    sigstore verify github \
  --bundle sabline_lang-7.2.0-py3-none-any.whl.sigstore.json \
  --cert-identity https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/heads/main \
  --trigger workflow_run \
  --sha "$(git rev-parse 'v7.2.0^{commit}')" \
  sabline_lang-7.2.0-py3-none-any.whl

    With cosign, add --certificate-github-workflow-trigger workflow_run and --certificate-github-workflow-sha <that commit>.

The OIDC issuer is https://token.actions.githubusercontent.com either way. The commands below name older releases; for 7.2.0 and later give the main identity instead, with the trigger and the commit.

The wheel and the sdist carry a sigstore bundle (<file>.sigstore.json, holding the signature and the certificate together). With pip install sigstore:

Text
sigstore verify identity \
  --bundle sabline_lang-2.63.0-py3-none-any.whl.sigstore.json \
  --cert-identity https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/tags/v2.63 \
  --cert-oidc-issuer https://token.actions.githubusercontent.com \
  sabline_lang-2.63.0-py3-none-any.whl

The three executables and sabline.mcpb carry a detached signature (.sig), the certificate (.pem) and the same bundle (.sigstore.json). With cosign:

Text
cosign verify-blob sabline-linux \
  --bundle sabline-linux.sigstore.json \
  --certificate-identity https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/tags/v2.63 \
  --certificate-oidc-issuer https://token.actions.githubusercontent.com

or, with the detached files:

Text
cosign verify-blob sabline-linux \
  --signature sabline-linux.sig \
  --certificate sabline-linux.pem \
  --certificate-identity https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/tags/v2.63 \
  --certificate-oidc-issuer https://token.actions.githubusercontent.com

The MCP tool manifest (from 3.4). sabline-mcp-tools-X.Y.Z.json lists every tool the MCP server in the wheel offers, with the sha256 of its description and of its input schema, and is signed like the wheel (sabline-mcp-tools-X.Y.Z.json.sigstore.json). sabline mcp-verify checks that signature against the identity above and then the server your MCP client runs against the manifest, and names every tool whose description or schema differs:

Text
pip install sigstore
sabline mcp-verify sabline-mcp-tools-3.4.0.json -- python -m sabline_mcp

EMBEDDING.md says what it does and does not tell you. The signature can also be checked on its own with the sigstore verify identity command above, naming the manifest and its bundle.

An attestation of one example program (from 4.2). sabline-attestation-X.Y.Z.intoto.json is the in-toto Statement sabline attest examples/effects.vel writes at the tagged commit, and the release workflow signs it twice as a DSSE envelope, keylessly: with cosign (sabline-attestation-X.Y.Z.cosign.sigstore.json) and with sigstore-python (sabline-attestation-X.Y.Z.sigstore-python.sigstore.json), verifying both before it attaches them. With examples/effects.vel from the tagged source:

Text
cosign verify-blob-attestation \
  --bundle sabline-attestation-8.3.0.cosign.sigstore.json \
  --type https://velaris-lang.dev/capability/v1 \
  --certificate-identity https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/heads/main \
  --certificate-oidc-issuer https://token.actions.githubusercontent.com \
  examples/effects.vel

It fails when the file is not the one the Statement names, by digest. What the Statement says, and what it does not, is in EMBEDDING.md.

A receipt of one run of it (from 8.1). sabline-receipt-X.Y.Z.intoto.json is the sabline.receipt/1 Statement sabline examples/effects.vel --receipt writes in the release workflow, for a run under the budget the example's audit names, with the same subjects as the attestation. It is signed the same two ways and verified before it is attached. With the same examples/effects.vel:

Text
cosign verify-blob-attestation \
  --bundle sabline-receipt-8.3.0.cosign.sigstore.json \
  --type https://velaris-lang.dev/receipt/v1 \
  --certificate-identity https://github.com/gowrishankar-infra/sabline-lang/.github/workflows/release.yml@refs/heads/main \
  --certificate-oidc-issuer https://token.actions.githubusercontent.com \
  examples/effects.vel

Which predicate type a Statement names (8.3). From 8.3.0 the attestation and the receipt name their types on sabline.dev, a domain this project holds: https://velaris-lang.dev/capability/v1 and https://velaris-lang.dev/receipt/v1. Those made by 4.2.0 to 8.2.1 name the same types at the project's earlier documentation address, which now redirects to sabline.dev, and sabline verify reads both spellings as the same type. For an earlier Statement, give cosign's --type the type the Statement names, which sabline verify prints. velaris.dev was never this project's domain: it is registered to someone else, no Sabline ever wrote a type under it, and sabline verify refuses a Statement that names one, as it refuses every type Sabline does not define.

Checksums. SHA256SUMS (for the wheel, sdist, SBOM and tool manifest) and <asset>.sha256 (for each binary and the bundle) are attached too; sha256sum -c checks them. A checksum proves the file is intact, not who built it - the signature does that.

The SBOM. sabline-lang-X.Y.Z.cdx.json is a CycloneDX bill of materials of an environment holding the wheel and its optional dependencies (z3-solver, llvmlite), signed like the wheel. Sabline itself has no required dependencies.

Reproducibility. The release workflow builds the wheel twice with the same SOURCE_DATE_EPOCH and fails if the two differ. To check on your own machine at the tagged commit:

Text
SOURCE_DATE_EPOCH=$(git log -1 --format=%ct) python -m build --wheel
sha256sum dist/*.whl          # compare with SHA256SUMS on the release

What verification does not tell you: that the code is correct, or that the version you verified is the one your agent framework will import. Pin the version, and run the suites named in THREAT_MODEL.md on the machine that will run untrusted code.