fold/skills/fold-sast/SKILL.md

name	description	tags
skill-fold-sast	Fold bounded symbolic SAST / binary-analysis / confirmation guide for C++, Rust, and Swift code review, scanning, precision measurement, and optimization. Use when selecting a Fold scan mode, interpreting findings, profiling a scan, or confirming a suspected vulnerability.	fold sast dast symbolic-execution cpp binary-analysis fuzzing rust swift code-review precision performance

Fold — Bounded Symbolic SAST, Binary Analysis, and Confirmation

Overview

Fold analyzes source and binaries while keeping evidence lanes separate:

• Source lane: Clang LibTooling, normalized IR/summaries, bounded Z3-backed detectors, and SARIF/versioned-findings-JSON/Markdown reporting.
• Binary lane: radare2-backed metadata/heuristics, Ghidra/SLEIGH P-Code semantics, Capstone gadget discovery, and candidate ROP evidence.
• Confirmation lane: shared FindingConfirmationTask / FindingConfirmationResult records used by fold confirm, fold fuzz prep, fold fuzz run, and optional adapters such as the KLEE smoke prototype.

Use this skill when working on the Fold codebase, running scans, adding observers or detectors, interpreting findings, updating CLI/report behavior, or comparing Fold against CSA, CodeQL, Infer, CBMC, Semgrep, clang-tidy, KLEE, angr, or concolic/fuzzing tools.

When to use

Use this skill when:

• working in the Fold repository;
• reviewing or scanning a C++, Rust, or Swift project with Fold;
• running fold scan with source, binary, hybrid, rust, swift, or auto mode;
• adding or modifying detectors, observers, summaries, binary heuristics, or report serialization;
• interpreting confidence levels, counterexamples, fix-its, fuzz witnesses, binary exploit context, or fact provenance;
• preparing or running confirmation with fold confirm or fold fuzz prep/run;
• using optional confirmation experiments such as KLEE smoke tests;
• updating CLI help, embedded skills, MCP surfaces, or docs.

When project input is available, run the appropriate scan rather than merely suggesting a command. Stop and state the missing prerequisite when a compile database, Rust crate, Swift source/package, binary, benchmark corpus, baseline, or precision oracle is absent.

When not to use

Do not use this skill for generic static-analysis tool selection with no Fold work, Semgrep rule authoring, variant hunting without a Fold seed finding, or a one-off Z3/SMT question unrelated to Fold.

Architecture

source / binary / rust / swift input
        ↓
scan router ── keeps source, binary, and language lanes separate
        ↓
frontend / binary extractor → IR, summaries, P-Code, facts
        ↓
detectors / observers → findings + evidence + provenance
        ↓
SARIF / findings-json / Markdown + optional confirmation tasks/results
        ↓
fold confirm / fold fuzz / optional KLEE-style adapters

Module boundaries

Module	Typical files	Responsibility
CLI/router	src/cli/, include/fold/cli/	commands, scan routing, confirm/fuzz orchestration
frontend	include/fold/frontend/, src/frontend/	Clang/Rust/Swift input collection
binary	include/fold/binary/, src/binary/	r2, Ghidra P-Code, Capstone gadgets, ROP candidates
ir	include/fold/ir/, src/ir/	expression/summary/fact identity models
symbolic	include/fold/symbolic/, src/symbolic/	Z3 encoding, observers, bounded proof
detect	include/fold/detect/, src/detect/	finding-class detectors
confirm	include/fold/confirm/, src/confirm/	shared confirmation task/result schema
fuzz	include/fold/fuzz/, src/fuzz/	harnesses, seeds, witness matching
report	include/fold/report/, src/report/	finding model, SARIF/Markdown/JSON
mcp/lsp	include/fold/mcp/, include/fold/lsp/	agent/server integrations

Evidence lanes and boundaries

• Keep source and binary backends separate unless router work explicitly asks for hybrid orchestration.
• Binary findings are heuristic unless source/Z3 or runtime confirmation corroborates them.
• ROP chains are candidate exploitability evidence; preserve caveats such as ASLR/PIE/canary/frame layout and input-control assumptions.
• Hybrid mode should preserve per-finding backend provenance and avoid silently hiding source coverage unless the user requested a capped candidate set.
• --detectors production-reachability is a serial whole-project pass. Treat unknown guards and incomplete roots/dispatch as reachable; only complete closed-world unreachable-production evidence may set removal_candidate. compile-variant-absent requires an explicit finite variant manifest.

