Velaris 8.5.0

Changelog: 8.x: 8.5 to 8.4

Every release of this major version, newest first, as CHANGELOG.md records it.

8.5 - Taste #

A minor version, additive throughout: what it is like to use. One command that shows a refusal and a run inside a budget with nothing to read first; four libraries, written in Velaris, so that an operations script against Azure, Kubernetes, GitHub or AWS calls no Python; a receipt and an audit as a page a person can read; and the first cut of the runner, in which a host process offers a program tools and the budget holds their arguments.

No program that compiles and runs under 8.4.0 inside its budget is refused by 8.5.0. Every new builtin gives way to a function of the program's own name (SPEC.md 10.1); uses tool did not compile and a tool grant did not parse until now; with no --tools there is no tool to reach. check_differential.py holds the examples, velaris-spec's corpus and the quick benchmark to 8.4.0's outputs.

compatibility: sha256, hex_encode, hex_decode, base64_encode, base64_decode and url_encode are new pure builtins, and each gives way to a function of that name in the program (they are in NEW_BUILTINS, SPEC.md 10.1), so a program that defined its own sha256 under 8.4 still calls its own; a program that called an undefined one did not compile (E200). compatibility: hmac_sha256 and hmac_sha256_chain are new builtins that give way to the program's own function in the same way; they need the declassify effect, which no program can come to need without calling them, and the E560, E561 and E609 they can give are given only to a program that calls them, which under 8.4 was E200. compatibility: tool is a ninth effect. uses tool was E300 under 8.4 and --allow tool a budget error, so no program or command line that worked changes meaning; --allow all now grants nine effects and says so in the line it has always written to standard error, and a program run under it that does not call tool runs as before; velaris.ALL_EFFECTS is one longer. compatibility: tool and tool_secret are new builtins that give way to the program's own function; E320, E321, E322, E323 and E324 are given only to a call of one of them, which no program that compiled under 8.4 makes, and the last four only under velaris run --tools. compatibility: velaris demo, velaris receipt show (and velaris receipts show, the same page), velaris skill verify, velaris audit --html [-o FILE] and velaris run --tools MANIFEST [--tool-timeout S] are new; a file named demo, receipt or skill in the working directory is now run with velaris run demo, as a file named audit or check always had to be. compatibility: velaris.receipt/1 gains grants_used in every receipt, tool_calls and tool_ceiling in the receipt of a run given --tools, and key_fingerprint on the declassification an hmac call records - all within version 1, where fields may be added (velaris-spec 8.7, 0.13.0); velaris replay and receipts diff compare what they compared, and a receipt written by 8.4 is read, shown and verified as before. compatibility: velaris.audit/1 gains tools within version 1, and secrets.declassifications gains an entry, with a builtin key, for each hmac call; effects may hold tool. compatibility: the audit and the capability ratchet now name the host of a URL that only begins fixed - "https://api.example.com/" + path, or format("https://api.example.com/{}", id) - when the fixed part holds the / that ends the host, where 8.4 said "a host built while running". net_hosts, safe_command and a derived baseline are narrower for such a program, never wider: the ratchet passes a narrowing against an 8.4 baseline, and the run-time check of net: grants is unchanged. velaris-spec 9.3 states the rule (0.13.0). compatibility: inside a library imported with a name, a call to a builtin older than 4.3 reaches the builtin, as it does in a flat import and as SPEC.md 10 says a named import behaves; until now a library's own get took a get(list, i) written inside it, a for loop's included. Only the shipped library may define such a name (E204) - http.vel has a get - and no shipped library made such a call, so no program's meaning changes. compatibility: stdlib/http.vel is byte for byte what it was in 8.4.0. What the batteries needed beside it - retries within a bound, JSON bodies, headers from a map - is in a new file, stdlib/rest.vel, because a function added to http.vel would stop a program that imports http.vel without a name and has a function of that name itself (E513), and items and succeeded are names a program has; azure.vel, github.vel, k8s.vel, aws.vel and rest.vel are new files that no 8.4 program imports. compatibility: host_refusal takes an optional count and the run state gains TOOL_GRANTS, TOOL_LIMITS, TOOL_COUNTS, GRANT_USES and TOOL_SESSION, none of which STABILITY.md covers and each of which has the value a run without tools had before. api: AuditResult gains the tools slot; velaris.ALL_EFFECTS gains tool; the run state gains TOOL_GRANTS, TOOL_LIMITS, TOOL_COUNTS, GRANT_USES and TOOL_SESSION; host_refusal(url) becomes host_refusal(url, count=False); the command line gains demo, receipt, skill, audit --html and run --tools/--tool-timeout; receipts from every door gain grants_used, and audits tools.

