Skip to content

Commit 4514341

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
Supply chain threat model + Sentinel v2 (binary/dep/model hashing)
SECURITY.md: comprehensive security architecture document - 6 invariants mapped to grammar/type/runtime layers - Supply chain threat model: compromised pest, serde, rustc, Hypatia models, proof tools, grammar PRs, transitive dependencies - Mitigations for each vector (cargo-audit/deny, reproducible builds, dual compilation, sentinel v2, ECHIDNA cross-checking) - Supply chain roadmap (P0-P3 priorities) - seL4 comparison table Grammar v0.5.0 — Sentinel v2 (Section 21.6): - hash_binary() — SHA-256 of compiled parser+typechecker binary - hash_deps() — Merkle root of Cargo.lock resolved dependencies - hash_neural_model("name") — model weights + training provenance - Full sentinel v2 example with supply chain invariant Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 507e6bb commit 4514341

2 files changed

Lines changed: 204 additions & 9 deletions

File tree

‎SECURITY.md‎

Lines changed: 164 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -22,15 +22,170 @@ Do NOT open a public issue for security vulnerabilities.
2222
This project is classified as dual-use technology (precautionary).
2323
See [DUAL-USE-NOTICE.adoc](DUAL-USE-NOTICE.adoc) for details.
2424

25-
## Security Considerations
25+
## Security Architecture — Verifiable Agent Security by Construction
2626

27-
007 is designed with safety as a core principle:
27+
007 enforces safety properties at the grammar level — violations are parse
28+
errors or type errors, not runtime exceptions. This is "security by
29+
construction": you cannot write an insecure 007 program any more than you
30+
can write a syntactically invalid one.
2831

29-
1. **Harvard Architecture** — agent injection is a parse error
30-
2. **Capability-based security** — agents cannot exceed granted permissions
31-
3. **Linear types** — agent handles cannot leak or duplicate
32-
4. **Session types** — communication protocols are verified at compile time
33-
5. **Supervision trees** — all agents have a known owner with shutdown authority
32+
### Layer 1 — Grammar-Level Safety
3433