Confidence model

Confidence	Meaning
concrete-witness	Runtime confirmation, typically libFuzzer/ASan, observed a matching crash. Strictly strongest tier.
proved	Z3 established the condition under Fold's bounded model.
latent	The bounded proof depends on a caller/environment precondition that is not discharged locally.
heuristic	Evidence is partial, approximate, binary-heuristic, or unsupported constructs were involved.
syntactic	Structural/hash/shape match only; no semantic proof.

Treat Fold as a bounded model. proved means proved within the model and budget, not universal program correctness. Prioritize concrete-witness, then proved, then latent findings whose preconditions are realistic, followed by high-impact heuristic findings.

Detectors

Source/security examples

Detector	Hazard
div-by-zero	divisor may be zero under path
null-deref	pointer/member dereference may be null
int-overflow	integer arithmetic may overflow at source width where modeled
int-truncation	narrowing conversion may lose information
sign-conversion	signed/unsigned conversion may change meaning
oob	index/buffer access may be out of bounds
taint-track	untrusted source reaches sensitive sink
uninit-read	local/object read may be uninitialized
use-after-move	C++ object use after move
iterator-invalidation	iterator may be used after invalidating operation
always-condition, unreachable	symbolic control-flow anomalies

Redundancy examples

Detector	Hazard
clone	Type-2/3 structural clone candidates
equiv	semantic equivalence under bounded Z3 encoding
dead	dead branch/path predicate evidence
class-dup	class/method duplication candidates

Binary examples

Binary mode can report hardcoded strings/credentials, unsafe calls, suspicious sections/imports/symbols, P-Code summaries, buffer-overflow-like evidence, gadget/ROP context, and other backend-specific heuristic findings depending on build options and available tools.

CLI recipes

Source scan

fold scan --mode source --compile-db build/compile_commands.json \
  --detectors div-by-zero,null-deref,int-overflow,oob,taint-track \
  --format sarif --output fold.sarif \
  --budget-seconds 300 --per-query-ms 2000 --processes 0

For native machine-readable output, use the explicitly versioned envelope:

fold scan --mode source --compile-db build/compile_commands.json \
  --detectors security --format findings-json --output fold-findings.json

Binary scan

fold scan --mode binary --binary ./app --detectors security \
  --binary-max-functions 0 --format sarif --output fold-binary.sarif

Hybrid scan

fold scan --mode hybrid --compile-db build/compile_commands.json \
  --binary ./app \
  --hybrid-strategy merge-only --detectors security \
  --format sarif --output fold-hybrid.sarif

Rust or Swift source scan

fold scan --mode rust path/to/crate --detectors rust-security \
  --format sarif --output fold-rust.sarif
fold scan --mode swift path/to/file.swift --detectors swift-security \
  --format sarif --output fold-swift.sarif

Rust and Swift source findings are heuristic today; use binary mode for compiled artifacts when binary evidence is desired.

Rust complexity scan

fold scan --mode rust path/to/crate --detectors complexity \
  --complexity-threshold 15 --format sarif --output fold-rust.sarif

The Rust frontend evaluates complexity from HIR control-flow structure. Keep the threshold explicit in reproducible runs; it is shared with the C++ detector.

Code-review and scan workflow

Use the installed CLI as the authority for the current release before forming a command. Normal help shows stable options; advanced help exposes tuning, profiling, cache, and watchdog controls:

fold scan --help
fold scan --advanced-help

1. Select the lane explicitly

