Security model
The agent is untrusted by default. Everything it can reach is granted by a policy that lives outside its sandbox, and every action and refusal is logged.
Threat model
We assume the agent may be wrong, prompt-injected or hostile. It may try to read secrets, write outside its workspace, push to protected branches, reach the network or escalate to the host. The design goal: what the agent can do is exactly what the policy grants, and the agent cannot change that policy.
Isolation: one microVM per agent
Each agent runs in its own microVM with its own kernel, not a container sharing the host kernel. Sandbox images are treated as untrusted input: they run only inside the microVM, and each sandbox records the content digest it booted from. Sandboxes restored from the same snapshot are reseeded so they never share random state.
Enforcement outside the agent
File access goes through a gateway on the host that applies the filesystem policy: deny beats allow, writes only under read-write grants, secrets kept out.
The policy is held and checked on the host. Nothing inside the guest can read, edit or disable it.
Credentials stay on the host
Git tokens, SSH keys and model sign-ins stay on the host. When the policy allows an action, the host performs it for the agent; the key never enters the sandbox. When a sandbox needs to call the platform API, it gets a short-lived token scoped to its organisation and run, which expires on its own. Secrets are redacted from the agent log.
Network and egress
Egress is set by the sandbox's security profile and enforced by host firewall rules outside the microVM. A floor (cloud metadata, link-local and other sandboxes' addresses) is always closed, whatever the profile allows.
SSH remote access with short-lived certificates
A sandbox can work on a registered remote machine only through an agent running on that machine. Each session uses a certificate signed by your CA, valid for at most 15 minutes and bound to one sandbox, one machine and one policy hash. Host keys are always verified. The remote side enforces its own file and command policy, fails closed on a policy it cannot verify, and runs sessions unprivileged.
Security profiles
Built-in profiles cover the common cases: offline, model-only, internet, internet-lan and unrestricted. Save your own as a base plus allows and denies; operators can lock profiles. A profile can change on a running sandbox and is rolled back if the new rules fail a probe.
Formally verified pieces
The policy decisions that matter most have machine-checked proofs in Lean 4, tied to the Go code by generated test vectors that the real implementation must agree with:
- Network profiles: the floor never opens, a deny beats every allow, deny-only overrides never widen, and each built-in admits exactly its contract, for every IPv4 address, port and protocol. The rendered firewall rules are checked against the model.
- Filesystem policy: deny beats allow, writes only under read-write grants, adding a deny never widens, traversal grants no read.
- Remote access: the remote file policy, the command gate, and certificate acceptance, where each binding (signer, machine, lifetime, policy hash) refuses on its own.
The proofs cover the decision models, not the kernel or the firewall itself.
Tamper-evident audit log
Every agent run, event, session and control action is appended to a hash-chained log. Policy refusals are recorded alongside.
Multi-tenancy
In the hosted control plane, every resource is scoped to an organisation and role-based access is enforced on the server. API keys are scoped, stored hashed, shown once and revocable; out-of-scope calls are refused.
On-prem for enterprise
Need sandboxes inside your own environment? On-prem is available for enterprise: talk to us.
Reporting a vulnerability
Please report security issues privately to support@semantic.sh. Include steps to reproduce and the version you tested. We will acknowledge your report and keep you updated while we fix it. Please do not disclose publicly until a fix is available.