Threat model

What Velaris defends against when it runs a program somebody - or something - else wrote, what it does not, and what to do about the gap. Written for the person who has to decide whether agent-written code may run on a machine they are responsible for. Every claim here names the suite that tests it; the numbers come from benchmark/RESULTS.md, which one command regenerates.

What Velaris is for #

A model hands you a script. You want to run it without reading it line by line, and you want the things it can do to be bounded by what you said, not by what it says about itself. Velaris is a small language in which a function's signature declares the effects it may perform, the failures it may raise and the promises it keeps, and a runtime that refuses any effect outside the budget the operator set.

It is not a general sandbox. It bounds programs written in Velaris; it does nothing for a Python or shell script the same model might write instead.

The trust boundary #

The budget is enforced inside the interpreter loop at the moment an effect is attempted, and a refusal (E310, E311, E313, E314, E315) is not a failure the program can check; it stops the program. The one catchable case is a redirect to a host outside the grants: the program did not choose it, so the request fails and the program hears why. check_sandbox.py holds the escape attempts that established this, including a helper two layers down and a program that tries to catch the refusal and carry on.

What it defends against #

On the 76-program benchmark (66 dangerous, 10 harmless), Velaris caught 64 of the 66 - 52 before running and 12 while running - and flagged none of the 10. Under the same rules Deno caught 42 (8 before, 34 during) and plain Python 31 (all while running). The two misses are named below. Three of the 66 (category 12, 7.1) are dependency upgrades, and Velaris's catch before running there is velaris deps-diff, whose limits are also below. Three more (category 15, 8.3) import a library that does not exist where the program says it is, which velaris check refuses before anything runs; three (category 14, 8.3) are skill scripts whose helper reads a credential and posts it, which the audit shows reaching beyond what the skill needs.

What it explicitly does NOT defend against #

No longer here: the permissive default. Fixed in 5.0, 2026-09-12. Until 5.0 a run given no budget - velaris program.vel, or velaris.run(source) with no allow - got all seven effects, and this repository said so plainly: the README's related-work paragraph and the paper both conceded that Velaris's command line granted every effect when no budget was given, where a WASI module given nothing reaches nothing. That was true until 5.0. It is not true now. The default is io - the console, and nothing else - in the command line, the library, Pool and both doors, and --allow all is the one way to ask for what a run used to get, which writes a line to stderr when it is used. The old text is not deleted anywhere it appeared; it is dated.

Moved, not removed: secrets. Until 6.0 this section had nothing about the values a program handles, and the residual-risks table below said only "do not grant env to code you have not read." From 6.0 a value read by env() or read_file_secret() is a Secret of Text the compiler will not let reach anything that emits it, and from 7.0 it will not let a program branch on one either; that moves to What it defends against above. What stays here is everything those rules do not cover, and it is more than one line:

• Only values the type system can see. A secret that arrives any other way is an ordinary Text with no protection at all: read through read_line, passed in through args(), fetched from a vault over net, returned by a granted ffi module, or hard-coded in the source. Secret marks two builtins' results; it does not discover secrets. A program that reads a password from standard input can print it, and nothing here stops that.
• Non-interference. A comparison over a secret gives a Secret of Bool, nothing prints one and nothing branches on one (E560, E563), so a program cannot read a secret out a character at a time and then say what it read. That was possible in 6.0.0, for one day, and closing it is what 7.0 is - see the CHANGELOG. What remains unbounded is everything a program controls that is not a value: how long it runs, how much it allocates, whether it stops at all. This is not a non-interference result and must not be described as one.
• A promise, once per run. A requires, ensures or invariant may be a Secret of Bool, because a broken promise stops the run, cannot be caught and cannot accumulate - so it is a statement about a secret, not a branch on one. An operator who runs the same program many times can still learn one bit per run from whether it stopped. If that matters, do not grant env at all.
• Where a declassified value goes. declassify returns an ordinary value. After it, the type system has nothing more to say: the audit records that it happened and why, and whether the reason was true is a person's judgement.
• What a granted ffi module reads for itself. A Secret is a compile-time distinction with no runtime representation, so Python code inside a granted module reads the environment directly if it wants to. ffi:os is the environment, whatever the Velaris types say.

