gargamelle-sandbox — Bubblewrap Linux Container Isolation & Resource Limiting Boundaries

1. Executive Summary & Problem Framing

Counterexample-Guided Inductive Synthesis (CEGIS), automated program generation, and multi-agent repair routines must execute untrusted, dynamically synthesized candidate programs against target test suites. Executing arbitrary candidate code directly on the host machine presents severe security and operational vulnerabilities:

1. Host Disk Corruption: Malicious or buggy candidates can overwrite repository files, corrupt build caches, or delete user directories.
2. Process Contamination & Fork Bombs: Unchecked candidates can spawn background daemons, kill running developer servers, or exhaust operating system PID tables.
3. Unbounded Latency & Infinite Loops: Non-terminating synthesis candidates can hang the synthesis pipeline indefinitely.

gargamelle-sandbox provides a robust, defense-in-depth isolation boundary:

• Unprivileged Linux Container Namespaces: Leverages Bubblewrap (/usr/bin/bwrap) to unshare mount, network, PID, IPC, and UTS namespaces without requiring root permissions or setuid binaries.
• Strict Read-Only Host Filesystems: Mounts / read-only (--ro-bind / /), providing candidate binaries access to necessary system libraries while strictly preventing modifications.
• Ephemeral Writable Sandboxes: Automatically scopes writable file operations to bracketed temporary directories (withTempSandboxDir), guaranteeing cleanup on exit.
• Deterministic Resource Bounds: Wraps execution in /usr/bin/timeout to enforce timeout and memory constraints deterministically.

2. Mathematical Foundations & Theoretical Invariants

2.1 The Bubblewrap Namespace Isolation Boundary

Bubblewrap establishes an unprivileged Linux container sandbox around the candidate process:

┌─────────────────────────────────────────────────────────────┐
│                      Host Linux OS                          │
│                                                             │
│   ┌─────────────────────────────────────────────────────┐   │
│   │        Bubblewrap Namespace Sandbox (bwrap)         │   │
│   │                                                     │   │
│   │  - Mount Namespace:                                 │   │
│   │      /         -> Read-Only Bind (--ro-bind / /)    │   │
│   │      /dev      -> Hermetic Devfs (--dev /dev)       │   │
│   │      /proc     -> Fresh Procfs (--proc /proc)       │   │
│   │      /tmp      -> In-Memory Tmpfs (--tmpfs /tmp)    │   │
│   │      workDir   -> Isolated Writable Bind            │   │
│   │  - PID / IPC / UTS / Net Namespaces: Private        │   │
│   │  - Lifetime: Bound to parent (--die-with-parent)    │   │
│   │                                                     │   │
│   │        ┌───────────────────────────────────┐        │   │
│   │        │   Synthesized Candidate Process   │        │   │
│   │        └───────────────────────────────────┘        │   │
│   └─────────────────────────────────────────────────────┘   │
└─────────────────────────────────────────────────────────────┘

1. Physical Containment: By mounting /proc anew within a private PID namespace, candidate processes cannot inspect, enumerate, or signal host processes.
2. Hermetic File Mutations: All scratch file creation occurs inside ephemeral directories or tmpfs mounts; no changes persist to the host.
3. Guaranteed Cleanup: --die-with-parent ensures the kernel sends SIGKILL to child processes if the parent Haskell runtime terminates abruptly.

3. Module Architecture & Repertoire Breadth

The package exports 2 modules providing declarative effects and production container handlers:

4. Executable Worked Examples

4.1 Running a Command in an Isolated Bubblewrap Sandbox

{-# LANGUAGE OverloadedStrings #-}

module ExampleSandbox where

import qualified Data.Text as T
import Sandbox.Effect
import Sandbox.Handler

-- Run candidate binary in an isolated sandbox with custom limits
runCandidate :: FilePath -> [String] -> IO ()
runCandidate bin args = do
  let limits = defaultLimits { limitTimeoutSeconds = 5 }
  res <- withTempSandboxDir "candidate-run" $ \workDir -> do
    (code, stdout, stderr) <- executeBubblewrapSandboxed limits workDir bin args
    if code == 0
      then putStrLn $ "Success: " ++ T.unpack stdout
      else putStrLn $ "Failed (code " ++ show code ++ "): " ++ T.unpack stderr
  case res of
    Right () -> pure ()
    Left err -> putStrLn $ "Sandbox execution error: " ++ T.unpack err

4.2 Bounded Pure Mock for Unit Tests

module ExampleMockSandbox where

import Sandbox.Effect
import Sandbox.Handler

-- Execute deterministic mock without spawning system processes
mockTest :: (Int, String)
mockTest =
  let (code, stdout, _) = pureMockSandboxRun defaultLimits "/bin/test" []
  in (code, show stdout)

5. Integration Points & Subsystem Boundaries

gargamelle-sandbox operates at Tier 1 (Host Integration) of the architecture:

┌────────────────────────────────────────────────────────┐
│               Downstream Consumers                     │
│  - gargamelle-workflow: Grounded CEGIS Execution       │
│  - gargamelle-evidence: Sandboxed Test Run Evidence    │
└──────────────────────────▲─────────────────────────────┘
                           │
                  [gargamelle-sandbox]
                           │
┌──────────────────────────▼─────────────────────────────┐
│               Upstream Substrates                      │
│  - Host OS: /usr/bin/bwrap (Bubblewrap Container)      │
│  - Host OS: /usr/bin/timeout (GNU Coreutils)           │
│  - polytropos-core: Flat Struct Payloads               │
└────────────────────────────────────────────────────────┘

6. Diagnostic & Troubleshooting Guide

6.1 Unprivileged User Namespaces Disabled

• Symptom: executeBubblewrapSandboxed returns error bwrap: No permissions to create new namespace.
• Root Cause: Some hardened Linux distributions disable unprivileged user namespaces via sysctl kernel.unprivileged_userns_clone = 0.
• Remedy: Enable unprivileged user namespaces (sudo sysctl kernel.unprivileged_userns_clone=1), or install Bubblewrap with setuid bit enabled (chmod u+s /usr/bin/bwrap). When disabled, executeSandboxed automatically falls back to bounded subprocess execution.

6.2 Synthesis Timeout Exceeded

• Symptom: executeSandboxed returns exit code 124 (GNU timeout standard exit status).
• Root Cause: Synthesized program entered an infinite loop or exceeded limitTimeoutSeconds.
• Remedy: Treat timeout as a non-terminating counterexample witness and feed back to synthesis engine to disallow unbounded recursive structures.

Part of the Gargamelle Verification Suite.