Crate portcullis 

Lattice Guard

A quotient lattice for AI agent permissions that prevents uninhabitable states.

The Uninhabitable State

The uninhabitable state (originally termed “lethal trifecta” by Simon Willison) describes three capabilities that, when combined in an AI agent, create critical security vulnerabilities:

1. Access to private data - reading files, credentials, secrets
2. Exposure to untrusted content - web search, fetching URLs, processing external input
3. External communication - git push, PR creation, API calls, command execution

When an agent has all three at autonomous levels, prompt injection attacks can exfiltrate private data without human oversight.

Solution: Quotient Lattice

This crate models permissions as a product lattice L with a nucleus operator that projects onto the quotient lattice L’ of safe configurations:

L  = Capabilities × Paths × Budget × Commands × Time
L' = { x ∈ L : ν(x) = x }  (safe configurations)

The nucleus operator ν:
• Is idempotent: ν(ν(x)) = ν(x)
• Is deflationary: ν(x) ≤ x
• Preserves meets: ν(x ∧ y) = ν(x) ∧ ν(y)

When the uninhabitable_state is detected, exfiltration operations gain approval obligations. The quotient L’ contains only configurations where this invariant holds.

Quick Start

use portcullis::{Operation, PermissionLattice, CapabilityLevel};

// Create a permission set with dangerous capabilities
let mut perms = PermissionLattice::default();
perms.capabilities.read_files = CapabilityLevel::Always;    // Private data
perms.capabilities.web_fetch = CapabilityLevel::LowRisk;    // Untrusted content
perms.capabilities.git_push = CapabilityLevel::LowRisk;     // Exfiltration

// The meet operation detects the uninhabitable_state and adds approval obligations
let safe = perms.meet(&perms);
assert!(safe.requires_approval(Operation::GitPush));

Integration with Claude Code / OpenClaw

See the examples/ directory for integration patterns with popular AI agent frameworks.

Security Model

See THREAT_MODEL.md for a complete description of what this crate prevents and what it does not prevent.

User-Defined Policies (CEL)

With the cel feature enabled, you can define policies with CEL constraints:

use portcullis::constraint::{Constraint, Policy, PolicyContext};
use portcullis::frame::Nucleus;
use portcullis::{Operation, PermissionLattice};

// Create a policy with custom constraints
let policy = Policy::new("secure-workspace")
    .with_constraint(
        Constraint::new(
            "workspace-only",
            r#"operation == "write_files" && !path.startsWith("/workspace/")"#,
        )?.with_obligation(Operation::WriteFiles)
    );

// Apply the policy as a nucleus
let perms = PermissionLattice::permissive();
let safe = policy.apply(&perms);

Re-exports

pub use exposure_core::apply_record;

pub use exposure_core::classify_operation;

pub use exposure_core::project_exposure;

pub use exposure_core::should_deny;

pub use frame::verify_nucleus_laws;

pub use frame::BoundedLattice;

pub use frame::CompleteLattice;

pub use frame::ComposedNucleus;

pub use frame::DistributiveLattice;

pub use frame::Frame;

pub use frame::Lattice;

pub use frame::Nucleus;

pub use frame::NucleusLaw;

pub use frame::NucleusLawViolation;

pub use frame::SafePermissionLattice;

pub use frame::UninhabitableQuotient;

pub use galois::Composable;

pub use galois::GaloisConnection;

pub use galois::GaloisVerificationError;

pub use galois::TranslationReport;

pub use galois::TranslationStep;

pub use galois::TrustDomainBridge;

pub use graded::Graded;

pub use graded::GradedPermissionCheck;

pub use graded::GradedPipeline;

pub use graded::RiskCost;

pub use graded::RiskGrade;

pub use guard::operation_exposure;

pub use guard::CheckProof;

pub use guard::CompositeGuard;

pub use guard::ExecuteError;

pub use guard::ExposureLabel;

pub use guard::ExposureSet;

pub use guard::ExtensionExposureLabel;

pub use guard::GradedExposureGuard;

pub use guard::GradedGuard;

pub use guard::GuardError;

pub use guard::GuardFn;

pub use guard::GuardedAction;

pub use guard::PermissionGuard;

pub use guard::RuntimeStateGuard;Deprecated

pub use guard::ToolCallGuard;

pub use heyting::ConditionalPermission;

pub use heyting::HeytingAlgebra;

pub use intent::IntentKind;

pub use intent::WorkIntent;

pub use isolation::FileIsolation;

pub use isolation::IsolationLattice;

pub use isolation::NetworkIsolation;

pub use isolation::ProcessIsolation;

pub use modal::CapabilityModal;

pub use modal::EscalationPath;

pub use modal::EscalationStep;

pub use modal::ModalContext;

pub use modal::ModalPermissions;

pub use permissive::ExecutionDenied;

pub use permissive::PermissiveExecution;

pub use permissive::PermissiveExecutionResult;

pub use permissive::PermissiveExecutor;

pub use permissive::PermissiveExecutorBuilder;

pub use progress::ProgressDimension;

pub use progress::ProgressLattice;

pub use progress::ProgressLevel;

pub use region::CodeRegion;

