Detector] token math - #861
Open
gloskull wants to merge 32 commits into
Open
Conversation
A watch mode that re-runs analysis automatically when .rs files change, tightening the fix-save-see-results loop. - notify-based recursive watcher over the target path; reacts only to create/modify/remove of .rs files - debounced (~300ms, configurable via --debounce) with a timer that resets on each change, so a burst of saves coalesces into one run and a change mid-window supersedes the pending run - clears the screen and re-runs 'analyze' as a child process between runs, so analyze's process::exit on findings doesn't kill the watcher - cooperative Ctrl-C shutdown via a polled flag - unit tests for the .rs event filter; docs/cli.md regenerated Usage: sanctifier watch --path contracts/ Closes Centurylong#361
…n rounding-to-zero Closes Centurylong#333. Implements a new AST-based detector that flags fee/interest calculations of the form `let fee = amount * rate / DENOM` where integer division can produce 0 for small inputs, allowing an attacker to split transactions into micro-amounts and pay no fees. Changes: - `src/rules/fee_rounding.rs`: new `FeeRoundingRule` using syn::visit::Visit; inspects each function body for fee-related `let` bindings (names containing fee/interest/rate/charge/bps/tax/…) whose init is a mul-then-div expression with a large integer denominator (≥ 100) and no subsequent minimum-fee guard (`if fee == 0 { fee = 1 }` or `.max(1)` in the binding). - `src/finding_codes.rs`: adds S017 `FEE_ROUNDING` constant and its `FindingCode` entry in `all_finding_codes()`. - `src/rules/mod.rs`: exports `fee_rounding` module and registers `FeeRoundingRule` in `RuleRegistry::with_default_rules()`. - `tests/fixtures/detectors/fee_rounding.rs`: fixture with two violations (`charge_fee`, `accrue_interest`) and two safe patterns (if-guard, `.max(1)`). - `tests/snapshots/detector_snapshots__fee_rounding.snap`: accepted insta golden snapshot for both expected violations. - `tests/detector_snapshots.rs`: adds `snapshot_fee_rounding` test. Safe patterns NOT flagged: • `let mut fee = …; if fee == 0 && amount > 0 { fee = 1; }` — guard present • `let fee = (amount * bps / 10_000).max(1)` — outer expression is `.max()`, not a bare division, so `is_mul_div_pattern` returns false
…nding-detector-333 feat(detector): add fee_rounding rule (S017) — catch integer division rounding to zero in fee calculations
…ctor-321 feat: detect unsafe integer casts
- Add report storage system with ID generation and expiry (30 days) - Create /report/[id] dynamic route for viewing shared reports - Update analyze API to save reports and return shareable ID - Add copy link button in scan results page - Display report metadata (timestamp, expiry) on shared pages - Include source snippet preview in shared reports - Implement automatic cleanup of expired reports - Add storage directory to .gitignore Closes Centurylong#375
…-report-permalink-375 feat: Shareable report permalink feature
…enturylong#389) - Document all implemented security features (slippage protection, MEV protection, k-invariant) - Detail comprehensive test suite (18 tests: 4 unit + 14 property tests) - Document 7 Kani formal verification harnesses - Mark Issue Centurylong#389 acceptance criteria as completed - Provide usage examples for hardened contract interface - Update architecture documentation All hardening requirements from Issue Centurylong#389 have been completed: ✅ Swaps enforce min-out + deadline ✅ k-invariant documented and tested ✅ Property/Kani tests for core invariants Status: AMM pool template is now production-ready with comprehensive security.
…ssue-389-amm-hardening-complete docs: Update AMM pool README to document completed hardening
feat: detect missing storage TTL bumps
Adds a GitHub Actions job that runs `cargo kani` on every proof-harness crate with a per-harness time budget and reports a pass/fail summary — a "we verify in CI" guard against silent regressions. - Runs Kani on the harness crates: kani-poc-contract, token-invariants, amm-pool, reentrancy-guard (each with `--harness-timeout 120s`, plus an outer wall-clock cap per package). - Caches the Kani toolchain (~/.kani), the verifier binary, the cargo registry, and build artifacts to keep reruns fast. - Writes a per-package pass/fail table to the GitHub step summary. - Non-blocking initially (per the issue): install + proof steps are `continue-on-error` and the runner exits 0, so the suite reports results without blocking merges while it stabilizes. `timeout-minutes: 30` is a hard ceiling against a runaway solver. Workflow-only change; no Rust/source changes, so the existing test/build CI is unaffected.
…i-proofs [FV] CI job: run Kani proofs on PRs with a time budget (Centurylong#348)
feat(cli): add 'sanctifier watch' for continuous re-analysis on file change (closes Centurylong#361)
…g#352) Closes Centurylong#352 Adds a new `tooling/zk` crate (`sanctifier-zk`) that implements a proof-of-concept zero-knowledge circuit proving that an audited WASM contract hash achieved at least a target score under a given ruleset, without revealing the per-rule finding set. ## Circuit design (Groth16 over BLS12-381) Public inputs (in allocation order — must match the on-chain verifier): 1. wasm_hash — SHA-256(wasm_bytes) mod |Fr| 2. ruleset_version — u32 identifying the applied rule set (v1 = 11 rules) 3. score_threshold — minimum passing score in [0, N_RULES] 4. rules_commitment — Poseidon(r₀ … r_{N−1}), binding the proof to specific per-rule results without revealing them Constraints (R1CS): • Boolean: r_i * (1 − r_i) = 0 for each of the 11 rules • Score: score = Σ weight_i * r_i (equal weights = 1 in v1) • Threshold: bit-decomposition of (score − threshold) fits in 8 bits, proving score ≥ threshold without revealing the exact score • Commitment: Poseidon(r₀ … r_{N−1}) == rules_commitment ## Files tooling/zk/ ├── src/ │ ├── lib.rs — public API: setup / prove / verify / helpers │ ├── circuit.rs — ConstraintSynthesizer implementation │ ├── encoding.rs — public-input encoding with full spec doc │ ├── params.rs — deterministic Poseidon parameters (PoC seed) │ └── bin/prover.rs — CLI: hash WASM → generate proof → verify → JSON └── benches/ └── zk_bench.rs — criterion benchmarks (setup / prove / verify / proof size / constraint count) ## Proof size Groth16/BLS12-381 produces a constant-size compressed proof of 128 bytes regardless of circuit size. ## Security note The Poseidon MDS matrix is generated from a fixed PRNG seed for this PoC. Production use requires a proper MPC-based parameter ceremony (Grain LFSR or similar) to guarantee the MDS property and eliminate a trusted party.
…-audit-circuit feat(zk): add Groth16/BLS12-381 audit-proof circuit (issue Centurylong#352)
…-327 Add SANCT_ARG_DOS detector for unbounded argument iteration
docs: add custom detector cookbook and update contributing guide
…ong#151) - Expand vulnerability-db.json from 12 to 32 entries with new fields: cvss (f64), affected_versions, poc_exploit, patch, tags, related_cves - Add 32 YAML source files in data/vulnerabilities/ (CVE-style format) - Update VulnEntry struct in vulndb.rs to support all new fields - Add VulnDatabase methods: search(), by_category(), by_severity(), get_by_id(), to_json(), to_rss() for RSS 2.0 feed generation - Add `sanctifier cve` subcommand (commands/cve.rs) with: cve search --keyword <kw> cve list [--category <cat>] [--severity <sev>] cve show <id> cve export --format <json|rss> [--output <file>] cve serve [--port <port>] (GET /api/vulndb, /api/vulndb/<id>, /api/vulndb/feed.rss)
- Create sep41-token-invariants contract with pure functions encoding all core SEP-41 token arithmetic semantics - 12 formal invariants covering: transfer conservation, transfer-from allowance enforcement, approve consistency, mint/burn correctness, rejection of invalid amounts and insufficient balances/allowances - 14 Kani proof harnesses verifying all invariants symbolically - Soroban contract implementation (Sep41Token) with #[invariant] attributes for sanctifier verify / cargo kani integration - Documentation at docs/sep41-formal-spec-template.md for reuse - 16 passing tests validating pure function correctness - Fix signed integer underflow: explicit balance checks for i128 Closes Centurylong#350
…ormal-spec-templates [FV] Formal spec templates for SEP-41 token compliance
Adds CLI reference entries for the new `cve` subcommand and its subcommands (search, list, show, export, serve) introduced in this PR. Fixes the CI staleness check.
…vulndb feat: public Soroban/Stellar CVE vulnerability database
Add SANCT_DECIMALS detector for mixed raw/scaled token arithmetic
github-actions
Bot
added
dependencies
github-actions
Bot
added
size/l
and removed
area: ci/cd
Contributor
|
@gloskull, ensure all ci passes and please stop spamming issues |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
10 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation
Description
tooling/sanctifier-core/src/rules/decimals_scale.rsthat heuristically infers token amount sources, detects raw vs scaled naming, and suppresses findings when a documented normalization call is present.tooling/sanctifier-core/src/rules/mod.rsand add a finding-code constantDECIMALS_SCALE(SANCT_DECIMALS) intooling/sanctifier-core/src/finding_codes.rswith metadata.tooling/sanctifier-core/tests/fixtures/corpus/differential-corpus.jsonto map the new rule for corpus-driven tests.Testing
cargo test -p sanctifier-core decimals_scale --manifest-path Cargo.toml, which passed.cargo test -p sanctifier-core --manifest-path Cargo.toml, and the package tests completed successfully (all tests passed).Closes #328