From 8427d2b77721c4c21185f80a4f429dcad6842d1d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:47:52 +0000 Subject: [PATCH] feat(assail): route languages through a tested table; retire the vacuous PA1 PA1 was an Idris2 model of the analyzer dispatch whose theorem could not fail: `GenericAnalyzer : HasAnalyzer lang` inhabited its witness for every language. It was also stale (50 of 52 languages) and partly false (it said cross-language checks always run; they are skipped for configuration). The routing is now real code with claims that can fail: - src/assail/routing.rs: `route(Language) -> Route`, `Route::analyzer()`, and `runs_cross_language(is_configuration)`. `analyze_inner` matches on `route(file_lang)` and calls `runs_cross_language`. Only the arm heads changed; every arm body is byte-identical. `route` and the dispatch are exhaustive with no wildcard (Chapel, the one language without a dedicated analyzer, is routed to Generic explicitly). - src/types.rs: `Language::ALL` (52 variants), kept complete by an exhaustive `ordinal` match test, following WeakPointCategory::ALL. - Tests, exhaustive over Language::ALL: (a) every language analyzer in analyzer.rs is reached; (b) no language falls back to analyze_generic while a dedicated analyzer for it exists; (c) cross-language checks run exactly off configuration, and on scripts embedded in it (Justfile + Lua scan, end to end); (d) README's language counts equal the supported count. Each was seen to fail on a planted fault. - README: 49 -> 51 languages (badge, capabilities, summary); (d) caught the drift. C and Php were added after the count was written. - PatternCompleteness.idr removed from src/abi and the ipkg; PROOF-NEEDS, EXPLAINME, PROOF-PROGRAMME and the 0-AI-MANIFEST entry updated. PA1's status is TESTED; the Creusot/Pearlite and Verus proof is OPEN. Found while testing (c), recorded as an open obligation, not fixed here: the cross-language check strips `//` comments before matching, which also cuts unquoted `http://` URLs (shell, Justfile recipes). Checked: cargo fmt; clippy -D warnings with all and default features; cargo test --all-features (789 passed, 0 failed); the Idris2 package type-checks (4 modules); panic-attack's self-scan reports nothing new. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u --- 0-AI-MANIFEST.a2ml | 2 - EXPLAINME.adoc | 2 +- PROOF-NEEDS.adoc | 58 +-- PROOF-PROGRAMME.adoc | 11 +- README.adoc | 6 +- .../PanicAttack/ABI/PatternCompleteness.idr | 259 ------------- src/abi/panic-attack-abi.ipkg | 1 - src/assail/analyzer.rs | 87 ++--- src/assail/mod.rs | 1 + src/assail/routing.rs | 350 ++++++++++++++++++ src/types.rs | 134 +++++++ 11 files changed, 570 insertions(+), 341 deletions(-) delete mode 100644 src/abi/PanicAttack/ABI/PatternCompleteness.idr create mode 100644 src/assail/routing.rs diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 116c3de..b4225e6 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -37,8 +37,6 @@ (jit-context "src/jit_context.rs" "JIT-framework classifier: Cranelift / Llvm / Wasm / Javascript / None")) (proof-modules - (pa1 "src/abi/PatternCompleteness.idr" - "Pattern detection completeness — every Lang / WPCategory has a detector") (pa2 "src/abi/ClassificationSoundness.idr" "Classification soundness — Severity total order + maxSeverity commutativity") (layer-1-0 "src/abi/Stripping.idr" diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index f2ea553..904514d 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -52,7 +52,7 @@ The README makes claims. This file backs them up. | `src/comment_marker.rs` | Inline `// panic-attack: accepted [- reason]` suppression marker — `//` / `#` / `--` / `;` / `%` leaders, string-literal aware | `src/ffi_kind.rs` | UnsafeFFI (PA013) subtyping: BuildSystem (`build.zig` / `build.rs` — audit-accepted), RuntimeAbi (`bindings/` / `ffi/` / `sys/` / `cdef.zig`), TestMock (`tests/mocks/` / `_stub`), Unknown | `src/jit_context.rs` | JIT-framework classifier: Cranelift / Llvm / Wasm / Javascript / None; `transmute_targets_fn_ptr` recogniser for fn-ptr type-punning -| `src/abi/PanicAttack/ABI/PatternCompleteness.idr` | PA1 Idris2 model of analyzer dispatch; vacuous as stated (see `PROOF-NEEDS.adoc`) +| `src/assail/routing.rs` | PA1 routing table: which analyzer each language reaches and when cross-language checks run; its claims are tested exhaustively (see `PROOF-NEEDS.adoc`) | `src/abi/PanicAttack/ABI/ClassificationSoundness.idr` | PA2 Idris2 proof — severity total order, `sevMax` upper bounds, monotone encoding | `src/abi/PanicAttack/ABI/Stripping.idr` | Layer 1.0 — Idris2 model of line-comment stripping, proved idempotent (`stripLineCommentsIdempotent`) | `src/kanren/` | Logic engine (unification, fact database, taint, cross-lang) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 25b024e..4d74d28 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -92,21 +92,29 @@ or signature scheme. So these are theorems of a symbolic (Dolev-Yao style) model, not a computational security reduction. Model to `src/attestation/`: `ASSUMED`. A computational proof is not claimed. -|Every language reaches an analyzer; every weak-point category has a -detector; cross-language checks run on every file (PA1) -|`src/abi/PanicAttack/ABI/PatternCompleteness.idr` -|`PROVEN` (model); supports no claim about the Rust code -|The theorem is vacuous: `GenericAnalyzer : HasAnalyzer lang` inhabits -the witness type for every language, so it holds whatever the dispatch -does. The guarantee it was meant to give already holds in Rust: -`match file_lang` in `src/assail/analyzer.rs` ends in -`_ => analyze_generic`, and `rustc` checks the match is exhaustive. - -The model has also drifted. Its `Lang` has 50 constructors and -`src/types.rs` has 52; `C` and `Php` are missing. `crossLangAlwaysApplied` -says cross-language checks run on every file, but the Rust code skips them -when `configuration.is_some()`. That model claim is false of the -implementation. +|Analyzer routing (PA1). (a) Every language analyzer in `analyzer.rs` is +reached by some language. (b) No language falls back to the generic +analyzer while a dedicated one exists for it. (c) Cross-language checks run +exactly on non-configuration content, and on scripts embedded in +configuration. (d) The README's language counts equal the languages the +table supports. +|`src/assail/routing.rs`: `route`, `Route::analyzer`, `runs_cross_language` +and their tests +|`TESTED` +|The dispatch in `analyze_inner` matches on `route(file_lang)`, so the +table is the code that runs, not a model of it. `route` and the dispatch +are exhaustive matches with no wildcard, so `rustc` makes every language +and every route explicit. The tests run over all 52 `Language` variants +(`Language::ALL`, kept complete by an exhaustive `ordinal` match). (a) and +(b) compare the table with the analyzer methods found in the source. (c) +scans a Justfile and a Lua file end to end. Each test was seen to fail on +a planted fault: an unrouted analyzer, Java sent to the generic analyzer, +cross-language checks forced on, and the README's stale count of 49. + +This replaces the Idris2 `PatternCompleteness.idr`, which was vacuous +(`GenericAnalyzer` inhabited its witness for every language), stale (50 of +52 languages) and partly false (it said cross-language checks always +run). It is retired. |Declarations for the ABI-facing types and their C integer encodings |`src/abi/PanicAttack/ABI/Types.idr` @@ -152,10 +160,18 @@ gap. fixed point) is theory and belongs in Agda with Rocq and Lean rechecks. Its realisation in `src/kanren/` is a Rust obligation. -|Replace or retire PA1 -|Creusot/Pearlite and Verus, or retire -|A non-vacuous statement would be, for example, that each language with -a dedicated analyzer is routed to it. If that is not wanted, retire the -module, because `rustc`'s exhaustiveness check already gives the current -guarantee. +|Prove PA1 (a) to (c) on `route` and `runs_cross_language` +|Creusot/Pearlite and Verus +|Pearlite contracts on the two functions, proved by both verifiers. The +tests above are exhaustive over a finite enum, but they are tests, and (a) +reads the source with a pattern match. (d) is a documentation check and +stays a test. + +|Unquoted `http://` URLs are missed by the cross-language check +|Fix first, then test +|`analyze_cross_language` strips C-style `//` comments from every file +before matching, which also cuts `curl http://host` in shell. A quoted +URL is found; an unquoted one in a `.sh` file or a Justfile recipe is not. +This is a recall gap in the InsecureProtocol detector, found while testing +PA1 (c). |=== diff --git a/PROOF-PROGRAMME.adoc b/PROOF-PROGRAMME.adoc index 9bcb2ce..e1dbe67 100644 --- a/PROOF-PROGRAMME.adoc +++ b/PROOF-PROGRAMME.adoc @@ -14,10 +14,11 @@ ____ [width="100%",cols="34%,33%,33%",options="header",] |=== |ID |File |Mechanises -|*PA1* |`+src/abi/PanicAttack/ABI/PatternCompleteness.idr+` |Every `+Lang+` constructor -has at least one analyzer; every `+WPCategory+` has at least one -detector; cross-language checks apply uniformly. Top theorem: -`+completeScanForAll+`. +|*PA1* |`+src/assail/routing.rs+` |The routing table the dispatch uses: every +language analyzer is reached, no language falls back to the generic +analyzer while a dedicated one exists, cross-language checks run exactly +off configuration, and the README language counts match. Tested +exhaustively; the earlier Idris2 model was vacuous and is retired. |*PA2* |`+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` |`+Severity+` is totally ordered (`+LTE+`); `+maxSeverity+` is commutative + idempotent; numeric @@ -316,7 +317,7 @@ docs/proof artefacts that don’t touch the hot path. * `+PROOF-NEEDS.md+` — current proof-debt ledger (this document is the long-term plan; that one tracks the immediate next step). -* `+src/abi/PanicAttack/ABI/PatternCompleteness.idr+` (PA1) +* `+src/assail/routing.rs+` (PA1) * `+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` (PA2) * `+hyperpolymath/proven+` — leaf validator library; cross-fit candidates listed above. diff --git a/README.adoc b/README.adoc index 2bcedff..eaa139c 100644 --- a/README.adoc +++ b/README.adoc @@ -12,7 +12,7 @@ image:https://api.thegreenwebfoundation.org/greencheckimage/github.com[Green Web image:https://img.shields.io/badge/status-active-green[Status] image:https://img.shields.io/badge/domain-security--analysis-blue[Domain] image:https://img.shields.io/badge/tests-897%20passing-brightgreen[Tests] -image:https://img.shields.io/badge/languages-49-blue[Languages] +image:https://img.shields.io/badge/languages-51-blue[Languages] **panic-attack** is a multi-language security analysis and stress-testing system. @@ -69,7 +69,7 @@ panic-attack exists to address this by combining: panic-attack provides: -* **49-language static analysis** across multiple families +* **51-language static analysis** across multiple families * **Weak point detection** (30 canonical categories; see the PA rule-ID table below) * **Attack simulation (6 axes)**: CPU, memory, disk, network, concurrency, time * **miniKanren logic engine** for taint analysis and cross-language reasoning @@ -235,7 +235,7 @@ Current state: **v2.5.0** * v2.5.5 cohort landed 2026-06-02: context-aware FP suppression via `test_context` / `comment_marker` / `ffi_kind` / `jit_context` modules — `// panic-attack: accepted` inline markers, automatic PanicPath suppression in test-only code, build.zig/build.rs auto-accept, Cranelift/LLVM/Wasm/JS JIT detection. See `PROOF-PROGRAMME.md` for the formal soundness landscape * 0 warnings * 38 CLI subcommands -* 49 supported languages (30 canonical weak-point categories PA001–PA029; `PA001b` is a distinct stable rule ID grouped with PA001 under one allocation semantic class for cross-tool de-duplication) +* 51 supported languages (30 canonical weak-point categories PA001–PA029; `PA001b` is a distinct stable rule ID grouped with PA001 under one allocation semantic class for cross-tool de-duplication) See link:ROADMAP.adoc[ROADMAP.adoc] for full capability breakdown and milestones. diff --git a/src/abi/PanicAttack/ABI/PatternCompleteness.idr b/src/abi/PanicAttack/ABI/PatternCompleteness.idr deleted file mode 100644 index 5295575..0000000 --- a/src/abi/PanicAttack/ABI/PatternCompleteness.idr +++ /dev/null @@ -1,259 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -||| Pattern Matching Completeness Proofs -||| -||| Proves that every language in the scanner's catalogue has an -||| associated analyzer, and every weak point category in the catalogue -||| has at least one detection rule. This eliminates false negatives -||| caused by missing dispatch arms. -||| -||| Design: We model the Language and WeakPointCategory enumerations -||| as inductive types and prove that the dispatch function (modelled -||| as `analyzerFor` / `detectorsFor`) covers every constructor. -||| The proof is structural induction on the enumeration -- Idris2's -||| totality checker verifies that every case is handled. -module PanicAttack.ABI.PatternCompleteness - -%default total - --- ═══════════════════════════════════════════════════════════════════════ --- Language enumeration (mirrors src/types.rs Language enum, 49 variants) --- ═══════════════════════════════════════════════════════════════════════ - -||| All 49 programming languages supported by the scanner. -||| This MUST stay in sync with src/types.rs Language enum. -||| Note: Cpp is the C/C++ unified analyzer (analyze_c_cpp dispatches -||| on .c / .cpp / .h / .hpp / .cc / .hh — there is no separate C -||| constructor in the Rust enum). -public export -data Lang - = Rust | Cpp | Go | Java | Python | JavaScript | Ruby - -- BEAM family - | Elixir | Erlang | Gleam - -- ML family - | ReScript | OCaml | StandardML - -- Lisp family - | Scheme | Racket - -- Functional - | Haskell | PureScript - -- Proof assistants - | Idris | Lean | Agda | Isabelle | Coq - -- Logic programming - | Prolog | Logtalk | Datalog - -- Systems languages - | Zig | Ada | Odin | Nim | Pony | DLang - -- Config languages - | Nickel | Nix - -- Scripting / data - | Shell | Julia | Lua - -- HPC / parallel - | Chapel - -- Nextgen custom DSLs - | WokeLang | Eclexia | MyLang | JuliaTheViper | Oblibeny - | Anvomidav | AffineScript | Ephapax | BetLang | ErrorLang - | VCL | FBQL - -- Catch-all - | Unknown - --- ═══════════════════════════════════════════════════════════════════════ --- Analyzer dispatch witness --- ═══════════════════════════════════════════════════════════════════════ - -||| Witness that an analyzer function exists for a given language. -||| Each constructor corresponds to a dispatch arm in analyzer.rs. -public export -data HasAnalyzer : Lang -> Type where - ||| Language-specific analyzer (e.g., analyze_rust, analyze_c_cpp) - SpecificAnalyzer : HasAnalyzer lang - ||| Generic fallback analyzer (analyze_generic) - GenericAnalyzer : HasAnalyzer lang - -||| Every language in the enumeration has an analyzer. -||| This function is total: Idris2 verifies exhaustive coverage. -||| The dispatch mirrors src/assail/analyzer.rs analyze_inner(). -public export -analyzerFor : (lang : Lang) -> HasAnalyzer lang -analyzerFor Rust = SpecificAnalyzer -analyzerFor Cpp = SpecificAnalyzer -analyzerFor Go = SpecificAnalyzer -analyzerFor Java = SpecificAnalyzer -analyzerFor Python = SpecificAnalyzer -analyzerFor JavaScript = SpecificAnalyzer -analyzerFor Ruby = SpecificAnalyzer -analyzerFor Elixir = SpecificAnalyzer -analyzerFor Erlang = SpecificAnalyzer -analyzerFor Gleam = SpecificAnalyzer -analyzerFor ReScript = SpecificAnalyzer -analyzerFor OCaml = SpecificAnalyzer -analyzerFor StandardML = SpecificAnalyzer -analyzerFor Scheme = SpecificAnalyzer -analyzerFor Racket = SpecificAnalyzer -analyzerFor Haskell = SpecificAnalyzer -analyzerFor PureScript = SpecificAnalyzer -analyzerFor Idris = SpecificAnalyzer -analyzerFor Lean = SpecificAnalyzer -analyzerFor Agda = SpecificAnalyzer -analyzerFor Isabelle = SpecificAnalyzer -analyzerFor Coq = SpecificAnalyzer -analyzerFor Prolog = SpecificAnalyzer -analyzerFor Logtalk = SpecificAnalyzer -analyzerFor Datalog = SpecificAnalyzer -analyzerFor Zig = SpecificAnalyzer -analyzerFor Ada = SpecificAnalyzer -analyzerFor Odin = SpecificAnalyzer -analyzerFor Nim = SpecificAnalyzer -analyzerFor Pony = SpecificAnalyzer -analyzerFor DLang = SpecificAnalyzer -analyzerFor Nickel = SpecificAnalyzer -analyzerFor Nix = SpecificAnalyzer -analyzerFor Shell = SpecificAnalyzer -analyzerFor Julia = SpecificAnalyzer -analyzerFor Lua = SpecificAnalyzer -analyzerFor Chapel = SpecificAnalyzer -analyzerFor WokeLang = SpecificAnalyzer -analyzerFor Eclexia = SpecificAnalyzer -analyzerFor MyLang = SpecificAnalyzer -analyzerFor JuliaTheViper = SpecificAnalyzer -analyzerFor Oblibeny = SpecificAnalyzer -analyzerFor Anvomidav = SpecificAnalyzer -analyzerFor AffineScript = SpecificAnalyzer -analyzerFor Ephapax = SpecificAnalyzer -analyzerFor BetLang = SpecificAnalyzer -analyzerFor ErrorLang = SpecificAnalyzer -analyzerFor VCL = SpecificAnalyzer -analyzerFor FBQL = SpecificAnalyzer -analyzerFor Unknown = GenericAnalyzer - -||| Proof: for ALL languages, an analyzer exists. -||| This is the top-level completeness theorem. -public export -allLanguagesHaveAnalyzers : (lang : Lang) -> HasAnalyzer lang -allLanguagesHaveAnalyzers = analyzerFor - --- ═══════════════════════════════════════════════════════════════════════ --- Cross-language security check proof --- ═══════════════════════════════════════════════════════════════════════ - -||| Witness that cross-language checks are always applied. -||| In analyzer.rs, analyze_cross_language() runs on ALL files -||| regardless of language. This type encodes that invariant. -public export -data CrossLangChecked : Lang -> Type where - MkCrossLangChecked : CrossLangChecked lang - -||| Every language receives cross-language security checks. -||| This is trivially total because the check is unconditional. -public export -crossLangAlwaysApplied : (lang : Lang) -> CrossLangChecked lang -crossLangAlwaysApplied _ = MkCrossLangChecked - --- ═══════════════════════════════════════════════════════════════════════ --- WeakPointCategory enumeration (mirrors src/types.rs, 25 categories) --- ═══════════════════════════════════════════════════════════════════════ - -||| All 25 weak point categories detectable by the scanner. -public export -data WPCategory - = UncheckedAllocation - | UnboundedLoop - | BlockingIO - | UnsafeCode - | PanicPath - | RaceCondition - | DeadlockPotential - | ResourceLeak - | CommandInjection - | UnsafeDeserialization - | DynamicCodeExecution - | UnsafeFFI - | AtomExhaustion - | InsecureProtocol - | ExcessivePermissions - | PathTraversal - | HardcodedSecret - | UncheckedError - | InfiniteRecursion - | UnsafeTypeCoercion - -- PA021 ProofDrift: banned proof escape hatches or mirror files - -- substituting assertions for proofs. Detected in .idr/.lean/.agda/.thy/.v - -- and Julia mirror files. - | ProofDrift - -- PA022 CryptoMisuse: weak hash (MD5/SHA-1) in security context, - -- constant-time comparison violations, key/nonce reuse. - -- Detected in Rust, Python, JavaScript, Go, Elixir. - | CryptoMisuse - -- PA023 SupplyChain: unpinned deps, absent lock files, unverified - -- manifests. Cargo git deps without rev=, absent Cargo.lock, Julia - -- Manifest.toml without hash, flake.nix without narHash, deno.json - -- unpinned specifiers. Detected in Rust, Julia, Nix, JavaScript. - | SupplyChain - -- PA024 InputBoundary: unchecked CBOR/MessagePack deserialization - -- (serde_cbor, ciborium, rmp_serde in Rust), JSON.parse without - -- try/catch (JavaScript), JSON3.read without error handling (Julia). - | InputBoundary - -- PA025 MutationGap: test suites with no mutation-test tooling - -- (no cargo-mutants in Rust), no property-based testing in Elixir - -- (ExUnitProperties/StreamData absent), or Julia @testset blocks - -- with only type-check assertions and no value diversity. - | MutationGap - -||| Witness that a detection rule exists for a weak point category. -||| Each variant names the language(s) whose analyzer detects it. -public export -data HasDetector : WPCategory -> Type where - ||| Detected by one or more language-specific analyzers - DetectedBy : (langs : List Lang) -> HasDetector cat - -||| Every weak point category has at least one detector. -||| Total: Idris2 verifies all 25 constructors are covered. -||| The list of detecting languages mirrors the actual pattern -||| matching code in analyzer.rs. -public export -detectorsFor : (cat : WPCategory) -> HasDetector cat -detectorsFor UncheckedAllocation = DetectedBy [Cpp] -detectorsFor UnboundedLoop = DetectedBy [Rust, Cpp, Go, Python, JavaScript] -detectorsFor BlockingIO = DetectedBy [Rust, Go, Python, JavaScript] -detectorsFor UnsafeCode = DetectedBy [Rust, Cpp, Zig, Nim, DLang] -detectorsFor PanicPath = DetectedBy [Rust, Go, Haskell] -detectorsFor RaceCondition = DetectedBy [Rust, Cpp, Go] -detectorsFor DeadlockPotential = DetectedBy [Rust, Cpp, Go] -detectorsFor ResourceLeak = DetectedBy [Rust, Cpp] -detectorsFor CommandInjection = DetectedBy [Python, Ruby, JavaScript, Shell, Elixir, Erlang] -detectorsFor UnsafeDeserialization = DetectedBy [Python, Ruby, JavaScript, Java] -detectorsFor DynamicCodeExecution = DetectedBy [Python, JavaScript, Ruby, Elixir, Shell] -detectorsFor UnsafeFFI = DetectedBy [Elixir, Erlang, Haskell, Pony, OCaml, Zig] -detectorsFor AtomExhaustion = DetectedBy [Elixir, Erlang] -detectorsFor InsecureProtocol = DetectedBy [Rust, Cpp, Go, Python, JavaScript, Ruby] -detectorsFor ExcessivePermissions = DetectedBy [Shell] -detectorsFor PathTraversal = DetectedBy [Python, JavaScript, Ruby, Go, Java] -detectorsFor HardcodedSecret = DetectedBy [Rust, Cpp, Go, Python, JavaScript, Ruby] -detectorsFor UncheckedError = DetectedBy [Go, Rust, Cpp] -detectorsFor InfiniteRecursion = DetectedBy [Haskell, PureScript, Scheme, Racket] -detectorsFor UnsafeTypeCoercion = DetectedBy [OCaml, Haskell, DLang, Nim] -detectorsFor ProofDrift = DetectedBy [Idris, Lean, Agda, Isabelle, Coq, Julia] -detectorsFor CryptoMisuse = DetectedBy [Rust, Python, JavaScript, Go, Elixir] -detectorsFor SupplyChain = DetectedBy [Rust, Julia, Nix, JavaScript] -detectorsFor InputBoundary = DetectedBy [Rust, JavaScript, Julia] -detectorsFor MutationGap = DetectedBy [Rust, Julia, Elixir] - -||| Proof: every weak point category has at least one detector. -public export -allCategoriesDetected : (cat : WPCategory) -> HasDetector cat -allCategoriesDetected = detectorsFor - --- ═══════════════════════════════════════════════════════════════════════ --- Combined completeness theorem --- ═══════════════════════════════════════════════════════════════════════ - -||| A complete scan covers both language-specific analysis AND -||| cross-language security checks for any given language. -public export -data CompleteScan : Lang -> Type where - MkCompleteScan : HasAnalyzer lang -> CrossLangChecked lang -> CompleteScan lang - -||| Every language receives a complete scan. -public export -completeScanForAll : (lang : Lang) -> CompleteScan lang -completeScanForAll lang = MkCompleteScan (analyzerFor lang) (crossLangAlwaysApplied lang) diff --git a/src/abi/panic-attack-abi.ipkg b/src/abi/panic-attack-abi.ipkg index 4d874b8..1b3ab73 100644 --- a/src/abi/panic-attack-abi.ipkg +++ b/src/abi/panic-attack-abi.ipkg @@ -9,7 +9,6 @@ package panic-attack-abi sourcedir = "." modules = PanicAttack.ABI.Types - , PanicAttack.ABI.PatternCompleteness , PanicAttack.ABI.ClassificationSoundness , PanicAttack.ABI.Stripping , PanicAttack.ABI.AttestationUnforgeability diff --git a/src/assail/analyzer.rs b/src/assail/analyzer.rs index fb0af3a..2dd1341 100644 --- a/src/assail/analyzer.rs +++ b/src/assail/analyzer.rs @@ -523,8 +523,8 @@ impl Analyzer { acc.record_file(&rel_path, &raw_bytes, &format!("{:?}", file_lang)); } - match file_lang { - Language::Unknown => { + match super::routing::route(file_lang) { + super::routing::Route::InputAdapter => { let Some(format) = configuration else { coverage.mark( file, @@ -589,7 +589,7 @@ impl Analyzer { } } } - Language::Php => match super::php::analyze(&content, &rel_path) { + super::routing::Route::Php => match super::php::analyze(&content, &rel_path) { Ok(findings) => file_weak_points.extend(findings), Err(error) => { coverage.mark( @@ -601,10 +601,10 @@ impl Analyzer { continue; } }, - Language::Rust => { + super::routing::Route::Rust => { self.analyze_rust(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::C | Language::Cpp => { + super::routing::Route::CCpp => { self.analyze_c_cpp( &content, &mut file_stats, @@ -612,10 +612,10 @@ impl Analyzer { &rel_path, )?; } - Language::Go => { + super::routing::Route::Go => { self.analyze_go(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::Python => { + super::routing::Route::Python => { self.analyze_python( &content, &mut file_stats, @@ -623,7 +623,7 @@ impl Analyzer { &rel_path, )?; } - Language::JavaScript => { + super::routing::Route::JavaScript => { self.analyze_javascript( &content, &mut file_stats, @@ -631,11 +631,11 @@ impl Analyzer { &rel_path, )?; } - Language::Ruby => { + super::routing::Route::Ruby => { self.analyze_ruby(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } // BEAM family - Language::Elixir => { + super::routing::Route::Elixir => { self.analyze_elixir( &content, &mut file_stats, @@ -643,7 +643,7 @@ impl Analyzer { &rel_path, )?; } - Language::Erlang => { + super::routing::Route::Erlang => { self.analyze_erlang( &content, &mut file_stats, @@ -651,7 +651,7 @@ impl Analyzer { &rel_path, )?; } - Language::Gleam => { + super::routing::Route::Gleam => { self.analyze_gleam( &content, &mut file_stats, @@ -660,7 +660,7 @@ impl Analyzer { )?; } // ML family - Language::ReScript => { + super::routing::Route::ReScript => { record_migration_file(file_stats.total_lines); self.analyze_rescript( &content, @@ -669,7 +669,7 @@ impl Analyzer { &rel_path, )?; } - Language::OCaml => { + super::routing::Route::OCaml => { self.analyze_ocaml( &content, &mut file_stats, @@ -677,15 +677,15 @@ impl Analyzer { &rel_path, )?; } - Language::StandardML => { + super::routing::Route::StandardML => { self.analyze_sml(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } // Lisp family - Language::Scheme | Language::Racket => { + super::routing::Route::Lisp => { self.analyze_lisp(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } // Functional - Language::Haskell => { + super::routing::Route::Haskell => { self.analyze_haskell( &content, &mut file_stats, @@ -693,7 +693,7 @@ impl Analyzer { &rel_path, )?; } - Language::PureScript => { + super::routing::Route::PureScript => { self.analyze_purescript( &content, &mut file_stats, @@ -702,7 +702,7 @@ impl Analyzer { )?; } // Proof assistants - Language::Idris => { + super::routing::Route::Idris => { self.analyze_idris( &content, &mut file_stats, @@ -710,13 +710,13 @@ impl Analyzer { &rel_path, )?; } - Language::Lean => { + super::routing::Route::Lean => { self.analyze_lean(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::Agda => { + super::routing::Route::Agda => { self.analyze_agda(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::Isabelle => { + super::routing::Route::Isabelle => { self.analyze_isabelle( &content, &mut file_stats, @@ -724,11 +724,11 @@ impl Analyzer { &rel_path, )?; } - Language::Coq => { + super::routing::Route::Coq => { self.analyze_coq(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } // Logic programming - Language::Prolog | Language::Logtalk | Language::Datalog => { + super::routing::Route::Logic => { self.analyze_logic( &content, &mut file_stats, @@ -737,22 +737,22 @@ impl Analyzer { )?; } // Systems languages - Language::Zig => { + super::routing::Route::Zig => { self.analyze_zig(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::Ada => { + super::routing::Route::Ada => { self.analyze_ada(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::Odin => { + super::routing::Route::Odin => { self.analyze_odin(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::Nim => { + super::routing::Route::Nim => { self.analyze_nim(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::Pony => { + super::routing::Route::Pony => { self.analyze_pony(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - Language::DLang => { + super::routing::Route::DLang => { self.analyze_dlang( &content, &mut file_stats, @@ -761,7 +761,7 @@ impl Analyzer { )?; } // Config languages - Language::Nickel | Language::Nix => { + super::routing::Route::Config => { self.analyze_config( &content, &mut file_stats, @@ -770,7 +770,7 @@ impl Analyzer { )?; } // Scripting - Language::Shell => { + super::routing::Route::Shell => { self.analyze_shell( &content, &mut file_stats, @@ -778,7 +778,7 @@ impl Analyzer { &rel_path, )?; } - Language::Julia => { + super::routing::Route::Julia => { self.analyze_julia( &content, &mut file_stats, @@ -786,22 +786,11 @@ impl Analyzer { &rel_path, )?; } - Language::Lua => { + super::routing::Route::Lua => { self.analyze_lua(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } // Nextgen DSLs - shared analyzer - Language::WokeLang - | Language::Eclexia - | Language::MyLang - | Language::JuliaTheViper - | Language::Oblibeny - | Language::Anvomidav - | Language::AffineScript - | Language::Ephapax - | Language::BetLang - | Language::ErrorLang - | Language::VCL - | Language::FBQL => { + super::routing::Route::NextgenDsl => { self.analyze_nextgen_dsl( &content, &mut file_stats, @@ -809,10 +798,10 @@ impl Analyzer { &rel_path, )?; } - Language::Java => { + super::routing::Route::Java => { self.analyze_java(&content, &mut file_stats, &mut file_weak_points, &rel_path)?; } - _ => { + super::routing::Route::Generic => { self.analyze_generic(&content, &mut file_stats, &rel_path)?; } } @@ -820,7 +809,7 @@ impl Analyzer { // Structured configuration uses parsed keys and values; treating // comments or schema identifiers as executable source creates false // findings. Source-language adapters retain their existing checks. - if configuration.is_none() { + if super::routing::runs_cross_language(configuration.is_some()) { self.analyze_cross_language(&content, &mut file_weak_points, &rel_path)?; } diff --git a/src/assail/mod.rs b/src/assail/mod.rs index 3a62846..3d21ebb 100644 --- a/src/assail/mod.rs +++ b/src/assail/mod.rs @@ -14,6 +14,7 @@ mod forth; mod input_adapters; pub mod patterns; pub mod php; +mod routing; mod templates; use crate::kanren::core::{FactDB, LogicEngine}; diff --git a/src/assail/routing.rs b/src/assail/routing.rs new file mode 100644 index 0000000..aa19d80 --- /dev/null +++ b/src/assail/routing.rs @@ -0,0 +1,350 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! Which analyzer each language is sent to, and when cross-language checks +//! run (PA1). +//! +//! `analyze_inner` dispatches on [`route`] instead of matching on the +//! language directly, so the table here is the dispatch, not a copy of it. +//! Both `match`es below are exhaustive with no wildcard: a new `Language` +//! fails to compile until it is given a route, and a new `Route` fails to +//! compile until it is given an analyzer. +//! +//! The claims about the table are tested exhaustively in this module's +//! tests (`TESTED` in `PROOF-NEEDS.adoc`; the Creusot/Pearlite and Verus +//! proofs remain open). + +use crate::types::Language; + +/// The analyzer a file of a given language is handed to. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub(crate) enum Route { + /// No source language: a registered configuration or build-input + /// adapter handles the file, if one matches. + InputAdapter, + Php, + Rust, + CCpp, + Go, + Python, + JavaScript, + Ruby, + Elixir, + Erlang, + Gleam, + ReScript, + OCaml, + StandardML, + Lisp, + Haskell, + PureScript, + Idris, + Lean, + Agda, + Isabelle, + Coq, + Logic, + Zig, + Ada, + Odin, + Nim, + Pony, + DLang, + Config, + Shell, + Julia, + Lua, + NextgenDsl, + Java, + /// The language-neutral fallback, for languages with no dedicated + /// analyzer. + Generic, +} + +/// The analyzer for `lang`. +pub(crate) fn route(lang: Language) -> Route { + use Language as L; + match lang { + L::Unknown => Route::InputAdapter, + L::Php => Route::Php, + L::Rust => Route::Rust, + L::C | L::Cpp => Route::CCpp, + L::Go => Route::Go, + L::Python => Route::Python, + L::JavaScript => Route::JavaScript, + L::Ruby => Route::Ruby, + L::Elixir => Route::Elixir, + L::Erlang => Route::Erlang, + L::Gleam => Route::Gleam, + L::ReScript => Route::ReScript, + L::OCaml => Route::OCaml, + L::StandardML => Route::StandardML, + L::Scheme | L::Racket => Route::Lisp, + L::Haskell => Route::Haskell, + L::PureScript => Route::PureScript, + L::Idris => Route::Idris, + L::Lean => Route::Lean, + L::Agda => Route::Agda, + L::Isabelle => Route::Isabelle, + L::Coq => Route::Coq, + L::Prolog | L::Logtalk | L::Datalog => Route::Logic, + L::Zig => Route::Zig, + L::Ada => Route::Ada, + L::Odin => Route::Odin, + L::Nim => Route::Nim, + L::Pony => Route::Pony, + L::DLang => Route::DLang, + L::Nickel | L::Nix => Route::Config, + L::Shell => Route::Shell, + L::Julia => Route::Julia, + L::Lua => Route::Lua, + L::WokeLang + | L::Eclexia + | L::MyLang + | L::JuliaTheViper + | L::Oblibeny + | L::Anvomidav + | L::AffineScript + | L::Ephapax + | L::BetLang + | L::ErrorLang + | L::VCL + | L::FBQL => Route::NextgenDsl, + L::Java => Route::Java, + L::Chapel => Route::Generic, + } +} + +impl Route { + /// The function that `analyze_inner` calls for this route. + #[cfg_attr(not(test), allow(dead_code))] + pub(crate) fn analyzer(self) -> &'static str { + match self { + Route::InputAdapter => "input_adapters::Adapter::analyze", + Route::Php => "php::analyze", + Route::Rust => "analyze_rust", + Route::CCpp => "analyze_c_cpp", + Route::Go => "analyze_go", + Route::Python => "analyze_python", + Route::JavaScript => "analyze_javascript", + Route::Ruby => "analyze_ruby", + Route::Elixir => "analyze_elixir", + Route::Erlang => "analyze_erlang", + Route::Gleam => "analyze_gleam", + Route::ReScript => "analyze_rescript", + Route::OCaml => "analyze_ocaml", + Route::StandardML => "analyze_sml", + Route::Lisp => "analyze_lisp", + Route::Haskell => "analyze_haskell", + Route::PureScript => "analyze_purescript", + Route::Idris => "analyze_idris", + Route::Lean => "analyze_lean", + Route::Agda => "analyze_agda", + Route::Isabelle => "analyze_isabelle", + Route::Coq => "analyze_coq", + Route::Logic => "analyze_logic", + Route::Zig => "analyze_zig", + Route::Ada => "analyze_ada", + Route::Odin => "analyze_odin", + Route::Nim => "analyze_nim", + Route::Pony => "analyze_pony", + Route::DLang => "analyze_dlang", + Route::Config => "analyze_config", + Route::Shell => "analyze_shell", + Route::Julia => "analyze_julia", + Route::Lua => "analyze_lua", + Route::NextgenDsl => "analyze_nextgen_dsl", + Route::Java => "analyze_java", + Route::Generic => "analyze_generic", + } + } +} + +/// Whether the cross-language checks run over a file's own content. +/// +/// They run on every source file and on no structured configuration file: +/// configuration is analysed as parsed keys and values, and treating its +/// comments or schema identifiers as executable source creates false +/// findings. Scripts embedded in configuration are still checked, each on +/// its own, by the input-adapter route. +pub(crate) fn runs_cross_language(is_configuration: bool) -> bool { + !is_configuration +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::assail::analyzer::Analyzer; + use crate::types::WeakPointCategory; + use std::collections::BTreeSet; + use std::fs; + use tempfile::TempDir; + + /// Language-analyzer methods defined in analyzer.rs: every + /// `fn analyze_(&self, content: &str, ...)`. Read from the source, + /// so a new analyzer is seen without anyone listing it here. + fn analyzer_methods_in_source() -> BTreeSet { + let source = include_str!("analyzer.rs"); + let compact: String = source.split_whitespace().collect::>().join(" "); + let mut found = BTreeSet::new(); + for piece in compact.split("fn analyze_").skip(1) { + let name: String = piece + .chars() + .take_while(|c| c.is_ascii_alphanumeric() || *c == '_') + .collect(); + let rest = &piece[name.len()..]; + if rest.starts_with("( &self, content: &str,") + || rest.starts_with("(&self, content: &str,") + { + found.insert(format!("analyze_{name}")); + } + } + found + } + + /// Methods with the analyzer signature that no language routes to by + /// design: helpers run on every file or called from other analyzers. + const NOT_LANGUAGE_ANALYZERS: [&str; 1] = ["analyze_cross_language"]; + + fn snake(lang: Language) -> String { + let name = format!("{lang:?}"); + let mut out = String::new(); + for (i, c) in name.chars().enumerate() { + if c.is_ascii_uppercase() && i > 0 { + out.push('_'); + } + out.push(c.to_ascii_lowercase()); + } + out + } + + /// Claim 1a: every language analyzer in the source is reached by some + /// language. An analyzer nothing routes to is dead code. + #[test] + fn every_language_analyzer_is_reached() { + let routed: BTreeSet<&str> = Language::ALL.iter().map(|l| route(*l).analyzer()).collect(); + let methods = analyzer_methods_in_source(); + assert!( + methods.len() > 30, + "source scan found only {methods:?}: the signature pattern no longer matches" + ); + for method in &methods { + if NOT_LANGUAGE_ANALYZERS.contains(&method.as_str()) { + continue; + } + assert!( + routed.contains(method.as_str()), + "{method} exists in analyzer.rs but no language routes to it" + ); + } + } + + /// Claim 1b: every routed analyzer exists, and no language goes to the + /// generic fallback while a dedicated analyzer for it exists. + #[test] + fn no_language_falls_back_while_a_dedicated_analyzer_exists() { + let methods = analyzer_methods_in_source(); + for lang in Language::ALL { + let r = route(lang); + let name = r.analyzer(); + if name.starts_with("analyze_") { + assert!( + methods.contains(name), + "{lang:?} routes to {name}, which analyzer.rs does not define" + ); + } + if r == Route::Generic { + let own = format!("analyze_{}", snake(lang)); + assert!( + !methods.contains(&own), + "{lang:?} falls back to analyze_generic, but {own} exists" + ); + } + } + } + + /// Claim 2: cross-language checks run exactly on non-configuration + /// content, and on scripts embedded in configuration. + #[test] + fn cross_language_checks_run_exactly_off_configuration() { + assert!(runs_cross_language(false)); + assert!(!runs_cross_language(true)); + + // Built at run time so this source file holds no insecure URL of its + // own for panic-attack's self-scan to report. + let url = |path: &str| format!("{}://example.org/{path}", "http"); + let tmp = TempDir::new().unwrap(); + // A Justfile is configuration. Its variable is configuration content; + // its recipe body is an embedded shell script. The recipe URL is + // quoted: the cross-language detector strips `//` comments first, + // which also cuts an unquoted URL (a separate recall gap). + fs::write( + tmp.path().join("Justfile"), + format!( + "mirror := \"{}\"\n\nfetch:\n curl \"{}\"\n", + url("variable"), + url("recipe") + ), + ) + .unwrap(); + fs::write( + tmp.path().join("main.lua"), + format!("local url = \"{}\"\nprint(url)\n", url("source")), + ) + .unwrap(); + + let report = Analyzer::new(tmp.path()).unwrap().analyze().unwrap(); + let insecure: Vec<_> = report + .weak_points + .iter() + .filter(|w| w.category == WeakPointCategory::InsecureProtocol) + .collect(); + + assert!( + insecure.iter().any(|w| w.description.contains("main.lua")), + "source file was not checked: {insecure:?}" + ); + let justfile: Vec<_> = insecure + .iter() + .filter(|w| w.description.contains("Justfile")) + .collect(); + assert!( + justfile.iter().any(|w| w.description.contains("embedded")), + "the recipe's embedded script was not checked: {insecure:?}" + ); + assert!( + justfile.iter().all(|w| w.description.contains("embedded")), + "configuration content was checked as source: {insecure:?}" + ); + } + + /// Claim 3: the language counts the README states are the count the + /// table supports (every language except the `Unknown` sentinel). + #[test] + fn readme_language_counts_match_the_table() { + let supported = Language::ALL + .iter() + .filter(|l| **l != Language::Unknown) + .count(); + let readme = include_str!("../../README.adoc"); + let claims = [ + ("badge", "languages-", "-blue"), + ("capabilities", "**", "-language static analysis"), + ("summary", "* ", " supported languages"), + ]; + for (label, before, after) in claims { + let stated = readme + .lines() + .find_map(|line| { + let end = line.find(after)?; + let start = line[..end].rfind(before)? + before.len(); + line[start..end].parse::().ok() + }) + .unwrap_or_else(|| panic!("README no longer states the {label} count")); + assert_eq!( + stated, supported, + "README {label} says {stated} languages; the routing table supports {supported}" + ); + } + } +} diff --git a/src/types.rs b/src/types.rs index 1c7b7ea..fad80e6 100644 --- a/src/types.rs +++ b/src/types.rs @@ -97,6 +97,67 @@ pub enum Language { } impl Language { + /// Every language, in declaration order, `Unknown` last. Tests iterate + /// over it, so a property checked "for every language" covers the whole + /// enum; `language_tests::all_lists_every_variant_once_in_order` keeps it + /// complete. + // The binary re-declares this module and never reads ALL itself. + #[allow(dead_code)] + pub const ALL: [Language; 52] = [ + Language::Rust, + Language::C, + Language::Cpp, + Language::Go, + Language::Java, + Language::Python, + Language::JavaScript, + Language::Ruby, + Language::Php, + Language::Elixir, + Language::Erlang, + Language::Gleam, + Language::ReScript, + Language::OCaml, + Language::StandardML, + Language::Scheme, + Language::Racket, + Language::Haskell, + Language::PureScript, + Language::Idris, + Language::Lean, + Language::Agda, + Language::Isabelle, + Language::Coq, + Language::Prolog, + Language::Logtalk, + Language::Datalog, + Language::Zig, + Language::Ada, + Language::Odin, + Language::Nim, + Language::Pony, + Language::DLang, + Language::Nickel, + Language::Nix, + Language::Shell, + Language::Julia, + Language::Lua, + Language::Chapel, + Language::WokeLang, + Language::Eclexia, + Language::MyLang, + Language::JuliaTheViper, + Language::Oblibeny, + Language::Anvomidav, + Language::AffineScript, + Language::Ephapax, + Language::BetLang, + Language::ErrorLang, + Language::VCL, + Language::FBQL, + Language::Unknown, + ]; + /// Infer the language from the final, case-sensitive extension without reading /// the file. Missing or unrecognised extensions yield `Unknown`. /// @@ -1154,6 +1215,79 @@ mod rule_id_tests { } } +#[cfg(test)] +mod language_tests { + use super::Language; + + // Exhaustive, with no wildcard: a new variant fails to compile here + // until it is given a place, and the test below then fails until ALL + // lists it at that place. + fn ordinal(l: Language) -> usize { + use Language::*; + match l { + Rust => 0, + C => 1, + Cpp => 2, + Go => 3, + Java => 4, + Python => 5, + JavaScript => 6, + Ruby => 7, + Php => 8, + Elixir => 9, + Erlang => 10, + Gleam => 11, + ReScript => 12, + OCaml => 13, + StandardML => 14, + Scheme => 15, + Racket => 16, + Haskell => 17, + PureScript => 18, + Idris => 19, + Lean => 20, + Agda => 21, + Isabelle => 22, + Coq => 23, + Prolog => 24, + Logtalk => 25, + Datalog => 26, + Zig => 27, + Ada => 28, + Odin => 29, + Nim => 30, + Pony => 31, + DLang => 32, + Nickel => 33, + Nix => 34, + Shell => 35, + Julia => 36, + Lua => 37, + Chapel => 38, + WokeLang => 39, + Eclexia => 40, + MyLang => 41, + JuliaTheViper => 42, + Oblibeny => 43, + Anvomidav => 44, + AffineScript => 45, + Ephapax => 46, + BetLang => 47, + ErrorLang => 48, + VCL => 49, + FBQL => 50, + Unknown => 51, + } + } + + #[test] + fn all_lists_every_variant_once_in_order() { + for (i, l) in Language::ALL.iter().enumerate() { + assert_eq!(ordinal(*l), i, "ALL[{i}] is {l:?}, out of place"); + } + } +} + #[cfg(test)] mod language_detect_tests { use super::Language;