velaris demo #

One command, no arguments, no network, about a second. It makes a directory, writes into it a .env whose one value is made up, a script of the kind an agent writes - read ./.env, post it to a webhook - and the same task rewritten to stay inside a budget. It runs the first with no budget given and shows the refusal, the exact line, the reason and the receipt; runs the second under io,fs:read:settings.txt,fs:write:out and shows it succeed, with its receipt; and prints what differs between the two receipts. --keep leaves the files. The documentation's first page now opens with it. check_demo.py runs it on every leg: under a minute, under a screen, exit 0, nothing left behind.

Batteries, written in Velaris #

  • stdlib/azure.vel: Azure Resource Manager over REST - read, put_resource, patch_resource, delete_resource, list with nextLink paging (a link that leaves the host is not followed), a 429 or a 5xx asked again within a bound, and ARM's {"error": {"code", "message"}} as the failure's words. The bearer token is the caller's Secret of Text; nothing in the library signs in. Every request is written "https://management.azure.com:443/" + path, so the audit of a program that uses it names exactly management.azure.com:443.
  • stdlib/k8s.vel: the API server over REST with a Secret token; in_cluster() reads the service-account file with read_file_secret; list (with metadata.continue), read, watch_once, and pods, pod, services, deployments, deployment, configmaps, events, nodes, namespaces. It reads; what changes the cluster is write_create, write_patch, write_delete and write_scale, and the suite fails if a function that sends a changing method is named otherwise. It has no function for reading a Secret resource, on purpose.
  • stdlib/github.vel: repos, issues, pulls, check runs, releases and contents; Link-header paging held to api.github.com; the rate limit in every reply (remaining, reset) and, when it is reached, a failure that says when it resets and is not asked again.
  • stdlib/aws.vel: Signature Version 4 in Velaris, to S3 (list buckets, list objects with continuation, get, put, delete) and STS (GetCallerIdentity), with a session token when there is one. The date is whole-number arithmetic on now(). It reproduces the signature AWS publishes for its own test request, and the stand-in checks each signature the way AWS does, from the request as it arrived.
  • hmac_sha256(key: Secret of Text, message: Text) -> Text and hmac_sha256_chain(key, messages). The result is not a Secret, so the call needs the declassify effect and grant, the audit lists it under secrets with the reason hmac signature, and the receipt records it with the key's fingerprint. The chain exists because SigV4's derived keys are credentials themselves: with it they are never values of the program. THREAT_MODEL.md has a new section saying why a MAC does not give the key away, what somebody holding one can do (replay it while it is valid), and the limit: a program with the declassify grant can MAC under a weak key it derived from a strong one - which is no more than declassify already let it do, and should be read in an audit as what it is.
  • sha256, hex_encode, hex_decode, base64_encode, base64_decode, url_encode: pure, over UTF-8; the decoders fail on what is not the encoding or not text.
  • Bearer tokens leave through declassify, once, where the header is built, with a reason that names the host. 8.5 adds no builtin that sends a Secret: one that did would make net a second declassify that no audit names.
  • stdlib/rest.vel is what the four needed that http.vel lacked: call_retrying (a bound of ten, no pause - a program has no clock unless granted one), call_json, header_map, header_of, items, succeeded, worth_retrying, after_prefix, no_leading_slash. It is a new file and http.vel is untouched: the first draft added these to http.vel, and a program that imports http.vel without a name and defines its own items then stopped compiling (E513). A minor version does not do that, so they moved.
  • The audit names the host of a URL that begins fixed (above), which is what lets a library written against one host audit as that host. azure.vel and github.vel import nothing, because an audit reads every function a program loads and http.vel's take any URL.
  • Each has an example under examples/ops/ - azure_groups.vel (resource groups and tag drift), k8s_pods.vel, github_issues.vel, aws_buckets.vel - a line on the Library page, and a test in check_batteries.py, which runs on every leg against a stand-in server in the suite's own process: the request goes to the real host's name over TLS, under the real host's grant, and only where that name connects to is changed (tests/standin/, a certificate nothing else trusts).

