GitHub - coproduct-opensource/nucleus: Enforced permissions for AI agents - policy + enforcement in one stack

Don't trust the agent. Verify it.

Signed identity, declared guarantees, receipts anyone can check.

Nucleus is a vendor-agnostic secure runtime for AI agents: it enforces what an agent may do, proves the enforcement boundary is sound, attests how every result was produced, and federates identity and trust — without a single long-lived secret.

Assume the agent is compromised. Constrain what it can do anyway. Prove the constraints hold.

At its core is a small, dependency-free information-flow algebra. Two primitives — join and flows_to — enforce information-flow control under four algebraic laws. Once untrusted web content enters a session, it cannot silently reach a privileged sink like git push. That property is machine-checked, not hoped.

This is the lethal trifecta — private data + untrusted content + an exfiltration sink — made safe by non-interference: attacker-tainted data cannot reach a consequential action, so a compromised agent cannot be turned into a confused deputy. We don't detect the prompt injection; we make its consequence impossible — and prove it. (Detection-based guardrails are probabilistic; this is a structural guarantee.)

let mut state = FlowState::bottom();           // clean session
state.join_operation(Operation::WebFetch);     // tainted by web content
assert!(!state.flows_to(SinkClass::GitPush));  // can't push tainted data

On top of that core, Nucleus adds three newer pillars — a Constitutional Kernel (policy may only tighten, never widen), verifiable keyless identity & trust federation (OIDC → SPIFFE, "Let's Encrypt for agents"), and provenance envelopes with an independent verifier (signed, portable bundles re-checkable in Rust, WASM/JS, or Python).

See it in 90 seconds

Two runnable hooks, nothing to configure (just, or run the commands directly):

just demo     # 30s, in your terminal — information-flow control, 4 scenarios
just vault    # play "The Vault" in your browser

just demo (cargo run -p nucleus-ifc --example ifc_demo) — a prompt-injection write is denied by adversarial ancestry, not by a classifier guessing at strings; a clean flow is allowed; a compartment transition clears taint; a deterministic bind excludes the model from the trust decision:

─ Scenario 1: Web injection blocked ─
  ModelPlan inherits Adversarial from WebContent
  ✗ Write DENIED — adversarial ancestry detected
─ Scenario 2: Clean workflow allowed ─
  ✓ Write ALLOWED — clean ancestry

just vault launches The Vault — a browser CTF where you try to exfiltrate a secret past a formally-verified permission lattice (Lean 4 + Kani-backed verdicts). Hosted at https://nucleus-ctf.fly.dev; point an LLM at its JSON/MCP API and watch it fail too.

Quick Start

cargo install --git https://github.com/coproduct-opensource/nucleus nucleus-cli

nucleus audit [PATH]                # Tier 0: scan agent configs, no runtime (CI exit codes)
nucleus run --local "your task"     # Tier 1: run with enforced permissions (process-level, no VM)

Every tool call flows through the permission kernel. nucleus run tracks data provenance and blocks dangerous combinations — like writing code derived from untrusted web content.

Vendor neutrality. The core library and the generic credentials.env / PodSpec interface are intended to be vendor-agnostic, but the surface is not fully clean today. Two things break it: (1) the reference agent runner shipped with nucleus run/shell is coupled to one specific assistant CLI (binary name, default model string, permission-bypass flag), and (2) nucleus-spec still hardcodes specific LLM-vendor hostnames and workload-identity defaults (see Known Gaps). A PreToolUse hook for AI coding assistants lives in the external private orchestrator nucleus-code, built on this runtime. Treat the runner as an integration example, not a vendor-agnostic component.

What Gets Proved

Formal assurance, recounted (June 2026)

