Threat model

last updated 27 Oct 2026

This threat model covers local environments only: Verbond runs on machines the caller controls.

Terms

• Contract. What the author publishes about their functions: the tasks each function runs, how data moves between them, the WebAssembly binary of each task, and the services each task may call. It is a CBOR document with exactly one encoding. The config file an author writes is not the contract: Verbond builds the contract from it, and only the contract is measured, endorsed and run.
• Input. A parameter of a function, or any part of one that its WIT type determines: a record field, a tuple element, the payload of a variant, option or result, or the elements of a list, taken together.
• Exposure. For each service, which of the caller’s inputs may reach it. Verbond derives it from the contract; the author doesn’t declare it.
• Identity digest. A digest of everything in a contract, or in one of its functions.
• Shape digest. A digest of what the caller can observe of a contract or function: its API, the services it may call, and its exposure.

Parties

• Author. Writes a contract and the code it covers, and publishes both. Untrusted: the author’s code may try to send the caller’s inputs anywhere, and the author’s description of the contract is not relied on.
• Caller. Endorses a contract and runs its functions on their inputs. The party the security properties protect. Trusted, along with their environment (see Assumptions).
• Service. An outside service a task may call (HTTP today). Untrusted: a service may collude with the author or with other services to learn more about the caller’s inputs. What it sends, its responses included, is its own: it may pass on anything it knows.

Assumptions

• The caller’s environment is trusted: its operating-system isolation, certificate store and clock.
• Wasmtime’s sandbox holds. A task can reach the outside world only through the imports the runtime provides.
• Cryptography holds up, TLS and SHA-256 in particular.
• The rest of the toolchain works as documented: Go, Rust and a small selection of WebAssembly packages.
• Services are responsible for what they send. A response can carry anything the service knows: from this call, from earlier calls, or from elsewhere. Verbond counts that as the service passing data on, not as part of the contract’s exposure.

Security properties

Verbond is built so that, under these assumptions, the following properties hold. How far each is today is under Status.

• Binary binding. A contract names, by SHA-256, the exact set of WebAssembly binaries its functions may execute. The runtime refuses to execute any other binary under that contract.
• Identity digest soundness. Any change to a contract or function changes its identity digest.
• Identity digest stability. The identity digest changes only when the contract or function changes.
• Shape digest soundness. Any change to the exposure or API of a contract or function changes its shape digest.
• Shape digest stability. The shape digest changes only when the exposure or API of a contract or function changes.
• Exposure soundness. When a contract’s functions execute in a Verbond runtime, any set of colluding services, together with the author, learns no more about the caller’s inputs than the combined exposure of those services allows, apart from what services outside the set pass on to it. Exception: a task’s duration, up to its timeout, is an unaccounted signal. A design to close it is in place but not yet implemented (see Limits).
• Endorsement. The runtime executes a function only under a contract the caller has endorsed. An endorsement names one exact contract by its identity digest. A shape pin only automates re-endorsing a new contract whose shape is unchanged.

Status

Each property has two sides: the code that keeps it, and the evidence that it does (tests, mutation tests and written proofs). A property holds when both are complete. None holds yet.

• Endorsement is designed: the runtime doesn’t check endorsements yet.
• Where evidence is incomplete, some tests, mutation tests or written proofs are still missing.

The assurance case argues each property from its claims, and names the code and tests that keep each claim. It will be published with Verbond’s source code, because the code is what lets you check it. It also covers hardening of the parts around the properties: strict decoding, resource limits, network egress, the executor process and the contract page.

Limits

• Timing. A task can tell a service it may call about data that service may not see, by changing how long it runs, up to its time limit. The caller’s deadline can’t be used for this: a call is refused unless its deadline covers every task running to its limit. Whether a call happens is counted in the exposure; its timing isn’t. Padding every span between external calls to a fixed length closes this; it is designed, not built.
• Exposure precision. Exposure is derived per input: a parameter, or a part of one its type fixes, such as a record field. A task counts as sending everything it was given to every service it may call, whatever its code does with it. This is never less than the true exposure, but it can be more.
• Services pass data on. The exposure says which services may receive an input, not where it goes from there. A service that stores or transforms what it’s sent, such as a database or a geocoder, can hand it to a later task in its response, and that task can send it to another service that never had it in its exposure. Every service that may receive an input should be trusted with it as far as the caller’s purpose needs. Bounding where a service sends data needs that service to run under Verbond too, with its own contract; that is for remote environments.
• Capabilities. Network access is the only capability covered. Storage is being designed.

Out of scope

• Correctness of the code a contract covers.
• What a service does with data the contract allows it to receive.
• Attacks on the caller’s environment (see Assumptions).
• Remote environments. Running on nodes the caller doesn’t control brings in node operators and Verbond itself as parties; they will be covered once remote environments exist.
• Micro-architectural side channels on hardware Verbond doesn’t control.

Reporting an issue

If you find an issue in the design or code, we’d love to hear it at security@verbond.dev.