What follows is what is still not defended.

• Anything a granted ffi module can do. ffi:os is the whole operating system as the current user. The allow-list narrows which modules a call may reach; it does not narrow what a module does. Plain ffi grants every module. From 3.3 the reach check bounds a scoped grant to the module actually reached along the attribute chain, so a granted module is no longer a door into the other modules it imported; but within a granted module, that module's full behaviour is still granted. Where the owning module of an object reached along the chain cannot be determined, the call is refused rather than allowed - the bound errs toward refusing more, not less.

• Native code inside a granted module. A granted module may be, or may ship, a compiled extension (.so/.pyd/.dylib), which has no source to read and whose behaviour a budget does not constrain any more than it constrains Python. From 8.0 velaris audit reports this per granted module in ffi_native - "native" when it finds a compiled extension on disk (found without importing the module), "unknown" otherwise, and never "false", since a pure-Python module can import a native one without that being visible. The audit names the risk; it does not remove it. Grant native modules only when you would grant the machine.

• Side channels. Timing, CPU load, cache effects, the size or timing of console output. Nothing measures or bounds them.

• Resource use below the limits. A program may run for 29 of its 30 seconds and hold 511 of its 512 MB, every time it is called. The limits stop a runaway; they do not ration.

• Rate, and the meaning of a request. A count (@100) bounds how many operations a run makes, not how fast, how large, or whether a request is a GET or a POST. A plain net grant is any number of requests to any host; a plain fs grant is any path the OS user can reach. Narrow them.

• What a granted host does with a request. The grant names a host as written; where the name resolves is DNS's business, and what the host does with the data it receives is outside the model.

• Closed in 8.0.0: the connection endpoint when a proxy is set. Through 7.1.x the network client honoured an ambient HTTP_PROXY / HTTPS_PROXY: a net: grant checked the URL's host, but the socket then went to the proxy, which need not be a granted host, so an http:// request carried its payload to the proxy. The grant bounded the URL string, not the peer. From 8.0 guarded_opener builds the opener with ambient proxies disabled, and honours one only when the proxy's own host:port is itself inside the net budget; a proxy the budget does not cover is refused (E317, uncatchable), naming the proxy and the grant that would allow it. velaris add ignores ambient proxies too. The grant now bounds the socket's peer, not only the URL - this moves to What it defends against. What is still not bounded is what a granted proxy does with the request, like any granted host.

• What a granted path contains. A hard link inside a granted directory is that directory's content. A file system changed by another process between the check and the open is outside the model; a Velaris program has no threads, so it cannot race itself.

• Still within io: args() and read_line(). Command-line arguments and standard input are the console.

• Logic errors with no contract. A function that returns the wrong number and promises nothing is correct as far as the compiler knows. Benchmark row 04c (a loop that stops one item early) is this, and is a miss. The audit lists such functions under contract_coverage so the gap is visible; it does not close it.

• The meaning of text. A program that prints rm -rf build for its caller touches nothing (benchmark row 09c, a miss); a program that prints the same words in a warning is harmless (row 10d). No effect system can tell them apart, and Velaris does not try.

• Code not written in Velaris. A model asked for Velaris may hand back Python. The guard applies only to what the Velaris runtime runs.

• Memory caps on macOS. max_memory_mb uses the OS address-space limit (RLIMIT_AS) on POSIX and, since 3.1, a job object with JOB_OBJECT_LIMIT_PROCESS_MEMORY on Windows - where the child is created suspended, put in the job and only then resumed, so nothing runs outside the cap. It is enforced on Linux and on Windows. On macOS it is best-effort: the limit is set but not reliably honoured, and in the suite the runaway program reached the timeout instead. If the Windows job object cannot be made, the cap is recorded and not enforced rather than the run failing, which is what a Windows before 3.1 always did. velaris.memory_cap_is_enforced() answers for the machine you are on. The timeout is enforced on every platform.