35-
These properties are enforced at the grammar level (Layer 1), the type
36-
system (Layer 2), and the operational semantics (Layer 3).
34+
| Property | Mechanism | What it prevents |
35+
|----------|-----------|-----------------|
36+
| **Harvard separation** | EBNF production rules (Invariant 1) | Agent injection — data cannot contain control flow |
37+
| **Hermeneutic isolation** | `given`/`trace` are Data-only (Invariant 2) | Decision context tampering |
38+
| **Trace immutability** | Traces are Data, Harvard-separated (Invariant 3) | Retroactive trace modification |
39+
| **Economic boundary** | Data = free, Control = costs tokens (Invariant 4) | Unaccounted resource consumption |
40+
| **Type-level Harvard** | Dependent indices are Data (Invariant 5) | Side effects in type system |
41+
| **Runtime integrity** | Sentinel is Data, hashes grammar/types (Invariant 6) | Grammar/type-checker tampering |
42+
43+
### Layer 2 — Type-Level Safety
44+
45+
| Property | Kategoria Level | What it prevents |
46+
|----------|----------------|-----------------|
47+
| **Type safety** | L1-3 (basic, ADTs, polymorphism) | Type confusion, missing cases |
48+
| **GADT refinement** | L5 | Incorrect type narrowing |
49+
| **Dependent types** | L6 | Value/type mismatch |
50+
| **Linear resources** | L7 | Handle leaks, double-use, use-after-consume |
51+
| **Refinement types** | L8 (via SMT/ECHIDNA) | Predicate violations |
52+
| **Session types** | L9 | Protocol violations, unexpected messages |
53+
| **Path types** | L10 (via Agda/ECHIDNA) | Type equivalence errors |
54+
| **Token budget** | @budget as linear type | Resource exhaustion (DoS) |
55+
| **Capability non-escalation** | Cap[] type checking | Privilege escalation |
56+
57+
### Layer 3 — Runtime Safety
58+
59+
| Property | Mechanism | What it prevents |
60+
|----------|-----------|-----------------|
61+
| **Sentinel verification** | Hash grammar + type rules at startup | Tampered parser/type-checker |
62+
| **Attested spawn** | `spawn attested` checks sentinel match | Compromised agents joining chain |
63+
| **Cross-agent attestation** | Session protocol attestation step | Man-in-the-middle between agents |
64+
| **Supervision trees** | Supervisors own children, can halt them | Runaway agents |
65+
| **Loop safety limit** | 10,000 iteration maximum | Infinite loops |
66+
67+
### Layer 4 — Observability (not safety, but enables verification)
68+
69+
| Property | Mechanism | What it enables |
70+
|----------|-----------|----------------|
71+
| **Decision traces** | Immutable Data records at branch points | Post-hoc audit of agent decisions |
72+
| **Trace memoisation** | `cached` branch + `query_trace()` | Verify consistency across executions |
73+
| **Agent-mode errors** | Structured errors with remediations | Automated vulnerability response |
74+
75+
## Supply Chain Threat Model
76+
77+
The sentinel catches internal tampering (grammar modifications, type rule
78+
weakening). It does NOT catch supply chain attacks. This section documents
79+
the threat model and mitigations.
80+
81+
### Threat: Compromised Parser Generator (pest)
82+
83+
**Risk:** The pest crate generates code that doesn't match the grammar. The
84+
sentinel says "grammar hash: OK" because the grammar FILE is fine, but the
85+
COMPILED PARSER behaves differently. Harvard separation silently broken.
86+
87+
**Mitigations:**
88+
- `cargo-audit` for known vulnerabilities (reactive)
89+
- `cargo-deny` for license/ban checking
90+
- Vendor pest + audit (planned)
91+
- Sentinel v2: hash the compiled binary, not just the grammar (planned)
92+
- Dual compilation with independent toolchains (planned)
93+
94+
### Threat: Compromised Serialisation (serde)
95+
96+
**Risk:** Traces serialised incorrectly. Immutable Data records corrupted
97+
in transit. Decision traces cannot be trusted for Layer 4 analysis.
98+
99+
**Mitigations:**
100+
- `cargo-audit` (reactive)
101+
- Trace integrity hashing — each trace record includes its own hash
102+
- Cross-verify traces via ECHIDNA (planned)
103+
104+
### Threat: Compromised Rust Compiler (Thompson's "Trusting Trust")
105+
106+
**Risk:** The compiler inserts behaviour the source doesn't specify. The
107+
binary does things the grammar, type checker, and sentinel don't know about.
108+
109+
**Mitigations:**
110+
- Reproducible builds via Nix (`flake.nix`) and Guix (`guix.scm`)
111+
- Dual compilation (rustc stable vs nightly, or rustc vs mrustc)
112+
- SLSA provenance attestation (workflow in CI)
113+
- This is an industry-wide problem, not 007-specific
114+
115+
### Threat: Poisoned @neural Models (Hypatia)
116+
117+
**Risk:** Training data (decision traces) are poisoned upstream. @neural
118+
functions learn adversarial patterns. Agents make subtly wrong decisions
119+
that appear type-safe.
120+
121+
**Mitigations:**
122+
- Hash training data provenance — model integrity verification
123+
- @neural functions are OPTIONAL — agents can always use @impure instead
124+
- Trace analysis can detect anomalous @neural outputs (statistical drift)
125+
- ECHIDNA cross-checking: verify @neural results against @impure fallback
126+
127+
### Threat: Compromised Proof Tools (Z3, Agda)
128+
129+
**Risk:** SMT solver or proof assistant returns false results. Refinement
130+
types or path types verified as correct when they aren't.
131+
132+
**Mitigations:**
133+
- ECHIDNA multi-backend cross-checking — same obligation on two provers
134+
- Proof certificates are Data (stored, verifiable, auditable)
135+
- Extension points (L8, L10) currently emit warnings, not guarantees
136+
137+
### Threat: Grammar Weakening via PR
138+
139+
**Risk:** A subtle change to a production rule (e.g., allowing one control
140+
construct in `data_expr`) breaks Harvard separation by design, not attack.
141+
142+
**Mitigations:**
143+
- `echidnabot` flags grammar changes as CRITICAL security events
144+
- Sentinel hash changes trigger mandatory review
145+
- Harvard invariant is testable: `just verify-harvard` recipe
146+
- Grammar diff review in every PR that touches `.ebnf` or `.pest`
147+
148+
### Threat: Dependency Chain
149+
150+
**Risk:** pest depends on X, which depends on Y, which is compromised.
151+
Transitive dependency attack.
152+
153+
**Mitigations:**
154+
- `cargo-deny` with deny-by-default policy
155+
- SBOM generation (SLSA, REUSE dep5)
156+
- Minimal dependency footprint (currently: pest, serde, chrono — 3 direct deps)
157+
- `Cargo.lock` committed and audited
158+
159+
## Supply Chain Roadmap
160+
161+
| Priority | Action | Status |
162+
|----------|--------|--------|
163+
| P0 | cargo-audit in CI | Done (quality.yml) |
164+
| P0 | cargo-deny configuration | Done (.machine_readable/compliance/rust/deny.toml) |
165+
| P0 | SLSA provenance | Workflow exists (release.yml) |
166+
| P1 | Vendor + audit pest crate | Planned |
167+
| P1 | Reproducible builds (Nix/Guix) | Stubs exist, need completion |
168+
| P1 | Sentinel v2 — binary hashing | Grammar designed (Sec 21) |
169+
| P2 | Dual compilation verification | Planned |
170+
| P2 | @neural model integrity | Planned |
171+
| P2 | ECHIDNA multi-backend cross-check | Architecture designed |
172+
| P3 | Grammar change CI gate | echidnabot directive exists |
173+
| P3 | Full SBOM with transitive dep hashes | Planned |
174+
175+
## Comparison to seL4
176+
177+
007's security model is inspired by seL4's approach: prove safety properties
178+
at design time rather than test them at runtime. The differences:
179+
180+
| | seL4 | 007 |
181+
|---|------|-----|
182+
| Scope | Microkernel | Agent language |
183+
| Proof | Complete (Isabelle/HOL) | Partial (grammar + types + sentinel) |
184+
| Capabilities | Runtime tokens | Compile-time types |
185+
| Information flow | Proven noninterference | Harvard separation (grammar-enforced) |
186+
| Supply chain | Minimal deps, audited | Small dep surface, audit planned |
187+
| Multi-party trust | Single kernel | Attestation chain between agents |
188+
189+
007's formal proof roadmap (Lean4 + Idris2 + Agda via ECHIDNA) aims to
190+
close the proof gap over time, following seL4's model of shipping first
191+
and proving progressively.