Honest scope. The Lean security core (lattice, IFC, exposure, noninterference) is sorry-free. As of June 2026 the portcullis-core-proven-lean.yml gate lake builds the proven tier (24 libraries) and fails if any proof-hole sorry/admit appears in a file not listed as research-tier in crates/portcullis-core/lean/CONJECTURES.md — so a real proof can no longer silently regress; aeneas-ifc-scoped.yml additionally asserts a clean axiom set for the one extracted integrity-noninterference theorem. (Two previously-orphaned files — CategoryProofs.lean, LabeledTypeProofs.lean — were found to no longer compile under the pinned toolchain when the gate was introduced; they are quarantined as Tier 3 "STALE" in CONJECTURES.md, not cited as proven, pending repair.) The exploratory alignment-tax / cohomology / braid formalizations are research-tier, are not discharged (40 open sorry proof holes across 11 files; ~100 raw sorry occurrences tree-wide are mostly doc comments), and are clearly separated from the core and labeled CONJECTURE in-file. Some research files are sorry-free but rely on native_decide, which trusts the native compiler (Lean.ofReduceBool) and is not pure-kernel-checked — disclosed, not hidden. Aeneas mechanically translates the core capability types from Rust to Lean so proofs run over generated code; ExposureSet/IFC use hand-written Lean models with structural correspondence tests, and exact function-level Rust↔Lean correspondence (that the Rust meet equals the Lean meet) is not yet proven. Kani is bounded — complete over the finite lattice state space, an approximation for string/path checks.

No Verus. Earlier docs cited "297 Verus VCs." Verus has been removed from the workspace; its guarantees are folded into the Lean 4 + Kani stack. A proptest-based conformance suite (verus_conformance.rs) is the surviving artifact — property tests, not SMT proofs.

Verified Claims · Formal Methods · Production Delta

The Flow Algebra

Each of these four laws is backed by a named, passing test, and the four-valued Belnap policy bilattice that composes decisions (Allow/Deny/Unknown/Conflict) has kernel-checked, sorry-free Lean proofs.

The information-flow core, precisely

Nucleus is built on a vendor-agnostic algebraic core (portcullis-core, dependency-free):

• Capability lattice — a Heyting algebra over 13 operation dimensions (read/write/exec/web/git/spawn/…), each a 3-level chain Never < LowRisk < Always, with pointwise meet/join/implies, a least-privilege builder, and work-type profiles (read-only, research, codegen, review). No LLM-vendor concepts appear in the core.
• Bidirectional information-flow control — a 6-dimension IFCLabel (confidentiality, integrity, authority, provenance, freshness, derivation) implementing BLP down-flow containment and Biba up-flow taint. A causal-DAG FlowTracker joins labels across operations and fails closed on unknown nodes, with monotonic per-session taint and confidentiality ceilings.
• Policy enforced by the type system — I/O goes through sealed effect traits (FileEffect, ShellEffect, GitEffect); the only constructor for a real handler is production_effects(policy), so unpoliced file/shell/git I/O is unconstructible. (Web fetch/search and agent-spawn effects on the real handler return NotImplemented and delegate to other crates.)
• Governed memory — a key-value store with per-entry IFC labels, authority classes, provenance flags, TTL, and poisoned_entries() detection for memory-poisoning attack classes.

This cluster carries over a thousand passing library unit tests (portcullis-core ~1081, portcullis-effects 69, nucleus-spec 32, nucleus-memory 17, nucleus-ifc 14, portcullis-profiles 4 — roughly ~1217 in total) plus ~95 Kani harnesses.

The Three New Pillars

The sections below cover three large subsystems that landed after the original docs and were previously under-described. Each carries an honest status note.

1. Constitutional Kernel — policy that can only tighten

A self-contained library trio (ck-types, ck-policy, ck-kernel) that decides whether a proposed change to an agent's own policy manifest is allowed to ship. Its governing rule is monotonicity: a self-amendment may only tighten authority, never widen it. The admission engine rejects any change that adds a capability, widens the I/O surface, raises a resource budget, or drops a required proof obligation — and reports exactly which invariant was violated. Constitutional (kernel-adjacent) changes can never be self-merged; they require a threshold of distinct, cryptographically-verified human signatures. Every accepted amendment is content-addressed (BLAKE3), carries an Ed25519-signed witness bundle (ring), and is appended to a replayable lineage.

Documented adversarial defenses pass with tests: patch laundering, witness replay, lineage tampering, sandbox relaxation, and policy_before forgery are all rejected.