Review input	Command shape	Rules
C++ project with compile_commands.json	fold scan --mode source --compile-db <db> ...	Use --scope security for security review, --scope quality for maintainability, or compose both.
One or more C++ files without a database	fold scan --mode source <paths...> ...	Fold infers a synthetic compile database; pass --std and required --extra-arg flags explicitly.
Cargo crate or Rust file	fold scan --mode rust <crate-or-file> --detectors rust-security ...	Do not pass --rust-allow-build-code for untrusted projects; it enables build scripts and proc macros.
Swift package or source file	fold scan --mode swift <package-or-file> --detectors swift-security ...	Keep Swift reports and provenance separate from source C++ or binary evidence.
Executable or firmware only	fold scan --mode binary --binary <path> ...	Binary results are heuristic unless independently corroborated.
Matching source and binary inputs	fold scan --mode hybrid --compile-db <db> --binary <path> --hybrid-strategy merge-only ...	merge-only is the only implemented strategy. It must not hide source coverage.

Use --mode auto only for exploratory work. Reproducible reviews and benchmark artifacts use an explicit mode, detector/scope selection, and file output. --input-type and --format json are compatibility aliases; do not use them in new commands.

2. Run the smallest complete review

Write reports to files so the original evidence remains available:

fold scan --mode source --compile-db build/compile_commands.json \
  --scope security,quality --format sarif --output fold-review.sarif

fold grep "overflow" fold-review.sarif --field message \
  --backend source --actionable-only --format json --output overflow-findings.json

Use findings-json instead of SARIF only when a consumer requires Fold's native versioned envelope. fold grep searches existing Fold reports; it does not scan source text.

For a Fold repository change, run the local quality gate after the focused scan:

fold quality --compile-db build/release/compile_commands.json

Do not invoke fold quality with missing project prerequisites or suppress its policy/test failures to obtain a scan result.

3. Review findings by evidence

1. Preserve the SARIF or findings-json report, profile, and logs.
2. Group findings by backend, rule, confidence, and stable ID.
3. Treat concrete-witness as runtime evidence; proved is bounded-model evidence; latent, heuristic, and syntactic require progressively more source and contract review.
4. Verify a suspected vulnerability with fp-check before calling it actionable. Trace callers, guards, API contracts, and the exact sink.
5. Suppress generated or third-party findings through --exclude-glob or a reviewed suppression file, never by editing the scanned dependency.

Precision and optimization workflow

Use this workflow only when the request involves performance, memory, false-positive reduction, precision claims, or benchmark changes.

1. Measure first. Use a checked-in project manifest with scripts/benchmarks/run_project_eval.py; preserve the immutable run artifacts, profile, target-set fingerprint, configuration fingerprint, and revision. Use scripts/benchmarks/run_optimization_harness.py for a compact project artifact.
2. Attribute the owner. Select one ranked detector, source phase, graph subphase, reliability failure, or focused microbenchmark. Do not optimize an unattributed aggregate wall-time bucket.
3. Use the required specialist skill. Invoke cpp-performance for a profiling decision; invoke paperbridge before a research-backed algorithm change; invoke fp-check for each suspected production vulnerability.
4. State the invariant. Behavior-preserving changes retain finding identity, source/binary provenance, operational coverage, and expected positive cases. A precision change names its expected identity delta before implementation.
5. Require labels for precision claims. TP, FP, FN, and TN require explicit positive and clean-negative oracle cases. A reviewed production alert sample is not a recall benchmark, and absent TN/FN values must remain unmeasured.
6. Run an ablation. Keep a default-on change only when the profiled owner improves beyond observed variance without unexpected coverage, identity, reliability, or RSS regression. Retain a useful unproven strategy as default-off; reject non-reproducible or unattributed wins.

Follow docs/architecture/optimization-loop.md when working in the Fold repository. It defines the full experiment record and validation matrix. Keep source, binary, and hybrid results as separate lanes unless router work explicitly changes merge-only orchestration.

Deeper bounded symbolic confirmation

fold confirm build/compile_commands.json --rule null-deref --unwind 10 \
  --budget 5000 --output confirm.json --witness witnesses/

Runtime confirmation with libFuzzer + ASan

fold fuzz prep --compile-db build/compile_commands.json --output /tmp/fold-fuzz
fold fuzz run --prep-dir /tmp/fold-fuzz --report /tmp/fold-fuzz/augmented.json

fold fuzz prep preserves legacy findings.predicted.json and also writes confirmation.tasks.json. fold fuzz run writes augmented findings and confirmation.results.json. Matched crashes promote findings to concrete-witness.

Query existing Fold findings