The ffi count over examples/ (velaris stats --ffi examples): at 8.4.0, 106 programs, 8 of which call Python; at 8.5.0, 112 programs, 8 of which call Python. The six new programs - the four under examples/ops/ and the two under examples/runner/ - call none, and the audit of each shows no ffi effect and no module. The eight are the ones that were there: database.vel, edges.vel, ffi.vel, json_ffi.vel, report_fixes.vel, sandbox.vel, stdlib_tools.vel and stress.vel, which exist to show ffi, db.vel and dates.vel; none of them was rewritten.

Viewers #

velaris receipt show <file> and velaris audit <file> --html write a page: what was read, written and fetched - by grant, with counts - which secrets were declassified and why, what was refused and where, the confinement level, the wall time, the subjects. Plain HTML with the documentation site's stylesheet inside it; no script, nothing fetched, every value escaped; --text for the terminal, with control characters written as escapes. The same input gives the same bytes on every system (tests/viewers/).

To say which host, a receipt had to know, and a receipt holds no value the program handled. So grants_used counts what each grant let through, by the grant's own text - net:management.azure.com:443 three times - which is the operator's and not the program's.

The runner, first cut #

velaris run program.vel --tools manifest.json. The manifest (velaris.tools/1) declares tools by name, a JSON Schema for each one's arguments, which results are secret, a cost, and a ceiling in calls and in the host's own cost unit. The budget grants them as it grants anything: tool, tool:search@20, tool:send_email:to=*@corp.com. A call goes through a door to the host - JSON lines on standard input and output now; an HTTP door later - pauses the run, and resumes with the result, which is a Secret of Text when the manifest says so. Untrusted arrives in 9.0, and the documents say so where it matters. Receipts record every call site, the patterns that held its arguments and the ceiling; the audit lists tool like any effect, and the tools a program names. examples/runner/ is a host in Python offering search and send_email, and a program that is refused (E321) when it mails outside the allowed domain, before the host hears of it. velaris skill verify <dir> reads a skill's programs and manifest and reports the tools and the budget it would need. There is no framework adapter; docs/runner.md is the whole protocol, and who trusts whom.

The adversarial pass #