• A pool worker's budget, once chosen. A Pool fixes its budget when it is made. That is the point - it is what lets a worker serve the next program safely - but it means a caller who wants a narrower budget for one program must make another pool, and a caller who hands the same pool to two tenants has given them the same budget. A worker is also a process that outlives one program: everything a granted ffi module could do to a fresh process, it can do to a worker, and the pool's promise is only that the next program does not inherit it. check_pool.py is the whole of that promise.

• The door's token, once it is out. The token is a password with no user behind it: whoever holds it has every grant the ceiling allows, and the door cannot tell holders apart or revoke one of them. From 8.1 it limits how often the token is used, all its holders together; one holder can spend that allowance for the rest. It is only as secret as the file or environment it came from. A program the ceiling allows to read the token file can read it, and one allowed net as well can send it away. The door speaks plain HTTP: on any address but loopback the token crosses the network in clear unless a TLS proxy sits in front. A made token printed to a stdout that something writes to a file is in that file.

• --no-auth. Any program on the machine, run by any user, can send the door programs. The checks that replace the token stop a web page in a browser, not a local process.

• The MCP server's caller. The ceiling bounds what velaris_run grants, not who calls it: the client decides that. A ceiling raised to ffi is ffi for whatever the model is told to do.

• What mcp-verify does not see. It compares what a server says about its tools with what was signed; it does not watch what the server does, and a server that returns the signed descriptions and behaves differently passes. It checks at the moment it runs. If both the velaris package and velaris_mcp.py in an installation were changed, the checker was changed too - verify the wheel (SECURITY.md), or run mcp-verify from a separately verified Velaris.

• What the capability ratchet does not see. It reads the program text. What a granted ffi module does once called is not in the text: ffi:os in the baseline is the operating system, and a program that newly calls os.system through it is inside the surface. A path or URL built while running is recorded as the unscoped grant, so it is caught, but only as "any path" or "any host". Paths are compared as text, never against the file system, so a symbolic link inside a recorded directory is that directory's content - the budget, which resolves every path, is what stops it at run time. A function is known by its file and name: one renamed while it gains an effect is a new function, held to its program's entry and the surface, not to what its old name declared. A file that does not compile adds nothing until it does, since it cannot run. The count bound is derived by fixed rules, and a loop whose number of turns is not written in the text has no bound. And the ratchet guards nothing if it is not required: a pull request that edits velaris.capabilities has accepted a widening, and the review of that edit is the control.

• What velaris deps-diff does not see. It sees declared surface, not behaviour. For a Velaris library that is the surface the ratchet derives from the text, with every limit of the ratchet above: what a granted ffi module does, a path or URL built while running seen only as "any path" or "any host", a function renamed while it gains an effect. For a package that is not Velaris it sees almost nothing. It reads the install-time scripts and the declared dependencies, says whether a script was added or changed - not what the script does - and reports the capability surface as unknown, with exit status 3, which is not a pass. It would not have caught postmark-mcp 1.0.16: by Koi Security's account that release changed only the code that sent the copy, which adds no install script and no dependency, so the report would have been "nothing gained that could be seen, surface unknown". Beyond that: it reads only the lockfile formats it names, and lists any other changed lockfile as not read; an entry resolved from git, a path, or a private registry or index is left out rather than compared with a public package of the same name; a dependency new in the upgrade has no earlier version and is listed, not examined; it compares at most 30 upgrades in one pull request and names the rest; it cannot read a version a registry has removed; it checks downloads against the digests the registry publishes, which a compromised registry would publish too; and in CI it informs and never fails the job, so what it finds is worth what the reading of its comment is.

• What an attestation does not say. velaris attest signs nothing: an unsigned Statement is a claim anyone could write, and a signed one says only that its signer ran this producer on those bytes and got this audit. It says no more than the audit - not that the program is safe, that the audit is right, or that any runtime will enforce its safe_command - and whatever the audit could not determine, it could not either.

