portcullis 1.0.0

A quotient lattice for AI agent permissions that prevents the 'uninhabitable state'
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
# portcullis

[![Crates.io](https://img.shields.io/crates/v/portcullis.svg)](https://crates.io/crates/portcullis)
[![Documentation](https://docs.rs/portcullis/badge.svg)](https://docs.rs/portcullis)
[![License](https://img.shields.io/crates/l/portcullis.svg)](LICENSE-MIT)

A **quotient lattice** for AI agent permissions that prevents the "uninhabitable state".

## The Uninhabitable State

The [uninhabitable state](https://simonwillison.net/2025/Jun/16/the-uninhabitable-state/) describes three capabilities that, when combined in an AI agent, create critical security vulnerabilities:

1. **Private Data Access** - reading files, credentials, secrets
2. **Untrusted Content Exposure** - web search, fetching URLs, processing external input
3. **Exfiltration Vector** - git push, PR creation, API calls, shell commands

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

```text
┌─────────────────────────────────────────────────────────────────┐
│                    THE LETHAL uninhabitable state                          │
│                                                                 │
│   ┌──────────────┐    ┌──────────────┐    ┌──────────────┐     │
│   │   Private    │    │  Untrusted   │    │ Exfiltration │     │
│   │    Data      │ +  │   Content    │ +  │    Vector    │     │
│   │   Access     │    │  Exposure    │    │              │     │
│   └──────────────┘    └──────────────┘    └──────────────┘     │
│         ↓                    ↓                   ↓              │
│   read_files ≥ LowRisk   web_fetch ≥ LowRisk   git_push ≥ LowRisk │
│                          web_search ≥ LowRisk  create_pr ≥ LowRisk│
│                                                run_bash ≥ LowRisk │
│                                                                 │
│   When ALL THREE are autonomous → Prompt injection = Data theft │
└─────────────────────────────────────────────────────────────────┘
```

## Solution: The Nucleus Operator

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

```text
L  = Capabilities × Obligations × Paths × Budget × Commands × Time
L' = { x ∈ L : ν(x) = x }  — the quotient of safe configurations

The portcullis ν satisfies:
• Idempotent:    ν(ν(x)) = ν(x)
• Deflationary:  ν(x) ≤ x
• Meet-preserving: ν(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.

See [THREAT_MODEL.md](THREAT_MODEL.md) for what this crate prevents and what it does NOT prevent.

## Quick Start

Add to your `Cargo.toml`:

```toml
[dependencies]
portcullis = "1"
```

Basic usage:

```rust
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 applies the portcullis and adds approval obligations
let safe = perms.meet(&perms);
assert!(safe.requires_approval(Operation::GitPush));
```

## Capability Levels

Permissions use a three-level lattice for autonomous capability:

| Level | Value | Description |
|-------|-------|-------------|
| `Never` | 0 | Never allow |
| `LowRisk` | 1 | Auto-approve for low-risk operations |
| `Always` | 2 | Always auto-approve |

Approval requirements are modeled separately as **Obligations**. The meet operation
takes the **minimum** of two capability levels (most restrictive).

## Lattice Properties

The permission lattice satisfies the algebraic lattice properties:

- **Commutative**: `a ∧ b = b ∧ a`
- **Associative**: `(a ∧ b) ∧ c = a ∧ (b ∧ c)`
- **Idempotent**: `a ∧ a = a`
- **Absorption**: `a ∧ (a ∨ b) = a`
- **Monotonic delegation**: `delegate(parent, request) ≤ parent`

These properties are verified by property-based tests using proptest.

## Components

### CapabilityLattice

Controls what tools/operations the agent can use autonomously:

```rust
use portcullis::{CapabilityLattice, CapabilityLevel};

let caps = CapabilityLattice {
    read_files: CapabilityLevel::Always,
    write_files: CapabilityLevel::LowRisk,
    edit_files: CapabilityLevel::LowRisk,
    run_bash: CapabilityLevel::Never,
    glob_search: CapabilityLevel::Always,
    grep_search: CapabilityLevel::Always,
    web_search: CapabilityLevel::LowRisk,
    web_fetch: CapabilityLevel::LowRisk,
    git_commit: CapabilityLevel::LowRisk,
    git_push: CapabilityLevel::LowRisk,
    create_pr: CapabilityLevel::LowRisk,
};
```

### Obligations

Obligations specify which operations require human approval:

```rust
use portcullis::{Obligations, Operation};

let mut obligations = Obligations::default();
obligations.insert(Operation::WebSearch);
obligations.insert(Operation::GitPush);
```

### PathLattice

Controls file system access with glob patterns and sandboxing:

```rust
use portcullis::PathLattice;
use std::path::Path;

// Block sensitive files
let paths = PathLattice::block_sensitive();
assert!(!paths.can_access(Path::new(".env")));
assert!(!paths.can_access(Path::new("secrets/api.key")));
assert!(paths.can_access(Path::new("src/main.rs")));

// Sandbox to a directory
let sandboxed = PathLattice::with_work_dir("/home/user/project");
```

### BudgetLattice

Controls cost and token limits with precision arithmetic:

```rust
use portcullis::BudgetLattice;

let mut budget = BudgetLattice::with_cost_limit(5.0);
assert!(budget.charge_f64(2.0));  // Returns true (within budget)
assert_eq!(budget.remaining_usd(), 3.0);
```

### CommandLattice

Controls shell command execution with proper parsing. Supports both string
allow/block rules and structured (program + argv) patterns:

```rust
use portcullis::CommandLattice;

let cmds = CommandLattice::default();
assert!(cmds.can_execute("cargo test"));
assert!(!cmds.can_execute("rm -rf /"));
assert!(!cmds.can_execute("\"sudo\" apt install"));  // Quoting bypass blocked

// Structured rules (program + args) for precision
let mut structured = CommandLattice::permissive();
structured.allow_rule(CommandPattern::exact("cargo", &["test"]));
structured.block_rule(CommandPattern {
    program: "bash".to_string(),
    args: vec![ArgPattern::AnyRemaining],
});
assert!(structured.can_execute("cargo test --release"));
assert!(!structured.can_execute("bash -c 'echo hi'"));
```

### TimeLattice

Controls temporal validity windows:

```rust
use portcullis::TimeLattice;

let time = TimeLattice::hours(2);
assert!(time.is_valid());
assert!(!time.is_expired());
```

## Delegation

Safely delegate permissions to subagents (monotonicity guaranteed):

```rust
use portcullis::PermissionLattice;

let parent = PermissionLattice::permissive();
let requested = PermissionLattice::default();

match parent.delegate_to(&requested, "code review task") {
    Ok(child_perms) => {
        // child_perms ≤ parent (guaranteed by the lattice structure)
        assert!(child_perms.leq(&parent));
    }
    Err(e) => println!("Delegation failed: {}", e),
}
```

## Builder Pattern

Use the builder for fluent construction:

```rust
use portcullis::{PermissionLattice, CapabilityLattice, BudgetLattice};

let perms = PermissionLattice::builder()
    .description("Code review task")
    .capabilities(CapabilityLattice::restrictive())
    .budget(BudgetLattice::with_cost_limit(1.0))
    .uninhabitable_constraint(true)
    .created_by("review-agent")
    .build();
```

## Preset Configurations

Common permission configurations:

```rust
use portcullis::PermissionLattice;

// Read-only: file reading and search only
let readonly = PermissionLattice::read_only();

// Filesystem read-only: read + search with sensitive paths blocked
let fs_readonly = PermissionLattice::filesystem_readonly();

// Web research: read + web search/fetch
let research = PermissionLattice::web_research();

// Code review: read + limited web search
let review = PermissionLattice::code_review();

// Edit-only: write + edit without exec or web
let edit_only = PermissionLattice::edit_only();

// Local dev: write + shell without web
let local_dev = PermissionLattice::local_dev();

// Fix issue: write + bash + git commit (PR requires approval)
let fix = PermissionLattice::fix_issue();

// Release: git push/PR with approvals
let release = PermissionLattice::release();

// Network-only: web access only
let network_only = PermissionLattice::network_only();

// Database client: CLI access for db tools
let db_client = PermissionLattice::database_client();

// Permissive: for trusted contexts (portcullis still enforced!)
let trusted = PermissionLattice::permissive();

// Restrictive: minimal permissions
let minimal = PermissionLattice::restrictive();
```

## Mathematical Framework Extensions

The crate provides advanced mathematical structures for principled permission modeling:

### Frame Theory and Nucleus Operators

The nucleus operator is formalized as a proper frame-theoretic construct, enabling type-safe quotient lattices:

```rust
use portcullis::{
    frame::{Nucleus, UninhabitableQuotient, SafePermissionLattice},
    PermissionLattice,
};

// Create the uninhabitable state quotient nucleus
let nucleus = UninhabitableQuotient::new();

// Project through the nucleus to get compile-time safety guarantee
let dangerous = PermissionLattice::permissive();
let safe = SafePermissionLattice::from_nucleus(&nucleus, dangerous);

// The inner lattice is guaranteed to be uninhabitable state-safe
assert!(nucleus.is_fixed_point(safe.inner()));
```

The nucleus satisfies:
- **Idempotent**: `j(j(x)) = j(x)`
- **Deflationary**: `j(x) ≤ x`
- **Meet-preserving**: `j(x ∧ y) = j(x) ∧ j(y)`

### Heyting Algebra (Intuitionistic Implication)

Conditional permissions using the Heyting adjunction `(c ∧ a) ≤ b ⟺ c ≤ (a → b)`:

```rust
use portcullis::{
    heyting::{HeytingAlgebra, entails, permission_gap, ConditionalPermission},
    CapabilityLattice, CapabilityLevel,
};

let current = CapabilityLattice {
    read_files: CapabilityLevel::Always,
    ..CapabilityLattice::bottom()
};

let target = CapabilityLattice {
    read_files: CapabilityLevel::Always,
    web_fetch: CapabilityLevel::LowRisk,
    ..CapabilityLattice::bottom()
};

// Check entailment (does current imply target?)
assert!(entails(&current, &target) == false);

// Compute what's missing to reach target
let gap = permission_gap(&current, &target);
```

### Galois Connections (Trust Domain Translation)

Principled security label translation across trust domains:

```rust
use portcullis::{galois::presets, PermissionLattice};

// Create a bridge between internal and external domains
let bridge = presets::internal_external(
    "spiffe://internal.corp",
    "spiffe://partner.org",
);

// Translate permissions (security-preserving)
let internal = PermissionLattice::permissive();
let external = bridge.to_target(&internal);

// Round-trip shows information loss (deflationary closure)
let round_trip = bridge.round_trip(&internal);
assert!(round_trip.capabilities.leq(&internal.capabilities));
```

Available presets: `internal_external`, `production_staging`, `human_agent`, `read_only`.

### Modal Operators (Necessity and Possibility)

Distinguish what is **guaranteed** (□) from what is **achievable** (◇):

```rust
use portcullis::{
    modal::{ModalPermissions, ModalContext},
    PermissionLattice,
};

let perms = PermissionLattice::fix_issue();
let context = ModalContext::new(perms);

// Necessity: what can be done without approval
let guaranteed = context.necessary;

// Possibility: what could be achieved with escalation
let achievable = context.possible;

// Check if escalation is required
if context.requires_escalation() {
    println!("Operations needing approval: {:?}", context.escalation_required_for());
}
```

### Graded Monad (Composable Risk Tracking)

Track risk through computation chains with proper monad laws:

```rust
use portcullis::{
    graded::{Graded, RiskGrade, evaluate_with_risk},
    StateRisk, PermissionLattice,
};

// Pure computation (no risk)
let safe: Graded<StateRisk, i32> = Graded::pure(42);

// Chain computations, risk accumulates via composition
let result = safe
    .and_then(|x| Graded::new(StateRisk::Low, x * 2))
    .and_then(|x| Graded::new(StateRisk::Medium, x + 1));

assert_eq!(result.grade, StateRisk::Medium); // max of grades

// Evaluate permission profile with automatic risk grading
let perms = PermissionLattice::fix_issue();
let graded = evaluate_with_risk(&perms, |p| p.description.clone());
```

The graded monad satisfies:
- **Left identity**: `pure(a).and_then(f) = f(a)`
- **Right identity**: `m.and_then(pure) = m`
- **Associativity**: `(m.and_then(f)).and_then(g) = m.and_then(|x| f(x).and_then(g))`

### Running the Examples

```bash
cargo run --example math_framework -p portcullis
```

## Type-Safe Enforcement

Use `PermissionGuard` for compile-time enforcement:

```rust
use portcullis::{PermissionGuard, GuardedAction, GuardError};

// The GuardedAction type cannot be constructed without passing checks
fn execute_with_permission<A>(action: GuardedAction<A>) {
    // We know permission was checked because GuardedAction
    // can only be created by the guard system
    let inner = action.into_action();
    // ... execute
}
```

## Security Model

### What We Prevent

-  Uninhabitable state completion at autonomous levels
- Privilege escalation via delegation
- Budget inflation via negative charges
- Path traversal attacks
- Command injection via quoting
- Deserialization bypass of constraints
- Permission tampering (checksum verification)

### What We Do NOT Prevent

- Human approval of malicious actions (social engineering)
- Attacks within a single capability
- Side-channel attacks
- Kernel-level escapes

See [THREAT_MODEL.md](THREAT_MODEL.md) for the complete security model.

## License

Licensed under either of:

- Apache License, Version 2.0 ([LICENSE-APACHE]LICENSE-APACHE)
- MIT license ([LICENSE-MIT]LICENSE-MIT)

at your option.

## References

### Security

- [The Uninhabitable State]https://simonwillison.net/2025/Jun/16/the-uninhabitable-state/ - Simon Willison
- [Container Hardening Against Agentic AI]https://securitytheatre.substack.com/p/container-hardening-against-agentic
- [Lattice-based Access Control]https://en.wikipedia.org/wiki/Lattice-based_access_control - Denning 1976, Sandhu 1993

### Mathematical Foundations

- [Nuclei in Locale Theory]https://ncatlab.org/nlab/show/nucleus - nLab
- [Heyting Algebra]https://ncatlab.org/nlab/show/Heyting+algebra - nLab
- [Galois Connections]https://en.wikipedia.org/wiki/Galois_connection - Wikipedia
- [Graded Monads]https://ncatlab.org/nlab/show/graded+monad - nLab
- [Modal Logic S4]https://plato.stanford.edu/entries/logic-modal/ - Stanford Encyclopedia
- [Sheaf Semantics for Noninterference]https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.5 - Sterling & Harper