Skip to content

Sandboxed Candidate Execution

Runtime control — instantiates Generate-and-Verify Separation

Executes an untrusted candidate inside a confined environment that enforces a resource-and-permission policy as it runs, so its behavior can be checked and contained rather than trusted.

Where its siblings check a static artifact — a proof, a certificate — Sandboxed Candidate Execution verifies by running the candidate under confinement. The untrusted output (a binary, a plugin, a model-generated script, a submitted solution) is executed inside an environment that mediates every privileged action against an explicit policy: which syscalls, files, network endpoints, memory, and CPU-time it may touch. Anything within policy proceeds; anything outside it is blocked, and the violation is surfaced. Its distinguishing idea is that the check is dynamic and enforced — the verifier is a runtime monitor, and containment means even a candidate that fails the check cannot harm the host while failing it.

Example

A code-grading service runs thousands of student submissions, any of which might loop forever, fork-bomb, read another student's files, or phone home. Each submission executes inside a sandbox that grants it a fixed CPU-time and memory budget, a read-only view of just the test fixtures, and no network. A well-behaved solution runs to completion and its output is scored. A submission that tries to open a socket is denied and flagged; one that spins is killed at the time limit; one that attempts to climb out of its directory is stopped at the boundary and the offending action is logged for the instructor. The grader never has to trust the code it runs, because the sandbox turns "is this submission safe to run?" into a question it answers by controlled execution rather than inspection.

How it works

  • Encode the policy as an enforced envelope. Allowed syscalls, filesystem view, network, and resource ceilings are declared up front; the monitor mediates each at runtime.
  • Run the candidate, don't reason about it. Behavior is observed as it happens, catching what the code does rather than what it claims — effects a static check would miss.
  • Contain first, judge second. Isolation is primary: a policy breach is blocked before it lands, so failing the check is safe.
  • Halt and report on violation. The first out-of-policy action stops execution and emits the offending action as the counterexample.

Tuning parameters

  • Policy tightness — how narrow the permission and resource envelope is. Tighter contains more but breaks candidates that legitimately need a capability, trading safety against false rejects.
  • Isolation strength — OS namespace vs. virtual machine vs. hardware enclave. Stronger isolation resists escape but costs startup latency and per-run overhead.
  • Observation depth — syscall-level only, or full data-flow / taint tracking. Deeper watching catches subtler misbehavior but slows execution and can flood the log.
  • Determinism controls — whether time, randomness, and scheduling are pinned so a verdict is reproducible. Pinning aids debugging and fairness but constrains what the candidate can do.

When it helps, and when it misleads

Its strength is that it is the only sibling that can verify behavior rather than a claim, so it handles candidates too opaque to prove anything about — arbitrary binaries, obfuscated code, model output — and its containment means an adverse verdict costs nothing. It is the right tool when you must run first-encounter, possibly hostile code.

Its failure modes come from the limits of watching. A sandbox bounds overt behavior but not necessarily covert channels — timing, cache, or resource side-channels can leak or signal without tripping the policy,[1] and a sandbox escape (a bug in the isolation layer) turns the whole guarantee off silently. Dynamic checking also only exercises the paths the candidate actually took on the inputs you gave it, so "passed the sandbox" is not "correct on all inputs." The classic misuse is treating the sandbox as a completeness guarantee — assuming unobserved means absent. The discipline is to keep the isolation layer small and patched, to threat-model covert channels explicitly, and to pair execution with adversarial or wide-coverage inputs.

How it implements the components

  • checkable_acceptance_predicate — the runtime policy (permitted syscalls, resources, endpoints) is the explicit predicate every executed action is checked against.
  • soundness_boundary — "no action outside policy takes effect on the host" is the soundness guarantee; a sandbox escape is exactly a soundness break.
  • coverage_and_completeness_boundary — it defines, and honestly bounds, what the monitor observes: covert channels and untaken paths are the acknowledged completeness gap.
  • failure_and_counterexample_route — a policy violation halts the run and surfaces the offending action as a concrete counterexample.

It does not price the asymmetry or arrange the generator/checker roles (generation_verification_cost_model, generator_verifier_role_separation) — that is Untrusted Solver with Trusted Checker — and it proves nothing about untaken inputs and keeps no per-translation provenance (candidate_evidence_binding, versioned_verification_provenance), which is Translation Validation Checker.

Notes

Because it checks behavior on the specific inputs it observed, its verdict is per-execution, not input-general: a clean run is evidence about that run, not a proof about all runs. It pairs naturally with a static sibling — the sandbox covers opaque candidates you can only run, the static checker covers the inputs you never exercised.

References

[1] A covert channel transmits information through a system feature not intended for communication — timing, cache occupancy, power draw — and so can carry data past a policy that mediates only explicit resources. Sandboxes bound overt actions; covert channels are the standard reason "contained" is weaker than "isolated." ↩