• What a receipt does not say. A receipt (8.1) holds no value the program handled, and nothing more careful than that: it holds what the program did, and a program controls some of that without handing it a value - its exit status, the line at which it was refused or stopped, how many times it did something, how long it ran. After a declassify, a program can choose any of those from the declassified value. A declassification's reason is text the program's author wrote, and nothing checks it. Velaris signs no receipt, and a signed one says its signer ran this Velaris on these bytes and saw this run - as strong as the machine it ran on, with confinement: "none" saying the budget was the only boundary (and, from 8.4, confinement_reason saying why), and silent about any other run. The level is what the run's own process reported of itself: a process altered to lie about its budget can lie about its confinement too. A receipt marked complete: false lists what the killed worker reported, and counts at least that. A receipt written by --receipt is written when the run ends; a process killed from outside writes none.

• What ejecting does not keep. An ejected directory runs the Velaris it was ejected with, and no later fix reaches it. Its main.py checks the runtime and the program against their digests and cannot check itself: if anything but its owner could have written to the directory, compare it with SHA256SUMS before running. The proofs recorded in it are a record, not something the launcher trusts. Its refusal of a budget that writes where Python imports from is made where and when it is launched: a directory added to PYTHONPATH later is not known to it.

• A write grant to where Python imports from. A program allowed to write into a directory on some Python's import path - a PYTHONPATH entry, a site-packages, a user site - can leave a sitecustomize.py or a module there that the next Python process started with that path runs. That is not a Velaris effect, and a plain velaris program.vel --allow fs:write:... does not look for it; the ejected launcher refuses such a budget, and python -I ignores PYTHONPATH and the user site. Grant writes to directories that hold data, not code.

• What the invocation log does not hold. The program's source, output, stdin and arguments, and request headers, are not recorded; what a granted ffi module does inside Python shows only as ffi calls. A refusal names the path or host the program tried, which is the program's choice of text. A log written to stderr is kept only if whatever runs the door keeps stderr.

• A tampered compiler. Velaris is one Python file running in the same process as the untrusted program's interpreter. If the file, the package or the binary you run has been altered, nothing above holds. The release workflow signs every artifact and publishes an SBOM; SECURITY.md says how to verify a download. Verify it.

• The compiler as a target. Checking runs the parser, the type checker and the prover on untrusted source. The prover has a time budget per query; the other passes do not, and a hostile source can make a check slow or large. From 8.0 velaris check and audit, and from 8.1 the library's check, audit and attest, the doors' check and audit, and a bounded run's compile, stop at a ceiling (E613, E614); what stays inside the ceiling - 59 seconds of it, every time - is still spent. The language server has no ceiling: an editor that opens a file written to stall the prover waits for it, and so does a program that calls check(timeout=None).

• Compile-time reads. import "path" reads that file when compiling, before any budget applies - the budget governs what a program does when it runs. Until 8.1 this section said such a read "reads Velaris source, not data". It was wrong: nothing held the path to a .vel file, and an error inside a file that was not Velaris source quoted what it found, so a program sent to a door or a platform could read the first word of a file (advisory-import-read.md). From 8.1 that error shows nothing of the file, and the doors, and the library given import_root=, refuse an import outside the directory they serve (E515). Without an import root - the command line, and the library by default - an import still reads any .vel file the process can read, and the audit's fs_paths, net_hosts and ffi_modules include that file's literals. Give the library an import_root for source you were sent.

• The proof cache: removed in 8.2. Every proof is made in the process that reports on it or runs it, and no proof result is kept anywhere between runs, so there is nothing on disk to plant. The cache existed from 2.29 to 8.1.1 and held two holes: from 2.29 to 7.1.1 a ./.velaris/proofs.json shipped beside an untrusted program was believed (advisory-proof-cache.md), and from 7.1.2 to 8.1.0 an entry planted in the per-user directory was (advisory-proof-cache-2.md); in both a false ensures was reported proven and, compiled to native code, ran unchecked. check_adversarial.py's CACHE-1 to CACHE-10 plant both files and hold that nothing reads them.