Status: ~75 passing unit/integration tests; 17 Kani harnesses. The kernel is now invoked by an in-repo PR gate (cargo xtask policy-gate, workflow ck-admit.yml): every PR touching PolicyManifest.toml or a may_not_modify protected file is run through ck-kernel::admit, and a non-monotone amendment fails the build — replacing reliance on the external/closed "Constitutional Gate" app. Signature verification now defaults to fail-closed outside test builds (an empty Enforced verifier rejects every witness until you install trusted keys via .with_signature_verifier()). Still roadmap: full Admit mode with real signed witnesses + committed trust roots (the CI gate currently runs Preflight — authoritative on monotonicity + may_not_modify, signatures skipped), and live-runtime (non-CI) enforcement of an admitted policy.

2. Verifiable Identity & Trust Federation — keyless, vendor-neutral

A SPIFFE workload-identity and federation stack that turns a CI/runtime OIDC token into a SPIFFE id with no long-lived secret.

• Keyless GitHub Actions OIDC → SPIFFE (nucleus-github-oidc) is proven live end-to-end. A real GitHub OIDC token (mintable only inside a job with id-token: write) is validated against GitHub's real JWKS (RS256 sig, issuer/audience/exp, repo+org allowlist, replay), and the SPIFFE id is derived from the verified repository claim — never from sub — with a green CI run on record. A Fly.io Machine validator (nucleus-fly-oidc) implements the same pattern (synthetic-fixture-tested; no live demo yet). Shared primitives (nucleus-oidc-core) provide RFC 7517/8037 JWKS, OIDC discovery, and replay defense, with a CI gate (ci/no-vendor-strings.sh) enforcing vendor neutrality on every PR.
• OIDC provider (nucleus-oidc-provider). A stateless OP that mints EdDSA JWT-SVIDs with key rotation + grace windows, publishes RFC 8414 discovery + JWKS, and performs RFC 8693 token exchange — verifying the inbound subject_token's Ed25519 signature and enforcing declarative federation rules.
• Trust registry — "Let's Encrypt for agents" (nucleus-trust-registry). A non-custodial (never a CA, never a keyholder) registry for SPIFFE federation enrollment: a fail-closed PR gate verifies a GitHub OIDC proof-of-control (pinning the numeric org id to defeat rename-squatting) and appends each trust-root binding to an append-only, witness-cosigned transparency log.
• Witness & split-trust (nucleus-witness). A C2SP tlog-witness server minting Ed25519 cosignatures under the full spec status matrix, with RFC 6962 consistency and rollback protection. Run your own k-of-n witnesses across failure domains so no single region, cloud account, or key store can forge or roll back your log — useful even to a single operator with zero counterparties.
• Verify-before-you-act (nucleus-agent-card). Secret-free, WASM-capable verification of signed agent cards that, by design, refuses to trust any key embedded in the card itself.

Status & honesty notes. (1) The OIDC provider verifies inbound subject_token signatures only against a statically-configured trust bundle; live SPIRE-Agent-mediated validation (Workload API over UNIX socket) is stubbed. (2) The trust registry's OIDC proof establishes GitHub-org control of the enrolling repo, not ownership of the SPIFFE trust-domain name (a DNS-01-style proof is v2); the MVP trust base is a single maintainer + single witness — no threshold key ceremony. (3) The witness store is in-memory; a restart resets last-cosigned positions, so production requires durable storage. (4) Paid-tier/metering seams are documented-only — no billing feature exists.

3. Provenance Envelopes & the Public Verifier — signed, portable, independently checkable

Every agent session can be packaged as a provenance bundle — the agent's payload plus a signed lineage envelope proving how it was produced. Each lineage edge (one per tool call, LLM call, or derived artifact) carries a child SPIFFE id encoding its derivation, an Ed25519 signature, and a prev_hash link; the whole log is committed to an RFC 9162 Merkle tree with signed tree heads, inclusion/consistency proofs, and optional external-witness cosignatures (Nucleus + C2SP tlog-witness).

