Document version: 0.3.0 Date: 2026-03-11 Status: Living document Companion: This document covers practical security guidance. For threat scenarios, attack surface analysis, and residual risk assessment, see THREAT_MODEL.md.

Gleisner provides three categories of security guarantee when Claude Code sessions are run via gleisner wrap, gleisner record, or gleisner-tui --sandbox:

Every session produces a cryptographically signed in-toto v1 attestation bundle (AttestationBundle) containing:

• Payload -- canonical JSON of the InTotoStatement (subjects, provenance predicate, materials, timestamps, sandbox profile summary).
• Signature -- ECDSA P-256 over the payload bytes.
• Verification material -- either the public key (local signing) or a Fulcio certificate chain plus Rekor log ID (Sigstore keyless).

The attestation cannot be modified after signing without invalidating the signature. Tampering with any field -- subjects, materials, timestamps, audit log digest -- is detected at verification time.

The sandbox (gleisner-polis) enforces process-level isolation using Linux kernel primitives. Claude Code runs inside a restricted environment where:

• Credential directories (~/.ssh/, ~/.aws/, etc.) are replaced with empty tmpfs mounts and are invisible to the sandboxed process.
• Filesystem writes are confined to the project directory and designated temp paths.
• Network egress is restricted to an explicit domain allowlist.
• Process visibility is limited to the sandbox's own PID namespace.
• Resource consumption is bounded by cgroups v2 and rlimits (FSIZE, NPROC, NOFILE).
• Syscall access is filtered by seccomp-BPF (blocking dangerous calls like mount, ptrace, bpf, io_uring).

These constraints are applied externally at the kernel level. Claude Code cannot disable them from within the sandbox.

gleisner-scapes records a timestamped, sequenced JSONL event stream of every observable action inside the sandbox. The SHA-256 digest of this log is embedded in the attestation's gleisner:auditLogDigest field, cryptographically binding the audit trail to the signed statement. Post-hoc verification confirms that the log has not been truncated or modified.

When packages declare verified_properties, gleisner-forge can invoke the Lean 4 proof kernel to verify mathematical correctness guarantees:

• Lean 4 kernel (lake build) -- type-checks all proofs during compilation

Verification results are embedded in the attestation's package_metadata as VerifiedProperty structs, enabling policies that require proof coverage for specific package categories (e.g., cryptographic libraries). See FORGE.md for details.

The Z3 SMT solver can prove whether a session's security policy meets named baselines (SLSA Build L1/L2/L3, Gleisner Strict). Results are embedded in CycloneDX 1.6 SBOMs as machine-readable claims and counter-claims. See Section 5.4 for details.

Gleisner uses ECDSA with the NIST P-256 curve and SHA-256 for all attestation signatures. The implementation is provided by aws-lc-rs, a Rust binding to AWS-LC -- a formally verified C cryptographic library maintained by AWS.

All content digests (subject artifacts, audit log, sandbox profile, CLAUDE.md) use SHA-256 via the sha2 crate, producing 64-character lowercase hex strings.

The attestation payload is the serde_json::to_string() serialization of the InTotoStatement. This produces deterministic JSON (keys in struct field order, no trailing whitespace). The signature is computed over the raw bytes of this string. Verification re-parses the payload from the bundle and checks the signature against those same bytes.

Consequence: re-serializing the payload with a different JSON library that reorders keys will invalidate the signature. Always verify against the payload field as stored in the bundle.

When Sigstore is available, Gleisner uses the keyless signing flow:

1. The developer authenticates via OIDC (typically a GitHub or Google identity).
2. Fulcio issues a short-lived X.509 certificate (10-minute validity) binding the OIDC identity to an ephemeral signing key.
3. Gleisner signs the attestation payload with the ephemeral key.
4. The signature and certificate are recorded in Rekor, Sigstore's transparency log, producing an immutable log entry.
5. The AttestationBundle stores the certificate chain and Rekor log ID as VerificationMaterial::Sigstore.