‎spec/grammar.ebnf‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1031,6 +1031,46 @@ control_expr = (* ... existing alternatives ... *)
10311031
(* } *)
10321032
(* } *)
10331033
1034+
(* --------------------------------------------------------- *)
1035+
(* 21.6 SENTINEL V2 — Supply chain defence *)
1036+
(* --------------------------------------------------------- *)
1037+
(* Sentinel v1 hashes the grammar and type rules. But a *)
1038+
(* compromised parser generator (pest) or compiler (rustc) *)
1039+
(* could produce a binary that doesn't match the grammar. *)
1040+
(* Sentinel v2 extends to hash the BINARY itself. *)
1041+
1042+
sentinel_hash_call = "hash_grammar" , "(" , ")"
1043+
| "hash_type_rules" , "(" , ")"
1044+
| "hash_invariant" , "(" , string_literal , ")"
1045+
| "hash_binary" , "(" , ")" (* v2 *)
1046+
| "hash_deps" , "(" , ")" (* v2 *)
1047+
| "hash_neural_model" , "(" , string_literal , ")" ; (* v2 *)
1048+
1049+
(* hash_binary() — SHA-256 of the compiled parser+typechecker *)
1050+
(* binary. Detects if the compiler produced unexpected *)
1051+
(* output, or if the binary was modified after compilation. *)
1052+
(* *)
1053+
(* hash_deps() — Merkle root of all dependency hashes *)
1054+
(* (Cargo.lock resolved). Detects transitive supply chain *)
1055+
(* changes. *)
1056+
(* *)
1057+
(* hash_neural_model(name) — hash of @neural model weights *)
1058+
(* and training data provenance. Detects poisoned models. *)
1059+
1060+
(* Full sentinel v2 example: *)
1061+
(* @sentinel integrity_v2 = { *)
1062+
(* grammar_hash: hash_grammar(), *)
1063+
(* type_rules_hash: hash_type_rules(), *)
1064+
(* binary_hash: hash_binary(), *)
1065+
(* deps_hash: hash_deps(), *)
1066+
(* neural_integrity: hash_neural_model("triage_classifier"),*)
1067+
(* invariant: [ *)
1068+
(* hash_invariant("harvard_separation"), *)
1069+
(* hash_invariant("economic_boundary"), *)
1070+
(* hash_invariant("supply_chain") *)
1071+
(* ] *)
1072+
(* } *)
1073+
10341074
(* ========================================================= *)
10351075
(* END OF GRAMMAR — VERSION 0.5.0-draft *)
10361076
(* ========================================================= *)

0 commit comments

Comments
 (0)