The point is independent verification. verify_bundle re-checks the entire bundle — per-edge signatures, hash chain, session membership, Merkle inclusion, cosignature thresholds, and payload binding — against a trust anchor you supply out-of-band. The bundle's own embedded keys are deliberately ignored. The same audited Rust verifier ships three ways:

A CI-gated adversarial corpus of 8 forged bundles (tampered edges, swapped signatures, truncation, attacker JWKS, unknown kid, foreign parent, non-pod root) must be rejected on every merge — every_corpus_case_is_rejected passes today. This is the security promise, not a slogan. For replication, nucleus-bundle-cas fetches bundles by BLAKE3 root over bao-verified iroh-blobs QUIC so a peer can't substitute or truncate bytes (alpha; single-operator split-trust, no discovery/mesh, pins pre-1.0 iroh).

Honest scope. A green verification proves the lineage is authentic and intact. It does not prove the agent behaved well, that information-flow policy held, or that any computation was correct — those are separate guarantees. Issuing/signing identities is demo-only in this repo (dev-feature-gated LocalIssuer); production needs an external SPIFFE issuer and witness. The public verifier service is not live (no hosted endpoint resolves today); it is self-hostable and deploy-ready. The @coproduct/verify npm package and in-browser tamper demo are publish-gated; the compiled .wasm is a build product, not committed.

How Nucleus Stops Real Exploits

Deployment Tiers

Tier 1 is process-level (env-clear isolation, cap-std, command allowlist) — it is not kernel/container isolation and does not prevent kernel escapes or network exfiltration when bash is allowed. The agent PreToolUse-hook variant of Tier 1 (nucleus run --hook, nucleus guard) is not runnable from this repo: it shells out to a nucleus-claude-hook binary that lives in the external private orchestrator, and the in-repo install hint (cargo install --path crates/nucleus-claude-hook) is stale — that crate does not exist here. Tier 2 isolation requires Linux with /dev/kvm; on macOS the node returns an explicit "firecracker requires Linux" error, and the macOS test suite exercises config/allocation logic, not a live VM boot.

Architecture

Agent → MCP → tool-proxy (inside VM) → portcullis check → OS operation
                  │
                  └─ emits signed lineage edges ─► provenance bundle ─► verify_bundle (Rust / WASM / Py)

┌───────────────────────────────────────────────────────────────┐
│  nucleus-cli  ·  nucleus audit [PATH]  ·  control-plane API    │  user-facing
├───────────────────────────────────────────────────────────────┤
│  ck-kernel / ck-policy / ck-types   (constitutional kernel)    │  policy admission
│   monotonic self-amendment · signed witness · lineage          │   (library, not yet runtime-wired)
├───────────────────────────────────────────────────────────────┤
│  nucleus (Sandbox + Executor + AtomicBudget + MonotonicGuard)  │  enforcement runtime
├───────────────────────────────────────────────────────────────┤
│  portcullis / portcullis-core / portcullis-effects             │  IFC core
│   13-dim Heyting capability lattice × 6-dim IFCLabel            │
│   sealed effect traits · FlowTracker · Belnap bilattice        │
├───────────────────────────────────────────────────────────────┤
│  identity & trust federation                                   │  keyless identity
│   oidc-core · github-oidc · fly-oidc · oidc-provider           │
│   trust-registry ("LE for agents") · witness (C2SP) · cards    │
├───────────────────────────────────────────────────────────────┤
│  provenance                                                    │  attestation
│   nucleus-lineage · nucleus-envelope · bundle-cas              │
│   verifier-service · verifier-js (WASM) · verifier-py          │
├───────────────────────────────────────────────────────────────┤
│  Firecracker microVM / seccomp / netns  (Linux + KVM)          │  isolation substrate
└───────────────────────────────────────────────────────────────┘

Crates

The workspace contains ~47 crates (42 workspace members + 5 excluded build targets), plus one orphan crate dir (nucleus-policy) not yet wired into the workspace. They are grouped below by function. Status reflects the most recent subsystem survey.