Kept as tests, so that each stays tried.

  • An argument that escapes its constraint (check_runner.py, fourteen ways against to=*@corp.com). The first matcher was a glob, and a glob star matches eve@evil.example, ann@corp.com. The rule that shipped: a pattern is matched against the whole value, nothing is trimmed or folded, and * never stands for the literal that follows it in the pattern, a separator (, ; < > " ' \), white space, a control or format character, or across ..; a list matches when every item does; a held argument that is left out is refused, since the host's default is not the operator's pattern; and an argument the schema does not name is refused, since what nobody described nobody constrained.
  • A ceiling exceeded: five of them - tool:NAME@N, tool@N, the manifest's calls, its cost, and a cost the host reports mid-run.
  • A host that lies: another call's id, a Bool for an id, a line that is not JSON, a result and an error, neither, a negative cost to win budget back, a cost that is not a number, NaN, a closed door, silence. Each is E324 and the program does not go on. A reply's other fields change nothing: a result is a Text and never a grant.
  • A result that steers a host or a path: it cannot leave the budget (the suite has a tool return a URL outside net:, which is E314), and inside the budget it can. That is the 9.0 Untrusted case and is written down as open in THREAT_MODEL.md, not fixed.
  • hmac_sha256: a key that reaches output other than as a MAC (check_digests.py). Sixteen routes - printed, logged, written, as a URL, as a tool's arguments, encoded first, through a list, a map, format, json_of, a loop over chars, as the message of another MAC - none compiles. One thing was changed for it: a call site that signs under many keys names sixteen fingerprints in a receipt and then says many, so a loop over keys derived from a secret cannot use the receipt as a channel. The limit above - a weak key derived from a strong one - is stated, not closed.
  • velaris demo turned on a real .env (check_demo.py): run from a directory holding a .env with a value only the suite knows, with seven argument forms, a proxy in the environment and the temporary directory pointed at the victim's. The value appears nowhere, nothing connects anywhere, and the directory is as it was.
  • A receipt somebody else wrote, shown as a page: markup in any value is text, and an escape sequence is written out, not sent to the terminal.

Known open #

  • A tool's result is not marked as the host's words (Untrusted, 9.0).
  • The pattern rule is conservative: *@corp.com does not match Ann@Corp.com, and /data/*.txt does not match /data/a.b.txt.
  • k8s.vel verifies TLS against the machine's trust store; a cluster with its own CA needs SSL_CERT_FILE set where the run starts. There is no switch that turns verification off, and no way yet to name a CA per run.
  • aws.vel and k8s.vel take their host from the caller, so an audit says "a host built while running" for them and the operator names the grant.
  • call_retrying does not pause between attempts.
  • A named import still renames a library's parameters that share a name with one of its functions; http.vel avoids the names. 9.0.
  • S3 and STS answer in XML, and aws.vel reads values out by tag.
  • embedding.html and threat-model.html are within a few hundred bytes of the site's 100,000-byte page budget. The runner's protocol and the viewers moved to docs/runner.md for that reason; the next addition to either document has to move text out as well.

Housekeeping #

  • build_docs.py hashes and copies line-feed bytes (lf_bytes): the digest on the receipt page, site.css, site.js, llms.txt and the playground are the same bytes from a Windows checkout and from a runner, so the release's own rebuild of docs/ no longer touches that page.
  • velaris/site.css is the site's stylesheet inside the package, for the viewers; check_viewers.py holds it to site/site.css.
  • velaris-spec 0.13.0: the tool effect and its grants (sections 3.1, 4.1 and 5.6), the URL-prefix rule (9.3), receipt grants_used, tool_calls, tool_ceiling and key_fingerprint (8.7), the audit's tools and the hmac declassification (8.6), and velaris.tools/1 (8.10, provisional).
  • velaris-kit, a template repository: the Azure script, a committed velaris.capabilities, the Action in a workflow, and an empty FRICTION.md.

Measured #

Measured by perf_gates.py --against v8.4.0 on Windows 11 (10.0.26200, AMD64, 16 CPUs), Python 3.13.13, z3-solver 5.1.0 and llvmlite 0.49.0: medians of 5 runs after one warm-up. The machine was not idle: 17% busy when it began, and this release's other suites ran beside the later measurements, so every figure here is higher than 8.4.0's table for that reason and not for a change in the code it measures. The comparison against v8.4.0 runs both versions in alternation under the same load, and is the figure to read; the release workflow repeats it on a runner that does nothing else, and fails the release past +25%.

Measure8.5.0
Cold start, velaris --version257 ms
Cold start, velaris check of a one-line file531 ms
Check, per 1,000 lines (a 1,013- and a 10,013-line program)1.11 s and 1.33 s; 0.07 s and 0.07 s without proofs
Proof time per example with contracts, p50 / p9523 ms / 488 ms, over 56 files
Native code on examples/bench.vel: compile, and llvmlite's import90 ms, and 78 ms; burn compiled
examples/bench.vel, native / --no-native6.76 s / 16.46 s, 2.44 times faster, 9.71 s saved
--lite buildthere is none
Pool worker's memory, after 1 run and after 1,000 more26.6 MB, 27.6 MB
z3 or llvmlite imported by velaris --version, or by check of a program with no promiseneither
Importing z3 when a command needs it+170 ms at cold start
Importing llvmlite when a command needs it+173 ms at cold start
Pure numeric against v8.4.0, native (bench.vel and an integer loop)6.76 s against 6.75 s, +0.2% (the gate allows +25%)
Pure numeric against v8.4.0, interpreted20.01 s against 18.64 s, +7.3%, measured under the load described above
velaris demo, start to finishabout 1 s: two runs of the command line and nothing else

check_differential.py against v8.4.0: none of the 97 examples' outputs differs, velaris-spec's 456 conformance cases give the same verdicts, and the quick benchmark's 15 programs the same verdicts.

8.4 - The kernel holds the line #

A minor version, and the last before 9.0. Until now the budget was enforced by the interpreter alone, in the process that runs the program, and THREAT_MODEL.md said so under "No OS confinement". From 8.4 the process that runs a program also asks the operating system to hold the same budget, before the program's first statement runs, so that a fault in Velaris itself - in the interpreter, a builtin, the budget's own checks - is a crash inside a box and not an escape. On Linux that is Landlock and seccomp-bpf, and a run under the default budget is fully held. On macOS and on Windows it is partial, and every run says which it got and why. Beside it: the release workflow now moves its own Action pins, so main does not go red after a release.

Nothing that compiles and runs under 8.3.1 inside its budget is refused: what the system is asked to refuse is what the budget already refused, and --no-confine restores 8.3.1 exactly.

compatibility: confinement is on by default for a run in a process of its own - the command line, run(timeout=...), Pool, both doors, velaris eval and velaris replay - and asks the operating system to refuse only what the run's budget already refuses, so a program that stays inside its budget runs as it did under 8.3.1, with the same output and exit status; a granted ffi module widens what is asked to what that module needs, and a module the table does not name, ffi:os, ffi:subprocess and plain ffi widen it to nothing enforced rather than risk refusing what worked. --no-confine on the command line, on velaris serve and on the MCP server, and confine=False in the library, do not ask, and say so on stderr. Against v8.3.1 no example's output and no conformance verdict changes. compatibility: E319 is given only under the fault-injection hook (VELARIS_FAULT_INJECT, new in 8.4), when the operating system refuses an effect the runtime itself attempted; no program and no run of 8.3.1 or earlier can meet it. compatibility: --confine was never a documented flag: 8.3's velaris eval passed it to the pool worker it started, with the directories the worker might write. From 8.4 every pool worker derives its OS policy from its own budget, and the worker's flags are --confine-at, --confine-temp and --no-confine; nothing a person or a script typed is removed. compatibility: velaris doctor prints one more line, the confinement level a run under --allow io gets on this machine, and a why: line under it when the level is not full; its exit status and every other line are as they were. compatibility: velaris.audit/1 gains confinement within version 1 - the level and reason on Linux, macOS and Windows for a run under safe_command, and the granted modules that widen the OS policy - derived from the budget alone, so an audit is still the same bytes on every system; the command line's audit prints a CONFINEMENT ON THIS MACHINE section after the lines it printed before. compatibility: a receipt's run_parameters.confinement, which 8.3 wrote as "none" for every run but velaris eval's and as the name of a mechanism (landlock-net, landlock, job-one-process, sandbox-exec) there, is now the level - full, partial or none - with confinement_reason, confinement_layers (where the mechanism names now are) and os_policy_sha256 added beside it, all within velaris.receipt/1; a receipt written before 8.4 still verifies, and velaris replay and velaris receipts diff compare the level only between receipts that have the new fields. compatibility: velaris eval refuses to run (exit 2, before the program is sent to the worker) where the operating system holds none of the budget; 8.3 ran such a program under the budget alone and wrote "confinement": "none". On Linux 5.13 and later, on macOS while it honours sandbox profiles, and on Windows, the level is full or partial and eval runs as before. velaris eval is documented as provisional. api: run(), Pool() and PoolRegistry() take confine=True; AuditResult gains the confinement slot; the run state gains CONFINE, CONFINEMENT, WORKER_CONFINEMENT, BEFORE_FIRST_STATEMENT and PROGRAM_FILES; velaris serve and the MCP server take --no-confine; the audit and the receipt the HTTP door and the MCP server return carry the new fields. Nothing is removed and no default argument changes.

The release workflow moves its own pins #

README.md and EMBEDDING.md pin the Action by commit, and run_tests.py fails unless that commit is the one the newest tag names. A release commit cannot name its own hash, so from the moment a release was tagged main's first test step failed until somebody pushed the pin move - twenty of twenty-one jobs, after 8.3.1.

  • release.yml's move_pins job runs once the tag exists, whatever the publishes after it did. It checks out main, runs release_checks.py move-pins vX.Y.Z --commit <sha> - the pins in both documents, the version: example beside them, the pre-commit rev: - rebuilds the pages, fails if anything outside README.md, EMBEDDING.md and docs/ changed, commits Move the Action pins to vX.Y.Z, asks the gate about that commit and pushes only when the gate says it is not a release, and does it again on top of main if main moved. A push made with GITHUB_TOKEN starts no workflow, so it then starts tests on main by name; test.yml takes workflow_dispatch for that, and the release run that follows those tests stops at its gate, which takes only a push's tests.
  • check_release.py runs the job's own steps in bash on a throwaway copy of this repository with a simulated tag, and holds the result to be that commit and nothing else: one commit past the tagged one, five lines in the two documents, pages under docs/, no tag made or moved, the tests started once; nothing pushed when it is run again; the pins moved on top of a commit that landed meanwhile; and a red job, with main where it was, when the tag does not name the released commit.

The operating system holds the budget #

velaris/confine.py's os_policy(budget) is the one derivation: budget in, OS policy out, reading nothing of the machine. THREAT_MODEL.md's new section, What the operating system enforces, prints the module's table - every budget item, and what each system enforces for it - and check_confine.py fails when the document and the module differ by a word.

  • Linux: Landlock and seccomp-bpf. Landlock holds reads to the fs:read grants and what the interpreter itself reads - Python's installation and import path, the package and the standard library, shared libraries, the devices and /proc entries Python asks for, time zone data, the program's own files, and the resolver's files and the TLS roots under a net grant only - and writes to the fs:write grants and a private temporary directory. seccomp-bpf answers EPERM to every socket call when no net is granted; to execve, execveat, fork, vfork and a clone without CLONE_THREAD, and ENOSYS to clone3; and always to ptrace, mount and its newer calls, pivot_root, chroot, unshare, setns, kernel modules, kexec, bpf, perf_event_open, process_vm_readv and writev, keyrings, io_uring, userfaultfd, open_by_handle_at, setting the clock, and a signal to any process but this one. The filter is installed on every thread; Landlock, which holds one thread, is applied to the main thread as well on Python 3.10, where a run is on a thread of its own, and a thread it could not reach makes the level partial and is named.
  • macOS: a sandbox profile, derived from the same policy and applied with sandbox_init, the call sandbox-exec makes: writes, the network and fork/exec held, reads refused under the home directory and /Volumes. Apple has deprecated both, and THREAT_MODEL.md says so.
  • Windows: a job object holding one process, the clipboard and the desktop; every privilege removed from the token but SeChangeNotifyPrivilege; and the low integrity level for a budget that grants no write, under which the kernel refuses a write to anything of the user's. Reads and the network are not held: that needs an AppContainer, which a running process cannot enter and which a python.exe from python.org, the Store or a virtual environment cannot start in, since it could not read its own installation there.
  • A granted ffi module widens the policy to what that module needs, named per module in FFI_WIDENS and in THREAT_MODEL.md: nothing, any path, any host, or - for ffi:os, ffi:subprocess, plain ffi and any module the table does not name - nothing enforced. The audit's confinement.widened_by says which.
  • The level a run reports - full, partial or none - is what was applied and held, with the reason: in the receipt, in the audit, in velaris doctor. velaris receipts diff names a run whose level no earlier run of the same program had, and says when it is weaker. velaris eval requires full or partial.
  • When it is applied. A single run - the command line, run(timeout=...), velaris replay - reads, proves and compiles its program first, from wherever its imports are, and is confined at the program's first statement. A pool worker is confined when it starts, before it is sent anything; it holds reads only when the pool has an import_root, as both doors' pools do, and says partial otherwise. A receipt and --record-responses are opened before the run and written after it, since a confined process cannot open them then.

The honesty test #

check_confine.py, on every leg. A fault-injection hook (VELARIS_FAULT_INJECT) makes the runtime itself, from Python and not from Velaris, read a file, write one, connect, start a process and - except on Windows, which has no signal to send - send a signal outside the budget. Under confinement, what that system's row says is held is refused by the kernel and the run ends with E319 naming the layers; what the row says is not held goes through; with --no-confine every one goes through. All three are asserted, through the command line, run(timeout=), a pool and the HTTP door, so the table is held true in both directions. The seccomp filter is also run instruction by instruction inside the suite, for x86_64 and aarch64, over thirty system calls each, so it is held on the Windows and macOS legs too.

Every escape target of check_sandbox.py, and the file and ffi targets of check_adversarial.py, were run again on a Velaris whose budget checks are knocked out (tests/confine/faulty_runtime.py), confined and not. Of the 44 targets, 5 are not applicable - refused before running, or not an effect. Of the rest, on Linux 19 of 39 now fail at the kernel as well as at the language - every read, write and network reach outside the budget, the symbolic link, .., and a process through py_json or a handle - and 20 at the language alone: a host, port or wildcard inside a net grant on a kernel without Landlock's TCP rules, the @N counts, env, declassify, and the ffi reach cases, where the target is a Python object in the same process. On Windows 8 of 38: the writes under a budget with no write grant, and the processes. They are recorded in tests/confine/kernel-linux.json and kernel-windows.json, and the suite fails if a target recorded as stopped at the kernel gets through it.

Nothing legitimate broke: the 97 examples, every suite, velaris-spec's 456 conformance cases, the quick benchmark, both doors, the pool, a name resolved and a request made under a net grant, a temporary file under ffi:tempfile, and a proof and native code made inside a worker that was already confined, all run under confinement by default.

The adversarial pass #

Against the confinement itself, kept in check_confine.py. It found three things to fix before release, all on Linux:

  • Input pushed at the terminal. A confined process could still make the TIOCSTI ioctl on the terminal it was started from, and what it pushed would be typed at the shell once it ended. The filter now refuses TIOCSTI and TIOCLINUX.
  • A Unix socket under a net grant. With any net grant the filter allowed every socket, and Landlock does not hold a connection to a Unix socket - which is how a process reaches a container runtime or the session bus. Under a net grant only IPv4, IPv6 and the resolver's netlink socket are allowed now; a granted Python module that widens the policy to any host keeps every family.
  • rt_sigqueueinfo. kill and tgkill to another process were refused; sigqueue was not.

Tried and refused: a symbolic link inside a granted path to a file outside it; /proc/self/root; the network and a process through a granted module that needs neither (ffi:json, ffi:shutil); a bind mount made by the confined run, even as root of its own user namespace; a process asked to leave the Windows job (CREATE_BREAKAWAY_FROM_JOB); a program that exhausts the job's memory (E611); confinement applied from a thread with no way to the main thread, which says partial and names the thread; and --no-confine after --, in a door's request in three spellings, and in a program's own arguments, none of which reaches the flag. velaris eval and velaris replay take no such flag.

Tried and not refused, and written down as such: a bind mount that was inside a granted path before the run is that path's content, to Landlock and to the language alike.

What the first runs on CI found #

It was built on Windows and on Linux under WSL, with no Mac. The pull request's twenty-one legs found four faults before it was merged:

  • macOS: an allow that never took effect. The profile denied file-read-data under the home directory and then allowed file-read* again for Python's installation. A rule for the one operation beats a rule for the family, whichever comes last, so the allow did nothing - and nothing showed it on the runners' Python 3.12, which is in /Library/Frameworks. Their 3.10 is under /Users/runner, and there a confined run could not import datetime. The denial is now one rule that names what it leaves out.
  • macOS: getcwd under the profile. A pool worker asked for its working directory after it was confined, and getcwd opens that directory. The worker takes its baseline first, and the profile leaves the names in the working directory and in each directory above it readable, which the table says.
  • Windows: os.kill(pid, 0) is CTRL_C_EVENT. The hook's signal attempt interrupted the suite that asked for it. No signal is attempted on Windows. And release_checks.py move-pins left the version: example alone in a checkout whose lines end \r\n; the fixture test caught it on every Windows leg.
  • Linux, Python 3.10: a race in applying Landlock to the main thread. The main thread said it was there to be asked only after it had started the run's thread, so about one run in forty on a loaded runner reported partial, correctly. It says so first now.

And the release workflow's own differential job found a fifth, after the merge and before anything was tagged: on Linux a program could not read back a file it had just written. examples/ledger.vel runs under fs:read:ledger.txt,fs:write:ledger.txt, saves, and loads; the file is not there when the run is confined, the read grant named nothing Landlock could open, and the load failed where 8.3.1's succeeded. A read grant that does not exist yet is now held to the nearest directory that does, as a write grant is, and the level says partial and why; on macOS the profile names the path whether or not it is there. The differential check had been run on Windows, where reads are not held; it is run on Linux as well now.

check_confine.py runs straight after the unit tests, and on macOS prints where Python is and the profile a run gets, for whoever reads a failed leg without a Mac.

Known open #

  • macOS and Windows are partial, for the reasons THREAT_MODEL.md's known open table gives per system, and macOS confinement is verified only on CI: on Intel and on Apple silicon runners, with Python inside the home directory and outside it.
  • Input written to the console on Windows, and TIOCSTI on macOS, are not held: a process attached to a console may write its input buffer, and the sandbox profile language has no rule for an ioctl.
  • A host in a net: grant is held by the language alone on every system; Linux holds the ports, with Landlock ABI 4 or later.
  • An in-process velaris.run(), the REPL, velaris test and velaris bench are not confined, and say so.
  • The command line's private temporary directory on Linux has a parent the same user's other confined runs share, because Landlock lets a directory be removed only by a right on the directory above it.
  • velaris review still has no check ceiling, db.vel still builds SQL from text, and csv.vel's quoted path is still quadratic (8.3's entry); all three are 9.0.

Housekeeping #

  • docs/confinement.md is a page of the site; docs/eval.md, docs/crosswalk.md, EMBEDDING.md, STABILITY.md, RELEASING.md, README.md and ARCHITECTURE.md say what is now true. The crosswalk's sandboxing rows (ASI05, ASI10, B006, B008, D003, F001, MEASURE 2.7) say what each system holds; their status stays partial, because no row of that page is enforced by a guard that a granted ffi:os takes away.
  • THREAT_MODEL.md's known-open table drops "No OS confinement" and gains one row per system, "Runs that are not confined" and "The fault-injection hook". "What 'not a security boundary' means here" is rewritten to say what is true on each system.
  • Issues #21 and #22 are left open: they close when the next monthly run is green.
  • velaris-spec 0.12.0 records the receipt's level and its three new fields, the audit's confinement, and E319.

Measured #

Measured by perf_gates.py --against v8.3.1 on Windows 11 (10.0.26200, AMD64, 16 CPUs, 6% busy when it began), Python 3.13.13, z3-solver 5.1.0 and llvmlite 0.49.0: medians of 5 runs after one warm-up. Wall-clock figures; another machine will differ.

Measure8.4.0
Cold start, velaris --version202 ms
Cold start, velaris check of a one-line file403 ms
Check, per 1,000 lines (a 1,013- and a 10,013-line program)1.02 s and 1.29 s; 0.05 s and 0.07 s without proofs
Proof time per example with contracts, p50 / p9524 ms / 435 ms, over 56 files
Native code on examples/bench.vel: compile, and llvmlite's import74 ms, and 64 ms; burn compiled
examples/bench.vel, native / --no-native4.88 s / 12.37 s, 2.54 times faster, 7.49 s saved
--lite buildthere is none
Pool worker's memory, after 1 run and after 1,000 more26.1 MB, 27.1 MB
z3 or llvmlite imported by velaris --version, or by check of a program with no promiseneither
Importing z3 when a command needs it+139 ms at cold start
Importing llvmlite when a command needs it+156 ms at cold start
Pure numeric against v8.3.1, native (bench.vel and an integer loop)4.88 s against 4.98 s, -1.9% (the gate allows +25%)
Pure numeric against v8.3.1, interpreted15.31 s against 15.92 s, -3.8%
velaris examples/hello.vel, confined and with --no-confine (median of 10)Windows: 358 ms and 368 ms, no difference outside the noise; Linux (WSL 2, kernel 6.6, Landlock ABI 3): 130 ms and 122 ms, about 8 ms for the ruleset and the filter

check_differential.py against v8.3.1: none of the 97 examples' outputs differs, velaris-spec's 456 conformance cases give the same verdicts, and the quick benchmark's 15 programs the same verdicts. The full benchmark, run at 8.4.0 with every bounded Velaris run confined, gives every one of its 76 programs the verdict it had at 8.3.0 (Velaris 52/12/2/0, Deno 8/34/24, Python 0/31/35); benchmark/results.json changes in its version line alone.