At verification time, gleisner-lacerta extracts the public key from the leaf certificate, verifies the ECDSA signature using the sigstore crate's CosignVerificationKey, and logs the Rekor entry ID. Online Rekor verification is recorded but not required (to support air-gapped verification).

For full implementation details, architecture diagrams, and design rationale, see ARCHITECTURE.md § Sandbox Architecture.

Gleisner implements defense in depth through six independent isolation layers, each enforced by a different Linux kernel subsystem:

Compromising one layer does not automatically compromise the others. For example, even if the mount namespace is bypassed, Landlock independently restricts filesystem access. Seccomp-BPF prevents the process from calling mount or ptrace regardless of namespace state.

When using local signing (the default for air-gapped or offline environments), Gleisner auto-generates an ECDSA P-256 key pair on first use:

~/.config/gleisner/keys/local.pem    # PKCS#8 PEM private key

The path is determined by directories::ProjectDirs (XDG-compliant on Linux). Fallback: $HOME/.config/gleisner/keys/local.pem.

File permissions are set to 0o600 (owner read/write only) on creation. The key is loaded on subsequent runs without regeneration.

The corresponding public key is derived at signing time from the private key and embedded in the AttestationBundle as VerificationMaterial::LocalKey.

Sigstore keyless signing eliminates persistent key material entirely:

• No private key is stored on disk.
• Identity is established via OIDC (GitHub, Google, or custom provider).
• Fulcio issues a 10-minute certificate, ensuring key compromise windows are minimal.
• Every signing event is recorded in the Rekor transparency log.

Use Sigstore keyless mode in any environment with internet access and OIDC identity. It provides stronger guarantees against insider threats (LACERTA-007 in the threat model) because there is no long-lived key to steal.

Local keys:

1. Delete ~/.config/gleisner/keys/local.pem.
2. Run any gleisner wrap command -- a new key pair is generated automatically.
3. Update any verification pipelines or CI jobs that reference the old public key.
4. Previous attestation bundles remain verifiable using the public key embedded in their verification_material field.

Sigstore keyless: No rotation needed. Each session uses a fresh ephemeral key. Rotate your OIDC identity (e.g., GitHub PAT) according to your organization's credential rotation policy.

When to rotate local keys:

• If the key file may have been exposed (copied to an insecure location, included in a backup, visible in a container image layer).
• Periodically (e.g., quarterly) as a hygiene measure.
• When transitioning between environments or machines.

To extract the public key for use in verification pipelines:

# The public key is embedded in every attestation bundle.
# Extract it from any bundle signed with the key:
jq -r '.verification_material.public_key' attestation.json > pubkey.pem

# Or derive it from the private key using OpenSSL:
openssl ec -in ~/.config/gleisner/keys/local.pem -pubout -out pubkey.pem

Gleisner's verification layer (gleisner-lacerta) evaluates attestations against configurable policy rules. Two backends are supported:

Create a JSON file with the rules you want to enforce. All fields are optional -- absent rules are skipped, not failed.

{
  "require_sandbox": true,
  "allowed_profiles": ["konishi", "ashton-laval"],
  "max_session_duration_secs": 3600,
  "require_audit_log": true,
  "allowed_builders": ["gleisner-cli/0.1.0"],
  "require_materials": true,
  "require_parent_attestation": false
}

Apply the policy during verification:

gleisner verify --policy policy.json attestation.json

For complex policy logic, compile OPA/Rego policies to WASM and pass the .wasm file to the verifier. Gleisner uses Wasmtime 27 as the WASM runtime, providing sandboxed policy execution. Module loading is implemented; the full OPA ABI evaluation layer is in progress. The built-in JSON engine covers immediate policy needs.

# Compile a Rego policy to WASM (requires OPA CLI):
opa build -t wasm -e 'data.gleisner.allow' policy.rego