pub use trust::EnforcementResult;

pub use trust::TrustProfile;

pub use weakening::WeakeningCost;

pub use weakening::WeakeningCostConfig;

pub use weakening::WeakeningDimension;

pub use weakening::WeakeningGap;

pub use weakening::WeakeningRequest;

pub use workspace::WorkspaceGuard;

pub use pipeline::algebraic_gap;

pub use pipeline::evaluate_and_escalate;

pub use pipeline::full_pipeline;

pub use pipeline::justify_necessity;

pub use pipeline::require_or_escalate;

pub use pipeline::translate_with_cost;

pub use pipeline::AlgebraicWeakeningGap;

pub use pipeline::CostAnnotatedTranslation;

pub use pipeline::EscalationTrigger;

pub use pipeline::HopCost;

pub use pipeline::IntentRegionMapping;

pub use pipeline::ModalJustification;

pub use pipeline::ModalJustificationEntry;

pub use pipeline::PipelineTrace;

pub use pipeline::RiskEvaluation;

pub use audit::AuditEntry;

pub use audit::AuditLog;

pub use audit::ChainVerificationError;

pub use audit::IdentityAuditSummary;

pub use audit::PermissionEvent;

pub use audit::RetentionPolicy;

pub use certificate::canonical_permissions_hash;

pub use certificate::verify_certificate;

pub use certificate::CertificateDelegationError;

pub use certificate::CertificateError;

pub use certificate::LatticeCertificate;

pub use certificate::VerifiedPermissions;

pub use delegation::meet_with_justification;

pub use delegation::DelegationChain;

pub use delegation::DelegationLink;

pub use delegation::MeetJustification;

pub use delegation::RestrictionDetail;

pub use delegation::RestrictionReason;

pub use metrics::build_deviation_report;

pub use metrics::DeviationDetail;

pub use metrics::DeviationReport;

pub use metrics::InMemoryMetrics;

pub use metrics::MetricEvent;

pub use metrics::MetricsCollector;

pub use metrics::MetricsReport;

pub use metrics::ReputationMetrics;

pub use metrics::ReputationWeights;

pub use token::AttenuationToken;

pub use token::SessionProvenance;

pub use token::TokenError;

pub use uninhabitable_state::ConstraintNucleus;

pub use uninhabitable_state::CoreExposureRequirement;

pub use uninhabitable_state::UninhabitableState;

Modules

audit

Audit logging primitives for permission tracking.

audit_backend

Pluggable audit backends for persistent storage.

certificate

Cryptographically attested delegation certificates for AI agent permissions.

constraint

Constraint algebra for composable policy nuclei.

delegation

Delegation chain reconstruction from audit events.

dropout

Lattice dropout for the permission product lattice.

escalation

SPIFFE trace chains for agent provenance and escalation.

exposure_core

Pure decision kernel for exposure-based guard logic.

frame

Frame-theoretic foundations for permission lattices.

galois

Galois connections for principled trust domain translation.

graded

Graded monad for composable risk tracking.

guard

Type-safe permission enforcement via the PermissionGuard trait.

heyting

Heyting algebra for intuitionistic implication in permissions.

identity

SPIFFE identity matching for policy selection.

intent

Work intent lattice for predicting code region impact.

isolation

Isolation level lattice for executor context.

kernel

Kernel decision engine — complete mediation with monotone session state. Kernel decision engine — complete mediation with monotone session state.

metrics

Metrics primitives for reputation tracking.

modal

Modal operators for necessity (□) and possibility (◇) in permissions.

permissive

Permissive execution with fallback tracking.

pipeline

Unified pipeline composing portcullis modules into a single analysis flow.

progress

Work progress lattice for monotone agent loop movement.

region

Code region lattice for coordinating concurrent agent modifications.

token

Attenuation tokens — compact delegation credentials for wire transport.

trust

Trust profiles: named presets mapping trust tiers to capability + isolation ceilings.

uninhabitable_state

Parameterized constraint system for dangerous exposure combinations.

weakening

Weakening tracking for permissive execution.

workspace

Multi-agent workspace exposure composition.

Structs

BudgetLattice

Budget constraints lattice.

CapabilityLattice

Capability lattice for tool permissions.

CommandLattice

Shell command access lattice.

CommandPattern

Structured command rule (program + args).

EffectivePermissions

Effective permissions for a work assignment. This is the fully computed permission set after delegation.

ExtensionOperation

Extension operation not covered by Verus proofs.

IncompatibilityConstraint

The “uninhabitable_state” is the combination of:

Obligations

Approval obligations that gate autonomous capabilities.

PathLattice

Path access lattice with allowed/blocked semantics.

PermissionLattice

The full product lattice combining all permission dimensions.

PermissionLatticeBuilder

Builder for constructing PermissionLattice instances.

TimeLattice

Temporal bounds lattice.

Enums

ArgPattern

Structured argument rule.

CapabilityLevel

Tool permission levels in lattice ordering.

DelegationError

Error type for delegation failures.

Operation

Operations that can be gated by approval.

StateRisk

Incompatibility constraint that enforces uninhabitable_state prevention.

Functions

glob_match

Check if a glob pattern matches a path.