From 7ce680d3a8876c8675f10fb46fac4740a4beb870 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 20:35:01 +0200 Subject: [PATCH 1/2] docs: Mythos-style bug-hunt pipeline + spar ranking MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ships the four-prompt bug-hunt pipeline modeled on Anthropic's Claude Mythos (red.anthropic.com, April 2026) adapted for spar. The architecture: let an agent reason freely about code but require a machine-checkable oracle (Kani harness + PoC test) for every reported bug so hallucinations don't ship. Contents: - HOWTO.md — pipeline overview, prerequisites, worked example - rank.md — tier-1-through-5 rubric specific to spar's pipeline (parser/syntax/hir-def/annex = tier 5; analysis/solver = tier 4; …) - discover.md — Mythos-verbatim discovery prompt + spar context + AADL-specific hypothesis priors (parser edge cases, HIR drift, proof-code drift from the 180 Kani harnesses) - validate.md — fresh-session validator enforcing both oracle halves - emit.md — converts a confirmed finding into a draft STPA artifact entry under safety/stpa/*.yaml - rank.json — ranking of 144 spar source files produced by running rank.md (tier 5: 43 files; tier 4: 51; tier 3: 35; tier 2: 14; tier 1: 1). Kept as evidence the pipeline works end-to-end. First parallel run on the top-5 tier-5 files surfaced three shipped bugs (fixed in PR #132) and two confirmed-but-no-uca findings that were filtered by validation. Co-Authored-By: Claude Opus 4.7 (1M context) --- scripts/mythos/HOWTO.md | 120 +++++++++++++++++++++++++++ scripts/mythos/discover.md | 68 ++++++++++++++++ scripts/mythos/emit.md | 33 ++++++++ scripts/mythos/rank.json | 161 +++++++++++++++++++++++++++++++++++++ scripts/mythos/rank.md | 52 ++++++++++++ scripts/mythos/validate.md | 35 ++++++++ 6 files changed, 469 insertions(+) create mode 100644 scripts/mythos/HOWTO.md create mode 100644 scripts/mythos/discover.md create mode 100644 scripts/mythos/emit.md create mode 100644 scripts/mythos/rank.json create mode 100644 scripts/mythos/rank.md create mode 100644 scripts/mythos/validate.md diff --git a/scripts/mythos/HOWTO.md b/scripts/mythos/HOWTO.md new file mode 100644 index 0000000..c306501 --- /dev/null +++ b/scripts/mythos/HOWTO.md @@ -0,0 +1,120 @@ +# Mythos-Style Bug Hunt — Portable Pipeline + +A four-prompt pipeline modeled on Anthropic's Claude Mythos (red.anthropic.com, +April 2026) plus Vidoc's open-model reproduction. The architecture is: let +the agent reason about code freely, but require a machine-checkable oracle +for every reported bug so hallucinations don't ship. + +## Prerequisites + +- Claude Code or any agent harness that can read files and drive test runs +- A truth oracle for your language/domain (see §5) +- A bug-tracking format (STPA-Sec, STPA, in-house, whatever) +- Optional: parallel sessions (rank → N parallel discoveries → validate → emit) + +## 1. Four prompt templates in `scripts/mythos/` + +- **`rank.md`** — agent ranks every source file 1–5 by bug likelihood. The + rubric is the one non-portable part — write it per repo (§2). +- **`discover.md`** — Mythos-verbatim discovery prompt plus repo-specific + context plus the oracle requirement (§3). +- **`validate.md`** — fresh-agent validator that enforces the oracle and + filters uninteresting findings. +- **`emit.md`** — converts a confirmed finding into a draft entry in your + bug-tracking format. + +## 2. Ranking rubric (non-portable) + +5 tiers, named by concrete path patterns not abstract categories. Skeleton: + +``` +5 (crown jewels): secrets, parse-before-trust, canonicalization +4 (direct security boundary): verification, signing, argv+env +3 (one hop from untrusted input): token parsers, network clients, format parsers +2 (supporting, no direct security role): HTTP plumbing, policy eval, logging +1 (config / constants / proof artifacts): error types, wiring, proofs +``` + +Straddle rule: if a file sits between two tiers, pick the higher. Run the +rank pass once, then **patch the rubric** to eliminate files that required +overrides. A good rubric produces zero overrides on re-run. + +## 3. Oracle choice (drives `discover.md`) + +The oracle separates "agent thinks there's a bug" from "there is a bug." + +| Hunting… | Oracle candidates | +|---|---| +| Memory corruption in C/C++/unsafe Rust | AddressSanitizer, MemorySanitizer, UBSan | +| Logic bugs in safe Rust | Kani + property tests (proptest/quickcheck) | +| Compiler correctness | Rocq + Z3 SMT + differential testing | +| Kernel primitives | Verus + Kani + Rocq; proof-skip analysis | +| Python/TypeScript | Hypothesis, fast-check, concrete PoC | +| Go | fuzz, property tests | +| Crypto protocols | Proverif, Tamarin, CryptoVerif counterexample | + +`discover.md` MUST require BOTH (1) a failing machine-checkable proof AND +(2) a failing concrete PoC. "If you cannot produce both, do not report. +Hallucinations are more expensive than silence." — load-bearing sentence. + +## 4. Run the pipeline + +From a Claude Code session in the repo: + +1. `Read scripts/mythos/rank.md` → JSON ranking +2. For each rank-≥4 file: new session (parallel), paste `discover.md` with + `{{file}}` substituted. Output = structured finding report. +3. For each finding: fresh session with `validate.md`. Both oracle halves + must fail on unfixed code. Reject anything that doesn't confirm. +4. For each confirmed: `emit.md` produces a `draft` tracking entry. Human + promotes to `approved`. + +One agent per file in step 2 is Mythos's parallelism trick. Don't run one +agent across the whole codebase. + +## 5. Per-project customization + +- **`rank.md`**: your threat model in 5 tiers +- **`discover.md`**: repo context paragraph + oracle requirement + optional + hypothesis priors (e.g., wasmtime 2026-04-09 CVE wave for any WASM tool) +- **`validate.md`**: reject against your known-mitigations / system + constraints / existing scenarios. Swap threat-agent checks for + hazard-only checks if the repo is safety not security. +- **`emit.md`**: match the exact YAML/JSON shape of your artifact store. + +## 6. Gotchas + +- **Failing tests directly in source break CI.** Use `#[ignore]` / `@skip` + and put the rerun command in the ignore reason. +- **The rubric is wrong the first time.** Expect to patch after pass 1. + Sign you need to patch: "straddle rule → promoted X" lines in output. +- **Validators must be fresh sessions.** Reusing discovery context lets + the agent defend its own hypothesis. +- **One agent per file, not per codebase.** Parallel agents on different + files find diverse bugs; a single agent converges on surface issues. +- **Keep the discovery prompt minimal.** Mythos's "Please find a security + vulnerability" outperforms elaborate CWE checklists because the agent + has tools (oracle, debugger, runtime) and the environment filters truth. + +## 7. Worked example — sigil `signature/sig_sections.rs` + +First tier-5 file produced a finding: + +```rust +let certificate_chain = if let Ok(cert_count) = varint::get32(&mut reader) { + // ... read chain +} else { + None // ← silently swallows ALL parse errors, not just EOF +}; +``` + +Intent: backward-compat (missing cert_count → None). Bug: any error — +including malformed bytes — gets converted to "no chain," downgrading a +cert-based signature to a bare-key signature. + +- **PoC test**: append 5 MSB-set bytes after a valid prefix; expect `Err`; + current code returns `Ok { certificate_chain: None }`. **Confirmed failing.** +- **Kani harness**: symbolic 5-byte cert_count with MSB-set constraint; + `assert!(result.is_err())`. + +Maps to STPA-Sec UCA-6. Emitted as `draft AS-N` under UCA-6. diff --git a/scripts/mythos/discover.md b/scripts/mythos/discover.md new file mode 100644 index 0000000..29add34 --- /dev/null +++ b/scripts/mythos/discover.md @@ -0,0 +1,68 @@ +Please find a correctness-relevant vulnerability in this program. + +Context you must use: +- This is spar, a toolchain for AADL v2.2/v2.3 (Architecture Analysis + and Design Language, SAE AS-5506D) with a deployment solver. The + pipeline is: AADL text → parser → syntax → HIR → analysis → + transform → solver → codegen/render. The invariant: every valid + AADL input produces a semantically faithful model, and every + emitted deployment satisfies the input's constraints. +- Focus on ONE file: {{file}}. You may read any other file to + confirm/refute, but do not report bugs outside {{file}}. +- Spar's output drives deployment decisions on embedded safety- + critical systems. A solver that emits an infeasible schedule as + feasible is a functional-safety event. + +Hypothesis priors (AADL-specific + classical compiler-frontend classes): +Use as anchors, NOT recipes. + - Parser: accepts non-AADL input; rejects a valid AADL construct + in edge cases (mixed-case keywords, unusual Unicode in + identifiers, nested comments). + - Syntax: typed-tree invariants violated (a node has fewer + children than the grammar guarantees — unwrap panics later). + - HIR: sub-component references resolved against the wrong scope; + feature-group inversion not handled correctly. + - Annex handling: unknown annex body text silently skipped or + forwarded to a no-op handler. + - Analysis: a property that is spec-required-to-be-static + computed dynamically; a latency bound that assumes a specific + scheduler policy not checked against the model. + - Solver: feasibility check uses float arithmetic where rational + is required; integer overflow on task period × priority + product; solver reports UNSAT for SAT inputs due to a wrong + encoding of deadline constraints. + - Incremental DB: stale cache returned after source change + (salsa-style bugs); query cycle that should be detected as + an error silently returns default. + - Proof-code drift: a Kani harness proves property P for a + function F, but F has since been refactored such that P no + longer matches the function's actual contract. + +To help us appropriately triage any bug you find, please write a +minimal AADL input that triggers the bug. + +Oracle requirement (non-negotiable): +For every bug you report you MUST produce both: + (1) A failing Kani harness using `#[kani::proof]` — spar has 180 + existing proofs, style is established. Harness must fail on + unfixed code. + (2) A failing property or unit test (standard `#[test]` or + `proptest!`) that reproduces the bug with a concrete AADL + input or IR fragment. For solver bugs, a natural PoC is a + differential check: solver result vs. hand-solved reference. + +If you cannot produce both, the finding does not count. +Do not report it. Hallucinations are more expensive than silence. + +Output format: +- FILE: {{file}} +- FUNCTION / LINES: ... +- HYPOTHESIS: one sentence +- KANI HARNESS: fenced Rust block +- POC TEST: fenced Rust block (AADL input or IR fragment) +- IMPACT: which hazard this enables; whether it's parser + over-acceptance/under-acceptance, HIR semantic drift, analysis + unsoundness, solver miscount, or proof-code drift +- CANDIDATE UCA: the single most likely `UCA-N` from + `safety/stpa/ucas.yaml` (consult the actual UCA set there). + Cite the AS-5506D section the bug violates. diff --git a/scripts/mythos/emit.md b/scripts/mythos/emit.md new file mode 100644 index 0000000..4a9be8b --- /dev/null +++ b/scripts/mythos/emit.md @@ -0,0 +1,33 @@ +You are emitting a new entry to spar's safety artifact store. +Consult `safety/stpa/` for the existing shape. Spar's safety +directory uses several analysis files (`analysis.yaml`, +`validation.yaml`, `security.yaml`, `solver-analysis.yaml`) — pick +the one whose category best fits the finding, or the equivalent of +loss-scenarios if it exists. + +Input: +- Confirmed bug report (below) +- Chosen `UCA-N` from the validator +--- +{{confirmed_report}} +UCA: {{uca_id}} +--- + +Rules: +1. Read `safety/stpa/` first. Match the existing field shape + exactly. Do not invent fields. +2. Grouping invariant: new entries are siblings of existing ones + under the same UCA. +3. In the prose, reference the Kani harness and the PoC test by + fully-qualified Rust path. Cite the AS-5506D section the bug + violates (e.g., "AADL v2.2 §11.2.1 feature-group mapping"). +4. If this is proof-code drift, say so explicitly — drift requires + re-verification or code reversion, not a primitive fix. +5. Optional: classify the finding under `category` with one of: + parser-over-acceptance, parser-under-acceptance, hir-drift, + analysis-unsoundness, solver-miscount, proof-drift, + codegen-divergence. Use the existing schema if present. +6. Set `status: draft`. Deployments built on spar output must not + consume draft findings until a human promotes them. + +Emit ONLY the artifact YAML block, nothing else. diff --git a/scripts/mythos/rank.json b/scripts/mythos/rank.json new file mode 100644 index 0000000..c0b8e4f --- /dev/null +++ b/scripts/mythos/rank.json @@ -0,0 +1,161 @@ +[ + {"file": "crates/spar-parser/src/grammar/components.rs", "rank": 5, "reason": "AADL component-type/impl production — core of accept-valid-reject-invalid surface"}, + {"file": "crates/spar-parser/src/grammar/connections.rs", "rank": 5, "reason": "Connection/flow arrow grammar; misparse = wrong instance connectivity"}, + {"file": "crates/spar-parser/src/grammar/features.rs", "rank": 5, "reason": "Feature-direction/kind grammar; wrong direction = downstream binding_rules false negative"}, + {"file": "crates/spar-parser/src/grammar/flows.rs", "rank": 5, "reason": "Flow-spec/e2e-flow grammar; misparse corrupts latency analysis"}, + {"file": "crates/spar-parser/src/grammar/properties.rs", "rank": 5, "reason": "Property-set + property-assoc grammar; recent #125-127 gaps prove high bug density"}, + {"file": "crates/spar-parser/src/grammar/packages.rs", "rank": 5, "reason": "Package/with-clause grammar — visibility-scope correctness"}, + {"file": "crates/spar-parser/src/grammar/modes.rs", "rank": 5, "reason": "Mode + in-modes grammar; modal-filtering is a known AS5506D gap"}, + {"file": "crates/spar-parser/src/grammar/annexes.rs", "rank": 5, "reason": "Annex subclause dispatch; EMV2/BA grammar mis-dispatch = silent drop (H-5)"}, + {"file": "crates/spar-parser/src/grammar/mod.rs", "rank": 5, "reason": "Grammar entry + shared helpers (classifier_ref, name, component_category)"}, + {"file": "crates/spar-parser/src/lexer.rs", "rank": 5, "reason": "Tokenization; line-number regression (#125-127 side) originated in offsets here"}, + {"file": "crates/spar-parser/src/syntax_kind.rs", "rank": 5, "reason": "Keyword table + component-category classification"}, + {"file": "crates/spar-parser/src/parser.rs", "rank": 5, "reason": "Core parser state machine + at_name/expect/recover semantics"}, + {"file": "crates/spar-parser/src/token_set.rs", "rank": 5, "reason": "Recovery token-set masks; off-by-one here causes silent parse advance"}, + + {"file": "crates/spar-syntax/src/ast/mod.rs", "rank": 5, "reason": "Typed AST accessors over rowan green tree; returning wrong child = lowering bug"}, + {"file": "crates/spar-syntax/src/parsing.rs", "rank": 5, "reason": "Event→tree builder; wrong byte offset feeds ParseError (recent #125-127 side-note)"}, + + {"file": "crates/spar-hir/src/lib.rs", "rank": 5, "reason": "Public semantic-model facade (2.4k lines incl. to_serializable for #129)"}, + + {"file": "crates/spar-hir-def/src/instance.rs", "rank": 5, "reason": "Instance expansion + properties_for + applies_to resolution (#128/#129)"}, + {"file": "crates/spar-hir-def/src/item_tree/lower.rs", "rank": 5, "reason": "CST → ItemTree lowering; dropped CST node = invisible to all analyses (H-5)"}, + {"file": "crates/spar-hir-def/src/item_tree/mod.rs", "rank": 5, "reason": "ItemTree types incl. PropertyAssociationItem.applies_to (#128 drop site)"}, + {"file": "crates/spar-hir-def/src/properties.rs", "rank": 5, "reason": "PropertyMap + inheritance layering (type→impl→sub override)"}, + {"file": "crates/spar-hir-def/src/property_check.rs", "rank": 5, "reason": "Property type/value validation — wrong accept = meaningless analysis"}, + {"file": "crates/spar-hir-def/src/property_eval.rs", "rank": 5, "reason": "Property expression evaluation incl. unit arithmetic"}, + {"file": "crates/spar-hir-def/src/property_value.rs", "rank": 5, "reason": "Property value typing — drives downstream analyses reading numerics"}, + {"file": "crates/spar-hir-def/src/resolver.rs", "rank": 5, "reason": "Name resolution across packages/renames — ambiguity warning path (STPA-REQ-007)"}, + {"file": "crates/spar-hir-def/src/feature_group.rs", "rank": 5, "reason": "Feature-group inverse + direction inheritance — subtle AS5506 rules"}, + {"file": "crates/spar-hir-def/src/category_rules.rs", "rank": 5, "reason": "Component-category constraints — subcomponent legality"}, + {"file": "crates/spar-hir-def/src/name.rs", "rank": 5, "reason": "PropertyRef / CiName case-insensitive identity — hash-map key invariants"}, + {"file": "crates/spar-hir-def/src/prototype.rs", "rank": 5, "reason": "Prototype binding resolution — a known spec-conformance gap area"}, + {"file": "crates/spar-hir-def/src/standard_properties.rs", "rank": 5, "reason": "Standard AADL property names/types — mismatch = silent analysis bypass"}, + {"file": "crates/spar-hir-def/src/lib.rs", "rank": 5, "reason": "HirDef salsa root + top-level queries"}, + + {"file": "crates/spar-annex/src/emv2/grammar.rs", "rank": 5, "reason": "EMV2 error-model grammar — fault-tree + safety assumption source"}, + {"file": "crates/spar-annex/src/emv2/lexer.rs", "rank": 5, "reason": "EMV2 tokenizer"}, + {"file": "crates/spar-annex/src/emv2/parser.rs", "rank": 5, "reason": "EMV2 parser + error propagation pattern parse"}, + {"file": "crates/spar-annex/src/emv2/mod.rs", "rank": 5, "reason": "EMV2 annex entry + dispatch to parser"}, + {"file": "crates/spar-annex/src/emv2/syntax_kind.rs", "rank": 5, "reason": "EMV2 keyword table"}, + {"file": "crates/spar-annex/src/ba/grammar.rs", "rank": 5, "reason": "Behavior-annex grammar — state-machine semantics"}, + {"file": "crates/spar-annex/src/ba/lexer.rs", "rank": 5, "reason": "BA tokenizer"}, + {"file": "crates/spar-annex/src/ba/parser.rs", "rank": 5, "reason": "BA parser — action/guard/transition parsing"}, + {"file": "crates/spar-annex/src/ba/mod.rs", "rank": 5, "reason": "BA annex entry + dispatch"}, + {"file": "crates/spar-annex/src/ba/syntax_kind.rs", "rank": 5, "reason": "BA keyword table"}, + {"file": "crates/spar-annex/src/registry.rs", "rank": 5, "reason": "AnnexRegistry dispatches subclause text → correct parser (H-5 if miswired)"}, + {"file": "crates/spar-annex/src/types.rs", "rank": 5, "reason": "AnnexParseResult type — downstream contract"}, + {"file": "crates/spar-annex/src/lib.rs", "rank": 5, "reason": "Annex crate root + pub dispatch API"}, + + {"file": "crates/spar-analysis/src/binding_rules.rs", "rank": 4, "reason": "Actual_Processor_Binding validation (#128 analyzer) — misses = missed hazards"}, + {"file": "crates/spar-analysis/src/binding_check.rs", "rank": 4, "reason": "Binding classifier-match — safety-co-location/redundancy (SOLVER-REQ-014)"}, + {"file": "crates/spar-analysis/src/scheduling.rs", "rank": 4, "reason": "Schedulability analysis — wrong result = unsafe deployment approved (H-1)"}, + {"file": "crates/spar-analysis/src/scheduling_verified.rs", "rank": 4, "reason": "Kani-verified scheduling paths — proof-code-drift risk class"}, + {"file": "crates/spar-analysis/src/rta.rs", "rank": 4, "reason": "Response-time analysis (SOLVER-REQ-002,003) — WCET, blocking, overhead"}, + {"file": "crates/spar-analysis/src/latency.rs", "rank": 4, "reason": "E2E latency path computation (SOLVER-REQ-013) — incomplete path = underreport"}, + {"file": "crates/spar-analysis/src/bus_bandwidth.rs", "rank": 4, "reason": "Aggregate bus bandwidth (SOLVER-REQ-009) — over-subscription detection"}, + {"file": "crates/spar-analysis/src/memory_budget.rs", "rank": 4, "reason": "Memory budget check — overflow = deployable but crashes (H-1)"}, + {"file": "crates/spar-analysis/src/resource_budget.rs", "rank": 4, "reason": "Resource accounting across components (SOLVER-REQ-006)"}, + {"file": "crates/spar-analysis/src/weight_power.rs", "rank": 4, "reason": "Weight/power budgets — recent PR #123 debt work, high change density"}, + {"file": "crates/spar-analysis/src/arinc653.rs", "rank": 4, "reason": "ARINC-653 partition rules — safety-certification relevant"}, + {"file": "crates/spar-analysis/src/modal_rules.rs", "rank": 4, "reason": "Modal rule validation — modal-filtering is known AS5506D gap"}, + {"file": "crates/spar-analysis/src/modal.rs", "rank": 4, "reason": "Modal analysis core"}, + {"file": "crates/spar-analysis/src/mode_check.rs", "rank": 4, "reason": "Mode specification validation"}, + {"file": "crates/spar-analysis/src/mode_rules.rs", "rank": 4, "reason": "Mode transition legality"}, + {"file": "crates/spar-analysis/src/mode_reachability.rs", "rank": 4, "reason": "Mode reachability + NuSMV export (STPA-REQ dead-mode detection)"}, + {"file": "crates/spar-analysis/src/connection_rules.rs", "rank": 4, "reason": "Connection endpoint validation — direction + compatibility"}, + {"file": "crates/spar-analysis/src/connectivity.rs", "rank": 4, "reason": "Cross-processor connection enumeration (SOLVER-REQ-011)"}, + {"file": "crates/spar-analysis/src/direction_rules.rs", "rank": 4, "reason": "Port direction check — LSP quickfix swap depends on this"}, + {"file": "crates/spar-analysis/src/flow_rules.rs", "rank": 4, "reason": "Flow-spec coverage and direction"}, + {"file": "crates/spar-analysis/src/flow_check.rs", "rank": 4, "reason": "Flow implementation validation"}, + {"file": "crates/spar-analysis/src/category_check.rs", "rank": 4, "reason": "Component-category containment rules"}, + {"file": "crates/spar-analysis/src/subcomponent_rules.rs", "rank": 4, "reason": "Subcomponent category legality"}, + {"file": "crates/spar-analysis/src/hierarchy.rs", "rank": 4, "reason": "Containment hierarchy depth/cycle detection"}, + {"file": "crates/spar-analysis/src/classifier_match.rs", "rank": 4, "reason": "Classifier match-and-substitution — prototype binding substrate"}, + {"file": "crates/spar-analysis/src/extends_rules.rs", "rank": 4, "reason": "Extends-chain inheritance (known AS5506D gap: extends not inherited)"}, + {"file": "crates/spar-analysis/src/legality.rs", "rank": 4, "reason": "General legality constraints"}, + {"file": "crates/spar-analysis/src/naming_rules.rs", "rank": 4, "reason": "Name convention + ambiguity warnings"}, + {"file": "crates/spar-analysis/src/completeness.rs", "rank": 4, "reason": "Completeness checks — missing type/impl/feature detection"}, + {"file": "crates/spar-analysis/src/feature_group_check.rs", "rank": 4, "reason": "Feature-group inverse matching"}, + {"file": "crates/spar-analysis/src/property_rules.rs", "rank": 4, "reason": "Property constraint validation — reads property_eval"}, + {"file": "crates/spar-analysis/src/property_accessors.rs", "rank": 4, "reason": "Validated property accessors (CC-10 controller constraint)"}, + {"file": "crates/spar-analysis/src/emv2_analysis.rs", "rank": 4, "reason": "EMV2 fault-tree computation — single-point-of-failure detection"}, + {"file": "crates/spar-analysis/src/emv2_stpa_bridge.rs", "rank": 4, "reason": "EMV2 → STPA artifact generation (#89 bridge)"}, + {"file": "crates/spar-analysis/src/ai_ml/mod.rs", "rank": 4, "reason": "AI/ML-specific analysis (STPA-for-AI patterns)"}, + {"file": "crates/spar-analysis/src/wrpc_binding.rs", "rank": 4, "reason": "wRPC binding validation for WASM deployment"}, + {"file": "crates/spar-analysis/src/lib.rs", "rank": 4, "reason": "Analysis registry + pass orchestration (STPA-REQ-014)"}, + + {"file": "crates/spar-solver/src/allocate.rs", "rank": 4, "reason": "Feasibility-aware allocation (SOLVER-REQ-005 incremental schedulability)"}, + {"file": "crates/spar-solver/src/milp.rs", "rank": 4, "reason": "MILP encoding — LS-5 'rewriter inserts on wrong subcomponent' origin"}, + {"file": "crates/spar-solver/src/nsga2.rs", "rank": 4, "reason": "NSGA-II Pareto front (REQ-SOLVER-006) — optimality certificates TBD"}, + {"file": "crates/spar-solver/src/constraints.rs", "rank": 4, "reason": "Constraint encoding — affinity/anti-affinity (SOLVER-REQ-007)"}, + {"file": "crates/spar-solver/src/topology.rs", "rank": 4, "reason": "Topology graph — cross-processor + bus routing"}, + + {"file": "crates/spar-transform/src/cargo_metadata.rs", "rank": 4, "reason": "Cargo.toml parsing + WASM metadata extraction"}, + {"file": "crates/spar-transform/src/protocol_library.rs", "rank": 4, "reason": "Protocol library — security-zone enforcement (SOLVER-REQ-010)"}, + {"file": "crates/spar-transform/src/rust_crate.rs", "rank": 4, "reason": "AADL → Rust crate lowering (REQ-CODEGEN-RUST planned)"}, + {"file": "crates/spar-transform/src/wit.rs", "rank": 4, "reason": "WIT export — component-model interface correctness"}, + {"file": "crates/spar-transform/src/wit_parser.rs", "rank": 4, "reason": "WIT parser — round-trip with wit.rs"}, + {"file": "crates/spar-transform/src/wac.rs", "rank": 4, "reason": "WAC composition format emit"}, + {"file": "crates/spar-transform/src/wac_parser.rs", "rank": 4, "reason": "WAC parser — matches wac.rs"}, + {"file": "crates/spar-transform/src/wrpc.rs", "rank": 4, "reason": "wRPC-specific transform for distributed deployment"}, + {"file": "crates/spar-transform/src/lib.rs", "rank": 4, "reason": "Transform module roots + shared types"}, + + {"file": "crates/spar-codegen/src/rust_gen.rs", "rank": 3, "reason": "Rust crate skeleton emission"}, + {"file": "crates/spar-codegen/src/wit_gen.rs", "rank": 3, "reason": "WIT interface emission"}, + {"file": "crates/spar-codegen/src/workspace_gen.rs", "rank": 3, "reason": "Workspace + Bazel BUILD emission (REQ-CODEGEN-BAZEL planned)"}, + {"file": "crates/spar-codegen/src/config_gen.rs", "rank": 3, "reason": "Build configuration generation"}, + {"file": "crates/spar-codegen/src/doc_gen.rs", "rank": 3, "reason": "Documentation generation"}, + {"file": "crates/spar-codegen/src/proof_gen.rs", "rank": 3, "reason": "Lean4/Kani proof skeleton emission (REQ-CODEGEN-VERIFY-PROOF planned)"}, + {"file": "crates/spar-codegen/src/test_gen.rs", "rank": 3, "reason": "Test skeleton emission (REQ-CODEGEN-VERIFY-TEST planned)"}, + {"file": "crates/spar-codegen/src/lib.rs", "rank": 3, "reason": "Codegen orchestration"}, + + {"file": "crates/spar-render/src/lib.rs", "rank": 3, "reason": "SVG/HTML renderer — instance → etch graph (LS-9 diagram-drops-feature risk)"}, + + {"file": "crates/spar-wasm/src/graph.rs", "rank": 3, "reason": "WASM component graph assembly"}, + {"file": "crates/spar-wasm/src/render.rs", "rank": 3, "reason": "WASM graph render path"}, + {"file": "crates/spar-wasm/src/lib.rs", "rank": 3, "reason": "WASM crate root"}, + + {"file": "crates/spar-sysml2/src/parser.rs", "rank": 3, "reason": "SysML v2 parser — part of bridge #90, not safety-critical"}, + {"file": "crates/spar-sysml2/src/lexer.rs", "rank": 3, "reason": "SysML v2 tokenizer"}, + {"file": "crates/spar-sysml2/src/grammar/parts.rs", "rank": 3, "reason": "SysML v2 part-def/usage grammar"}, + {"file": "crates/spar-sysml2/src/grammar/requirements.rs", "rank": 3, "reason": "SysML v2 requirement grammar"}, + {"file": "crates/spar-sysml2/src/grammar/packages.rs", "rank": 3, "reason": "SysML v2 package grammar"}, + {"file": "crates/spar-sysml2/src/grammar/mod.rs", "rank": 3, "reason": "SysML v2 grammar dispatch"}, + {"file": "crates/spar-sysml2/src/lower.rs", "rank": 3, "reason": "SysML v2 → AADL lowering (UCA-20: subcomponent category hardcoded)"}, + {"file": "crates/spar-sysml2/src/tree_builder.rs", "rank": 3, "reason": "SysML v2 CST builder"}, + {"file": "crates/spar-sysml2/src/extract.rs", "rank": 3, "reason": "SysML v2 → rivet artifact extraction"}, + {"file": "crates/spar-sysml2/src/generate.rs", "rank": 3, "reason": "SysML v2 generate/bidirectional edit"}, + {"file": "crates/spar-sysml2/src/syntax_kind.rs", "rank": 3, "reason": "SysML v2 keyword table"}, + {"file": "crates/spar-sysml2/src/token_set.rs", "rank": 3, "reason": "SysML v2 token recovery sets"}, + {"file": "crates/spar-sysml2/src/lib.rs", "rank": 3, "reason": "SysML v2 crate root"}, + + {"file": "crates/spar-cli/src/lsp.rs", "rank": 3, "reason": "LSP server — large (4k lines); code actions touch analysis, rewrite paths"}, + {"file": "crates/spar-cli/src/diff.rs", "rank": 3, "reason": "Three-way merge + architectural diff (REQ-DIFF-003)"}, + {"file": "crates/spar-cli/src/refactor.rs", "rank": 3, "reason": "Rewriter — SOLVER-REQ-017 fully-qualified CST targeting"}, + {"file": "crates/spar-cli/src/verify.rs", "rank": 3, "reason": "Verify command orchestration"}, + {"file": "crates/spar-cli/src/sarif.rs", "rank": 3, "reason": "SARIF diagnostic emission — schema correctness"}, + {"file": "crates/spar-cli/src/assertion/eval.rs", "rank": 3, "reason": "Assertion language evaluator — semantic correctness"}, + {"file": "crates/spar-cli/src/assertion/parser.rs", "rank": 3, "reason": "Assertion language parser"}, + {"file": "crates/spar-cli/src/assertion/lexer.rs", "rank": 3, "reason": "Assertion tokenizer"}, + {"file": "crates/spar-cli/src/assertion/mod.rs", "rank": 3, "reason": "Assertion module entry + engine wiring"}, + {"file": "crates/spar-cli/src/assertion/syntax.rs", "rank": 3, "reason": "Assertion AST types"}, + {"file": "crates/spar-cli/src/main.rs", "rank": 2, "reason": "argv dispatch + subcommand orchestration"}, + + {"file": "crates/spar-base-db/src/lib.rs", "rank": 2, "reason": "Salsa DB + offset_to_line_col utility — no analysis logic"}, + + {"file": "crates/spar-parser/src/marker.rs", "rank": 2, "reason": "Parser event marker infrastructure (plumbing)"}, + {"file": "crates/spar-parser/src/event.rs", "rank": 2, "reason": "Parser event types (plumbing)"}, + {"file": "crates/spar-parser/src/lib.rs", "rank": 2, "reason": "Crate root + doc + re-exports"}, + {"file": "crates/spar-syntax/src/lib.rs", "rank": 2, "reason": "Pure re-exports"}, + {"file": "crates/spar-syntax/src/language.rs", "rank": 2, "reason": "Rowan language binding — 27 lines"}, + {"file": "crates/spar-solver/src/lib.rs", "rank": 2, "reason": "Crate root; solver modules re-exported"}, + {"file": "crates/spar-verify/src/lib.rs", "rank": 2, "reason": "Verify facade — 23 lines"}, + {"file": "crates/spar-sysml2/src/language.rs", "rank": 2, "reason": "Rowan language binding — small"}, + {"file": "crates/spar-sysml2/src/event.rs", "rank": 2, "reason": "Parser event types"}, + {"file": "crates/spar-sysml2/src/marker.rs", "rank": 2, "reason": "Parser marker plumbing"}, + {"file": "crates/spar-sysml2/src/stdlib.rs", "rank": 2, "reason": "1-line stub"}, + {"file": "crates/spar-sysml2/src/grammar/constraints.rs", "rank": 2, "reason": "5-line stub"}, + + {"file": "crates/spar-verify-macros/src/lib.rs", "rank": 1, "reason": "Proc-macro for verification harness — proof/constants tier"} +] diff --git a/scripts/mythos/rank.md b/scripts/mythos/rank.md new file mode 100644 index 0000000..5d31432 --- /dev/null +++ b/scripts/mythos/rank.md @@ -0,0 +1,52 @@ +Rank source files in this repository by likelihood of containing a +correctness-relevant bug (AADL parsing accepts invalid models, HIR +construction drops semantic detail, solver emits infeasible +deployment, codegen produces wrong WASM), on a 1–5 scale. Output +JSON: `[{"file": "...", "rank": N, "reason": "..."}]`, sorted +descending. + +Scope: `crates/spar-*/src/**/*.rs`. Exclude tests, benches. + +Ranking rubric (spar-specific — AADL v2.2/v2.3 toolchain with +multi-phase pipeline): + +5 (frontend correctness — bugs here = wrong semantic model downstream): + - crates/spar-parser/** # AADL text → AST + - crates/spar-syntax/** # AST → typed syntax tree + - crates/spar-hir/** # semantic model (intermediate rep) + - crates/spar-hir-def/** # HIR definitions / database queries + - crates/spar-annex/** # annex sub-languages (BLESS, EMV2, etc.) + +4 (analysis + transform + solver): + - crates/spar-analysis/** # dataflow / property checks + - crates/spar-transform/** # HIR → optimized HIR + - crates/spar-solver/** # constraint solver — infeasible-deployment class + - crates/spar-verify/** # verification checks (proof-code drift class) + +3 (codegen + rendering): + - crates/spar-codegen/** # any output emission + - crates/spar-render/** # report generation + - crates/spar-wasm/** # WASM output path + - crates/spar-sysml2/** # SysML v2 bridge + +2 (base + wiring): + - crates/spar-base-db/** # salsa-style incremental DB + - crates/spar-cli/** # argv + env + +1 (proof / constants): + - crates/spar-verify-macros/** # proof macros + - **/verify/** + +When ranking: +- Spar parses a real standard (AS-5506D / AADL v2.2/v2.3). Like any + standard-parser, the attack surface is "accept every valid model, + reject every invalid one." Silent acceptance of invalid AADL is a + crown-jewel bug. +- The solver phase is the Loom/synth-equivalent: it MUST preserve + semantics (feasibility, timing constraints). A miscalculation + there produces a deployment that silently violates requirements. +- 180 Kani proofs exist in the codebase — coverage does not mean + absence. Proof-code drift is a finding class here as in loom/synth. +- If a file straddles two tiers, pick the higher. +- Files you haven't seen default to rank 2. +- Do not guess rank 5 from path alone — open the file. diff --git a/scripts/mythos/validate.md b/scripts/mythos/validate.md new file mode 100644 index 0000000..ba486fc --- /dev/null +++ b/scripts/mythos/validate.md @@ -0,0 +1,35 @@ +I have received the following bug report. Can you please confirm if +it's real and interesting? + +Report: +--- +{{report}} +--- + +You are a fresh validator. Spar outputs drive real embedded-system +deployment decisions — be strict. + +Procedure: +1. Read the cited file and function BEFORE the hypothesis. For + spec-related claims, locate the AS-5506D clause cited and read + it (or the spar comment citing it). +2. Run the provided Kani harness. If no counterexample appears on + unfixed code, reply `VERDICT: not-confirmed`. Stop. +3. Run the PoC test. If it passes on unfixed code, reply + `VERDICT: not-confirmed`. Stop. +4. If both confirm, ask: is this *interesting*? + A finding is NOT interesting if any of the following hold: + - the AADL input is flagged by the parser's static-validation + pass that the test bypasses + - the "miscalculation" is actually a legal choice given the + spec's ambiguity (AS-5506D has some) + - the solver output is marked `unknown` rather than + `feasible` / `infeasible` — that's documented-by-design + - the feature requires an annex sub-language that spar has + not yet implemented (stubs return documented sentinels) +5. If real and interesting, map to `UCA-N`. Prefer grouping. + +Output: +- `VERDICT: confirmed | not-confirmed | confirmed-but-no-uca` +- `UCA: UCA-N` (only on confirmed) +- `REASON:` one paragraph From 29b157b71145646bd376925727705d0c41008e2a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Apr 2026 21:04:48 +0200 Subject: [PATCH 2/2] chore(deps): bump thin-vec to 0.2.16 to clear RUSTSEC-2026-0103 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Same patch as fix/mythos-batch-1 — `thin-vec 0.2.14` has a UAF/Double Free in `IntoIter::drop` reachable from safe Rust (RustSec 2026-0103), 0.2.16 ships the fix. Indirect through salsa. Unblocks `Cargo Deny` + `Security Audit (RustSec)` CI checks on this branch too. Co-Authored-By: Claude Opus 4.7 (1M context) --- Cargo.lock | 4 ++-- supply-chain/config.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 5f91b24..4012961 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1229,9 +1229,9 @@ checksum = "f18aa187839b2bdb1ad2fa35ead8c4c2976b64e4363c386d45ac0f7ee85c9233" [[package]] name = "thin-vec" -version = "0.2.14" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "144f754d318415ac792f9d69fc87abbbfc043ce2ef041c60f16ad828f638717d" +checksum = "259cdf8ed4e4aca6f1e9d011e10bd53f524a2d0637d7b28450f6c64ac298c4c6" [[package]] name = "toml" diff --git a/supply-chain/config.toml b/supply-chain/config.toml index 5eb1b8f..5c936e4 100644 --- a/supply-chain/config.toml +++ b/supply-chain/config.toml @@ -465,7 +465,7 @@ version = "1.1.1" criteria = "safe-to-deploy" [[exemptions.thin-vec]] -version = "0.2.14" +version = "0.2.16" criteria = "safe-to-deploy" [[exemptions.toml]]