Python: sdk/python/nucleus ships a self-contained information-flow kernel (taint propagation, exposure accumulation; 168 passing tests). Native PyO3 bindings to the Rust core live in portcullis-python and verifier-py. The companion nucleus_sdk proxy client is self-labeled pre-alpha / draft (v0.0.0, "API will change").

Known Gaps

Documented in SECURITY_TODO.md and docs/production-delta.md. Key items, stated plainly:

• The reference agent runner is not vendor-agnostic. nucleus run/shell is currently hardcoded to one specific assistant CLI (binary name, default model string, and a permission-bypass flag), and some audit/MCP identifiers are named for that vendor. Only the core library and the generic credentials.env / PodSpec interface are vendor-agnostic today.
• The agent PreToolUse-hook path is not runnable in this repo. nucleus run --hook and nucleus guard shell out to a nucleus-claude-hook binary that is not built here (it moved to the external private orchestrator), and the in-repo install hint (cargo install --path crates/nucleus-claude-hook) is stale — that crate directory does not exist.
• nucleus-spec still embeds specific LLM-vendor strings. package_registries() hardcodes api.anthropic.com; the default workload_identity is name: "anthropic" / audience: "https://api.anthropic.com"; and doc-comment examples reference https://api.openai.com and an openai-prod logical name. All of these violate vendor neutrality and need generalizing (e.g. api.example-llm.invalid / LLM_API_HOST / a generic logical name) before the top-line "vendor-agnostic" claim is fully defensible.
• nucleus-policy is an orphan crate. It has a full Cargo.toml but is not a workspace member and is not wired into anything — it must be integrated or documented as a stub.
• The constitutional kernel is a library, not yet runtime-wired. It decides admissibility in isolation; it does not yet gate the live sandbox, and signature enforcement is opt-in.
• The public verifier service is not hosted. It is self-hostable and deploy-ready (fly.toml; 26 integration / 70 total tests); no hosted endpoint resolves today. The @coproduct/verify npm package and /verify/ demo are publish-gated.
• Tier 2 isolation is Linux + KVM only. macOS test passes do not imply a live VM boot.
• bash -c bypasses command-level checks. Firecracker network policy is the real defense.
• verify-receipts checks the hash chain, not yet the Ed25519 signature. Tool-proxy-log HMAC verification is real; C2PA verification is feature-gated.
• Issuance/signing of identities is demo-only. LocalIssuer is dev-feature-gated; there is no SPIRE-backed JWT-SVID issuer in this repo.
• The research-tier Lean formalizations are not discharged. 40 open sorry proof holes remain across 11 exploratory alignment-tax / cohomology / braid files (each labeled CONJECTURE; manifest at crates/portcullis-core/lean/CONJECTURES.md); only the security core is sorry-free and CI-gated against regression.
• Some crate-level READMEs are stale (nucleus-lineage under-claims; a few doc comments lag the code). The code/tests are the source of truth.

Threat Model

Protects against: prompt-injection side effects, invisible Unicode injection, misconfigured permissions, network policy drift, budget exhaustion, privilege escalation via delegation, audit-log tampering, memory poisoning, substitution/truncation of provenance bundles, and silent policy widening (constitutional kernel).

Does not protect against: compromised host/kernel, malicious human approvals, side-channel attacks, VM kernel escapes — nor does a green provenance verification imply the agent behaved well or that any computation was correct.

Versioning: v1.0 means the interface contract is stable (see STABILITY.md), not "production-secure by default." The lattice is heavily verified; the runtime is tested but not yet battle-hardened.

Development

cargo build --workspace
cargo test --workspace
make demo              # taint → block → receipt → compartment switch

License

Licensed under either of Apache License, Version 2.0 or the MIT license at your option.

References

• The Uninhabitable State — Simon Willison
• Lattice-based Access Control — Denning 1976, Sandhu 1993
• SPIFFE — Secure Production Identity Framework for Everyone
• RFC 8693 — OAuth 2.0 Token Exchange
• RFC 9162 — Certificate Transparency Version 2.0
• C2SP — Community Cryptography Specification Project (tlog-witness)
• Aeneas — A Verification Toolchain for Rust
• verify-rust-std — AWS's verification density benchmark