fold grep searches Fold SARIF or native findings-json reports, not raw source text. It uses bounded fixed-string matching and preserves finding IDs and backend provenance.

fold grep "null pointer" fold.sarif --field message --ignore-case
fold grep "fold.null-deref" fold.sarif --field rule \
  --backend source --path-glob 'src/*.cpp' --actionable-only
fold grep "token" source.sarif binary.sarif \
  --format json --output matches.json

Searchable fields are message, id, rule, path, function, and evidence. Typed filters include rule, confidence, backend, path glob, baseline status, suppression, and actionable-only. JSON query output includes deterministic pagination and truncation metadata.

MCP scan and query lifecycle

Use the canonical tools fold.scan, fold.scan_start, fold.scan_status, fold.scan_jobs, fold.scan_job_findings, fold.scan_activate, fold.get_scan_context, fold.get_findings, fold.query_findings, fold.suggest_merge, and fold.explain.

For long scans, call fold.scan_start, poll fold.scan_status, then query the completed job_id with fold.query_findings or activate it with fold.scan_activate. MCP accepts paths only under configured --allow-root roots and enforces server-owned queue, process, solver-budget, path-count, and work-item limits before execution. Deprecated tool/argument aliases remain callable but hidden and return structured deprecation metadata; do not use them in new recipes.

Embedded skill output

fold skill                # print this embedded SKILL.md
fold skill -o SKILL.md    # write it to a file
fold --help               # shows the skill command for agents

Long-running scans in Pi

Use MonitorCreate for large scans instead of blocking inline:

MonitorCreate(command="fold scan --compile-db ... --format sarif "
                      "--output /tmp/fold/results.sarif ...",
              description="Fold scan", timeout=600000,
              onDone="Parse the Fold results and summarize findings")

Key flags

