Skip to content

SECURITY.md

Latest commit

 

History

History
187 lines (139 loc) · 7.78 KB

SECURITY.md

File metadata and controls

187 lines (139 loc) · 7.78 KB
Raw

Security Policy

Supported Versions

Version Supported
0.1.x Yes

Reporting a Vulnerability

This project is currently in private development. If you have access and discover a security issue, please report it to:

Email: j.d.a.jewell@open.ac.uk

Do NOT open a public issue for security vulnerabilities.

Dual-Use Notice

This project is classified as dual-use technology (precautionary). See DUAL-USE-NOTICE.adoc for details.

Security Architecture — Verifiable Agent Security by Construction

007 enforces safety properties at the grammar level — violations are parse errors or type errors, not runtime exceptions. This is "security by construction": you cannot write an insecure 007 program any more than you can write a syntactically invalid one.

Layer 1 — Grammar-Level Safety

Property Mechanism What it prevents
Harvard separation EBNF production rules (Invariant 1) Agent injection — data cannot contain control flow
Hermeneutic isolation given/trace are Data-only (Invariant 2) Decision context tampering
Trace immutability Traces are Data, Harvard-separated (Invariant 3) Retroactive trace modification
Economic boundary Data = free, Control = costs tokens (Invariant 4) Unaccounted resource consumption
Type-level Harvard Dependent indices are Data (Invariant 5) Side effects in type system
Runtime integrity Sentinel is Data, hashes grammar/types (Invariant 6) Grammar/type-checker tampering

Layer 2 — Type-Level Safety

Property Kategoria Level What it prevents
Type safety L1-3 (basic, ADTs, polymorphism) Type confusion, missing cases
GADT refinement L5 Incorrect type narrowing
Dependent types L6 Value/type mismatch
Linear resources L7 Handle leaks, double-use, use-after-consume
Refinement types L8 (via SMT/ECHIDNA) Predicate violations
Session types L9 Protocol violations, unexpected messages
Path types L10 (via Agda/ECHIDNA) Type equivalence errors
Token budget @budget as linear type Resource exhaustion (DoS)
Capability non-escalation Cap[] type checking Privilege escalation

Layer 3 — Runtime Safety

Property Mechanism What it prevents
Sentinel verification Hash grammar + type rules at startup Tampered parser/type-checker
Attested spawn spawn attested checks sentinel match Compromised agents joining chain
Cross-agent attestation Session protocol attestation step Man-in-the-middle between agents
Supervision trees Supervisors own children, can halt them Runaway agents
Loop safety limit 10,000 iteration maximum Infinite loops

Layer 4 — Observability (not safety, but enables verification)

Property Mechanism What it enables
Decision traces Immutable Data records at branch points Post-hoc audit of agent decisions
Trace memoisation cached branch + query_trace() Verify consistency across executions
Agent-mode errors Structured errors with remediations Automated vulnerability response

Supply Chain Threat Model

The sentinel catches internal tampering (grammar modifications, type rule weakening). It does NOT catch supply chain attacks. This section documents the threat model and mitigations.

Threat: Compromised Parser Generator (pest)

Risk: The pest crate generates code that doesn't match the grammar. The sentinel says "grammar hash: OK" because the grammar FILE is fine, but the COMPILED PARSER behaves differently. Harvard separation silently broken.

Mitigations:

  • cargo-audit for known vulnerabilities (reactive)
  • cargo-deny for license/ban checking
  • Vendor pest + audit
  • Sentinel v2: hash the compiled binary, not just the grammar
  • Dual compilation with independent toolchains

Threat: Compromised Serialisation (serde)

Risk: Traces serialised incorrectly. Immutable Data records corrupted in transit. Decision traces cannot be trusted for Layer 4 analysis.

Mitigations:

  • cargo-audit (reactive)
  • Trace integrity hashing — each trace record includes its own hash
  • Cross-verify traces via ECHIDNA

Threat: Compromised Rust Compiler (Thompson's "Trusting Trust")

Risk: The compiler inserts behaviour the source doesn't specify. The binary does things the grammar, type checker, and sentinel don't know about.

Mitigations:

  • Reproducible builds via Nix (flake.nix) and Guix (guix.scm)
  • Dual compilation (rustc stable vs nightly, or rustc vs mrustc)
  • SLSA provenance attestation (workflow in CI)
  • This is an industry-wide problem, not 007-specific

Threat: Poisoned @neural Models (Hypatia)

Risk: Training data (decision traces) are poisoned upstream. @neural functions learn adversarial patterns. Agents make subtly wrong decisions that appear type-safe.

Mitigations:

  • Hash training data provenance — model integrity verification
  • @neural functions are OPTIONAL — agents can always use @impure instead
  • Trace analysis can detect anomalous @neural outputs (statistical drift)
  • ECHIDNA cross-checking: verify @neural results against @impure fallback

Threat: Compromised Proof Tools (Z3, Agda)

Risk: SMT solver or proof assistant returns false results. Refinement types or path types verified as correct when they aren't.

Mitigations:

  • ECHIDNA multi-backend cross-checking — same obligation on two provers
  • Proof certificates are Data (stored, verifiable, auditable)
  • Extension points (L8, L10) currently emit warnings, not guarantees

Threat: Grammar Weakening via PR

Risk: A subtle change to a production rule (e.g., allowing one control construct in data_expr) breaks Harvard separation by design, not attack.

Mitigations:

  • echidnabot flags grammar changes as CRITICAL security events
  • Sentinel hash changes trigger mandatory review
  • Harvard invariant is testable: just verify-harvard recipe
  • Grammar diff review in every PR that touches .ebnf or .pest

Threat: Dependency Chain

Risk: pest depends on X, which depends on Y, which is compromised. Transitive dependency attack.

Mitigations:

  • cargo-deny with deny-by-default policy
  • SBOM generation (SLSA, REUSE dep5)
  • Minimal dependency footprint (currently: pest, serde, chrono — 3 direct deps)
  • Cargo.lock committed and audited

Supply Chain Mitigations

Action Status
cargo-audit in CI Done (quality.yml)
cargo-deny configuration Done (.machine_readable/compliance/rust/deny.toml)
SLSA provenance Done (release.yml)
Reproducible builds (Nix/Guix) In progress
Sentinel v2 — binary hashing In progress (Sec 21)
Grammar change CI gate Done (echidnabot directive)
ECHIDNA multi-backend cross-check In progress

Comparison to seL4

007's security model is inspired by seL4's approach: prove safety properties at design time rather than test them at runtime. The differences:

seL4 007
Scope Microkernel Agent language
Proof Complete (Isabelle/HOL) Partial (grammar + types + sentinel)
Capabilities Runtime tokens Compile-time types
Information flow Proven noninterference Harvard separation (grammar-enforced)
Supply chain Minimal deps, audited Small dep surface, audited
Multi-party trust Single kernel Attestation chain between agents

007's formal proof roadmap (Lean4 + Idris2 + Agda via ECHIDNA) aims to close the proof gap over time, following seL4's model of shipping first and proving progressively.