• The prover's reach. Three benchmark rows (03d, 03f, 04e) are caught only while running: a division on the unguarded of two paths, a remainder inside a loop, a read at i + 1 in a loop over length(xs). The runtime check stopped each; the prover did not settle them beforehand. These are limits of the current prover, listed in RESULTS.md rather than worked around.

Signing with a secret key: hmac_sha256 (8.5) #

A request to AWS is signed with an HMAC-SHA256 under a key derived from the secret key. The signature is sent in the clear; the key must never be. So 8.5 has two builtins that take a Secret of Text and give back an ordinary Text: hmac_sha256(key, message) and hmac_sha256_chain(key, messages), which applies HMAC again and again, each result the next key as raw bytes. They are the second way out of Secret, after declassify, and are held the same way: the function needs uses declassify, the run needs the declassify grant, the audit lists the call under secrets with the fixed reason hmac signature and the builtin's name, and a receipt records each call site with that reason and the key's fingerprint.

Why this is sound. HMAC-SHA256 is a pseudorandom function of the message under the key: a MAC, or any number of them over messages an attacker chose, does not reveal the key or help forge a MAC over another message, for a key with the entropy of a real credential. Every service that accepts a signed request relies on exactly that. The message may not carry a secret (E560): a MAC of a secret message under a key the program chose would be a digest of that message, in the open. The chain exists because Signature Version 4's derived keys - for a date, a region, a service - are credentials themselves for as long as they are valid; with the chain they are never values of the program, and only the last MAC, the signature, comes out.

What somebody holding the MAC can do. Replay it, for as long as the service accepts it: a SigV4 signature is good for the one request it covers, for about fifteen minutes around its timestamp, and a program that prints one, or a log that keeps one, has given that request away for that long. It cannot be turned into another request, and it does not shorten the search for the key.

What this does not hold, and why it is not worse than before. Every pure operation over a secret gives a secret, so a program can build a weak key out of a strong one - one character of it, or length(key) as text - and a MAC under a weak key can be matched against guesses offline. A program that does this in a loop reads the key out through its MACs. Nothing in the type system stops that, and nothing needs to: it requires the declassify effect and grant, and a program that holds those can already write declassify(key, "..."). hmac_sha256 lets out no more than the effect it needs already allowed. What it changes is what an audit says: a program that only signs shows hmac signature and nothing else under secrets.declassifications, and a reviewer who sees a key argument that is not the credential itself, or an hmac call in a loop over pieces of one, should read it as a declassification of the key, because it is one.

The fingerprint a receipt carries is twelve hexadecimal digits of a SHA-256 over a fixed label and the key. It tells two keys apart and the same key from run to run. It is a function of the key, so for a guessable key it confirms a guess, as a MAC does; for a real credential it does not help find it. One call site names at most sixteen fingerprints and then says many, so a loop over derived keys cannot use the receipt as a second channel. check_digests.py holds RFC 4231's vectors, the refusals, and sixteen routes for a key other than as a MAC, none of which compiles.

Bearer tokens. azure.vel, github.vel and k8s.vel send a token in an Authorization header. A Secret cannot be handed to request (E560), and 8.5 adds no builtin that would let one be: that would make net a second declassify no audit names. The libraries call declassify once, where the header is built, with a reason that names the host; what holds the token to that host is the library's text - the URL begins with a literal https://host:443/ - and the operator's net: grant.

Tools a host offers: the runner's first cut (8.5) #