• --mode: auto, source, binary, hybrid, rust, or swift.
• --compile-db: path to compile_commands.json or a build directory.
• --binary: binary/firmware path for binary or hybrid mode.
• --detectors: repeatable or comma-separated detector list.
• --source-detectors / --binary-detectors: backend-specific hybrid overrides.
• --format: sarif, versioned native findings-json, or markdown/md. json is a deprecated compatibility alias for SARIF.
• --fix-output: write a unified diff for available FixIts; no in-place edits.
• --exclude-glob: repeatable file exclusion patterns. Project-relative patterns such as third_party/** also match absolute compile-database paths at a path component boundary.
• --budget-seconds, --per-query-ms, --loop-unroll: symbolic budgets.
• --processes 0: auto worker count. 1 means one isolated worker for ordinary source scans, not in-process execution; profile and incremental scans currently use the serial in-process path because their state is not worker-mergeable.
• --incremental + --cache-dir: changed-function/caller reruns.
• --config-profile: strict v1 runtime assumptions and explicit production entrypoints for privacy-safe guarded callsite/root evidence; source/hybrid only, and discovery alone does not prune graph edges.
• --portfolio: SMT plus bit-blast SAT portfolio for QF_BV queries.
• --nullable-allocations: model allocations as nullable for null-deref.
• --suppressions, --baseline, --quarantine-dir, --per-tu-timeout: operational stability and triage controls.
• --profile, --profile-output, --profile-solver, --profile-reach, --trace: diagnostics. Supplying --profile-output enables profiling; report and profile paths must be distinct.
• --advanced-help: print the catalog-generated tuning/profile/cache options omitted from normal scan help.

New automation should use canonical spellings. Compatibility aliases such as --input-type, scan --format json, hidden MCP tool names, and hidden MCP argument aliases remain callable only for migration. They are omitted from normal help/schema documentation and emit deprecation details. Fold 1.0.0 is the earliest eligible—not automatic—removal boundary; see docs/compatibility.md.

Project evaluation and profiles

Use the manifest-driven runner for repeatable evaluation of a real source, Rust, or binary project. Manifests pin the corpus, lane, detector scope, limits, and stability/performance budgets; do not check in a generated baseline before reviewing it.

python3 scripts/benchmarks/run_project_eval.py \
  --manifest tests/benchmarks/projects/yams_source.json
python3 scripts/benchmarks/run_project_eval.py \
  --manifest tests/benchmarks/projects/sage_rust.json

For Rust projects with a pinned toolchain, put the toolchain in the manifest so the fold-rust child process receives it. The runner writes SARIF, profile JSON, logs, immutable run artifacts, finding-stability data, and an optional gold/disposition/performance comparison.

Use --profile-output when inspecting a scan. Requested report/profile files are written through sibling temporary files and atomically renamed; an open/write/rename failure returns exit 2. Console actionability, exit status, FixIts, SARIF, and native JSON derive from one filtered/deduplicated finding set. Profiles expose findings_before_filter and findings_report_visible so count changes remain explainable. Source profiles report solver metrics; Rust and Swift profiles report frontend extraction plus ingestion/IR rows; binary profiles report heuristic, BinaryIR, and P-Code rows. P-Code solver statistics remain separate from source solver statistics.

Check fold --version before retaining evidence. Development builds report the Meson semantic version plus Git revision and a .dirty suffix when configured from a modified tree. The same provenance is written to SARIF, native JSON, profile JSON, and benchmark run artifacts.

Interpreting findings

1. Group by detector/rule and confidence.
2. Prioritize concrete-witness and proved security findings.
3. Read counterexamples, path predicates, witness metadata, and backend evidence.
4. For heuristic findings, identify the approximation: unresolved calls, unknown lengths, unsupported control flow, partial binary metadata, or missing interprocedural summaries. Invalid sink-model argument indexes and unsupported portfolio expressions fail closed with bounded diagnostics; they are not findings.
5. De-duplicate repeated findings by finding ID / ruleId:file:line:col.
6. Exclude generated/vendor code with --exclude-glob or suppressions rather than editing third-party sources. Missing generated dependencies, frontend exits, TU timeouts, and worker signals are coverage failures, not findings; preserve their logs and quarantine provenance.
7. Preserve complete SARIF or findings-json artifacts for machine triage; summarize only bounded actionable findings to users.

Confirmation and fact identity

• FindingConfirmationTask is the shared adapter input.
• FindingConfirmationResult is the shared adapter output.
• Fuzz prediction compatibility remains: old consumers can still read findings.predicted.json.
• Optional fact provenance can link findings/tasks to cross-lane identities such as functions, blocks, operations, and values. Do not duplicate wire-format key strings; centralize JSON keys in the owning C++ header/source.

Development workflow

Read AGENTS.md before router/backend work. Keep source and binary paths separate. For complex detector or backend changes, write focused tests first where practical.

Focused validation:

ninja -C build/release
meson test -C build/release fold:scan_e2e fold:cli_paths fold:mcp_stdio --print-errorlogs
meson test -C build/release fold:confirm_cli --print-errorlogs
meson test -C build/release fold:fuzz_prep fold:fuzz_run --print-errorlogs
meson test -C build/release fold:confirmation_task fold:fact_id --print-errorlogs
git diff --check

Binary/ROP validation:

meson test -C build/release \
  fold:binary_backend fold:gadget_capstone fold:gadget_semantics \
  fold:rop_chain \
  --print-errorlogs

Optional KLEE smoke:

tests/confirmation/klee/run_klee_smoke.sh

It skips cleanly when KLEE is absent.

Full validation for CLI/router/backend changes:

ninja -C build/release
meson test -C build/release --print-errorlogs
git diff --check

Evaluation-runner changes also require:

python3 tests/benchmarks/test_fold_eval.py
python3 scripts/benchmarks/run_rust_swift_goldens.py

Companion skills

Skill	Use for
cpp-review	Mandatory for C++ code-review requests; covers API safety, UB, and C++ correctness.
rust-style	Mandatory for Rust code-review requests; applies Rust-specific idioms and boundaries.
cpp-performance	Mandatory when profiling or selecting a C++ performance optimization.
fp-check	Mandatory before classifying a suspected vulnerability as actionable.
paperbridge	Mandatory for literature-backed optimization or analysis-design proposals.
static-analysis	General SAST tooling, CodeQL/Semgrep/SARIF triage
variant-analysis	Bug-variant hunting after a seed finding
semgrep-rule-creator	Writing Semgrep rules
cpp-meson-ninja-conan	Meson/Ninja/Conan C++ build work
radare2-reversing	Manual radare2 binary analysis