# Extract the wasm file:
tar -xzf bundle.tar.gz /policy.wasm

# Use it with gleisner:
gleisner verify --policy policy.wasm attestation.json

Policy auto-detection: gleisner-lacerta inspects the file extension -- .json files load as BuiltinPolicy, .wasm files load as WasmPolicy.

The policy_lattice module (behind the lattice feature flag in gleisner-lacerta) encodes BuiltinPolicy rules as Z3 QF_LIA constraints to answer questions that runtime evaluation cannot:

• Subsumption: Is every input accepted by policy A also accepted by policy B?
• Comparison: Full lattice ordering (strictly stricter, strictly looser, equivalent, incomparable)
• Witnesses: Concrete counterexample inputs when subsumption fails

Standard baselines are provided for compliance checking:

These form a strict chain: L1 ⊃ L2 ⊃ L3 ⊂ Gleisner Strict.

Results are embedded in CycloneDX 1.6 SBOMs as Declarations claims. See FORGE.md and LEAN-INTEGRATION-RESEARCH.md for details.

The policy engine receives a PolicyInput struct extracted from the attestation payload:

pub struct PolicyInput {
    pub sandboxed: Option<bool>,
    pub sandbox_profile: Option<String>,
    pub session_duration_secs: Option<f64>,
    pub has_audit_log: bool,
    pub builder_id: Option<String>,
    pub has_materials: bool,
    pub has_parent_attestation: bool,
    pub chain_length: Option<u64>,
    pub denial_count: Option<u64>,
}

For WASM policies, this struct is passed as JSON input. Your Rego policy should evaluate data.gleisner.allow to true or false based on these fields.

For the full chain algorithm (walk_chain pseudocode, digest indexing, cycle detection, mermaid diagrams), see ARCHITECTURE.md § Chain Verification.

Each attestation records the SHA-256 digest of its parent's payload in the gleisner:chain.parentDigest field, creating a verifiable history of Claude Code sessions.

Key security properties:

• Digest integrity -- each link's parentDigest must match the actual sha256(payload) of the parent bundle.
• Unsigned link detection -- chain verification flags bundles with VerificationMaterial::None as failures.
• Cycle detection -- visited digest tracking prevents infinite loops on malformed chains.

What "broken chain" means: A gap in the attestation history -- an intermediate bundle was deleted, a session was run without Gleisner, or the chain directory is incomplete. Policies can enforce chain completeness via require_parent_attestation.

Payload digest vs. bundle digest: The chain links on sha256(bundle.payload), not sha256(entire file). This means re-signing (key rotation) does not break the chain.

Gleisner's own dependency tree is hardened through multiple mechanisms:

The deny.toml at the repository root enforces:

Cargo.lock is committed to the repository, pinning every transitive dependency to an exact version. This ensures reproducible builds and prevents supply chain attacks that exploit version ranges.

All dependency versions are centralized in the workspace Cargo.toml under [workspace.dependencies]. Individual crate Cargo.toml files use dep.workspace = true only. This prevents version drift across the nine workspace crates (gleisner-cli, gleisner-tui, gleisner-polis, gleisner-forge, gleisner-introdus, gleisner-lacerta, gleisner-bridger, gleisner-scapes, gleisner-sandbox-init) and ensures a single point of audit for version updates.

The workspace lint configuration sets unsafe_code = "forbid", meaning no unsafe block can appear in any Gleisner library crate. This eliminates memory corruption vulnerabilities in Gleisner's own code.

Exception: gleisner-sandbox-init uses nix crate syscall wrappers (namespace creation, mount operations, pivot_root) which involve unsafe internally. The crate itself does not contain unsafe blocks — the unsafety is encapsulated by nix.

Note: this lint applies only to Gleisner's source. Dependencies such as aws-lc-rs, nix, wasmtime, and landlock use unsafe internally for FFI and kernel interfaces. These crates are widely audited but represent a trust boundary.

