feat: STPA-Sec gap closure — 112 new artifacts for v0.6.x features

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. |
 

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