A run started with --tools may call tools its host process offers. The host is trusted and the program is not: a call has to pass the manifest, the tool's schema, the operator's grants - which may hold an argument to a pattern matched against the whole value - and the ceilings before the host hears of it, and each failure is a refusal in the receipt. A host that lies about a result cannot be detected and is the operator's own process; what a reply can do is bounded - it is never a grant, and a cost cannot win budget back. What this release does not close is a result that steers: a result is a Text like any other, so it cannot take a program outside its budget (a host outside net: is still E314) and can direct it inside. The mark that tells the host's words from the program's, Untrusted of T, arrives in 9.0. docs/runner.md has the whole of it, and check_runner.py the attempts.

velaris demo (8.5) #

The demo runs a script that reads ./.env and posts it, so it must be impossible to turn on a real one. It takes no argument but --keep; works in a directory it has just made, whose .env it wrote and whose one value is made up; gives the first run no --allow, so the read is refused (E310) before the post is reached; and posts to a host under .invalid. check_demo.py runs it beside a .env holding a value only the suite knows: the value appears nowhere and nothing connects anywhere.

Known open #

The gaps this model does not close, kept as a table so the list is one place and stays current. None is a defect to be reported under SECURITY.md's challenge; each is a stated limit of what the effect budget is. A finding that a guarantee above is broken - a "proven" promise that breaks at run time, or an effect performed outside the budget - is a different thing, and SECURITY.md says how it is handled.

Residual risks, and what to do about each #

What the operating system enforces #

From 8.4 the process that runs a program asks the operating system to hold the budget it was given, before the program's first statement runs, so that a fault in Velaris itself is a crash inside a box and not an escape. The derivation is one function, os_policy in velaris/confine.py: budget in, OS policy out, reading nothing of the machine. This table is that module's ENFORCES, and check_confine.py fails when the two differ.

What the interpreter itself must read is allowed beside the grants, on Linux by name: Python's own installation and every directory it imports from, the velaris package and the standard library beside it, the system's shared libraries, /dev/null, /dev/urandom and the /proc and /sys entries Python asks for, the time zone data, the files the program was read from, a private temporary directory - and, under a net grant only, the resolver's configuration and the TLS roots. @N counts stay in the language.

A granted ffi module widens the OS policy to what that module needs, named per module (FFI_WIDENS). A module that is not in this table widens to nothing enforced - what it needs is not known, and a run that worked before 8.4 is not refused - and the audit's confinement.widened_by names every module that widened the policy and to what.

The level is what was applied and held, not what was asked for. full: every file, network and process limit of this run's budget is held by the kernel. partial: some are, and confinement_reason names each that is not. none: nothing is - --no-confine, a module that widens to nothing enforced, a system that offers nothing, or a run that is exempt:

What "not a security boundary" means here #

Until 8.4 this section said the budget was enforced by an interpreter written in Python, in a process that also holds the compiler, on a host that trusts that process, and that it was not a substitute for an OS-level sandbox. The first half is still true. What is now true beside it:

• On Linux, with full confinement, a fault in the interpreter cannot read, write or make a file outside the run's fs: grants and what the interpreter itself reads, cannot open a socket when no net is granted, and cannot start a process, short of a defect in the kernel's Landlock or seccomp. A run says full only when that is so; the known-open table says what full still leaves.
• On macOS it is partial: writes, the network and new processes are held; reads are held only under the home directory and /Volumes; and the mechanism is one Apple has deprecated.
• On Windows it is partial: a second process is refused, every privilege is gone from the token, and a budget with no write grant can write nothing of the user's. Reads, the network, and writes under a budget that grants any, are not held, because that needs an AppContainer that a running Python cannot enter and a fresh one cannot start in.
• Everywhere: the process still runs as the user; a granted ffi module still widens what is held, to nothing at all for ffi:os, ffi:subprocess, plain ffi and any module the table does not name; env is not held; timing still leaks; and an in-process velaris.run() is not confined.

So the README's sentence stands for macOS, for Windows, for any run whose receipt does not say "confinement": "full", and for what full leaves. It is a strong guard against a program that does what it was not asked to, tested as such on every push, and on Linux a second guard the kernel keeps under it. It is still not a separate user account, a network policy or a virtual machine, and it should sit inside one of those when the stakes warrant it.