The workspace enables clippy::all = "deny", clippy::pedantic = "warn", and clippy::nursery = "warn", catching common correctness and performance issues at compile time.

When updating dependencies:

# Check for known vulnerabilities and license violations:
cargo deny check

# Review what changed:
cargo update --dry-run

# After updating, verify the lockfile diff:
git diff Cargo.lock

If you discover a security vulnerability in Gleisner, please report it responsibly.

Email: security@gleisner.dev

What to include:

• Description of the vulnerability.
• Steps to reproduce.
• Affected version(s).
• Potential impact assessment.

What to expect:

• Acknowledgment within 48 hours.
• Assessment and severity classification within 7 days.
• Fix or mitigation timeline communicated after assessment.

Scope: This policy covers the Gleisner codebase and its documented security properties. Issues in upstream dependencies (e.g., aws-lc-rs, wasmtime, sigstore) should be reported to the respective projects, though we appreciate a heads-up if the issue affects Gleisner's security guarantees.

Please do not file security vulnerabilities as public GitHub issues.

Practical steps for users setting up Gleisner in a new environment.

• Build gleisner-sandbox-init. The sandbox runtime is built automatically with cargo build --workspace.
• Install passt (for network filtering via pasta). (apt install passt / pacman -S passt / emerge net-misc/passt)
• Verify kernel version. Landlock requires Linux 5.13+. Run uname -r to check.
• Verify cgroups v2. Check that /sys/fs/cgroup is the unified hierarchy. Run mount | grep cgroup2.
• Use gleisner wrap or gleisner-tui --sandbox, never bare claude. Gleisner's protections are opt-in. Running claude directly bypasses all sandboxing and attestation.

• Prefer Sigstore keyless in connected environments. It eliminates persistent key material and provides transparency logging.
• Verify key file permissions if using local signing. The file at ~/.config/gleisner/keys/local.pem must be 0600. Run stat -c '%a' ~/.config/gleisner/keys/local.pem.
• Never commit signing keys to version control. Add *.pem to .gitignore if keys are anywhere near the repository.
• Back up local keys securely if attestation continuity matters (e.g., for CI verification). Use encrypted storage or a secrets manager.

• Start with the ashton-laval profile and relax only as needed.
• Review the allow_domains list. Every allowed domain is a potential exfiltration channel. Minimize to what is actually required (typically api.anthropic.com plus package registries).
• Set allow_dns: false in high-security environments to prevent DNS tunneling. Pre-resolve required domains or use a local DNS proxy.
• Review readwrite_bind paths. Only the project directory and temp paths should be writable.
• Set resource limits (max_memory_mb, max_pids, max_cpu_percent) to prevent resource exhaustion.

• Verify attestations before trusting session output. Run gleisner verify attestation.json.
• Enable chain verification (--chain) to detect gaps in the attestation history.
• Use policy files to codify your organization's requirements (require sandbox, require audit log, allowed profiles, etc.).
• Check audit log integrity. Pass --audit-log <path> to verify the log digest matches the attestation.
• Check subject digests. Pass --base-dir <path> to verify that output file hashes match what the attestation claims.

• Store the public key (or use Sigstore) in your CI environment for automated verification.
• Fail the pipeline if gleisner verify reports any Fail outcomes.
• Archive attestation bundles alongside build artifacts for audit trails.
• Run cargo deny check in CI to catch dependency issues before they reach production.

• Keep Gleisner updated. Dependency updates may include security fixes.
• Review SBOM diffs (gleisner-bridger output) after Claude Code sessions to audit newly introduced dependencies.
• Monitor the audit log (gleisner-scapes JSONL) for unexpected commands, especially curl, wget, nc, or any command targeting credential paths.
• Rotate local signing keys periodically (see Section 4.3).
• Re-read the threat model when Gleisner is updated -- new features may introduce new attack surface.