diff --git a/AGENTS.md b/AGENTS.md index d7e9bfe..b6a33ff 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -4,23 +4,12 @@ > This file was generated by `rivet init --agents`. Re-run the command > any time artifacts change to keep this file current. -## Formal Verification - -This project uses a three-layer verification pyramid. Follow the -[PulseEngine Verification Guide](https://pulseengine.eu/guides/VERIFICATION-GUIDE.md) -for all proof work. - -- **Kani** (bounded model checking): `#[cfg(kani)]` harnesses in source files -- **Verus** (SMT/Z3): `verus! { }` specs in `src/lib/src/verus_proofs/`, built via `rules_verus` -- **Lean4** (Mathlib): algebraic proofs in `lean/Ed25519.lean`, built via `rules_lean` -- **Rocq** (coq-of-rust): strip Verus annotations → translate via `rules_rocq_rust` - ## Project Overview This project uses **Rivet** for SDLC artifact traceability. - Config: `rivet.yaml` - Schemas: common, dev, stpa, stpa-sec, cybersecurity -- Artifacts: 340 across 23 types +- Artifacts: 452 across 23 types - Validation: `rivet validate` (current status: 9 errors) ## Available Commands @@ -42,29 +31,29 @@ This project uses **Rivet** for SDLC artifact traceability. | Type | Count | Description | |------|------:|-------------| -| `asset` | 22 | An item of value requiring protection — data, function, or component. Identified during TARA (ISO 21434 clause 8). | -| `attack-scenario` | 21 | A security-specific causal pathway describing how a threat agent could cause an unsecure control action or exploit a data flow. Extends STPA loss scenarios with attacker intent, attack feasibility scoring (ISO 21434 Annex H), and links to threat agents. | -| `control-action` | 11 | An action issued by a controller to a controlled process or another controller. | -| `controlled-process` | 7 | A process being controlled — the physical or data transformation acted upon by controllers. | -| `controller` | 10 | A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process. | -| `controller-constraint` | 12 | A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do. | -| `cybersecurity-design` | 22 | Architecture or design element addressing cybersecurity requirements. SEC.2 outcome — security mechanisms, protocols, algorithms. | +| `asset` | 25 | An item of value requiring protection — data, function, or component. Identified during TARA (ISO 21434 clause 8). | +| `attack-scenario` | 33 | A security-specific causal pathway describing how a threat agent could cause an unsecure control action or exploit a data flow. Extends STPA loss scenarios with attacker intent, attack feasibility scoring (ISO 21434 Annex H), and links to threat agents. | +| `control-action` | 14 | An action issued by a controller to a controlled process or another controller. | +| `controlled-process` | 8 | A process being controlled — the physical or data transformation acted upon by controllers. | +| `controller` | 13 | A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process. | +| `controller-constraint` | 26 | A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do. | +| `cybersecurity-design` | 27 | Architecture or design element addressing cybersecurity requirements. SEC.2 outcome — security mechanisms, protocols, algorithms. | | `cybersecurity-goal` | 13 | A top-level cybersecurity requirement derived from TARA results. Equivalent to a cybersecurity goal in ISO 21434 clause 9. | | `cybersecurity-implementation` | 3 | Implementation artifact for a cybersecurity design element. SEC.3 outcome — code, configuration, key management. | -| `cybersecurity-req` | 17 | A detailed cybersecurity requirement derived from cybersecurity goals. SEC.1 outcome (ISO 21434 clause 9). | -| `cybersecurity-verification` | 29 | Verification measure for cybersecurity requirements. SEC.4 outcome — includes penetration testing, fuzzing, code review, static analysis, vulnerability scanning. | -| `data-flow` | 16 | A flow of data between controllers, controlled processes, or external entities. Data flows are first-class objects in STPA-DFSec, enabling analysis of confidentiality, integrity, and availability properties on data in transit — not just control actions. Critical for reasoning about key material, tokens, certificates, and trust bundles moving through the system. | +| `cybersecurity-req` | 24 | A detailed cybersecurity requirement derived from cybersecurity goals. SEC.1 outcome (ISO 21434 clause 9). | +| `cybersecurity-verification` | 34 | Verification measure for cybersecurity requirements. SEC.4 outcome — includes penetration testing, fuzzing, code review, static analysis, vulnerability scanning. | +| `data-flow` | 22 | A flow of data between controllers, controlled processes, or external entities. Data flows are first-class objects in STPA-DFSec, enabling analysis of confidentiality, integrity, and availability properties on data in transit — not just control actions. Critical for reasoning about key material, tokens, certificates, and trust bundles moving through the system. | | `design-decision` | 7 | An architectural or design decision with rationale | -| `feature` | 10 | A user-visible capability or feature | -| `hazard` | 20 | A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. | -| `loss` | 9 | An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. | +| `feature` | 11 | A user-visible capability or feature | +| `hazard` | 35 | A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. | +| `loss` | 10 | An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. | | `requirement` | 14 | A functional or non-functional requirement | | `risk-assessment` | 24 | Combined risk level from threat feasibility and impact. Determines whether a cybersecurity goal is needed (ISO 21434 clause 8). | -| `security-property` | 10 | A security property (CIA + authenticity + non-repudiation) required on a controlled process, data flow, or controller. Annotates the STPA control structure with security-specific requirements that drive the identification of unsecure control actions. | -| `system-constraint` | 19 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. | +| `security-property` | 12 | A security property (CIA + authenticity + non-repudiation) required on a controlled process, data flow, or controller. Annotates the STPA control structure with security-specific requirements that drive the identification of unsecure control actions. | +| `system-constraint` | 33 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. | | `threat-agent` | 5 | An entity (person, organization, or automated system) that could intentionally or unintentionally cause an unsecure control action. Models attacker capability, motivation, and access level for feasibility assessment aligned with ISO/SAE 21434 Annex H. | -| `threat-scenario` | 18 | A potential attack scenario against an asset. Part of TARA (ISO 21434 clause 8). | -| `uca` | 21 | An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long | +| `threat-scenario` | 24 | A potential attack scenario against an asset. Part of TARA (ISO 21434 clause 8). | +| `uca` | 35 | An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long | | `loss-scenario` | 0 | A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. | | `sub-hazard` | 0 | A refinement of a hazard into a more specific unsafe condition. | diff --git a/artifacts/cybersecurity/assets-and-threats.yaml b/artifacts/cybersecurity/assets-and-threats.yaml index 9412b0c..3ad550d 100644 --- a/artifacts/cybersecurity/assets-and-threats.yaml +++ b/artifacts/cybersecurity/assets-and-threats.yaml @@ -840,3 +840,145 @@ artifacts: links: - type: assesses target: TS-018 + + # ── Post-quantum and advanced assets ─────────────────────────────────── + + - id: ASSET-023 + type: asset + title: SLH-DSA Key Pair + status: approved + description: > + Post-quantum signing key pair for hybrid signatures using SLH-DSA + (FIPS 205). Used alongside Ed25519 to provide quantum-resistant + signature capability for long-lived embedded targets. + fields: + asset-type: key-material + cybersecurity-properties: + - confidentiality + - integrity + + - id: ASSET-024 + type: asset + title: CT Log Public Keys + status: approved + description: > + Trusted public keys for SCT (Signed Certificate Timestamp) verification, + used to validate that Fulcio certificates were logged in Certificate + Transparency logs. + fields: + asset-type: key-material + cybersecurity-properties: + - integrity + - availability + + - id: ASSET-025 + type: asset + title: DSSE Envelope + status: approved + description: > + Dead Simple Signing Envelope wrapping in-toto statements, providing + authenticated payload type and content binding for attestation + signatures. + fields: + asset-type: data + cybersecurity-properties: + - integrity + - authenticity + + # ── Advanced threat scenarios ────────────────────────────────────────── + + - id: TS-019 + type: threat-scenario + title: PQC Signature Stripping + status: approved + description: > + Attacker strips the post-quantum (SLH-DSA) signature from a hybrid-signed + module, leaving only the classical Ed25519 signature. If verification + accepts partial signatures, the module loses quantum resistance. + fields: + attack-vector: network + attack-feasibility: low + impact: major + links: + - type: threatens + target: ASSET-023 + + - id: TS-020 + type: threat-scenario + title: PQC Algorithm Negotiation Downgrade + status: approved + description: > + Attacker manipulates algorithm negotiation to force classical-only + signing, bypassing post-quantum protection. Mitigated by requiring + all-or-nothing hybrid verification when PQC is configured. + fields: + attack-vector: network + attack-feasibility: low + impact: major + links: + - type: threatens + target: ASSET-023 + + - id: TS-021 + type: threat-scenario + title: Proof Cache Poisoning via Verified-then-Revoked Entry + status: approved + description: > + Attacker exploits a cached Rekor inclusion proof for a key that has + since been revoked. If the cache does not invalidate entries on key + revocation, verification succeeds with a compromised key. + fields: + attack-vector: network + attack-feasibility: low + impact: major + links: + - type: threatens + target: ASSET-007 + + - id: TS-022 + type: threat-scenario + title: CT Log Key Compromise + status: approved + description: > + Attacker compromises a Certificate Transparency log's signing key, + enabling fabrication of SCTs that appear to prove certificate logging + without actual log inclusion. + fields: + attack-vector: network + attack-feasibility: very-low + impact: severe + links: + - type: threatens + target: ASSET-024 + + - id: TS-023 + type: threat-scenario + title: SCT Stripping Attack + status: approved + description: > + Attacker strips Signed Certificate Timestamps from a Fulcio certificate, + preventing verification of CT log inclusion. If SCT presence is not + enforced, certificates may be accepted without transparency guarantees. + fields: + attack-vector: network + attack-feasibility: low + impact: major + links: + - type: threatens + target: ASSET-024 + + - id: TS-024 + type: threat-scenario + title: Build Environment Metadata Spoofing + status: approved + description: > + Attacker spoofs build environment metadata (compiler version, Nix hash, + platform) in SLSA provenance attestations, masking a compromised build + pipeline while producing apparently-legitimate provenance claims. + fields: + attack-vector: adjacent + attack-feasibility: low + impact: major + links: + - type: threatens + target: ASSET-017 diff --git a/artifacts/cybersecurity/goals-and-requirements.yaml b/artifacts/cybersecurity/goals-and-requirements.yaml index a708c86..eb318ef 100644 --- a/artifacts/cybersecurity/goals-and-requirements.yaml +++ b/artifacts/cybersecurity/goals-and-requirements.yaml @@ -1149,6 +1149,9 @@ artifacts: type: cybersecurity-verification title: Kani bounded model checking — varint status: approved + description: > + Formally verifies varint encoding roundtrip correctness, absence of + panics, overflow safety, bounded allocation, and deterministic output. fields: method: formal-verification steps: cargo kani --harness proof_put_get32_roundtrip proof_get32_no_panic proof_get32_no_overflow proof_get_slice_bounded_allocation proof_put_deterministic @@ -1160,6 +1163,9 @@ artifacts: type: cybersecurity-verification title: Kani bounded model checking — format detection status: approved + description: > + Formally verifies format detection correctness and domain separation + between WASM, ELF, and MCUboot signing formats. fields: method: formal-verification links: @@ -1172,6 +1178,9 @@ artifacts: type: cybersecurity-verification title: Kani bounded model checking — Merkle tree status: approved + description: > + Formally verifies Merkle tree inclusion proof construction and + verification correctness under bounded inputs. fields: method: formal-verification links: @@ -1182,6 +1191,9 @@ artifacts: type: cybersecurity-verification title: Kani bounded model checking — DSSE PAE injectivity status: approved + description: > + Formally verifies DSSE Pre-Authentication Encoding injectivity, + ensuring distinct payloads produce distinct PAE encodings. fields: method: formal-verification links: @@ -1298,7 +1310,7 @@ artifacts: JSON, deserializes back identically, and that the builder pattern produces correct attestations for all field combinations. fields: - method: test + method: automated-test tool: cargo-test links: - type: verifies @@ -1313,7 +1325,7 @@ artifacts: runs and that cargo build produces deterministic output within the Nix environment. fields: - method: test + method: automated-test tool: nix links: - type: verifies @@ -1341,7 +1353,7 @@ artifacts: from_env_vars() reads WSC_* variables, to_slsa_internal_params() produces valid JSON, and serialization roundtrips correctly. fields: - method: test + method: automated-test tool: cargo-test links: - type: verifies @@ -1393,7 +1405,7 @@ artifacts: cosign config serialization, binary integrity checks, and signing/verification result types. fields: - method: test + method: automated-test tool: cargo-test links: - type: verifies @@ -1410,8 +1422,283 @@ artifacts: invalidation, multiple entries, key serialization, and thread safety properties. fields: - method: test + method: automated-test tool: cargo-test links: - type: verifies target: CD-22 + + # ────────────────────────────────────────────────── + # Phase 3: Component Model, PQC, and Advanced Requirements + # ────────────────────────────────────────────────── + + # Requirements + - id: CR-18 + type: cybersecurity-req + title: Component model section handling must be complete + status: approved + description: > + WASM Component Model signing must correctly parse, preserve, and sign + all component sections including nested modules, ensuring no section + is silently dropped or corrupted during the signing process. + fields: + req-type: integrity + priority: must + verification-criteria: > + Component model roundtrip preserves all sections; nested modules + are correctly handled; no silent section dropping. + links: + - type: derives-from + target: CG-13 + + - id: CR-19 + type: cybersecurity-req + title: Hybrid signature verification must be all-or-nothing + status: approved + description: > + When post-quantum hybrid signing is configured, verification must + require both the classical (Ed25519) and post-quantum (SLH-DSA) + signatures to be present and valid. Partial signatures must be + rejected to prevent downgrade attacks. + fields: + req-type: integrity + priority: must + verification-criteria: > + Verification rejects modules with only classical or only PQC + signature when hybrid mode is configured. + links: + - type: derives-from + target: CG-1 + + - id: CR-20 + type: cybersecurity-req + title: Proof cache entries must be invalidated on key revocation + status: approved + description: > + Rekor proof cache entries must be invalidated when the associated + signing key is revoked, preventing acceptance of modules signed by + compromised keys through stale cache hits. + fields: + req-type: integrity + priority: must + verification-criteria: > + Cache lookup returns miss for entries whose signing key has been + revoked; revocation triggers immediate cache invalidation. + links: + - type: derives-from + target: CG-8 + + - id: CR-21 + type: cybersecurity-req + title: Fulcio certificates MUST embed valid SCTs from trusted CT logs + status: approved + description: > + Fulcio certificates must contain Signed Certificate Timestamps (SCTs) + from trusted Certificate Transparency logs. Verification must reject + certificates without valid SCTs to ensure transparency guarantees. + fields: + req-type: authentication + priority: must + verification-criteria: > + Verification rejects Fulcio certificates missing SCTs or containing + SCTs from untrusted CT logs. + links: + - type: derives-from + target: CG-7 + + - id: CR-22 + type: cybersecurity-req + title: Checkpoint persistence MUST be atomic and integrity-protected + status: approved + description: > + Rekor checkpoint files must be written atomically using temp-file-plus- + rename to prevent partial writes. Checkpoint integrity must be verified + on load to detect corruption. + fields: + req-type: integrity + priority: must + verification-criteria: > + Checkpoint writes are atomic; partial writes do not corrupt existing + checkpoints; integrity check detects tampered checkpoints on load. + links: + - type: derives-from + target: CG-8 + + - id: CR-23 + type: cybersecurity-req + title: Bundle serialization MUST preserve all verification material fields + status: approved + description: > + Sigstore bundle serialization and deserialization must preserve all + verification material fields including certificates, inclusion proofs, + and signed timestamps without loss or reordering. + fields: + req-type: integrity + priority: must + verification-criteria: > + Bundle roundtrip serialization preserves all fields; schema validation + rejects bundles with missing required fields. + links: + - type: derives-from + target: CG-3 + + - id: CR-24 + type: cybersecurity-req + title: DSSE verification must support configurable threshold policies + status: approved + description: > + DSSE envelope verification must support configurable signature threshold + policies (e.g., require N-of-M valid signatures) to enable multi-party + signing workflows. + fields: + req-type: authentication + priority: should + verification-criteria: > + Verification enforces configured threshold; rejects envelopes with + fewer valid signatures than the threshold requires. + links: + - type: derives-from + target: CG-1 + + # Design + - id: CD-23 + type: cybersecurity-design + title: Component-aware recursive parser + status: draft + description: > + WASM Component Model parser that recursively handles nested components + and modules, preserving all sections during signing. Uses bounded + recursion depth to prevent stack overflow from crafted inputs. + fields: + mechanism: format-handler + links: + - type: satisfies + target: CR-18 + + - id: CD-24 + type: cybersecurity-design + title: Hybrid signature format and verification pipeline + status: draft + description: > + Dual-signature format embedding both Ed25519 and SLH-DSA signatures + in the WASM custom section. Verification pipeline enforces all-or-nothing + validation when hybrid mode is configured, rejecting partial signatures. + fields: + mechanism: hybrid-signing + algorithm: Ed25519+SLH-DSA + links: + - type: satisfies + target: CR-19 + + - id: CD-25 + type: cybersecurity-design + title: SCT verification pipeline with trusted CT log set + status: draft + description: > + Verifier for Signed Certificate Timestamps embedded in Fulcio + certificates. Maintains a configurable set of trusted CT log public + keys and validates SCT signatures against them. + fields: + mechanism: certificate-transparency + algorithm: ECDSA-P256-SHA256 + links: + - type: satisfies + target: CR-21 + + - id: CD-26 + type: cybersecurity-design + title: Atomic file checkpoint store with temp+rename + status: draft + description: > + Checkpoint persistence using atomic temp-file-plus-rename pattern. + Writes checkpoint to a temporary file in the same directory, then + atomically renames to the target path. Integrity verified via + embedded checksum on load. + fields: + mechanism: atomic-persistence + links: + - type: satisfies + target: CR-22 + + - id: CD-27 + type: cybersecurity-design + title: SigstoreBundle with schema validation + status: draft + description: > + Sigstore bundle serialization with strict schema validation ensuring + all verification material fields (certificates, inclusion proofs, + signed timestamps) are preserved through serialization roundtrips. + fields: + mechanism: bundle-serialization + algorithm: JSON-canonical + links: + - type: satisfies + target: CR-23 + + # Verification + - id: CV-30 + type: cybersecurity-verification + title: Component model signing roundtrip tests + status: draft + description: > + Verify that WASM Component Model modules can be signed and verified + with all sections preserved, including nested components and modules. + fields: + method: automated-test + links: + - type: verifies + target: CD-23 + + - id: CV-31 + type: cybersecurity-verification + title: PQC hybrid signing roundtrip tests + status: draft + description: > + Verify that hybrid Ed25519+SLH-DSA signing and verification works + end-to-end, and that partial signature stripping is detected and + rejected. + fields: + method: automated-test + links: + - type: verifies + target: CD-24 + + - id: CV-32 + type: cybersecurity-verification + title: SCT verification tests + status: draft + description: > + Verify that SCT validation correctly accepts valid SCTs from trusted + CT logs and rejects invalid or missing SCTs. + fields: + method: automated-test + links: + - type: verifies + target: CD-25 + + - id: CV-33 + type: cybersecurity-verification + title: Checkpoint consistency verification tests + status: draft + description: > + Verify that checkpoint persistence is atomic, partial writes do not + corrupt existing checkpoints, and integrity checks detect tampering. + fields: + method: automated-test + links: + - type: verifies + target: CD-26 + + - id: CV-34 + type: cybersecurity-verification + title: Bundle format conformance tests + status: draft + description: > + Verify that Sigstore bundle serialization roundtrips preserve all + fields and that schema validation rejects bundles with missing + required verification material. + fields: + method: automated-test + links: + - type: verifies + target: CD-27 diff --git a/artifacts/dev/features.yaml b/artifacts/dev/features.yaml index 0428f11..a63d19e 100644 --- a/artifacts/dev/features.yaml +++ b/artifacts/dev/features.yaml @@ -484,3 +484,14 @@ artifacts: Kani bounded model checking on every PR touching proof files. fields: phase: phase-2 + + - id: FEAT-11 + type: feature + title: WASM Component Model signing + status: in-progress + description: > + Support signing and verification of WASM Component Model modules, + including recursive handling of nested components and preservation + of all component sections during the signing process. + fields: + phase: phase-2 diff --git a/artifacts/stpa/attack-scenarios.yaml b/artifacts/stpa/attack-scenarios.yaml index b10f5b9..ee6c0c8 100644 --- a/artifacts/stpa/attack-scenarios.yaml +++ b/artifacts/stpa/attack-scenarios.yaml @@ -591,3 +591,297 @@ artifacts: target: TA-3 - type: leads-to-hazard target: H-17 + + # ────────────────────────────────────────────────── + # Round 3: v0.6.x Feature Coverage — Attack Scenarios + # ────────────────────────────────────────────────── + + - id: AS-22 + type: attack-scenario + title: Nested module substitution in WASM component + status: draft + description: > + Attacker replaces a nested module within a signed WASM component + with a malicious version. Because the signing process does not + traverse nested modules, the outer signature remains valid and the + modified component passes verification. + fields: + attack-type: supply-chain-compromise + attack-feasibility: low + impact-safety: severe + impact-financial: severe + impact-operational: severe + impact-privacy: none + links: + - type: exploits + target: UCA-22 + - type: executed-by + target: TA-1 + - type: leads-to-hazard + target: H-22 + + - id: AS-23 + type: attack-scenario + title: Quantum downgrade -- strip PQC from hybrid sig + status: draft + description: > + Attacker strips the post-quantum (ML-DSA) component from a hybrid + signature, leaving only the classical Ed25519 component. If the + verifier does not require the PQC component, the downgraded + signature passes verification and the system loses quantum + resistance. + fields: + attack-type: exploit-vulnerability + attack-feasibility: low + impact-safety: moderate + impact-financial: major + impact-operational: major + impact-privacy: none + links: + - type: exploits + target: UCA-24 + - type: executed-by + target: TA-1 + - type: leads-to-hazard + target: H-23 + + - id: AS-24 + type: attack-scenario + title: Cache pre-population with verified-then-revoked proof + status: draft + description: > + Insider obtains a legitimately signed and verified proof, waits for + the signing key to be revoked, then exploits the cache TTL window. + The cached proof continues to return success for the revoked key + until the cache entry expires. + fields: + attack-type: replay-attack + attack-feasibility: low + impact-safety: moderate + impact-financial: major + impact-operational: major + impact-privacy: none + links: + - type: exploits + target: UCA-27 + - type: executed-by + target: TA-2 + - type: leads-to-hazard + target: H-26 + + - id: AS-25 + type: attack-scenario + title: Cache memory exhaustion via unique hashes + status: draft + description: > + Attacker submits a large number of verification requests with unique + module hashes, causing the proof cache to grow without bound. Without + cache size limits, this exhausts available memory and causes denial + of service for the verification service. + fields: + attack-type: denial-of-service + attack-feasibility: medium + impact-safety: none + impact-financial: negligible + impact-operational: moderate + impact-privacy: none + links: + - type: exploits + target: UCA-26 + - type: executed-by + target: TA-3 + - type: leads-to-hazard + target: H-25 + + - id: AS-26 + type: attack-scenario + title: CT log key compromise enables undetected mis-issuance + status: draft + description: > + Attacker compromises a CT log signing key and forges SCTs for + mis-issued Fulcio certificates. Because the SCT monitor verifies + against the wrong (compromised) key, the forged SCTs pass + validation and the mis-issued certificates appear monitored. + fields: + attack-type: credential-theft + attack-feasibility: very-low + impact-safety: severe + impact-financial: severe + impact-operational: severe + impact-privacy: none + links: + - type: exploits + target: UCA-29 + - type: executed-by + target: TA-1 + - type: leads-to-hazard + target: H-28 + + - id: AS-27 + type: attack-scenario + title: SCT stripping from Fulcio certificate + status: draft + description: > + Insider with access to the signing pipeline strips the embedded SCT + extension from a Fulcio certificate before it is stored in the + Sigstore bundle. If the SCT monitor does not require SCTs, the + certificate is accepted without CT monitoring. + fields: + attack-type: exploit-vulnerability + attack-feasibility: low + impact-safety: moderate + impact-financial: major + impact-operational: major + impact-privacy: none + links: + - type: exploits + target: UCA-28 + - type: executed-by + target: TA-2 + - type: leads-to-hazard + target: H-27 + + - id: AS-28 + type: attack-scenario + title: Checkpoint file replacement with stale state + status: draft + description: > + Insider replaces the persisted checkpoint file with an older + checkpoint. Without a consistency proof requirement, the verifier + accepts the stale checkpoint and cannot detect log entries that + were added after the replaced checkpoint. + fields: + attack-type: replay-attack + attack-feasibility: low + impact-safety: moderate + impact-financial: major + impact-operational: major + impact-privacy: none + links: + - type: exploits + target: UCA-30 + - type: executed-by + target: TA-2 + - type: leads-to-hazard + target: H-29 + + - id: AS-29 + type: attack-scenario + title: Split-view log attack via concurrent checkpoint corruption + status: draft + description: > + Attacker triggers concurrent checkpoint writes to exploit non-atomic + persistence. The resulting corrupted checkpoint file causes the + verifier to reset to a known-good but stale state, enabling a + split-view attack where the attacker presents a forked log view. + fields: + attack-type: exploit-vulnerability + attack-feasibility: low + impact-safety: moderate + impact-financial: major + impact-operational: major + impact-privacy: none + links: + - type: exploits + target: UCA-31 + - type: executed-by + target: TA-1 + - type: leads-to-hazard + target: H-30 + + - id: AS-30 + type: attack-scenario + title: Bundle tlog entry stripping + status: draft + description: > + Insider strips the transparency log entry from a Sigstore bundle + before distributing it. If the verification module does not require + tlog entries, the bundle is accepted without transparency log + proof, bypassing the accountability guarantee. + fields: + attack-type: exploit-vulnerability + attack-feasibility: low + impact-safety: moderate + impact-financial: major + impact-operational: major + impact-privacy: none + links: + - type: exploits + target: UCA-32 + - type: executed-by + target: TA-2 + - type: leads-to-hazard + target: H-31 + + - id: AS-31 + type: attack-scenario + title: PATH poisoning for build env capture + status: draft + description: > + Supply chain attacker modifies the PATH environment variable in the + build environment to point to a directory containing trojanized tool + binaries. When the CLI controller captures build environment metadata + by running tools via PATH, the attacker's binaries execute with + signing process privileges. + fields: + attack-type: supply-chain-compromise + attack-feasibility: low + impact-safety: severe + impact-financial: severe + impact-operational: severe + impact-privacy: none + links: + - type: exploits + target: UCA-34 + - type: executed-by + target: TA-3 + - type: leads-to-hazard + target: H-34 + + - id: AS-32 + type: attack-scenario + title: WSC_RUSTC_VERSION env var spoofing + status: draft + description: > + Supply chain attacker sets the WSC_RUSTC_VERSION or similar + environment variables to spoof build provenance metadata. The + signed artifact's attestation claims a trusted toolchain version + while the actual build used a compromised compiler. + fields: + attack-type: supply-chain-compromise + attack-feasibility: medium + impact-safety: none + impact-financial: moderate + impact-operational: moderate + impact-privacy: none + links: + - type: exploits + target: UCA-34 + - type: executed-by + target: TA-3 + - type: leads-to-hazard + target: H-34 + + - id: AS-33 + type: attack-scenario + title: DSSE policy bypass via single compromised key + status: draft + description: > + Attacker compromises one of N signing keys in a multi-party signing + setup. Because DSSE verification accepts any single valid signature + regardless of the configured threshold policy, the attacker can sign + and verify payloads unilaterally, bypassing the k-of-n requirement. + fields: + attack-type: exploit-vulnerability + attack-feasibility: low + impact-safety: severe + impact-financial: severe + impact-operational: severe + impact-privacy: none + links: + - type: exploits + target: UCA-35 + - type: executed-by + target: TA-1 + - type: leads-to-hazard + target: H-35 diff --git a/artifacts/stpa/control-structure.yaml b/artifacts/stpa/control-structure.yaml index 7823153..a6e1ddf 100644 --- a/artifacts/stpa/control-structure.yaml +++ b/artifacts/stpa/control-structure.yaml @@ -386,3 +386,107 @@ artifacts: status: draft description: > Pushing, pulling, and managing signatures in OCI container registries. + + # ────────────────────────────────────────────────── + # Round 3: STPA-Sec Gap Closure + # ────────────────────────────────────────────────── + + - id: CTRL-11 + type: controller + title: Component Model Parser + status: draft + description: > + Parses and hashes WASM component model sections, ensuring nested + modules and their relationships are correctly identified for + component-aware signing and verification. + fields: + controller-type: automated + process-model: + - "Component model structure is valid" + - "All nested modules are enumerated" + - "Component hash covers all child modules" + + - id: CTRL-12 + type: controller + title: SCT Monitor + status: draft + description: > + Monitors Certificate Transparency logs for mis-issuance by verifying + Signed Certificate Timestamps embedded in Fulcio certificates. + fields: + controller-type: automated + process-model: + - "SCT signature is valid against trusted CT log key" + - "CT log is in the trusted log list" + - "SCT timestamp is within acceptable window" + + - id: CTRL-13 + type: controller + title: Checkpoint Consistency Verifier + status: draft + description: > + Verifies Rekor checkpoint monotonicity to detect log tampering or + split-view attacks by ensuring checkpoints only grow over time. + fields: + controller-type: automated + process-model: + - "Checkpoint tree size is monotonically increasing" + - "Consistency proof verifies between old and new root" + - "Checkpoint signature is valid" + + - id: CP-8 + type: controlled-process + title: WASM Component Processing + status: draft + description: > + Component-model-aware module processing that handles nested modules, + type imports/exports, and component-level hashing for signing and + verification of WASM components. + + - id: CA-12 + type: control-action + title: Parse and hash component model tree + status: draft + description: > + The component model parser traverses the component structure, enumerates + nested modules, and computes a Merkle hash over the component tree for + signing and verification. + fields: + action: Parse and hash component model tree + links: + - type: issued-by + target: CTRL-11 + - type: acts-on + target: CP-8 + + - id: CA-13 + type: control-action + title: Verify SCT signature against trusted CT log + status: draft + description: > + The SCT monitor verifies the Signed Certificate Timestamp signature + embedded in a Fulcio certificate against the trusted Certificate + Transparency log public key. + fields: + action: Verify SCT signature against trusted CT log + links: + - type: issued-by + target: CTRL-12 + - type: acts-on + target: CP-3 + + - id: CA-14 + type: control-action + title: Verify checkpoint consistency proof + status: draft + description: > + The checkpoint consistency verifier checks that a new Rekor checkpoint + is consistent with the previously observed checkpoint, ensuring log + append-only semantics. + fields: + action: Verify checkpoint consistency proof + links: + - type: issued-by + target: CTRL-13 + - type: acts-on + target: CP-3 diff --git a/artifacts/stpa/data-flows.yaml b/artifacts/stpa/data-flows.yaml index da40fa6..6a7fe60 100644 --- a/artifacts/stpa/data-flows.yaml +++ b/artifacts/stpa/data-flows.yaml @@ -480,8 +480,11 @@ artifacts: fields: source: CTRL-3 destination: CP-5 - data-type: attestation-chain - sensitivity: integrity-critical + data-type: attestation + sensitivity: critical + protection: + - cryptographic-binding + - hash-chain links: - type: flows-from target: CTRL-3 @@ -491,3 +494,154 @@ artifacts: target: SP-2 - type: carries target: SP-6 + + # ────────────────────────────────────────────────── + # Round 3: STPA-Sec Gap Closure + # ────────────────────────────────────────────────── + + - id: DF-17 + type: data-flow + title: Component Nested Module Content Flow + status: draft + description: > + Nested module binary content flows from the component model parser + to the WASM component processing pipeline for hashing and signature + coverage. + fields: + data-type: binary + sensitivity: critical + persistence: transient + protection: + - hash-verification + links: + - type: flows-from + target: CTRL-11 + - type: flows-to + target: CP-8 + + - id: DF-18 + type: data-flow + title: PQC Key Material Flow + status: draft + description: > + Post-quantum cryptographic key material flows from the CLI controller + to the WASM module processing pipeline for quantum-resistant signing + operations. + fields: + data-type: cryptographic-key + sensitivity: critical + persistence: transient + protection: + - memory-only + - zeroization-on-drop + links: + - type: flows-from + target: CTRL-1 + - type: flows-to + target: CP-1 + + - id: DF-19 + type: data-flow + title: Cached Proof Data Flow + status: draft + description: > + Cached Rekor inclusion and consistency proofs flow from the verification + module to key material storage for offline verification support. + fields: + data-type: attestation + sensitivity: high + persistence: persistent + protection: + - integrity-check + links: + - type: flows-from + target: CTRL-4 + - type: flows-to + target: CP-2 + + - id: DF-20 + type: data-flow + title: SCT from Fulcio Certificate + status: draft + description: > + Signed Certificate Timestamp extracted from Fulcio certificate flows + to the SCT monitor for Certificate Transparency verification. + fields: + data-type: attestation + sensitivity: high + persistence: transient + protection: + - signature-verification + links: + - type: flows-from + target: CTRL-12 + - type: flows-to + target: CP-2 + + - id: DF-21 + type: data-flow + title: Checkpoint Persistence Flow + status: draft + description: > + Rekor checkpoint data flows from the checkpoint consistency verifier + to key material storage for persistence and future consistency checks. + fields: + data-type: attestation + sensitivity: high + persistence: persistent + protection: + - integrity-check + links: + - type: flows-from + target: CTRL-13 + - type: flows-to + target: CP-2 + + - id: DF-22 + type: data-flow + title: Bundle Format Conversion + status: draft + description: > + Trust bundle attestation data flows from the verification module to + Sigstore infrastructure for format conversion between bundle versions. + fields: + data-type: attestation + sensitivity: high + persistence: transient + protection: + - integrity-check + links: + - type: flows-from + target: CTRL-4 + - type: flows-to + target: CP-3 + + - id: SP-11 + type: security-property + title: PQC key material confidentiality + status: draft + description: > + Post-quantum cryptographic key material must never be exposed outside + the signing module boundary, in memory dumps, logs, or error messages, + maintaining the same confidentiality guarantees as classical keys. + fields: + property-type: confidentiality + required-level: critical + links: + - type: property-of + target: DF-18 + + - id: SP-12 + type: security-property + title: Proof cache integrity + status: draft + description: > + Cached Rekor inclusion and consistency proofs must maintain integrity + to prevent replay or substitution attacks that could cause acceptance + of revoked or invalid signatures. + fields: + property-type: integrity + required-level: high + links: + - type: property-of + target: DF-19 diff --git a/artifacts/stpa/losses-and-hazards.yaml b/artifacts/stpa/losses-and-hazards.yaml index e6bfbff..6e88ed2 100644 --- a/artifacts/stpa/losses-and-hazards.yaml +++ b/artifacts/stpa/losses-and-hazards.yaml @@ -666,3 +666,399 @@ artifacts: links: - type: prevents target: H-17 + + # --------------------------------------------------------------------------- + # Round 3: v0.6.x Feature Coverage — Losses + # --------------------------------------------------------------------------- + - id: L-10 + type: loss + title: Loss of WASM component model integrity + status: draft + description: > + Nested module content within a WASM component is not covered by the + outer signature, allowing an attacker to substitute or tamper with + inner modules while the top-level signature remains valid. This + undermines the component model's compositional trust guarantees. + + # --------------------------------------------------------------------------- + # Round 3: v0.6.x Feature Coverage — Hazards + # --------------------------------------------------------------------------- + - id: H-21 + type: hazard + title: Component section reordering invalidates signature + status: draft + description: > + Reordering sections within a WASM component invalidates the signature + even though the semantic content is unchanged, causing false + verification failures for legitimately signed components. + links: + - type: leads-to-loss + target: L-10 + + - id: H-22 + type: hazard + title: Nested module substitution in signed component + status: draft + description: > + An attacker substitutes a nested module within a signed WASM component + without invalidating the outer signature, because the signature does + not cover the full component tree recursively. + links: + - type: leads-to-loss + target: L-10 + + - id: H-23 + type: hazard + title: PQC hybrid verification skips post-quantum component + status: draft + description: > + Hybrid signature verification accepts the classical (Ed25519) component + alone without verifying the post-quantum (ML-DSA) component, leaving + the system vulnerable to quantum-capable adversaries. + links: + - type: leads-to-loss + target: L-2 + + - id: H-24 + type: hazard + title: PQC key material too large for embedded flash + status: draft + description: > + Post-quantum key material exceeds the available flash storage on + constrained embedded devices, causing key truncation or storage + failures that prevent successful verification. + links: + - type: leads-to-loss + target: L-6 + + - id: H-25 + type: hazard + title: Proof cache poisoning accepts revoked entries + status: draft + description: > + An attacker poisons the proof cache with entries that reference + revoked or invalid transparency log proofs, causing subsequent + verifications to accept stale or revoked signatures from cache. + links: + - type: leads-to-loss + target: L-2 + + - id: H-26 + type: hazard + title: Cache TTL too long allows stale proofs after revocation + status: draft + description: > + The proof cache time-to-live is set too long, allowing cached proofs + to remain valid after the underlying certificate or key has been + revoked, creating a window of vulnerability. + links: + - type: leads-to-loss + target: L-2 + + - id: H-27 + type: hazard + title: SCT verification accepts forged CT log signature + status: draft + description: > + Signed Certificate Timestamp verification accepts a forged CT log + signature because the verification does not properly validate the + log's signing key against a trusted key set. + links: + - type: leads-to-loss + target: L-2 + + - id: H-28 + type: hazard + title: SCT monitoring fails silently + status: draft + description: > + SCT monitoring encounters errors (network failures, malformed + responses) but fails open, allowing certificates without valid SCTs + to be accepted without alerting operators. + links: + - type: leads-to-loss + target: L-3 + + - id: H-29 + type: hazard + title: Checkpoint store corruption accepts split-view log + status: draft + description: > + The checkpoint store is corrupted or tampered with, causing the + verifier to accept a split-view transparency log where different + clients see different log contents. + links: + - type: leads-to-loss + target: L-2 + + - id: H-30 + type: hazard + title: Checkpoint race condition leaves stale state + status: draft + description: > + Concurrent checkpoint updates create a race condition where a stale + checkpoint overwrites a newer one, allowing the verifier to accept + log entries that have been superseded or revoked. + links: + - type: leads-to-loss + target: L-2 + + - id: H-31 + type: hazard + title: Sigstore bundle format mismatch breaks cosign verify + status: draft + description: > + The Sigstore bundle produced by sigil uses a format or media type + that cosign or other verifiers do not recognize, causing + interoperability failures and verification rejection. + links: + - type: leads-to-loss + target: L-4 + + - id: H-32 + type: hazard + title: Bundle missing mandatory fields accepted as valid + status: draft + description: > + A Sigstore bundle with missing mandatory fields (verification + material, message signature, or log entries) is accepted as valid, + allowing incomplete or forged bundles to pass verification. + links: + - type: leads-to-loss + target: L-2 + + - id: H-33 + type: hazard + title: Build environment metadata spoofed via env vars + status: draft + description: > + Build environment attestation metadata is captured from environment + variables that an attacker can control, allowing spoofed build + provenance to be embedded in signatures. + links: + - type: leads-to-loss + target: L-3 + + - id: H-34 + type: hazard + title: Build environment capture executes attacker-controlled binaries + status: draft + description: > + Build environment capture invokes tool binaries discovered via PATH, + allowing an attacker who controls PATH to execute arbitrary code + during the signing process. + links: + - type: leads-to-loss + target: L-5 + + - id: H-35 + type: hazard + title: DSSE verify() accepts single valid sig hiding compromised key + status: draft + description: > + DSSE multi-signature verification accepts a payload when any single + signature is valid, allowing an attacker with one compromised key to + bypass a multi-party signing policy. + links: + - type: leads-to-loss + target: L-3 + + # --------------------------------------------------------------------------- + # Round 3: v0.6.x Feature Coverage — System Constraints + # --------------------------------------------------------------------------- + - id: SC-20 + type: system-constraint + title: Signature MUST cover full component tree including nested modules + status: draft + description: > + Signature computation MUST cover the full component tree including + all nested modules, ensuring that substitution of any inner module + invalidates the outer signature. + links: + - type: prevents + target: H-22 + - type: protects + target: SP-2 + + - id: SC-21 + type: system-constraint + title: Parser MUST recursively traverse component nesting + status: draft + description: > + The component parser MUST recursively traverse all levels of + component nesting to produce a canonical byte sequence for signing, + preventing section reordering attacks. + links: + - type: prevents + target: H-21 + - type: protects + target: SP-2 + + - id: SC-22 + type: system-constraint + title: Hybrid verification MUST check both classical and PQC signatures + status: draft + description: > + Hybrid signature verification MUST independently verify both the + classical and post-quantum signature components, rejecting the + bundle if either component fails. + links: + - type: prevents + target: H-23 + - type: protects + target: SP-1 + + - id: SC-23 + type: system-constraint + title: PQC key material MUST be zeroized on drop + status: draft + description: > + Post-quantum key material MUST be zeroized from memory on drop, + using the same zeroize-on-drop guarantees applied to classical + key material. + links: + - type: prevents + target: H-24 + - type: protects + target: SP-3 + + - id: SC-24 + type: system-constraint + title: Cache MUST only store proofs verified cryptographically + status: draft + description: > + The proof cache MUST only store entries whose cryptographic proofs + have been independently verified, preventing cache poisoning with + invalid or revoked entries. + links: + - type: prevents + target: H-25 + - type: protects + target: SP-6 + + - id: SC-25 + type: system-constraint + title: Cache MUST be bounded in size + status: draft + description: > + The proof cache MUST enforce a maximum entry count and total size + bound, evicting oldest entries first, to prevent unbounded growth + and resource exhaustion. + links: + - type: prevents + target: H-25 + - type: protects + target: SP-8 + + - id: SC-26 + type: system-constraint + title: SCT signatures MUST be verified against trusted CT log keys + status: draft + description: > + Signed Certificate Timestamp signatures MUST be verified against + a trusted set of CT log public keys, rejecting SCTs signed by + unknown or untrusted logs. + links: + - type: prevents + target: H-27 + - type: protects + target: SP-6 + + - id: SC-27 + type: system-constraint + title: SCT monitoring MUST fail-closed when no valid SCTs found + status: draft + description: > + SCT monitoring MUST fail-closed, rejecting certificates when no + valid SCTs can be obtained or verified, rather than silently + accepting unmonitored certificates. + links: + - type: prevents + target: H-28 + - type: protects + target: SP-6 + + - id: SC-28 + type: system-constraint + title: Checkpoint store MUST be atomically updated + status: draft + description: > + Checkpoint store updates MUST be atomic (write-then-rename), + ensuring that a crash or concurrent access never leaves the + store in a corrupt or partially-written state. + links: + - type: prevents + target: H-29 + - type: protects + target: SP-6 + + - id: SC-29 + type: system-constraint + title: Checkpoint MUST persist across process restarts + status: draft + description: > + The latest verified checkpoint MUST be persisted to durable + storage and loaded on process restart, preventing rollback to + an earlier log state. + links: + - type: prevents + target: H-30 + - type: protects + target: SP-6 + + - id: SC-30 + type: system-constraint + title: Bundle MUST include complete verification material + status: draft + description: > + Sigstore bundles MUST include all mandatory verification material + (certificate chain, transparency log entry, timestamps) and MUST + be rejected if any required field is absent. + links: + - type: prevents + target: H-32 + - type: protects + target: SP-6 + + - id: SC-31 + type: system-constraint + title: Bundle media type MUST be validated before parsing + status: draft + description: > + The Sigstore bundle media type MUST be validated against the + expected value before parsing, ensuring interoperability with + cosign and other Sigstore verifiers. + links: + - type: prevents + target: H-31 + - type: protects + target: SP-2 + + - id: SC-32 + type: system-constraint + title: Build env capture MUST NOT trust user-supplied PATH + status: draft + description: > + Build environment capture MUST use hardcoded absolute paths for + tool invocation and MUST NOT rely on the user-supplied PATH + environment variable, preventing PATH injection attacks. + links: + - type: prevents + target: H-34 + - type: protects + target: SP-3 + + - id: SC-33 + type: system-constraint + title: DSSE multi-sig verification policy MUST be configurable + status: draft + description: > + DSSE multi-signature verification MUST support configurable + threshold policies (e.g., k-of-n), defaulting to requiring all + signatures to be valid, preventing single-key compromise from + bypassing multi-party signing requirements. + links: + - type: prevents + target: H-35 + - type: protects + target: SP-6 diff --git a/artifacts/stpa/ucas.yaml b/artifacts/stpa/ucas.yaml index 6a2a73f..0552341 100644 --- a/artifacts/stpa/ucas.yaml +++ b/artifacts/stpa/ucas.yaml @@ -699,3 +699,573 @@ artifacts: target: CTRL-10 - type: leads-to-hazard target: H-17 + + # ────────────────────────────────────────────────── + # Round 3: v0.6.x Feature Coverage — UCAs + # ────────────────────────────────────────────────── + + - id: UCA-22 + type: uca + title: Sign component WITHOUT traversing nested modules + status: draft + description: > + Component Model Parser signs a WASM component without recursively + traversing nested modules. The outer signature covers only top-level + sections, allowing an attacker to substitute inner modules without + invalidating the signature. + fields: + uca-type: providing + context: > + WASM component with nested modules signed using flat section hash + rationale: > + Nested module substitution bypasses signature integrity for + component model artifacts. + links: + - type: issued-by + target: CTRL-11 + - type: leads-to-hazard + target: H-22 + + - id: UCA-23 + type: uca + title: Verify component with core-module-only parser + status: draft + description: > + Component Model Parser uses a core-module-only parser to verify a + WASM component, ignoring component-specific sections such as type + imports, nested modules, and component-level metadata. Verification + succeeds on partial content. + fields: + uca-type: providing + context: > + WASM component verified using core module parser that ignores + component sections + rationale: > + Component sections not covered by verification allow tampering + with type bindings and nested module references. + links: + - type: issued-by + target: CTRL-11 + - type: leads-to-hazard + target: H-21 + + - id: UCA-24 + type: uca + title: Verify hybrid sig WITHOUT checking PQC component + status: draft + description: > + Verification Module checks only the classical Ed25519 component of a + hybrid signature, skipping the post-quantum ML-DSA component. A + quantum-capable adversary can forge the classical signature while the + PQC component is never validated. + fields: + uca-type: not-providing + context: > + Hybrid signature verified with classical-only code path + rationale: > + Skipping PQC verification negates the entire purpose of hybrid + signatures for quantum resistance. + links: + - type: issued-by + target: CTRL-4 + - type: leads-to-hazard + target: H-23 + + - id: UCA-25 + type: uca + title: Sign with PQC key WITHOUT domain separation + status: draft + description: > + CLI Controller signs using a post-quantum key without domain + separation between classical and PQC signature contexts. This allows + cross-protocol signature reuse where a signature from one context is + replayed in the other. + fields: + uca-type: providing + context: > + PQC signing context shares same domain tag as classical signing + rationale: > + Lack of domain separation enables signature confusion attacks + between classical and post-quantum verification paths. + links: + - type: issued-by + target: CTRL-1 + - type: leads-to-hazard + target: H-23 + + - id: UCA-26 + type: uca + title: Insert cache entry WITHOUT prior verification + status: draft + description: > + Verification Module inserts a proof into the cache without first + cryptographically verifying it. An attacker who can influence cache + inputs can pre-populate the cache with invalid or fabricated proofs. + fields: + uca-type: providing + context: > + Proof inserted into cache before cryptographic verification completes + rationale: > + Unverified cache entries poison subsequent lookups, accepting + invalid proofs from cache. + links: + - type: issued-by + target: CTRL-4 + - type: leads-to-hazard + target: H-25 + + - id: UCA-27 + type: uca + title: Return cached proof AFTER key revocation + status: draft + description: > + Verification Module returns a cached proof after the underlying + signing key or certificate has been revoked. The cache does not + check revocation status, creating a window where revoked signatures + continue to verify successfully. + fields: + uca-type: providing + context: > + Cached proof served after certificate revocation but before TTL expiry + rationale: > + Stale cached proofs bypass revocation, allowing revoked keys to + remain effective for the cache TTL duration. + links: + - type: issued-by + target: CTRL-4 + - type: leads-to-hazard + target: H-26 + + - id: UCA-28 + type: uca + title: Accept Fulcio cert WITHOUT valid SCT + status: draft + description: > + SCT Monitor accepts a Fulcio certificate that does not contain a + valid Signed Certificate Timestamp, failing to detect certificates + issued outside of Certificate Transparency monitoring. + fields: + uca-type: not-providing + context: > + Fulcio certificate accepted without embedded SCT validation + rationale: > + Missing SCT check allows mis-issued certificates to go + undetected by CT monitoring. + links: + - type: issued-by + target: CTRL-12 + - type: leads-to-hazard + target: H-27 + + - id: UCA-29 + type: uca + title: Verify SCT against wrong CT log key + status: draft + description: > + SCT Monitor verifies the Signed Certificate Timestamp against an + incorrect or attacker-controlled CT log public key, accepting forged + SCTs that appear valid but were not issued by a trusted log. + fields: + uca-type: providing + context: > + SCT verified against stale or attacker-substituted CT log key + rationale: > + Wrong key for SCT verification allows forged timestamps to pass, + undermining Certificate Transparency guarantees. + links: + - type: issued-by + target: CTRL-12 + - type: leads-to-hazard + target: H-28 + + - id: UCA-30 + type: uca + title: Accept checkpoint WITHOUT consistency proof + status: draft + description: > + Checkpoint Consistency Verifier accepts a new Rekor checkpoint + without verifying a consistency proof against the previously observed + checkpoint. An attacker can present a forked or truncated log without + detection. + fields: + uca-type: not-providing + context: > + New checkpoint accepted without consistency proof from previous state + rationale: > + Missing consistency proof allows split-view log attacks where + different clients see different log contents. + links: + - type: issued-by + target: CTRL-13 + - type: leads-to-hazard + target: H-29 + + - id: UCA-31 + type: uca + title: Persist checkpoint with non-atomic write + status: draft + description: > + Checkpoint Consistency Verifier persists a checkpoint using a + non-atomic write operation. A crash or concurrent access during the + write leaves the checkpoint file in a corrupt or partially-written + state, causing the verifier to fall back to an earlier checkpoint or + fail to detect log tampering. + fields: + uca-type: providing + context: > + Checkpoint written directly to file without atomic rename + rationale: > + Non-atomic writes can corrupt checkpoint state, enabling rollback + to stale log views. + links: + - type: issued-by + target: CTRL-13 + - type: leads-to-hazard + target: H-30 + + - id: UCA-32 + type: uca + title: Produce bundle WITHOUT tlog entries + status: draft + description: > + Verification Module produces a Sigstore bundle that omits + transparency log entries. Downstream verifiers (cosign, policy + controllers) that require tlog entries reject the bundle, breaking + interoperability. + fields: + uca-type: providing + context: > + Bundle serialized without tlog entry after Rekor submission failure + rationale: > + Incomplete bundles cause verification failures in downstream + Sigstore ecosystem tools. + links: + - type: issued-by + target: CTRL-4 + - type: leads-to-hazard + target: H-31 + + - id: UCA-33 + type: uca + title: Parse bundle WITHOUT media type validation + status: draft + description: > + Verification Module parses a Sigstore bundle without validating the + media type field, accepting bundles in unrecognized or deprecated + formats that may have different field semantics or missing mandatory + fields. + fields: + uca-type: not-providing + context: > + Bundle parsed without checking mediaType matches expected version + rationale: > + Missing media type check allows malformed or forged bundles with + unexpected structure to be accepted. + links: + - type: issued-by + target: CTRL-4 + - type: leads-to-hazard + target: H-32 + + - id: UCA-34 + type: uca + title: Capture build env from untrusted PATH + status: draft + description: > + CLI Controller captures build environment metadata by invoking tool + binaries discovered via the PATH environment variable. An attacker + who controls PATH can cause arbitrary code execution during the + signing process or inject spoofed build metadata. + fields: + uca-type: providing + context: > + Build env capture runs rustc --version via user-controlled PATH + rationale: > + PATH-based tool discovery allows code injection and build + provenance spoofing. + links: + - type: issued-by + target: CTRL-1 + - type: leads-to-hazard + target: H-34 + + - id: UCA-35 + type: uca + title: Verify DSSE with any-one-of when policy requires all + status: draft + description: > + Verification Module verifies a DSSE envelope by accepting the + payload when any single signature is valid, ignoring the configured + multi-signature threshold policy. An attacker with one compromised + key bypasses k-of-n signing requirements. + fields: + uca-type: providing + context: > + DSSE verify() returns success on first valid signature regardless + of threshold + rationale: > + Any-one-of verification defeats multi-party signing policies + intended to prevent single-key compromise. + links: + - type: issued-by + target: CTRL-4 + - type: leads-to-hazard + target: H-35 + + # ────────────────────────────────────────────────── + # Round 3: v0.6.x Feature Coverage — Controller Constraints + # ────────────────────────────────────────────────── + + - id: CC-13 + type: controller-constraint + title: Component Model Parser MUST traverse nested modules when signing + status: draft + description: > + The component model parser must recursively traverse all nested + modules within a WASM component and include them in the hash + computation, ensuring substitution of any inner module invalidates + the signature. + fields: + constraint: "The component model parser must recursively traverse all nested modules within a WASM component and include them in the hash computation" + links: + - type: constrains-controller + target: CTRL-11 + - type: inverts-uca + target: UCA-22 + - type: prevents + target: H-22 + + - id: CC-14 + type: controller-constraint + title: Component Model Parser MUST use component-aware parser + status: draft + description: > + The component model parser must use a component-aware parser that + recognizes component-specific sections, type imports, and nested + module references, never falling back to a core-module-only parser. + fields: + constraint: "The component model parser must use a component-aware parser that recognizes component-specific sections, type imports, and nested module references" + links: + - type: constrains-controller + target: CTRL-11 + - type: inverts-uca + target: UCA-23 + - type: prevents + target: H-21 + + - id: CC-15 + type: controller-constraint + title: Verification Module MUST verify both PQC and classical components + status: draft + description: > + The verification module must independently verify both the classical + and post-quantum signature components of a hybrid signature, rejecting + the bundle if either component fails verification. + fields: + constraint: "The verification module must independently verify both the classical and post-quantum signature components of a hybrid signature" + links: + - type: constrains-controller + target: CTRL-4 + - type: inverts-uca + target: UCA-24 + - type: prevents + target: H-23 + + - id: CC-16 + type: controller-constraint + title: CLI Controller MUST use domain-separated signing for PQC + status: draft + description: > + The CLI controller must use distinct domain separation tags for + classical and post-quantum signing contexts, preventing cross-protocol + signature reuse between Ed25519 and ML-DSA verification paths. + fields: + constraint: "The CLI controller must use distinct domain separation tags for classical and post-quantum signing contexts" + links: + - type: constrains-controller + target: CTRL-1 + - type: inverts-uca + target: UCA-25 + - type: prevents + target: H-23 + + - id: CC-17 + type: controller-constraint + title: Verification Module MUST verify proof before caching + status: draft + description: > + The verification module must cryptographically verify a proof before + inserting it into the cache, ensuring the cache never contains + unverified or fabricated entries. + fields: + constraint: "The verification module must cryptographically verify a proof before inserting it into the cache" + links: + - type: constrains-controller + target: CTRL-4 + - type: inverts-uca + target: UCA-26 + - type: prevents + target: H-25 + + - id: CC-18 + type: controller-constraint + title: Verification Module MUST check revocation before returning cached proof + status: draft + description: > + The verification module must check the revocation status of the + underlying certificate or key before returning a cached proof, + ensuring revoked credentials are not accepted via stale cache entries. + fields: + constraint: "The verification module must check the revocation status of the underlying certificate or key before returning a cached proof" + links: + - type: constrains-controller + target: CTRL-4 + - type: inverts-uca + target: UCA-27 + - type: prevents + target: H-26 + + - id: CC-19 + type: controller-constraint + title: SCT Monitor MUST require valid SCTs + status: draft + description: > + The SCT monitor must require at least one valid Signed Certificate + Timestamp in every Fulcio certificate, rejecting certificates that + lack SCTs or contain only invalid SCTs. + fields: + constraint: "The SCT monitor must require at least one valid Signed Certificate Timestamp in every Fulcio certificate" + links: + - type: constrains-controller + target: CTRL-12 + - type: inverts-uca + target: UCA-28 + - type: prevents + target: H-27 + + - id: CC-20 + type: controller-constraint + title: SCT Monitor MUST verify SCT against correct trusted log key + status: draft + description: > + The SCT monitor must verify each Signed Certificate Timestamp against + the correct trusted CT log public key from the trusted log list, + rejecting SCTs signed by unknown or mismatched keys. + fields: + constraint: "The SCT monitor must verify each Signed Certificate Timestamp against the correct trusted CT log public key from the trusted log list" + links: + - type: constrains-controller + target: CTRL-12 + - type: inverts-uca + target: UCA-29 + - type: prevents + target: H-28 + + - id: CC-21 + type: controller-constraint + title: Checkpoint Consistency Verifier MUST require consistency proof + status: draft + description: > + The checkpoint consistency verifier must require a valid consistency + proof between the previously observed checkpoint and any new + checkpoint before accepting the new state. + fields: + constraint: "The checkpoint consistency verifier must require a valid consistency proof between the previously observed checkpoint and any new checkpoint" + links: + - type: constrains-controller + target: CTRL-13 + - type: inverts-uca + target: UCA-30 + - type: prevents + target: H-29 + + - id: CC-22 + type: controller-constraint + title: Checkpoint Consistency Verifier MUST use atomic write for checkpoint persistence + status: draft + description: > + The checkpoint consistency verifier must use atomic write operations + (write-then-rename) for checkpoint persistence, ensuring a crash or + concurrent access never leaves the checkpoint in a corrupt state. + fields: + constraint: "The checkpoint consistency verifier must use atomic write operations (write-then-rename) for checkpoint persistence" + links: + - type: constrains-controller + target: CTRL-13 + - type: inverts-uca + target: UCA-31 + - type: prevents + target: H-30 + + - id: CC-23 + type: controller-constraint + title: Verification Module MUST include tlog entries in bundle + status: draft + description: > + The verification module must include transparency log entries in + every Sigstore bundle, ensuring downstream verifiers can validate + the bundle without additional network requests. + fields: + constraint: "The verification module must include transparency log entries in every Sigstore bundle" + links: + - type: constrains-controller + target: CTRL-4 + - type: inverts-uca + target: UCA-32 + - type: prevents + target: H-31 + + - id: CC-24 + type: controller-constraint + title: Verification Module MUST validate bundle media type + status: draft + description: > + The verification module must validate the bundle media type against + the expected value before parsing, rejecting bundles with + unrecognized or deprecated media types. + fields: + constraint: "The verification module must validate the bundle media type against the expected value before parsing" + links: + - type: constrains-controller + target: CTRL-4 + - type: inverts-uca + target: UCA-33 + - type: prevents + target: H-32 + + - id: CC-25 + type: controller-constraint + title: CLI Controller MUST NOT use PATH for tool discovery + status: draft + description: > + The CLI controller must use hardcoded absolute paths for build + environment tool invocation, never relying on the user-supplied + PATH environment variable for tool discovery. + fields: + constraint: "The CLI controller must use hardcoded absolute paths for build environment tool invocation, never relying on the user-supplied PATH" + links: + - type: constrains-controller + target: CTRL-1 + - type: inverts-uca + target: UCA-34 + - type: prevents + target: H-34 + + - id: CC-26 + type: controller-constraint + title: Verification Module MUST enforce configured multi-sig threshold policy + status: draft + description: > + The verification module must enforce the configured multi-signature + threshold policy during DSSE verification, requiring the specified + k-of-n valid signatures rather than accepting any single valid + signature. + fields: + constraint: "The verification module must enforce the configured multi-signature threshold policy during DSSE verification" + links: + - type: constrains-controller + target: CTRL-4 + - type: inverts-uca + target: UCA-35 + - type: prevents + target: H-35 diff --git a/docs/superpowers/plans/2026-03-27-component-model-stpa-pqc.md b/docs/superpowers/plans/2026-03-27-component-model-stpa-pqc.md new file mode 100644 index 0000000..5e45f0f --- /dev/null +++ b/docs/superpowers/plans/2026-03-27-component-model-stpa-pqc.md @@ -0,0 +1,430 @@ +# WASM Component Model Signing + STPA-Sec Gap Closure + PQC Implementation Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** Add WASM Component Model signing support, close all STPA-Sec analysis gaps for v0.6.x features, and prepare for v0.7.0 release with full traceability. + +**Architecture:** Three phases: (1) STPA-Sec gap closure — add 80+ rivet artifacts for features A-H, fix validation warnings; (2) WASM Component Model signing — extend the parser for component-layer sections, recursive nested module hashing, and roundtrip tests; (3) PQC integration preparation — domain-separated hybrid signing pipeline with all-or-nothing verification. + +**Tech Stack:** Rust 1.90.0, Bazel 8.5.1, rivet CLI, Kani, cargo-mutants + +--- + +## File Structure + +### Phase 1: STPA-Sec Artifacts (rivet YAML) +- Modify: `artifacts/stpa/losses-and-hazards.yaml` — add L-10, H-21–H-35, SC-20–SC-33 +- Modify: `artifacts/stpa/control-structure.yaml` — add CTRL-11–13, CA-12–14, CP-8 +- Modify: `artifacts/stpa/data-flows.yaml` — add DF-17–22, SP-11–12, fix DF-16 +- Modify: `artifacts/stpa/ucas.yaml` — add UCA-22–35, CC-13–26 +- Modify: `artifacts/stpa/attack-scenarios.yaml` — add AS-22–32 +- Modify: `artifacts/cybersecurity/goals-and-requirements.yaml` — add CR-18–24, CD-23–27, CV-30–34, fix existing +- Modify: `artifacts/cybersecurity/assets-and-threats.yaml` — add ASSET-023–25, TS-019–24 +- Modify: `artifacts/dev/features.yaml` — add FEAT-11 (component model), fix REQ links + +### Phase 2: WASM Component Model Signing (Rust) +- Modify: `src/lib/src/wasm_module/mod.rs` — extend SectionId for component sections, add recursive nesting support +- Create: `src/lib/src/wasm_module/component.rs` — component-model-aware parsing and hashing +- Modify: `src/lib/src/wasm_module/mod.rs` tests — add component model roundtrip tests +- Create: `fuzz/fuzz_targets/fuzz_component_model.rs` — fuzz target for component parsing +- Modify: `fuzz/Cargo.toml` — add fuzz target + +### Phase 3: PQC Hybrid Signing (Rust) +- Modify: `src/lib/src/pqc.rs` — add HybridSigner/HybridVerifier traits, domain separation +- Modify: `src/lib/src/signature/mod.rs` — wire hybrid signing into signature pipeline +- Modify: `src/cli/main.rs` — add --pqc flag + +--- + +## Phase 1: STPA-Sec Gap Closure + +### Task 1: Add losses, hazards, and system constraints for new features + +**Files:** +- Modify: `artifacts/stpa/losses-and-hazards.yaml` + +- [ ] **Step 1: Add L-10 (component model integrity loss)** + +```yaml + - id: L-10 + type: loss + title: Loss of WASM component model integrity + description: > + Nested module content within a WASM component is not covered by + the outer signature, allowing substitution of inner modules + without detection. + links: + - type: leads-to-loss + target: L-1 +``` + +- [ ] **Step 2: Add H-21 through H-35 (15 new hazards)** + +Add hazards for: component section reordering (H-21), nested module substitution (H-22), PQC hybrid verification skip (H-23), PQC key size constraints (H-24), proof cache poisoning (H-25), cache TTL staleness (H-26), SCT signature forgery (H-27), SCT silent failure (H-28), checkpoint corruption (H-29), checkpoint race condition (H-30), bundle format mismatch (H-31), bundle field stripping (H-32), build env spoofing (H-33), build env PATH poisoning (H-34), DSSE single-sig acceptance (H-35). + +Each hazard must have `leads-to-loss` link to the appropriate loss. + +- [ ] **Step 3: Add SC-20 through SC-33 (14 system constraints)** + +Each constraint inverts its hazard. SC-20: signature covers full component tree. SC-21: parser recurses component nesting. SC-22: hybrid verification checks both. SC-23: PQC zeroization. SC-24: cache stores only verified proofs. SC-25: cache bounded size. SC-26: SCT verified against trusted logs. SC-27: SCT fail-closed. SC-28: checkpoint atomic update. SC-29: checkpoint persists across restarts. SC-30: bundle includes complete material. SC-31: bundle media type validated. SC-32: build env doesn't trust PATH. SC-33: DSSE multi-sig policy configurable. + +Each constraint must have `prevents` link to its hazard and `protects` link to relevant security properties. + +- [ ] **Step 4: Run `rivet validate` and fix any errors** + +Run: `rivet validate 2>&1 | grep -v "synth:" | grep -v "kiln:" | grep ERROR` +Expected: 0 local errors + +- [ ] **Step 5: Commit** + +```bash +git add artifacts/stpa/losses-and-hazards.yaml +git commit -m "stpa: add losses, hazards, constraints for component model, PQC, cache, SCT, checkpoint, bundle, build-env, DSSE" +``` + +### Task 2: Add controllers, control actions, processes, and data flows + +**Files:** +- Modify: `artifacts/stpa/control-structure.yaml` +- Modify: `artifacts/stpa/data-flows.yaml` + +- [ ] **Step 1: Add CTRL-11 (Component Model Parser), CTRL-12 (SCT Monitor), CTRL-13 (Checkpoint Verifier)** + +- [ ] **Step 2: Add CA-12 (parse/hash component tree), CA-13 (verify SCT), CA-14 (verify checkpoint consistency)** + +- [ ] **Step 3: Add CP-8 (WASM Component Processing)** + +- [ ] **Step 4: Add DF-17 through DF-22 (6 data flows) and SP-11, SP-12** + +DF-17: component nested module content. DF-18: PQC key material. DF-19: cached proof data. DF-20: SCT from certificate. DF-21: checkpoint persistence. DF-22: bundle format conversion. + +SP-11: PQC key material confidentiality. SP-12: proof cache integrity. + +- [ ] **Step 5: Fix DF-16 field values** (`data-type`, `sensitivity`) + +- [ ] **Step 6: Run `rivet validate`, fix errors, commit** + +```bash +git add artifacts/stpa/control-structure.yaml artifacts/stpa/data-flows.yaml +git commit -m "stpa: add controllers, data flows, security properties for new features" +``` + +### Task 3: Add UCAs, controller constraints, and attack scenarios + +**Files:** +- Modify: `artifacts/stpa/ucas.yaml` +- Modify: `artifacts/stpa/attack-scenarios.yaml` + +- [ ] **Step 1: Add UCA-22 through UCA-35 (14 UCAs)** + +Each UCA links to its controller and hazard. Full list: + +- UCA-22: Sign component WITHOUT traversing nested modules (→ H-22) +- UCA-23: Verify component with core-module-only parser (→ H-21) +- UCA-24: Verify hybrid sig WITHOUT checking PQC component (→ H-23) +- UCA-25: Sign with PQC key WITHOUT domain separation (→ H-23) +- UCA-26: Insert cache entry WITHOUT prior verification (→ H-25) +- UCA-27: Return cached proof AFTER key revocation (→ H-26) +- UCA-28: Accept Fulcio cert WITHOUT valid SCT (→ H-27) +- UCA-29: Verify SCT against wrong CT log key (→ H-28) +- UCA-30: Accept checkpoint WITHOUT consistency proof (→ H-29) +- UCA-31: Persist checkpoint with non-atomic write (→ H-30) +- UCA-32: Produce bundle WITHOUT tlog entries (→ H-31) +- UCA-33: Parse bundle WITHOUT media type validation (→ H-32) +- UCA-34: Capture build env from untrusted PATH (→ H-34) +- UCA-35: Verify DSSE with any-one-of when policy requires all (→ H-35) + +- [ ] **Step 2: Add CC-13 through CC-26 (controller constraints inverting UCAs)** + +Also add missing CC for existing container UCAs (UCA-16 through UCA-21). + +- [ ] **Step 3: Add AS-22 through AS-32 (11 attack scenarios)** + +AS-22: nested module substitution. AS-23: quantum downgrade. AS-24: cache pre-population. AS-25: cache memory exhaustion. AS-26: CT log compromise. AS-27: SCT stripping. AS-28: checkpoint file replacement. AS-29: split-view. AS-30: bundle field stripping. AS-31: PATH poisoning. AS-32: env var spoofing. + +Plus AS-33: DSSE policy bypass — attacker compromises one of N signing keys, DSSE verify() succeeds on the remaining valid signature, hiding the compromise. + +Each links to its UCA, hazard, and threat agent. + +- [ ] **Step 4: Run `rivet validate`, fix errors, commit** + +```bash +git add artifacts/stpa/ucas.yaml artifacts/stpa/attack-scenarios.yaml +git commit -m "stpa: add UCAs, controller constraints, attack scenarios for all new features" +``` + +### Task 4: Add cybersecurity requirements, designs, verifications + +**Files:** +- Modify: `artifacts/cybersecurity/goals-and-requirements.yaml` +- Modify: `artifacts/cybersecurity/assets-and-threats.yaml` +- Modify: `artifacts/dev/features.yaml` + +- [ ] **Step 1: Add ASSET-023 (SLH-DSA key pair), ASSET-024 (CT log keys), ASSET-025 (DSSE envelope)** + +- [ ] **Step 2: Add TS-019 through TS-024 (6 threat scenarios)** + +- [ ] **Step 3: Add CR-18 through CR-24 (7 cybersecurity requirements)** + +- [ ] **Step 4: Add CD-23 through CD-27 (5 cybersecurity designs)** + +- [ ] **Step 5: Add CV-30 through CV-34 (5 cybersecurity verifications)** + +- [ ] **Step 6: Fix existing validation warnings** + +- Fix CV-25–29: `method: test` → `method: automated-test` +- Fix CV-16–19: add `description` field +- Fix REQ-3, REQ-12, REQ-13, REQ-14: add satisfying links +- Add FEAT-11 (Component Model Signing) to features.yaml + +- [ ] **Step 7: Run `rivet validate`, fix all local errors, commit** + +```bash +git add artifacts/ +git commit -m "cybersecurity: add requirements, designs, verifications, assets, threats; fix validation warnings" +``` + +### Task 5: PR and merge Phase 1 + +- [ ] **Step 1: Run full test suite** `cargo test -p wsc` +- [ ] **Step 2: Run `rivet validate` — verify 0 local errors** +- [ ] **Step 3: Run `rivet init --agents` to refresh AGENTS.md** +- [ ] **Step 4: Create PR, watch CI, merge** + +--- + +## Phase 2: WASM Component Model Signing + +### Task 5b: Verify rivet and Bazel before starting Phase 2 + +- [ ] **Step 1: Confirm rivet is clean** + +Run: `rivet validate 2>&1 | grep -v "synth:" | grep -v "kiln:" | grep ERROR` +Expected: 0 local errors + +- [ ] **Step 2: Confirm Bazel builds** + +Run: `bazel build //src/lib:wsc //src/cli:wasmsign_cli` +Expected: BUILD SUCCESSFUL + +--- + +### Task 6: Write failing tests for component model signing + +**Files:** +- Modify: `src/lib/src/wasm_module/mod.rs` (tests section) + +- [ ] **Step 1: Write test_component_model_sign_verify** + +```rust +#[test] +fn test_component_model_sign_verify() { + // Component model header: \0asm + version 0x0d 0x00 0x01 0x00 + let component_bytes = build_minimal_component(); + let module = Module::deserialize(&component_bytes).expect("should parse component"); + + let kp = KeyPair::generate(); + let signed = module.sign(&kp.sk).expect("should sign component"); + let verified = signed.verify(&kp.pk); + assert!(verified.is_ok(), "should verify component signature"); +} +``` + +- [ ] **Step 2: Write test_component_nested_module_coverage** + +```rust +#[test] +fn test_component_nested_module_coverage() { + // Component with a nested core module inside + let component = build_component_with_nested_module(b"inner module content"); + let module = Module::deserialize(&component).expect("should parse"); + + let kp = KeyPair::generate(); + let signed = module.sign(&kp.sk).expect("should sign"); + + // Tamper with the nested module content + let mut tampered = signed.serialize(); + // Modify a byte in the nested module region + tamper_nested_content(&mut tampered); + + let tampered_module = Module::deserialize(&tampered).expect("should parse tampered"); + assert!(tampered_module.verify(&kp.pk).is_err(), "tampered nested content must fail verification"); +} +``` + +- [ ] **Step 3: Run tests to verify they fail** + +Run: `cargo test -p wsc test_component_model` +Expected: FAIL (functions not implemented) + +- [ ] **Step 4: Commit failing tests** + +```bash +git commit -m "test: add failing tests for WASM component model signing (SC-20)" +``` + +### Task 7: Implement component model section parsing + +**Files:** +- Create: `src/lib/src/wasm_module/component.rs` +- Modify: `src/lib/src/wasm_module/mod.rs` + +- [ ] **Step 1: Add component section IDs** + +Extend `SectionId` or create `ComponentSectionId` enum per the WASM Component Model binary spec: +- 0x00 = Custom (same as core) +- 0x01 = CoreModule (nested core module) +- 0x02 = CoreInstance +- 0x03 = CoreType +- 0x04 = Component (nested component) +- 0x05 = Instance +- 0x06 = Alias +- 0x07 = Type +- 0x08 = Canon +- 0x09 = Start +- 0x0A = Import +- 0x0B = Export + +- [ ] **Step 2: Add recursive component traversal** + +When a component-layer section contains a nested core module or component, recurse into it and include its content in the hash computation. + +- [ ] **Step 3: Ensure signature covers full component tree** + +The hash must cover ALL bytes from the component header through all sections including nested modules. The existing full-module hash approach should work, but verify with the nested module test. + +- [ ] **Step 4: Run tests** + +Run: `cargo test -p wsc test_component_model` +Expected: PASS + +- [ ] **Step 5: Commit** + +```bash +git commit -m "feat: WASM component model signing with nested module coverage (SC-20, SC-21)" +``` + +### Task 8: Add Kani proofs and fuzz target for component model + +**Files:** +- Modify: `src/lib/src/wasm_module/mod.rs` (kani section) +- Create: `fuzz/fuzz_targets/fuzz_component_model.rs` + +- [ ] **Step 1: Add Kani proof for component header detection** + +```rust +#[cfg(kani)] +mod component_proofs { + use super::*; + + /// Prove: component and module headers are mutually exclusive + /// for any 8-byte input (no polyglot attack possible). + #[kani::proof] + fn proof_component_module_header_mutual_exclusivity() { + let b: [u8; 8] = kani::any(); + let is_module = b == WASM_HEADER; + let is_component = b == WASM_COMPONENT_HEADER; + assert!(!(is_module && is_component), "Cannot be both module and component"); + } + + /// Prove: hash computation over component bytes is deterministic. + #[kani::proof] + fn proof_component_hash_deterministic() { + let b0: u8 = kani::any(); + let b1: u8 = kani::any(); + let data = [0x00, 0x61, 0x73, 0x6d, 0x0d, 0x00, 0x01, 0x00, b0, b1]; + use sha2::{Sha256, Digest}; + let h1 = Sha256::digest(&data); + let h2 = Sha256::digest(&data); + assert_eq!(h1, h2); + } +} +``` + +- [ ] **Step 2: Add fuzz target** + +- [ ] **Step 3: Run tests + mutation testing** + +Run: `cargo test -p wsc` and check mutation testing catches component signing mutations. + +- [ ] **Step 4: Commit** + +```bash +git commit -m "feat: add Kani proof and fuzz target for component model (CV-30)" +``` + +### Task 9: PR and merge Phase 2 + +- [ ] **Step 1: Run full test suite** +- [ ] **Step 2: Run `rivet validate`** +- [ ] **Step 3: Create PR, watch CI, merge** + +--- + +## Phase 3: PQC Hybrid Signing Preparation + +### Task 10: Add hybrid signing traits and domain separation + +**Files:** +- Modify: `src/lib/src/pqc.rs` + +- [ ] **Step 1: Write failing test for hybrid sign/verify** + +```rust +#[test] +fn test_hybrid_signature_requires_both_valid() { + let hybrid = HybridSignature { + classical: vec![0u8; 64], // fake Ed25519 sig + post_quantum: vec![], // empty PQC sig + pqc_algorithm: PqcAlgorithm::SlhDsaSha2_128s, + message_hash: vec![0u8; 32], + }; + // Verification must fail if PQC component is missing + assert!(!hybrid.is_complete()); +} +``` + +- [ ] **Step 2: Implement is_complete() and domain separation** + +```rust +impl HybridSignature { + pub fn is_complete(&self) -> bool { + !self.classical.is_empty() + && !self.post_quantum.is_empty() + && self.classical.len() == 64 // Ed25519 + && self.post_quantum.len() <= self.pqc_algorithm.max_signature_size() + } + + pub fn domain_separator() -> &'static [u8] { + b"wsc-hybrid-v1" + } +} +``` + +- [ ] **Step 3: Run tests, commit** + +```bash +git commit -m "feat: hybrid signature completeness check and domain separation (SC-22, SC-23)" +``` + +### Task 11: Version bump and release preparation + +- [ ] **Step 1: Bump version to 0.7.0** +- [ ] **Step 2: Run `rivet init --agents`** +- [ ] **Step 3: Run full test suite + `rivet validate`** +- [ ] **Step 4: Create release PR** +- [ ] **Step 5: Watch CI, merge, tag v0.7.0** + +--- + +## Verification Checklist + +After all phases: + +- [ ] `rivet validate` — 0 local errors +- [ ] `cargo test -p wsc` — all tests pass +- [ ] Component model sign+verify roundtrip works +- [ ] Hybrid signature completeness enforced +- [ ] Mutation testing passes (0 surviving mutants) +- [ ] All new STPA artifacts have bidirectional links +- [ ] AGENTS.md refreshed with new artifact count