admin/trailofbits-skills
1
0
Fork 0
mirror of https://github.com/trailofbits/skills synced 2026-06-21 14:12:00 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat(trailmark): skills that reason about code as graphs (#133)

Browse Source 
* feat(trailmark): skills that reason about code as graphs

* Add Codex skill symlinks for trailmark plugin

The trailmark plugin's 10 skills were missing .codex/skills/ mappings,
which caused the validate_codex_skills CI check to fail.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Address PR #133 review feedback

- Add Rationalizations (Do Not Skip) sections to 5 security skills:
  trailmark, audit-augmentation, crypto-protocol-diagram,
  mermaid-to-proverif, graph-evolution
- Fix requires-python: diagram.py >= 3.12 (was 3.13), protocol.py
  >= 3.12 (was 3.11) to match trailmark's actual requirement
- Rename diagram/ to diagramming-code/ to match SKILL.md frontmatter
  name and all cross-skill references; update Codex symlink

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Fix diagram skill to use uv run instead of plain python

The diagram.py script carries PEP 723 inline metadata declaring
trailmark as a dependency. Plain python ignores this metadata,
causing ImportError for users who haven't pre-installed trailmark.
uv run processes the metadata and handles dependency resolution.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Address second round of PR #133 review feedback

- Fix README directory tree: diagram/ -> diagramming-code/
- Fix diagram-types.md: python -> uv run for all script invocations
- Fix graph-evolution Phase 3: replace undefined shell variables
  ($BEFORE_JSON etc) with template substitutions ({before_json} etc)
- Fix vector-forge mutation-frameworks.md: replace cross-skill file
  link with prose reference to genotoxic skill (avoids reference chain)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Local skill-improver review pass across all 10 trailmark skills

diagramming-code:
- Fix arrow syntax inconsistency: uncertain edges use ..-> not -.->
- Fix extra closing paren in diagram-types.md
- Fix diagram.py docstring to match uv run invocation

crypto-protocol-diagram:
- Remove reference chain: spec-parsing-patterns.md no longer links to
  mermaid-sequence-syntax.md, inlines the arrow syntax instead
- Fix ProVerif example note: "Tamarin/ProVerif" -> "ProVerif"

trailmark:
- Replace "path/to/project" with {targetDir} in query-patterns.md
- Add uv run prefix to CLI examples in query-patterns.md
- Add circom to supported language list
- Add pre-analysis annotation kinds to annotation docs

genotoxic:
- Remove reference chains: triage-methodology.md and
  mutation-frameworks.md no longer link to graph-analysis.md

vector-forge:
- Add trailmark to Prerequisites section
- Fix bare trailmark commands to use uv run with {targetDir}

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Address third round of PR #133 review feedback

mermaid-to-proverif:
- Fix ProVerif type error: verify(...) = true is a type mismatch
  since verify returns bitstring. Use let _ = verify(...) in instead,
  which aborts on destructor failure (correct ProVerif pattern)

trailmark-summary, trailmark-structural:
- Add 8 missing language extensions to find command (.rb, .php, .cs,
  .java, .hs, .erl, .cairo, .circom)
- Remove unsupported .lean extension
- Split .c -> --language c and .cpp -> --language cpp (separate parsers)

All 7 security skills:
- Rename "Rationalizations (Do Not Skip)" to "Rationalizations to
  Reject" per CLAUDE.md convention

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Address fourth round of PR #133 review feedback

mermaid-to-proverif:
- Fix ProVerif type errors in process template: pkey values cannot
  appear in bitstring positions. Add pkey2bs() and concat() to the
  function declarations and rewrite the template to use them,
  matching the sample-output.pv example

trailmark-summary:
- Split .js/.ts mapping: .js -> --language javascript,
  .ts -> --language typescript (separate parsers)

graph-evolution:
- Replace bare python with python3 in graph_diff.py invocations
  (python does not exist on modern Ubuntu/Debian/macOS)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Address fifth round of PR #133 review feedback

graph-evolution:
- Change python3 to uv run for graph_diff.py invocations to match
  ecosystem convention

trailmark-structural, trailmark-summary:
- Add Rationalizations to Reject sections (both are security skills
  running blast radius, taint, and privilege boundary analysis)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Fix ProVerif type consistency and graph-evolution template vars

mermaid-to-proverif:
- Rename senc/sdec to aead_enc/aead_dec in Step 3 preamble to match
  the process template and sample-output.pv
- Fix hkdf signature: hkdf(key, bitstring): key (first arg is DH
  shared secret which has type key, not bitstring)

crypto-to-proverif-mapping.md:
- Fix hkdf declaration and summary table to match corrected signature
- Fix example to use concat/pkey2bs for type-correct HKDF input

graph-evolution:
- Replace $BEFORE_DIR/$AFTER_DIR shell vars in Phase 5 with
  {before_dir}/{after_dir} template substitutions

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Comprehensive vivisect-style review of all trailmark skills

ProVerif correctness (mermaid-to-proverif):
- Fix broken ForwardSecrecyTest pattern in security-properties.md:
  process waited on c_fs but nothing sent on it, past_session_key
  was never bound to any session. Replaced with working pattern
  that leaks long-term keys and checks session key secrecy.
- Fix hkdf(bitstring,bitstring) -> hkdf(key,bitstring) in
  proverif-syntax.md to match SKILL.md and sample-output.pv
- Fix type-incorrect example in proverif-syntax.md: tuple of
  (key,pkey,pkey) passed where bitstring expected. Now uses
  concat2/pkey2bs for type-correct serialization.
- Align senc/sdec -> aead_enc/aead_dec in proverif-syntax.md and
  crypto-to-proverif-mapping.md to match SKILL.md and example
- Fix auth query parameter count in security-properties.md:
  beginI fires before session key is known, so has fewer params

Cross-skill consistency:
- Fix 3 stale "diagram skill" references -> "diagramming-code"
  in trailmark/SKILL.md and preanalysis-passes.md
- Add PEP 723 header to graph_diff.py for convention consistency

README and helper skills:
- Add trailmark-summary and trailmark-structural to README skills
  table and directory tree
- Add secondary file extensions (.jsx, .tsx, .h, .hpp, .cc, .cxx)
  to language detection in summary and structural skills
- Inline language mapping in trailmark-structural (was deferred
  to trailmark-summary, violating one-level-deep rule)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Fix ProVerif type consistency and graph-evolution template vars

- Fix endInitiator -> endI in mermaid-to-proverif Step 6 template
  (endInitiator was never declared as an event)
- Add missing msg2_label constant to Step 3 constants block
- Add .hh/.hxx C++ header extensions to language detection in
  trailmark-summary and trailmark-structural

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Fix mermaid-to-proverif template: missing beginI event and secrecy witness

Step 6 Initiator template:
- Add missing event beginI(pk(sk_I), pk_R) before first out —
  without it, authentication queries always report false attacks
- Replace local new secret_I with free private_I [private] to
  match sample-output.pv's secrecy witness pattern

security-properties.md:
- Fix beginI/beginR from 3 args to 2 args in mutual auth section
  and query checklist (begin events fire before session key is
  known, so they only take the two public keys)
- Update "Placing Events" table to match 2-param form

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Address sixth round of PR #133 review feedback

proverif-syntax.md Two-Party Process example:
- Fix type errors: pkey values passed directly to bitstring params
  in sign() and verify(). Now uses concat2(pkey2bs(...)) pattern.
- Add missing pkey2bs declaration to function list
- Add missing info_session constant declaration
- Fix msg2_label -> msg2 in verification check example to match
  the file's own constant declarations

trailmark-structural:
- Fix contradiction: Rationalizations table said "Install trailmark
  first" but Execution section forbids install commands. Changed
  to "Report not installed and return" to match execution policy.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This commit is contained in:
Scott Arciszewski
2026-03-31 17:31:30 -04:00
committed by GitHub
parent 4b9a4e9087
commit 6b79b5e879
55 changed files with 10573 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.claude-plugin/marketplace.json
+10
View File
@@ -212,6 +212,16 @@
},
"source": "./plugins/testing-handbook-skills"
},
{
"name": "trailmark",
"version": "0.8.0",
"description": "Builds multi-language source code graphs for security analysis: call graphs, attack surface mapping, blast radius, taint propagation, complexity hotspots, and entry point enumeration. Generates Mermaid diagrams (call graphs, class hierarchies, dependency maps, heatmaps). Compares code graph snapshots for structural diff and evolution analysis. Runs graph-informed mutation testing triage (genotoxic). Generates mutation-driven test vectors (vector-forge). Extracts crypto protocol message flows and converts Mermaid diagrams to ProVerif models. Projects SARIF and weAudit findings onto code graphs. Use when analyzing call paths, mapping attack surface, visualizing code architecture, triaging survived mutants, generating cryptographic test vectors, diagramming crypto protocols, formally verifying protocols, or augmenting audits with static analysis findings.",
"author": {
"name": "Scott Arciszewski",
"url": "https://github.com/tob-scott-a"
},
"source": "./plugins/trailmark"
},
{
"name": "variant-analysis",
"version": "1.0.0",
.codex/skills/audit-augmentation
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/audit-augmentation
.codex/skills/crypto-protocol-diagram
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/crypto-protocol-diagram
.codex/skills/diagramming-code
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/diagramming-code
.codex/skills/genotoxic
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/genotoxic
.codex/skills/graph-evolution
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/graph-evolution
.codex/skills/mermaid-to-proverif
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/mermaid-to-proverif
.codex/skills/trailmark
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/trailmark
.codex/skills/trailmark-structural
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/trailmark-structural
.codex/skills/trailmark-summary
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/trailmark-summary
.codex/skills/vector-forge
Symlink
+1
View File
@@ -0,0 +1 @@
../../plugins/trailmark/skills/vector-forge
CODEOWNERS
+1
View File
@@ -34,6 +34,7 @@
/plugins/static-analysis/ @axelm-tob @dguido
/plugins/supply-chain-risk-auditor/ @smichaels-tob @dguido
/plugins/testing-handbook-skills/ @GrosQuildu @dguido
/plugins/trailmark/ @tob-scott-a @pbottine @tob-joe @dguido
/plugins/variant-analysis/ @axelm-tob @dguido
/plugins/workflow-skill-design/ @bsamuels453 @dguido
/plugins/yara-authoring/ @dguido
README.md
+1
View File
@@ -66,6 +66,7 @@ cd /path/to/parent # e.g., if repo is at ~/projects/skills, be in ~/projects
| [static-analysis](plugins/static-analysis/) | Static analysis toolkit with CodeQL, Semgrep, and SARIF parsing |
| [supply-chain-risk-auditor](plugins/supply-chain-risk-auditor/) | Audit supply-chain threat landscape of project dependencies |
| [testing-handbook-skills](plugins/testing-handbook-skills/) | Skills from the [Testing Handbook](https://appsec.guide): fuzzers, static analysis, sanitizers, coverage |
| [trailmark](plugins/trailmark/) | Code graph analysis, Mermaid diagrams, mutation testing triage, and protocol verification |
| [variant-analysis](plugins/variant-analysis/) | Find similar vulnerabilities across codebases using pattern-based analysis |
### Malware Analysis
plugins/trailmark/.claude-plugin/plugin.json
+9
View File
@@ -0,0 +1,9 @@
{
"name": "trailmark",
"version": "0.8.0",
"description": "Builds multi-language source code graphs for security analysis: call graphs, attack surface mapping, blast radius, taint propagation, complexity hotspots, and entry point enumeration. Generates Mermaid diagrams (call graphs, class hierarchies, dependency maps, heatmaps). Compares code graph snapshots for structural diff and evolution analysis. Runs graph-informed mutation testing triage (genotoxic). Generates mutation-driven test vectors (vector-forge). Extracts crypto protocol message flows and converts Mermaid diagrams to ProVerif models. Projects SARIF and weAudit findings onto code graphs. Use when analyzing call paths, mapping attack surface, visualizing code architecture, triaging survived mutants, generating cryptographic test vectors, diagramming crypto protocols, formally verifying protocols, or augmenting audits with static analysis findings.",
"author": {
"name": "Scott Arciszewski",
"url": "https://github.com/tob-scott-a"
}
}
plugins/trailmark/README.md
+59
View File
@@ -0,0 +1,59 @@
# trailmark
**Source code graph analysis for security auditing.** Parses code into queryable graphs of functions, classes, and calls, then uses that structure for diagram generation, mutation testing triage, protocol verification, and differential review.
## Prerequisites
[Trailmark](https://pypi.org/project/trailmark/) ([source](https://github.com/trailofbits/trailmark)) must be installed:
```bash
uv pip install trailmark
```
## Skills
| Skill | Description |
|-------|-------------|
| `trailmark` | Build and query multi-language code graphs with pre-analysis passes (blast radius, taint, privilege boundaries, entrypoints) |
| `diagramming-code` | Generate Mermaid diagrams from code graphs (call graphs, class hierarchies, complexity heatmaps, data flow) |
| `crypto-protocol-diagram` | Extract protocol message flow from source code or specs (RFC, ProVerif, Tamarin) into sequence diagrams |
| `genotoxic` | Triage mutation testing results using graph analysis — classify survived mutants as false positives, missing tests, or fuzzing targets |
| `vector-forge` | Mutation-driven test vector generation — find coverage gaps via mutation testing, then generate Wycheproof-style vectors that close them |
| `graph-evolution` | Compare code graphs at two snapshots to surface security-relevant structural changes text diffs miss |
| `mermaid-to-proverif` | Convert Mermaid sequence diagrams into ProVerif formal verification models |
| `audit-augmentation` | Project SARIF and weAudit findings onto code graphs as annotations and subgraphs |
| `trailmark-summary` | Quick structural overview (language detection, entry points, dependencies) for vivisect/galvanize |
| `trailmark-structural` | Full structural analysis with all pre-analysis passes (blast radius, taint, privilege boundaries, complexity) |
## Directory Structure
```text
trailmark/
├── .claude-plugin/
│ └── plugin.json
├── README.md
└── skills/
├── trailmark/ # Core graph querying
├── diagramming-code/ # Mermaid diagram generation
│ └── scripts/diagram.py
├── crypto-protocol-diagram/ # Protocol flow extraction
│ └── examples/
├── genotoxic/ # Mutation testing triage
├── vector-forge/ # Mutation-driven test vector generation
│ └── references/
├── graph-evolution/ # Structural diff
│ └── scripts/graph_diff.py
├── mermaid-to-proverif/ # Sequence diagram → ProVerif
│ └── examples/
├── audit-augmentation/ # SARIF/weAudit integration
├── trailmark-summary/ # Quick overview for vivisect/galvanize
└── trailmark-structural/ # Full structural analysis
```
## Related Skills
| Skill | Use For |
|-------|---------|
| `mutation-testing` | Guidance for running mutation frameworks (mewt, muton) — use before genotoxic for triage |
| `differential-review` | Text-level security diff review — complements graph-evolution's structural analysis |
| `audit-context-building` | Deep architectural context before vulnerability hunting |
plugins/trailmark/skills/audit-augmentation/SKILL.md
+171
View File
@@ -0,0 +1,171 @@
---
name: audit-augmentation
description: >
Augments Trailmark code graphs with external audit findings from SARIF static
analysis results and weAudit annotation files. Maps findings to graph nodes by
file and line overlap, creates severity-based subgraphs, and enables
cross-referencing findings with pre-analysis data (blast radius, taint, etc.).
Use when projecting SARIF results onto a code graph, overlaying weAudit
annotations, cross-referencing Semgrep or CodeQL findings with call graph
data, or visualizing audit findings in the context of code structure.
---
# Audit Augmentation
Projects findings from external tools (SARIF) and human auditors (weAudit)
onto Trailmark code graphs as annotations and subgraphs.
## When to Use
- Importing Semgrep, CodeQL, or other SARIF-producing tool results into a graph
- Importing weAudit audit annotations into a graph
- Cross-referencing static analysis findings with blast radius or taint data
- Querying which functions have high-severity findings
- Visualizing audit coverage alongside code structure
## When NOT to Use
- Running static analysis tools (use semgrep/codeql directly, then import)
- Building the code graph itself (use the `trailmark` skill)
- Generating diagrams (use the `diagramming-code` skill after augmenting)
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "The user only asked about SARIF, skip pre-analysis" | Without pre-analysis, you can't cross-reference findings with blast radius or taint | Always run `engine.preanalysis()` before augmenting |
| "Unmatched findings don't matter" | Unmatched findings may indicate parsing gaps or out-of-scope files | Report unmatched count and investigate if high |
| "One severity subgraph is enough" | Different severities need different triage workflows | Query all severity subgraphs, not just `error` |
| "SARIF results speak for themselves" | Findings without graph context lack blast radius and taint reachability | Cross-reference with pre-analysis subgraphs |
| "weAudit and SARIF overlap, pick one" | Human auditors and tools find different things | Import both when available |
| "Tool isn't installed, I'll do it manually" | Manual analysis misses what tooling catches | Install trailmark first |
---
## Installation
**MANDATORY:** If `uv run trailmark` fails, install trailmark first:
```bash
uv pip install trailmark
```
## Quick Start
### CLI
```bash
# Augment with SARIF
uv run trailmark augment {targetDir} --sarif results.sarif
# Augment with weAudit
uv run trailmark augment {targetDir} --weaudit .vscode/alice.weaudit
# Both at once, output JSON
uv run trailmark augment {targetDir} \
--sarif results.sarif \
--weaudit .vscode/alice.weaudit \
--json
```
### Programmatic API
```python
from trailmark.query.api import QueryEngine
engine = QueryEngine.from_directory("{targetDir}", language="python")
# Run pre-analysis first for cross-referencing
engine.preanalysis()
# Augment with SARIF
result = engine.augment_sarif("results.sarif")
# result: {matched_findings: 12, unmatched_findings: 3, subgraphs_created: [...]}
# Augment with weAudit
result = engine.augment_weaudit(".vscode/alice.weaudit")
# Query findings
engine.findings() # All findings
engine.subgraph("sarif:error") # High-severity SARIF
engine.subgraph("weaudit:high") # High-severity weAudit
engine.subgraph("sarif:semgrep") # By tool name
engine.annotations_of("function_name") # Per-node lookup
```
## Workflow
```
Augmentation Progress:
- [ ] Step 1: Build graph and run pre-analysis
- [ ] Step 2: Locate SARIF/weAudit files
- [ ] Step 3: Run augmentation
- [ ] Step 4: Inspect results and subgraphs
- [ ] Step 5: Cross-reference with pre-analysis
```
**Step 1:** Build the graph and run pre-analysis for blast radius and taint
context:
```python
engine = QueryEngine.from_directory("{targetDir}", language="{lang}")
engine.preanalysis()
```
**Step 2:** Locate input files:
- **SARIF**: Usually output by tools like `semgrep --sarif -o results.sarif`
or `codeql database analyze --format=sarif-latest`
- **weAudit**: Stored in `.vscode/<username>.weaudit` within the workspace
**Step 3:** Run augmentation via `engine.augment_sarif()` or
`engine.augment_weaudit()`. Check `unmatched_findings` in the result — these
are findings whose file/line locations didn't overlap any parsed code unit.
**Step 4:** Query findings and subgraphs. Use `engine.findings()` to list all
annotated nodes. Use `engine.subgraph_names()` to see available subgraphs.
**Step 5:** Cross-reference with pre-analysis data to prioritize:
- Findings on tainted nodes: overlap `sarif:error` with `tainted` subgraph
- Findings on high blast radius nodes: overlap with `high_blast_radius`
- Findings on privilege boundaries: overlap with `privilege_boundary`
## Annotation Format
Findings are stored as standard Trailmark annotations:
- **Kind**: `finding` (tool-generated) or `audit_note` (human notes)
- **Source**: `sarif:<tool_name>` or `weaudit:<author>`
- **Description**: Compact single-line:
`[SEVERITY] rule-id: message (tool)`
## Subgraphs Created
| Subgraph | Contents |
|----------|----------|
| `sarif:error` | Nodes with SARIF error-level findings |
| `sarif:warning` | Nodes with SARIF warning-level findings |
| `sarif:note` | Nodes with SARIF note-level findings |
| `sarif:<tool>` | Nodes flagged by a specific tool |
| `weaudit:high` | Nodes with high-severity weAudit findings |
| `weaudit:medium` | Nodes with medium-severity weAudit findings |
| `weaudit:low` | Nodes with low-severity weAudit findings |
| `weaudit:findings` | All weAudit findings (entryType=0) |
| `weaudit:notes` | All weAudit notes (entryType=1) |
## How Matching Works
Findings are matched to graph nodes by file path and line range overlap:
1. Finding file path is normalized relative to the graph's `root_path`
2. Nodes whose `location.file_path` matches AND whose line range overlaps are
selected
3. The tightest match (smallest span) is preferred
4. If a finding's location doesn't overlap any node, it counts as unmatched
SARIF paths may be relative, absolute, or `file://` URIs — all are handled.
weAudit uses 0-indexed lines which are converted to 1-indexed automatically.
## Supporting Documentation
- **[references/formats.md](references/formats.md)** — SARIF 2.1.0 and
weAudit file format field reference
plugins/trailmark/skills/audit-augmentation/references/formats.md
+121
View File
@@ -0,0 +1,121 @@
# SARIF and weAudit Format Reference
## SARIF 2.1.0
SARIF (Static Analysis Results Interchange Format) is an OASIS standard for
encoding static analysis results as JSON.
### Structure Used by Trailmark
```
sarifLog
├── version: "2.1.0"
└── runs[]
├── tool.driver.name → source field ("sarif:<name>")
└── results[]
├── ruleId → included in description
├── message.text → included in description
├── level → "error" | "warning" | "note"
└── locations[]
└── physicalLocation
├── artifactLocation.uri → matched to node file
└── region
├── startLine → matched to node lines
└── endLine → matched to node lines
```
### Level Values
| Level | Subgraph |
|-------|----------|
| `error` | `sarif:error` |
| `warning` (default) | `sarif:warning` |
| `note` | `sarif:note` |
### Example SARIF Result
```json
{
"ruleId": "python.lang.security.audit.exec-detected",
"level": "warning",
"message": {"text": "Detected use of exec()"},
"locations": [{
"physicalLocation": {
"artifactLocation": {"uri": "src/handler.py"},
"region": {"startLine": 42, "endLine": 42}
}
}]
}
```
## weAudit
weAudit is a VSCode extension by Trail of Bits for collaborative security
auditing. Files are stored as `.vscode/<username>.weaudit`.
### Structure Used by Trailmark
```
root
├── clientRemote → fallback author extraction
├── treeEntries[] → active findings/notes
│ ├── label → included in description
│ ├── entryType → 0=Finding, 1=Note
│ ├── author → source field ("weaudit:<author>")
│ ├── details
│ │ ├── severity → "High" | "Medium" | "Low" | "Informational"
│ │ ├── type → finding category
│ │ └── description → included in annotation
│ └── locations[]
│ ├── path → relative to git root
│ ├── startLine → 0-indexed (converted to 1-indexed)
│ └── endLine → 0-indexed (converted to 1-indexed)
└── resolvedEntries[] → same structure as treeEntries
```
### Entry Types
| entryType | AnnotationKind | Subgraph |
|-----------|---------------|----------|
| 0 (Finding) | `finding` | `weaudit:findings` |
| 1 (Note) | `audit_note` | `weaudit:notes` |
### Severity Values
| Severity | Subgraph |
|----------|----------|
| `High` | `weaudit:high` |
| `Medium` | `weaudit:medium` |
| `Low` | `weaudit:low` |
| `Informational` | `weaudit:informational` |
### Example weAudit Entry
```json
{
"label": "SQL Injection in user input",
"entryType": 0,
"author": "alice",
"details": {
"severity": "High",
"difficulty": "Low",
"type": "Data Validation",
"description": "User input not sanitized before SQL query.",
"exploit": "Attacker injects malicious SQL.",
"recommendation": "Use parameterized queries."
},
"locations": [{
"path": "src/database/queries.py",
"startLine": 41,
"endLine": 44,
"label": "executeQuery function",
"description": ""
}]
}
```
### Line Indexing
weAudit uses **0-indexed** line numbers. Trailmark uses **1-indexed** (from
tree-sitter). The augmentation module adds 1 to both `startLine` and `endLine`
during conversion.
plugins/trailmark/skills/crypto-protocol-diagram/SKILL.md
+440
View File
@@ -0,0 +1,440 @@
---
name: crypto-protocol-diagram
description: "Extracts protocol message flow from source code, RFCs, academic papers, pseudocode, informal prose, ProVerif (.pv), or Tamarin (.spthy) models and generates Mermaid sequenceDiagrams with cryptographic annotations. Use when diagramming a crypto protocol, visualizing a handshake or key exchange flow, extracting message flow from a spec or RFC, diagramming a ProVerif or Tamarin model, or drawing sequence diagrams for TLS, Noise, Signal, X3DH, Double Ratchet, FROST, DH, or ECDH protocols."
---
# Crypto Protocol Diagram
Produces a Mermaid `sequenceDiagram` (written to file) and an ASCII sequence
diagram (printed inline) from either:
- **Source code** implementing a cryptographic protocol, or
- **A specification** — RFC, academic paper, pseudocode, informal prose,
ProVerif (`.pv`), or Tamarin (`.spthy`) model.
**Tools used:** Read, Write, Grep, Glob, Bash, WebFetch (for URL specs).
Unlike the `diagramming-code` skill (which visualizes code structure), this skill
extracts **protocol semantics**: who sends what to whom, what cryptographic
transformations occur at each step, and what protocol phases exist.
For call graphs, class hierarchies, or module dependency maps, use the
`diagramming-code` skill instead.
## When to Use
- User asks to diagram, visualize, or extract a cryptographic protocol
- Input is source code implementing a handshake, key exchange, or multi-party protocol
- Input is an RFC, academic paper, pseudocode, or formal model (ProVerif/Tamarin)
- User names a specific protocol (TLS, Noise, Signal, X3DH, FROST)
## When NOT to Use
- User wants a call graph, class hierarchy, or module dependency map — use `diagramming-code`
- User wants to formally verify a protocol — use `mermaid-to-proverif` (after generating the diagram)
- Input has no cryptographic protocol semantics (no parties, no message exchange)
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "The protocol is simple, I can diagram from memory" | Memory-based diagrams miss steps and invert arrows | Read the source or spec systematically |
| "I'll skip the spec path since code exists" | Code may diverge from the spec — both paths catch different bugs | When both exist, run spec workflow first, then annotate code divergences |
| "Crypto annotations are optional decoration" | Without crypto annotations, the diagram is just a message flow — useless for security review | Annotate every cryptographic operation |
| "The abort path is obvious, no need for alt blocks" | Implicit abort handling hides missing error checks | Show every abort/error path with `alt` blocks |
| "I don't need to check the examples first" | The examples define the expected output quality bar | Study the relevant example before working on unfamiliar input |
| "ProVerif/Tamarin models are code, not specs" | Formal models are specifications — they describe intended behavior, not implementation | Use the spec workflow (S1–S5) for `.pv` and `.spthy` files |
---
## Workflow
```
Protocol Diagram Progress:
- [ ] Step 0: Determine input type (code / spec / both)
- [ ] Step 1 (code) or S1–S5 (spec): Extract protocol structure
- [ ] Step 6: Generate sequenceDiagram
- [ ] Step 7: Verify and deliver
```
---
### Step 0: Determine Input Type
Before doing anything else, classify the input:
| Signal | Input type |
|--------|-----------|
| Source file extensions (`.py`, `.rs`, `.go`, `.ts`, `.js`, `.cpp`, `.c`) | **Code** |
| Function/class definitions, import statements | **Code** |
| RFC-style section headers (`§`, `Section X.Y`, `MUST`/`SHALL` keywords) | **Spec** |
| `Algorithm`/`Protocol`/`Figure` labels, mathematical notation | **Spec** |
| ProVerif file (`.pv`) with `process`, `let`, `in`/`out` | **Spec** |
| Tamarin file (`.spthy`) with `rule`, `--[...]->` | **Spec** |
| Plain prose or numbered steps describing a protocol | **Spec** |
| Both source files and a spec document | **Both** (annotate divergences with `⚠️`) |
- **Code only** → skip to Step 1 below
- **Spec only** → skip to Spec Workflow (S1–S5) below
- **Both** → run Spec Workflow first, then use the code-reading steps to verify
the implementation against the spec diagram and annotate any divergences with `⚠️`
- **Ambiguous** → ask the user: "Is this a source code file, a specification
document, or both?"
---
### Step 1: Locate Protocol Entry Points
Grep for function names, type names, and comments that reveal the protocol:
```bash
# Find handshake, session, round, phase entry points
rg -l "handshake|session_init|round[_0-9]|setup|keygen|send_msg|recv_msg" {targetDir}
# Find crypto primitives in use
rg "sign|verify|encrypt|decrypt|dh|ecdh|kdf|hkdf|hmac|hash|commit|reveal|share" \
{targetDir} --type-add 'src:*.{py,rs,go,ts,js,cpp,c}' -t src -l
```
Start reading from the highest-level orchestration function — the one that calls
into handshake phases or the main protocol loop.
### Step 2: Identify Parties and Roles
Extract participant names from:
- Struct/class names: `Client`, `Server`, `Initiator`, `Responder`, `Prover`,
`Verifier`, `Dealer`, `Party`, `Coordinator`
- Function parameter names that carry state for a role
- Comments declaring the protocol role
- Test fixtures that set up two-party or N-party scenarios
Map these to Mermaid `participant` declarations. Use short, readable aliases:
```
participant I as Initiator
participant R as Responder
```
### Step 3: Trace Message Flow
Follow state transitions and network sends/receives. Look for patterns like:
| Pattern | Meaning |
|---------|---------|
| `send(msg)` / `recv()` | Direct message exchange |
| `serialize` + `transmit` | Structured message sent |
| Return value passed to other party's function | Logical message (in-process) |
| `round1_output` → `round2_input` | Round-based MPC step |
| Struct fields named `ephemeral_key`, `ciphertext`, `mac`, `tag` | Message contents |
For **in-process** protocol implementations (where both parties run in the same
process), treat function call boundaries as logical message sends when they
represent what would be a network boundary in deployment.
### Step 4: Annotate Cryptographic Operations
At each protocol step, identify and label:
| Operation | Diagram annotation |
|-----------|-------------------|
| Key generation | `Note over A: keygen(params) → pk, sk` |
| DH / ECDH | `Note over A,B: DH(sk_A, pk_B)` |
| KDF / HKDF | `Note over A: HKDF(ikm, salt, info)` |
| Signing | `Note over A: Sign(sk, msg) → σ` |
| Verification | `Note over B: Verify(pk, msg, σ)` |
| Encryption | `Note over A: Enc(key, plaintext) → ct` |
| Decryption | `Note over B: Dec(key, ct) → plaintext` |
| Commitment | `Note over A: Commit(value, rand) → C` |
| Hash | `Note over A: H(data) → digest` |
| Secret sharing | `Note over D: Share(secret, t, n) → {s_i}` |
| Threshold combine | `Note over C: Combine({s_i}) → secret` |
Keep annotations concise — use mathematical shorthand, not code.
### Step 5: Identify Protocol Phases
Group message steps into named phases using `rect` or `Note` blocks:
Common phases to detect:
- **Setup / Key Generation**: party key creation, trusted setup, parameter gen
- **Handshake / Init**: ephemeral key exchange, nonce exchange, version negotiation
- **Authentication**: identity proof, certificate exchange, signature verification
- **Key Derivation**: session key derivation from shared secrets
- **Data Transfer / Main Protocol**: encrypted application data exchange
- **Finalization / Teardown**: session close, MAC verification, abort handling
Detect abort/error paths and show them with `alt` blocks.
---
## Spec Workflow (S1–S5)
Use this path when the input is a specification document rather than source code.
After completing S1–S5, continue with Step 6 (Generate sequenceDiagram) and
Step 7 (Verify and deliver) from the code workflow above.
### Step S1: Ingest the Spec
Obtain the full spec text:
- **File path provided** → read with the Read tool
- **URL provided** → fetch with WebFetch
- **Pasted inline** → work directly from conversation context
Then identify the spec format and read
[references/spec-parsing-patterns.md](references/spec-parsing-patterns.md)
for format-specific extraction guidance:
| Format | Signals |
|--------|---------|
| RFC | `RFC XXXX`, `MUST`/`SHALL`/`SHOULD`, ABNF grammars, section-numbered prose |
| Academic paper / pseudocode | `Algorithm X`, `Protocol X`, `Figure X`, numbered steps, `←`/`→` in math mode |
| Informal prose | Numbered lists, "A sends B ...", plain English descriptions |
| ProVerif (`.pv`) | `process`, `let`, `in(ch, x)`, `out(ch, msg)`, `!` (replication) |
| Tamarin (`.spthy`) | `rule`, `--[ ]->`, `Fr(~x)`, `!Pk(A, pk)`, `In(m)`, `Out(m)` |
If the spec references a known named protocol (TLS, Noise, Signal, X3DH, Double
Ratchet, FROST), also read
[references/protocol-patterns.md](references/protocol-patterns.md) to use its
canonical flow as a skeleton and fill in spec-specific details.
### Step S2: Extract Parties and Roles
Identify all protocol participants. Look for:
- **Named roles** in prose or pseudocode: `Alice`, `Bob`, `Client`, `Server`,
`Initiator`, `Responder`, `Prover`, `Verifier`, `Dealer`, `Party_i`,
`Coordinator`, `Signer`
- **Section headers**: "Parties", "Roles", "Participants", "Setup", "Notation"
- **ProVerif**: process names at top level (`let ClientProc(...)`, `let ServerProc(...)`)
- **Tamarin**: rule names and fact arguments (e.g. `!Pk($A, pk)` — `$A` is a party)
Map each role to a Mermaid `participant` declaration. Use short IDs with
descriptive aliases (see naming conventions in
[references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md)).
### Step S3: Extract Message Flow
Trace what each party sends to whom and in what order. Extraction patterns by format:
**RFC / informal prose:**
- Arrow notation: `A → B: msg`, `A -> B`
- Sentence patterns: "A sends B ...", "B responds with ...", "A transmits ...",
"upon receiving X, B sends Y"
- Numbered steps: extract in order, inferring sender/receiver from context
**Pseudocode:**
- Function signatures with explicit `sender`/`receiver` parameters
- `send(party, msg)` / `receive(party)` calls
- Return values passed as inputs to the other party's function in the next step
**ProVerif (`.pv`):**
- `out(ch, msg)` — send on channel `ch`
- `in(ch, x)` — receive on channel `ch`, bind to `x`
- Match `out`/`in` pairs on the same channel to identify message flows
- `!` (replication) signals a role that handles multiple sessions
**Tamarin (`.spthy`):**
- `In(m)` premise — receive message `m`
- `Out(m)` conclusion — send message `m`
- Rule name and ordering of rules reveal protocol rounds
- `Fr(~x)` — fresh random value generated by a party
- `--[ Label ]->` facts — security annotations, not messages
Preserve the ordering and round structure. Group concurrent sends (broadcast)
using `par` blocks in the final diagram.
### Step S4: Extract Cryptographic Operations
For each protocol step, identify the cryptographic operations performed and which
party performs them:
| Spec notation | Operation | Diagram annotation |
|---------------|-----------|-------------------|
| `keygen()`, `Gen(1^λ)` | Key generation | `Note over A: keygen() → pk, sk` |
| `DH(a, B)`, `g^ab` | DH / ECDH | `Note over A,B: DH(sk_A, pk_B)` |
| `KDF(ikm)`, `HKDF(...)` | Key derivation | `Note over A: HKDF(ikm, salt, info) → k` |
| `Sign(sk, m)`, `σ ← Sign` | Signing | `Note over A: Sign(sk, msg) → σ` |
| `Verify(pk, m, σ)` | Verification | `Note over B: Verify(pk, msg, σ)` |
| `Enc(k, m)`, `{m}_k` | Encryption | `Note over A: Enc(k, plaintext) → ct` |
| `Dec(k, c)` | Decryption | `Note over B: Dec(k, ct) → plaintext` |
| `H(m)`, `hash(m)` | Hash | `Note over A: H(data) → digest` |
| `Commit(v, r)`, `com` | Commitment | `Note over A: Commit(value, rand) → C` |
| ProVerif `senc(m, k)` | Symmetric encryption | `Note over A: Enc(k, m) → ct` |
| ProVerif `pk(sk)` | Public key derivation | `Note over A: pk = pk(sk)` |
| ProVerif `sign(m, sk)` | Signing | `Note over A: Sign(sk, m) → σ` |
Identify security conditions and abort paths:
- Prose: "if verification fails, abort", "only if ...", "reject if ..."
- Pseudocode: `assert`, `require`, `if ... abort`
- ProVerif: `if m = expected then ... else 0`
- Tamarin: contradicting facts or restriction lemmas
These become `alt` blocks in the final diagram.
### Step S5: Flag Spec Ambiguities
Before moving to Step 6, check for gaps:
- **Unclear message ordering**: infer from round structure or section order;
annotate with `⚠️ ordering inferred from spec structure`
- **Implied parties**: if a party's role is implied but unnamed, give it a
descriptive name and note the inference
- **Missing steps**: if the spec omits a step that the canonical pattern for
this protocol requires, annotate:
`⚠️ spec omits [step] — canonical protocol requires it`
- **Underspecified crypto**: if the spec says "encrypt" without specifying
the scheme, annotate: `⚠️ encryption scheme not specified`
- **ProVerif/Tamarin**: private channels (`c` declared with `new c` or as a
private free name) represent out-of-band channels — note them
---
<!-- Both code path (Steps 1–5) and spec path (Steps S1–S5) continue here -->
### Step 6: Generate sequenceDiagram
Produce Mermaid syntax following the rules in
[references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md).
**Completeness over brevity.** Show every distinct message type. Omit repeated
loop iterations (use `loop` blocks instead), but never omit a distinct protocol
step.
**Correctness over aesthetics.** The diagram must match what the code actually
does. If the code diverges from a known spec, annotate the divergence:
```
Note over A,B: ⚠️ spec requires MAC here — implementation omits it
```
### Step 7: Verify and Deliver
Before delivering:
- [ ] Every participant declared actually sends or receives at least one message
- [ ] Arrows point in the correct direction (sender → receiver)
- [ ] Cryptographic operations are on the correct party (the one computing them)
- [ ] If protocol phases are used, no arrows appear outside a phase block
- [ ] `alt` blocks cover known abort/error paths
- [ ] Diagram renders without syntax errors (check
[references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md)
for common pitfalls)
- [ ] If spec divergence found, annotated with `⚠️`
**Write the diagram to a file.** Choose a filename derived from the protocol
name, e.g. `noise-xx-handshake.md` or `x3dh-key-agreement.md`. Write a
Markdown file with this structure:
```markdown
# <Protocol Name> Sequence Diagram
\`\`\`mermaid
sequenceDiagram
...
\`\`\`
## Protocol Summary
- **Parties:** ...
- **Round complexity:** ...
- **Key primitives:** ...
- **Authentication:** ...
- **Forward secrecy:** ...
- **Notable:** [spec deviations or security observations, or "none"]
```
After writing the file, print an **ASCII sequence diagram** inline in the
response, followed by the Protocol Summary. State the output filename so the
user knows where to find the Mermaid source.
Follow all drawing conventions in
[references/ascii-sequence-diagram.md](references/ascii-sequence-diagram.md),
including the inline output format.
---
## Decision Tree
```
── Input is a spec document (not code)?
│ └─ Step S1: identify format, read references/spec-parsing-patterns.md
│
── Input is source code (not a spec)?
│ └─ Step 1: grep for handshake/round/send/recv entry points
│
── Both spec and code provided?
│ └─ Run Spec Workflow (S1–S5) first to build canonical diagram,
│ then read code and annotate divergences with ⚠️
│
── Spec is a known protocol (TLS, Noise, Signal, X3DH, FROST)?
│ └─ Read references/protocol-patterns.md and use canonical flow as skeleton
│
── Spec is ProVerif (.pv) or Tamarin (.spthy)?
│ └─ Read references/spec-parsing-patterns.md → Formal Models section
│
── Spec message ordering is ambiguous?
│ └─ Infer from round/section structure, annotate with ⚠️
│
── Can't identify parties from spec?
│ └─ Check "Parties"/"Notation" sections; for ProVerif read process names;
│ for Tamarin read rule names and fact arguments
│
── Don't know which code files implement the protocol?
│ └─ Step 1: grep for handshake/round/send/recv entry points
│
── Can't identify parties from struct names?
│ └─ Read test files — test setup reveals roles
│
── Protocol runs in-process (no network calls)?
│ └─ Treat function argument passing at role boundaries as messages
│
── MPC / threshold protocol with N parties?
│ └─ Read references/protocol-patterns.md → MPC section
│
── Mermaid syntax error?
│ └─ Read references/mermaid-sequence-syntax.md → Common Pitfalls
│
└─ ASCII drawing conventions?
└─ Read references/ascii-sequence-diagram.md
```
---
## Examples
**Code path** — `examples/simple-handshake/`:
- **`protocol.py`** — two-party authenticated key exchange (X25519 DH +
Ed25519 signing + HKDF + ChaCha20-Poly1305)
- **`expected-output.md`** — exact ASCII diagram and Mermaid file the skill
should produce for that protocol
**Spec path (ProVerif)** — `examples/simple-proverif/`:
- **`model.pv`** — HMAC challenge-response authentication modeled in ProVerif
- **`expected-output.md`** — step-by-step extraction walkthrough (parties,
message flow, crypto ops) and the exact ASCII diagram and Mermaid file the
skill should produce
Study the relevant example before working on an unfamiliar input.
---
## Supporting Documentation
- **[references/spec-parsing-patterns.md](references/spec-parsing-patterns.md)** —
Extraction rules for RFC, academic paper/pseudocode, informal prose, ProVerif,
and Tamarin input formats; read during Step S1
- **[references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md)** —
Participant syntax, arrow types, activations, grouping blocks, escaping rules,
and common rendering pitfalls
- **[references/protocol-patterns.md](references/protocol-patterns.md)** —
Canonical message flows for TLS 1.3, Noise, X3DH, Double Ratchet, Shamir
secret sharing, commit-reveal, and generic MPC rounds; use as a reference
when comparing implementation against spec
- **[references/ascii-sequence-diagram.md](references/ascii-sequence-diagram.md)** —
Column layout, arrow conventions, self-loops, phase labels, and inline
output format for the ASCII diagram
plugins/trailmark/skills/crypto-protocol-diagram/examples/simple-handshake/expected-output.md
+120
View File
@@ -0,0 +1,120 @@
# Expected Skill Output
This file shows what the `crypto-protocol-diagram` skill should produce when
run on `protocol.py`. It covers both the inline response (ASCII diagram +
Protocol Summary) and the written Mermaid file.
---
## Inline Response
```
Protocol: Simple Authenticated Key Exchange
Output: simple-authenticated-key-exchange.md
Initiator Responder
| |
| -- Setup (out-of-band) -- |
+--. |
| | keygen() → sk_i, pk_i |
|<-' |
| +--.
| keygen() → sk_r, pk_r |
| |<-'
| |
| -- Handshake -- |
+--. |
| | keygen() → ek_i, epk_i |
| | sig_i = Sign(sk_i, "msg1"||epk_i) |
|<-' |
| |
+---------------------------------->| epk_i || sig_i
| |
| +--.
| Verify(pk_i, sig_i) | |
| keygen() → ek_r, epk_r | |
| sig_r = Sign(sk_r, "msg2"||transcript) |
| dh = DH(ek_r, epk_i) | |
| sk = HKDF(dh, transcript) |<-'
| |
|<- - - - - - - - - - - - - - - - - + epk_r || sig_r
| |
+--. |
| | Verify(pk_r, sig_r) |
| | dh = DH(ek_i, epk_r) |
| | sk = HKDF(dh, transcript) |
|<-' |
| |
| -- Application Data -- |
| |
+---------------------------------->| ChaCha20Poly1305(sk, nonce, plaintext)
| |
[on signature verification failure]
| abort(INVALID_SIGNATURE) |
|<- - - - - - - - - - - - - - - - - +
## Protocol Summary
- **Parties:** Initiator, Responder
- **Round complexity:** 1 round trip (2 messages)
- **Key primitives:** X25519 (ephemeral DH), Ed25519 (signing), HKDF-SHA256, ChaCha20-Poly1305
- **Authentication:** mutual — both parties sign their ephemeral keys with long-term Ed25519 keys
- **Forward secrecy:** yes — session key derived from ephemeral DH; compromise of static keys does not expose past sessions
- **Notable:** static keys are assumed registered out-of-band (no in-protocol key transmission); transcript binding covers only ephemeral public keys, not party identities — an implementation that doesn't bind pk_i and pk_r into the transcript is vulnerable to identity mislabeling
```
---
## Written Mermaid File (`simple-authenticated-key-exchange.md`)
```markdown
# Simple Authenticated Key Exchange Sequence Diagram
\`\`\`mermaid
sequenceDiagram
participant I as Initiator
participant R as Responder
rect rgba(100, 149, 237, 0.15)
Note over I,R: Setup (out-of-band key registration)
Note over I: keygen() → sk_i, pk_i
Note over R: keygen() → sk_r, pk_r
end
rect rgba(46, 204, 113, 0.15)
Note over I,R: Handshake
Note over I: keygen() → ek_i, epk_i
Note over I: sig_i = Sign(sk_i, "msg1" || epk_i)
I->>R: epk_i || sig_i
Note over R: Verify(pk_i, "msg1" || epk_i, sig_i)
Note over R: keygen() → ek_r, epk_r
Note over R: transcript = epk_i || epk_r
Note over R: sig_r = Sign(sk_r, "msg2" || transcript)
Note over R: dh = DH(ek_r, epk_i)
Note over R: sk_r = HKDF(dh || transcript, info="session-key-v1")
R-->>I: epk_r || sig_r
Note over I: Verify(pk_r, "msg2" || transcript, sig_r)
Note over I: dh = DH(ek_i, epk_r)
Note over I: sk_i = HKDF(dh || transcript, info="session-key-v1")
end
rect rgba(241, 196, 15, 0.15)
Note over I,R: Application Data
I->>R: ChaCha20Poly1305(sk, nonce, plaintext)
end
alt signature verification failure
R-->>I: abort(INVALID_SIGNATURE)
end
\`\`\`
## Protocol Summary
- **Parties:** Initiator, Responder
- **Round complexity:** 1 round trip (2 messages)
- **Key primitives:** X25519 (ephemeral DH), Ed25519 (signing), HKDF-SHA256, ChaCha20-Poly1305
- **Authentication:** mutual — both parties sign their ephemeral keys with long-term Ed25519 keys
- **Forward secrecy:** yes — session key derived from ephemeral DH; compromise of static keys does not expose past sessions
- **Notable:** static keys are assumed registered out-of-band (no in-protocol key transmission); transcript binding covers only ephemeral public keys, not party identities — an implementation that doesn't bind pk_i and pk_r into the transcript is vulnerable to identity mislabeling
```
plugins/trailmark/skills/crypto-protocol-diagram/examples/simple-handshake/protocol.py
+196
View File
@@ -0,0 +1,196 @@
# /// script
# requires-python = ">=3.12"
# dependencies = ["cryptography>=42.0"]
# ///
"""
Simple authenticated key exchange protocol (2 messages, 1 round trip).
Both parties hold long-term Ed25519 signing keys registered out-of-band.
The protocol establishes a forward-secret session key via ephemeral X25519 DH,
with mutual authentication via signatures over the transcript.
Message flow:
1. Initiator → Responder : epk_i, sig_i
2. Responder → Initiator : epk_r, sig_r
Both derive: session_key = HKDF(DH(ek_i, epk_r), transcript)
"""
import os
from cryptography.hazmat.primitives import hashes, serialization # type: ignore
from cryptography.hazmat.primitives.asymmetric.ed25519 import ( # type: ignore
Ed25519PrivateKey,
Ed25519PublicKey,
)
from cryptography.hazmat.primitives.asymmetric.x25519 import ( # type: ignore
X25519PrivateKey,
X25519PublicKey,
)
from cryptography.hazmat.primitives.ciphers.aead import ChaCha20Poly1305 # type: ignore
from cryptography.hazmat.primitives.kdf.hkdf import HKDF # type: ignore
# ---------------------------------------------------------------------------
# Key types
# ---------------------------------------------------------------------------
class StaticKeypair:
"""Long-term Ed25519 signing keypair (registered out-of-band)."""
def __init__(self) -> None:
self._sk = Ed25519PrivateKey.generate()
self.pk = self._sk.public_key()
def sign(self, message: bytes) -> bytes:
return self._sk.sign(message)
def public_bytes(self) -> bytes:
return self.pk.public_bytes(serialization.Encoding.Raw, serialization.PublicFormat.Raw)
class EphemeralKeypair:
"""Single-use X25519 DH keypair."""
def __init__(self) -> None:
self._sk = X25519PrivateKey.generate()
self.pk = self._sk.public_key()
def exchange(self, peer_epk: X25519PublicKey) -> bytes:
return self._sk.exchange(peer_epk)
def public_bytes(self) -> bytes:
return self.pk.public_bytes(serialization.Encoding.Raw, serialization.PublicFormat.Raw)
# ---------------------------------------------------------------------------
# Protocol messages
# ---------------------------------------------------------------------------
def _derive_session_key(dh_output: bytes, transcript: bytes) -> bytes:
"""HKDF-SHA256 over DH output, bound to the full transcript."""
return HKDF(
algorithm=hashes.SHA256(),
length=32,
salt=None,
info=b"session-key-v1",
).derive(dh_output + transcript)
def initiator_send_msg1(
static: StaticKeypair,
) -> tuple[EphemeralKeypair, bytes]:
"""
Initiator builds message 1.
Returns (ephemeral_keypair, wire_bytes).
wire_bytes = epk_i (32 bytes) || sig_i (64 bytes)
"""
ek = EphemeralKeypair()
epk_bytes = ek.public_bytes()
sig = static.sign(b"msg1:" + epk_bytes)
return ek, epk_bytes + sig
def responder_recv_msg1_send_msg2(
msg1: bytes,
initiator_pk: Ed25519PublicKey,
static: StaticKeypair,
) -> tuple[bytes, bytes, bytes]:
"""
Responder processes message 1 and builds message 2.
Returns (session_key, msg2_wire_bytes, transcript).
msg2_wire_bytes = epk_r (32 bytes) || sig_r (64 bytes)
"""
epk_i_bytes, sig_i = msg1[:32], msg1[32:]
# Verify initiator's ephemeral key is authentic.
initiator_pk.verify(sig_i, b"msg1:" + epk_i_bytes)
epk_i = X25519PublicKey.from_public_bytes(epk_i_bytes)
ek_r = EphemeralKeypair()
epk_r_bytes = ek_r.public_bytes()
transcript = epk_i_bytes + epk_r_bytes
sig_r = static.sign(b"msg2:" + transcript)
dh_output = ek_r.exchange(epk_i)
session_key = _derive_session_key(dh_output, transcript)
return session_key, epk_r_bytes + sig_r, transcript
def initiator_recv_msg2(
msg2: bytes,
ek_i: EphemeralKeypair,
responder_pk: Ed25519PublicKey,
epk_i_bytes: bytes,
) -> bytes:
"""
Initiator processes message 2 and derives the session key.
Returns session_key.
"""
epk_r_bytes, sig_r = msg2[:32], msg2[32:]
transcript = epk_i_bytes + epk_r_bytes
# Verify responder's contribution is authentic.
responder_pk.verify(sig_r, b"msg2:" + transcript)
epk_r = X25519PublicKey.from_public_bytes(epk_r_bytes)
dh_output = ek_i.exchange(epk_r)
return _derive_session_key(dh_output, transcript)
# ---------------------------------------------------------------------------
# Application data (post-handshake)
# ---------------------------------------------------------------------------
def encrypt(session_key: bytes, plaintext: bytes, nonce: bytes) -> bytes:
return ChaCha20Poly1305(session_key).encrypt(nonce, plaintext, None)
def decrypt(session_key: bytes, ciphertext: bytes, nonce: bytes) -> bytes:
return ChaCha20Poly1305(session_key).decrypt(nonce, ciphertext, None)
# ---------------------------------------------------------------------------
# Demo
# ---------------------------------------------------------------------------
if __name__ == "__main__":
# Out-of-band key registration
initiator_static = StaticKeypair()
responder_static = StaticKeypair()
# --- Handshake ---
ek_i, msg1 = initiator_send_msg1(initiator_static)
epk_i_bytes = msg1[:32]
sk_r, msg2, _ = responder_recv_msg1_send_msg2(
msg1,
initiator_static.pk,
responder_static,
)
sk_i = initiator_recv_msg2(
msg2,
ek_i,
responder_static.pk,
epk_i_bytes,
)
if sk_i != sk_r:
raise RuntimeError("session keys must match")
print("Handshake complete. Session keys match.")
# --- Application data ---
nonce = os.urandom(12)
ct = encrypt(sk_i, b"hello, responder", nonce)
pt = decrypt(sk_r, ct, nonce)
print(f"Decrypted: {pt}")
plugins/trailmark/skills/crypto-protocol-diagram/examples/simple-proverif/expected-output.md
+131
View File
@@ -0,0 +1,131 @@
# Expected Output: simple-proverif
This is the exact ASCII diagram and Mermaid file the `crypto-protocol-diagram`
skill should produce when given `model.pv` as input.
---
## Step 0 classification
Input: `model.pv` — ProVerif file (`.pv` extension, contains `process`, `let`,
`in`/`out`). Input type: **Spec (ProVerif)**.
## Step S2: Parties extracted
- `AliceProc` → participant `A as Alice`
- `BobProc` → participant `B as Bob`
## Step S3: Message flow (channel `c`)
| # | `out` | `in` | Message |
|---|-------|------|---------|
| 1 | `AliceProc` | `BobProc` | `identity` |
| 2 | `BobProc` | `AliceProc` | `nonce` (fresh) |
| 3 | `AliceProc` | `BobProc` | `mac = HMAC(k, nonce \|\| identity)` |
| 4 | `BobProc` | — | `true` (auth success, conditional) |
## Step S4: Crypto operations
- `AliceProc`: `hmac(key, concat(nonce, identity))` → `Note over A: mac = HMAC(k, nonce \|\| id)`
- `BobProc`: `new nonce` → `Note over B: nonce ← fresh()`
- `BobProc`: `checkhmac(mac, key, ...)` → `alt` block (verify succeeds / fails)
## Step S5: Ambiguities
- Dolev-Yao model applies: annotate with `⚠️`
- Auth success sends `true` over `c` — in a real protocol this would be
implicit; annotate as optional output
---
## Inline ASCII Diagram
```
Protocol: HMAC Challenge-Response Authentication (ProVerif model)
Output: hmac-challenge-response.md
Alice Bob
| |
| -- Authentication | --
| |
+--------------------->| identity
| |
| +--.
| | | nonce ← fresh()
| |<-'
| |
| nonce |
|<- - - - - - - - - - -+
| |
+--. |
| | mac = HMAC(k, |
| | nonce || id) |
|<-' |
| |
+--------------------->| mac
| |
| +--.
| | | checkHMAC(mac, k,
| | | nonce || identity)
| |<-'
| |
| [on verify success] |
| +----.
| | | auth_ok
| |<---'
| |
| [on verify failure] |
| | (abort)
⚠️ ProVerif note: all messages transit adversary network (Dolev-Yao model)
```
## Protocol Summary
- **Parties:** Alice (initiator), Bob (responder/verifier)
- **Round complexity:** 1.5 RTT (3 messages)
- **Key primitives:** HMAC with shared symmetric key; fresh nonce
- **Authentication:** Unilateral (Alice authenticates to Bob only)
- **Forward secrecy:** No (static shared key `k`; compromise reveals all sessions)
- **Notable:** `query attacker(k)` verifies the shared key remains secret under
Dolev-Yao. No mutual authentication — Bob does not prove identity to Alice.
---
## Mermaid File: hmac-challenge-response.md
````markdown
# HMAC Challenge-Response Authentication Sequence Diagram
```mermaid
sequenceDiagram
participant A as Alice
participant B as Bob
Note over A,B: ⚠️ ProVerif Dolev-Yao model — all messages transit adversary network
rect rgba(241, 196, 15, 0.15)
Note over A,B: Authentication
A->>B: identity
Note over B: nonce ← fresh()
B-->>A: nonce
Note over A: mac = HMAC(k, nonce || identity)
A->>B: mac
Note over B: checkHMAC(mac, k, nonce || identity)
alt verification succeeds
Note over B: auth_ok
else verification fails
Note over B: abort
end
end
```
## Protocol Summary
- **Parties:** Alice (initiator), Bob (responder)
- **Round complexity:** 1.5 RTT (3 messages)
- **Key primitives:** HMAC with shared symmetric key; fresh nonce
- **Authentication:** Unilateral (Alice → Bob only)
- **Forward secrecy:** No
- **Notable:** No mutual authentication. `query attacker(k)` checks key secrecy.
````
plugins/trailmark/skills/crypto-protocol-diagram/examples/simple-proverif/model.pv
+59
View File
@@ -0,0 +1,59 @@
(* Simple challenge-response authentication protocol.
Alice authenticates to Bob using a shared symmetric key.
Protocol steps:
1. Alice sends her identity to Bob.
2. Bob generates a fresh nonce and sends it to Alice.
3. Alice computes mac = HMAC(k, nonce || identity) and sends it to Bob.
4. Bob verifies the MAC; if it matches, authentication succeeds.
*)
(* Declare a public channel *)
free c: channel.
(* Symmetric key shared between Alice and Bob — private (not known to attacker) *)
free k: bitstring [private].
(* Cryptographic functions *)
fun hmac(bitstring, bitstring): bitstring.
fun concat(bitstring, bitstring): bitstring.
(* Destructors *)
reduc forall m: bitstring, key: bitstring;
checkhmac(hmac(key, m), key, m) = true.
(* Security property: the attacker should not learn the shared key *)
query attacker(k).
(* Alice process *)
let AliceProc(identity: bitstring, key: bitstring) =
(* Step 1: Send identity to Bob *)
out(c, identity);
(* Step 2: Receive nonce from Bob *)
in(c, nonce: bitstring);
(* Step 3: Compute and send MAC *)
let mac = hmac(key, concat(nonce, identity)) in
out(c, mac).
(* Bob process *)
let BobProc(key: bitstring) =
(* Step 1: Receive Alice's identity *)
in(c, identity: bitstring);
(* Step 2: Generate fresh nonce and send to Alice *)
new nonce: bitstring;
out(c, nonce);
(* Step 3: Receive MAC from Alice *)
in(c, mac: bitstring);
(* Step 4: Verify MAC *)
if checkhmac(mac, key, concat(nonce, identity)) = true then
(* Authentication succeeded *)
out(c, true)
else
(* Authentication failed *)
0.
(* Main process: one session each *)
process
new alice_id: bitstring;
( AliceProc(alice_id, k)
| BobProc(k) )
plugins/trailmark/skills/crypto-protocol-diagram/references/ascii-sequence-diagram.md
+103
View File
@@ -0,0 +1,103 @@
# ASCII Sequence Diagram Reference
Rules for drawing ASCII sequence diagrams inline in responses.
## Column Layout
Lay out participants as column headers, each above a vertical `|` lifeline.
Space columns ~28–32 characters apart so labels fit without wrapping:
```
Initiator Responder
| |
| |
```
For three or more participants, extend the layout rightward:
```
Client Server CA
| | |
| | |
```
## Arrow Conventions
| Element | Syntax | Use for |
|---------|--------|---------|
| Request (→) | `+------>` | message send |
| Reply (←) | `<- - - -+` | response / reply |
| Lost / async | `+------x` | dropped message |
- Sending end: `+`
- Receiving end: `>` (rightward) or `<` (leftward)
- Solid lines `---` for sends; dashed `- - -` for responses/replies
- Label goes **on the arrow line**, positioned between the two lifelines
```
| |
+------------------------>| epk_I
| |
| epk_R, Enc(k, cert_R) |
|<- - - - - - - - - - - - +
| |
```
## Self-Loops (Local Computation)
For operations that happen at a single party without sending a message:
```
| |
+--. |
| | Sign(sk, transcript) |
|<-' |
| |
```
## Phase Labels
Group related steps under a phase label:
```
| -- Key Exchange -- |
| |
+------------------------>| epk_I
| |
```
## Abort / Error Paths
Place abort paths after the main flow, separated by a blank line:
```
| [on auth failure] |
| abort(AUTH_FAILED) |
|<- - - - - - - - - - - - +
```
## Width and Labels
- Keep lines under ~60 characters wide
- If a label is too long, abbreviate it (e.g. `Enc(k,id||σ)`) and add a
legend below the diagram explaining the abbreviations
## Inline Output Format
```
Protocol: <Name>
Output: <filename>
<Participant1> <Participant2>
| |
...
## Protocol Summary
- **Parties:** ...
- **Round complexity:** ...
- **Key primitives:** ...
- **Authentication:** ...
- **Forward secrecy:** ...
- **Notable:** none
```
plugins/trailmark/skills/crypto-protocol-diagram/references/mermaid-sequence-syntax.md
+311
View File
@@ -0,0 +1,311 @@
# Mermaid Sequence Diagram Syntax Reference
## Basic Structure
```
sequenceDiagram
participant A as Alice
participant B as Bob
A->>B: Hello
B-->>A: Hi
```
Every sequence diagram starts with `sequenceDiagram` on its own line (no
indentation). Participants are declared with `participant` before they appear
in messages; if undeclared, Mermaid auto-creates them in order of first
appearance — but always declare explicitly for crypto protocols to control
ordering.
---
## Participant Declarations
```
participant A # ID = display name
participant A as Alice # short ID, long display name
actor A as Alice # person icon instead of box
```
**Ordering:** Participants are rendered left-to-right in declaration order.
Arrange them so that the dominant message direction flows left-to-right:
Initiator → Responder, Client → Server, Prover → Verifier.
**Naming conventions for crypto:**
| Role | Suggested ID | Display name |
|------|-------------|--------------|
| Initiator | `I` | Initiator |
| Responder | `R` | Responder |
| Client | `C` | Client |
| Server | `S` | Server |
| Trusted third party | `TTP` | TTP |
| Prover | `P` | Prover |
| Verifier | `V` | Verifier |
| Dealer | `D` | Dealer |
| Party i | `P1`, `P2`, … | Party 1, Party 2, … |
| Certificate Authority | `CA` | CA |
---
## Arrow Types
| Syntax | Arrow | Use for |
|--------|-------|---------|
| `A->>B: msg` | solid, open arrowhead | synchronous message send |
| `A-->>B: msg` | dashed, open arrowhead | reply / response |
| `A->B: msg` | solid, no arrowhead | passive / internal note |
| `A-->B: msg` | dashed, no arrowhead | async / passive reply |
| `A-xB: msg` | solid, X head | message lost / dropped |
| `A--xB: msg` | dashed, X head | async lost message |
| `A-)B: msg` | solid, async arrowhead | fire-and-forget |
| `A--)B: msg` | dashed, async arrowhead | async reply |
**For crypto protocols**, use `->>` for all protocol messages and `-->>` for
responses/replies. Reserve `-->` and `--x` for error/abort paths inside `alt`
blocks.
---
## Notes
Attach explanatory text to one or two participants:
```
Note over A: keygen() → pk, sk
Note over A,B: shared_secret = DH(sk_A, pk_B)
Note right of A: internal computation
Note left of B: validation step
```
Use `Note over` for cryptographic operations that happen at a party without
a message being sent. Use `Note over A,B` to annotate a shared computation or
the meaning of a message between them.
**Keep notes short.** Use mathematical shorthand:
- `HKDF(IKM=DH_out, salt, info) → k`
- `Sign(sk, transcript) → σ`
- `Verify(pk, transcript, σ)`
- `Enc(k, plaintext, AD) → ct || tag`
- `H(nonce || msg) → c`
---
## Activation Bars
Show when a participant is "active" (processing):
```
activate A
A->>B: request
B-->>A: response
deactivate A
```
Or inline with `+` / `-`:
```
A->>+B: request
B-->>-A: response
```
Use activations sparingly in protocol diagrams — they add noise unless the
protocol has clear request/response pairing that benefits from showing
duration.
---
## Grouping Blocks
### `rect` — colored background region
```
rect rgba(100, 149, 237, 0.15)
Note over I,R: Phase 1: Key Exchange
I->>R: ephemeral_pk
R-->>I: ephemeral_pk
end
```
Use `rect` with a distinct color per protocol phase. Suggested palette:
| Phase | Color |
|-------|-------|
| Setup / Key Generation | `rgba(100, 149, 237, 0.15)` — blue |
| Handshake | `rgba(46, 204, 113, 0.15)` — green |
| Authentication | `rgba(241, 196, 15, 0.15)` — yellow |
| Key Derivation | `rgba(155, 89, 182, 0.15)` — purple |
| Data Transfer | `rgba(230, 196, 15, 0.12)` — gold |
| Error / Abort | `rgba(231, 76, 60, 0.15)` — red |
### `loop` — repeated block
```
loop for each data chunk
A->>B: Enc(k, chunk_i) → ct_i
B-->>A: ack
end
```
Use `loop` when a message exchange repeats N times. Avoid unrolling loops that
would add 5+ identical arrow pairs.
### `alt` — conditional / branching
```
alt verification succeeds
B-->>A: session_key
else verification fails
B-->>A: abort
end
```
Use `alt` for protocol branches: success path vs. abort/error paths. Always
show the error path — it's where security properties break down.
### `opt` — optional block
```
opt if session resumption requested
A->>B: session_ticket
end
```
Use `opt` for optional protocol extensions (e.g. session resumption, renegotiation).
### `par` — parallel execution
```
par
A->>B: msg_1
and
A->>C: msg_2
end
```
Use `par` for genuinely concurrent sends (broadcast in MPC, simultaneous sends
to multiple parties).
### `critical` — mutual exclusion region
```
critical database access
A->>DB: update
end
```
Rarely needed in protocol diagrams; use for atomic operations if relevant.
---
## Message Labels
Labels appear after the colon on arrow lines:
```
A->>B: ClientHello(random, cipher_suites, extensions)
B-->>A: ServerHello(random, chosen_cipher, session_id)
```
**Formatting guidance:**
- Use `FieldName(value)` or `Type{field: value, ...}` for structured messages
- Use `||` for concatenation: `nonce || ciphertext || tag`
- Use `→` to show output of a computation in a note: `KDF(shared) → k_enc, k_mac`
- Keep labels under ~60 characters; move detail into `Note over` annotations
- Subscript with underscore: `pk_e` (ephemeral pubkey), `k_1`, `σ_A`
---
## Common Pitfalls
### Colon in message label breaks parsing
**Broken:**
```
A->>B: key: value
```
**Fixed:** Use HTML entity or restructure:
```
A->>B: key=value
A->>B: "key: value"
```
### Special characters in participant IDs
Participant IDs must be alphanumeric + underscore. Avoid spaces, hyphens,
brackets.
**Broken:**
```
participant Party-1
```
**Fixed:**
```
participant P1 as Party 1
```
### `end` keyword clash
If a message label contains the word `end`, it may terminate a block early.
Quote it or rephrase.
### Unclosed blocks
Every `rect`, `loop`, `alt`, `opt`, `par` must have a matching `end`. Missing
`end` causes the entire diagram to fail silently.
### Long label lines
Labels longer than ~80 characters may overflow in some renderers. Break across
multiple notes rather than one very long label.
### `Note over A,B` with wrong participant order
The two participants in `Note over A,B` must be in left-to-right declaration
order, not reversed. `Note over B,A` when A is declared before B will fail in
some renderers.
---
## Complete Example
```mermaid
sequenceDiagram
participant I as Initiator
participant R as Responder
rect rgba(100, 149, 237, 0.15)
Note over I,R: Phase 1: Key Exchange
Note over I: keygen() → ek_I, epk_I
I->>R: epk_I
Note over R: keygen() → ek_R, epk_R
R-->>I: epk_R
Note over I,R: dh_out = DH(ek_I, epk_R) = DH(ek_R, epk_I)
Note over I,R: k_send, k_recv = HKDF(dh_out, salt, "handshake")
end
rect rgba(241, 196, 15, 0.15)
Note over I,R: Phase 2: Authentication
Note over I: σ_I = Sign(sk_I, transcript)
I->>R: Enc(k_send, identity_I || σ_I)
Note over R: Verify(pk_I, transcript, σ_I)
Note over R: σ_R = Sign(sk_R, transcript)
R-->>I: Enc(k_recv, identity_R || σ_R)
Note over I: Verify(pk_R, transcript, σ_R)
end
rect rgba(46, 204, 113, 0.15)
Note over I,R: Phase 3: Data Transfer
Note over I,R: k_app = HKDF(dh_out, transcript_hash, "application")
loop application data
I->>R: Enc(k_app, data_i, nonce_i)
R-->>I: ack_i
end
end
alt authentication failure
R-->>I: abort(AUTHENTICATION_FAILED)
end
```
plugins/trailmark/skills/crypto-protocol-diagram/references/protocol-patterns.md
+381
View File
@@ -0,0 +1,381 @@
# Crypto Protocol Patterns Reference
Canonical message flows for common cryptographic protocols. Use these as a
reference when comparing an implementation against a known spec, or as a
starting skeleton when the implementation follows a named protocol.
---
## TLS 1.3 Handshake (RFC 8446)
**Parties:** Client (C), Server (S)
**Round complexity:** 1 RTT (0-RTT with resumption)
```
C → S: ClientHello(random, legacy_session_id, cipher_suites,
key_share[ecdhe], supported_versions=[TLS 1.3])
S → C: ServerHello(random, legacy_session_id, cipher_suite,
key_share[ecdhe], supported_versions=TLS 1.3)
Note: ECDHE shared secret derived by both sides
Note: HKDF chain: early_secret → handshake_secret → master_secret
S → C: {EncryptedExtensions} (under handshake key)
S → C: {Certificate} (server cert chain)
S → C: {CertificateVerify} (Sign(sk_S, transcript))
S → C: {Finished} (HMAC over transcript)
C → S: {Certificate} (if mutual auth requested)
C → S: {CertificateVerify} (Sign(sk_C, transcript))
C → S: {Finished} (HMAC over transcript)
Both: derive application traffic keys from master_secret
C ↔ S: {Application Data} (under application keys)
```
**Code signals:** Look for `ClientHello`, `ServerHello`, `key_share`,
`supported_versions`, `cipher_suite`, `HKDF`, `transcript_hash`, `Finished`.
---
## Noise Protocol Framework (https://noiseprotocol.org)
**Pattern family:** NN, NK, NX, KN, KK, KX, XN, XK, XX, IX, ...
### Noise_XX (most common: mutual auth, no prior knowledge)
**Parties:** Initiator (I), Responder (R)
**Round complexity:** 1.5 RTT
```
I → R: msg_1 = e
(send ephemeral pubkey)
R → I: msg_2 = e, ee, s, es
(send ephemeral pubkey,
DH(e_R, e_I),
send static pubkey encrypted,
DH(s_R, e_I))
I → R: msg_3 = s, se
(send static pubkey encrypted,
DH(s_I, e_R))
Both: transport keys derived from chained hash state
I ↔ R: encrypted transport messages
```
**State machine:** `CipherState → SymmetricState → HandshakeState`.
Look for `MixKey`, `MixHash`, `EncryptAndHash`, `DecryptAndHash`,
`Split` (produces two `CipherState` objects for send/recv).
**Code signals:** `HandshakeState`, `CipherState`, `SymmetricState`,
`h` (handshake hash), `ck` (chaining key), `n` (nonce counter),
pattern strings like `"XX"`, `"IK"`.
### Noise_IK (identity-hiding initiator, known responder static key)
```
I → R: msg_1 = e, es, s, ss
(ephemeral, DH(e_I, s_R), static (encrypted), DH(s_I, s_R))
R → I: msg_2 = e, ee, se
(ephemeral, DH(e_R, e_I), DH(e_R, s_I))
```
---
## Signal Protocol
### X3DH (Extended Triple Diffie-Hellman) Key Agreement
**Parties:** Alice (A), Bob (B), Server (S)
**Purpose:** Establish shared secret for asynchronous messaging
```
Note over B: Publish to server:
IK_B (identity key),
SPK_B (signed prekey) + Sig(IK_B, SPK_B),
{OPK_B_i} (one-time prekeys)
Note over A: Fetch Bob's key bundle from server
A → S: fetch_prekey_bundle(Bob)
S → A: IK_B, SPK_B, Sig, OPK_B_1
Note over A: Verify Sig(IK_B, SPK_B)
Note over A: EK_A = generate ephemeral keypair
Note over A: DH1 = DH(IK_A, SPK_B)
DH2 = DH(EK_A, IK_B)
DH3 = DH(EK_A, SPK_B)
DH4 = DH(EK_A, OPK_B_1) [if one-time prekey available]
SK = KDF(DH1 || DH2 || DH3 || DH4)
A → B: InitialMessage(IK_A, EK_A, OPK_B_id, Enc(SK, initial_plaintext))
Note over B: Recompute DH1..DH4, derive SK
Decrypt initial message
```
**Code signals:** `identity_key`, `signed_prekey`, `one_time_prekey`,
`ephemeral_key`, `X3DH`, `triple_dh`, `prekey_bundle`.
### Double Ratchet Algorithm
**Parties:** Alice, Bob (symmetric, both have SK from X3DH)
**Purpose:** Forward-secret, break-in-recovery message encryption
```
Note over A,B: Initialize with SK from X3DH
A has B's ratchet public key
A → B: Header(dh_ratchet_pk_A, prev_chain_len, msg_num)
|| Enc(message_key, plaintext)
Note over B: DH ratchet step: new root_key, new chain_key
Derive message_key from chain_key
Decrypt
B → A: Header(dh_ratchet_pk_B, prev_chain_len, msg_num)
|| Enc(message_key, plaintext)
Note over A: DH ratchet step: new root_key, new chain_key
Derive message_key from chain_key
Decrypt
```
**Code signals:** `root_key`, `chain_key`, `message_key`, `ratchet_key`,
`sending_chain`, `receiving_chain`, `skip_message_keys`, `MessageKey`.
---
## Diffie-Hellman Key Exchange (Classic / ECDH)
**Parties:** Alice (A), Bob (B)
**Round complexity:** 1 RTT
```
Note over A: a = random scalar; g_a = g^a (or a·G for ECDH)
A → B: g_a
Note over B: b = random scalar; g_b = g^b (or b·G for ECDH)
B → A: g_b
Note over A: shared = g_b^a = g^(ab)
Note over B: shared = g_a^b = g^(ab)
Note over A,B: session_key = KDF(shared)
```
**Authenticated DH:** add signatures or MACs over the transcript to bind
identities. Without authentication, this is vulnerable to MITM.
---
## Challenge-Response Authentication
**Variants:** HMAC-based, signature-based, password-based (PAKE)
### Signature-based
```
C → S: authenticate_request(identity)
S → C: challenge(nonce, session_id)
Note over C: σ = Sign(sk_C, nonce || session_id || identity)
C → S: response(σ, pk_C)
Note over S: Verify(pk_C, nonce || session_id || identity, σ)
alt verification succeeds
S → C: session_token
else verification fails
S → C: auth_failure
end
```
**Code signals:** `challenge`, `nonce`, `sign`, `verify`, `response`,
`session_token`, `authenticate`.
### HMAC-based (shared secret)
```
C → S: auth_request(identity)
S → C: challenge(nonce)
Note over C: mac = HMAC(shared_key, nonce || identity)
C → S: response(mac)
Note over S: expected = HMAC(shared_key, nonce || identity)
ct_equal(mac, expected)
```
---
## Shamir Secret Sharing
**Parties:** Dealer (D), Parties P1…Pn, Combiner (C)
**Setup:** (t, n) threshold
```
Note over D: Split secret s into n shares using degree-(t-1) polynomial
f(x) = s + a_1·x + … + a_{t-1}·x^{t-1}
share_i = f(i) for i = 1..n
D → P1: Enc(pk_1, share_1)
D → P2: Enc(pk_2, share_2)
...
D → Pn: Enc(pk_n, share_n)
# (t-of-n parties agree to reconstruct)
P1 → C: share_1
P2 → C: share_2
...
Pt → C: share_t
Note over C: Lagrange interpolation on {(i, share_i)}
→ recover f(0) = s
```
**Code signals:** `split`, `share`, `combine`, `threshold`, `lagrange`,
`polynomial`, `evaluate`.
---
## Commit-Reveal
**Parties:** Committer (C), Verifier (V)
**Purpose:** Bind to a value without revealing it; reveal later
```
rect rgba(100, 149, 237, 0.15)
Note over C,V: Phase 1: Commit
Note over C: r = random nonce
commitment = H(value || r)
C → V: commitment
end
rect rgba(46, 204, 113, 0.15)
Note over C,V: Phase 2: Reveal
C → V: value, r
Note over V: Check H(value || r) == commitment
end
alt commitment matches
Note over V: value accepted
else mismatch
Note over V: ABORT — equivocation detected
end
```
**Code signals:** `commit`, `reveal`, `commitment`, `open`, `binding`,
`hiding`.
---
## Generic N-Party MPC (Round-Based)
**Parties:** P1, P2, …, Pn
**Structure:** Preprocessing + Online phases, or direct rounds
```
rect rgba(100, 149, 237, 0.15)
Note over P1,P3: Round 0: Input Commitment
Note over P1: share_1_j = Share(input_1, t, n) for j=1..n
P1 ->> P2: share_1_2
P1 ->> P3: share_1_3
Note over P2: share_2_j = Share(input_2, t, n)
P2 ->> P1: share_2_1
P2 ->> P3: share_2_3
Note over P3: share_3_j = Share(input_3, t, n)
P3 ->> P1: share_3_1
P3 ->> P2: share_3_2
end
rect rgba(46, 204, 113, 0.15)
Note over P1,P3: Round 1: Local Computation
Note over P1: result_share_1 = f(share_1_1, share_2_1, share_3_1)
Note over P2: result_share_2 = f(share_1_2, share_2_2, share_3_2)
Note over P3: result_share_3 = f(share_1_3, share_2_3, share_3_3)
end
rect rgba(155, 89, 182, 0.15)
Note over P1,P3: Round 2: Output Reconstruction
P1 ->> P2: result_share_1
P1 ->> P3: result_share_1
P2 ->> P1: result_share_2
P2 ->> P3: result_share_2
P3 ->> P1: result_share_3
P3 ->> P2: result_share_3
Note over P1: Combine(result_share_1, result_share_2, result_share_3) → output
Note over P2: Combine(...) → output
Note over P3: Combine(...) → output
end
```
**Broadcast channel:** In many MPC protocols, "send to all" is a broadcast.
Use `par` blocks or annotate with `Note over P1: broadcast to all`.
**Code signals:** `round`, `broadcast`, `send_share`, `recv_share`,
`local_computation`, `reconstruct`, `output`.
---
## Threshold Signature (FROST / GG20 pattern)
**Parties:** Signers S1…St (threshold-of-n), Aggregator (A)
**Setup:** n parties each hold a signing key share
```
rect rgba(100, 149, 237, 0.15)
Note over A: Coordinator selects t signers, distributes message m
A ->> S1: sign_request(m, participants=[S1..St])
A ->> S2: sign_request(m, participants=[S1..St])
A ->> St: sign_request(m, participants=[S1..St])
end
rect rgba(46, 204, 113, 0.15)
Note over S1..St: Round 1: Nonce Generation
Note over S1: (d_1, e_1) = random nonces; D_1=g^d_1, E_1=g^e_1
S1 ->> A: (D_1, E_1)
Note over S2: (d_2, e_2) = random nonces
S2 ->> A: (D_2, E_2)
Note over St: (d_t, e_t) = random nonces
St ->> A: (D_t, E_t)
end
rect rgba(155, 89, 182, 0.15)
Note over A: Aggregate binding factors, compute group commitment R
A ->> S1: commitment_list = [(D_i, E_i) for i in participants]
A ->> S2: commitment_list
A ->> St: commitment_list
end
rect rgba(241, 196, 15, 0.15)
Note over S1..St: Round 2: Partial Signatures
Note over S1: z_1 = d_1 + e_1·ρ_1 + λ_1·sk_1·c (partial sig)
S1 ->> A: z_1
Note over S2: z_2 = d_2 + e_2·ρ_2 + λ_2·sk_2·c
S2 ->> A: z_2
Note over St: z_t = ...
St ->> A: z_t
end
Note over A: σ = (R, z_1 + z_2 + ... + z_t) — final signature
Note over A: Verify(group_pk, m, σ)
```
**Code signals:** `partial_sign`, `aggregate`, `nonce`, `commitment`,
`binding_factor`, `lagrange_coefficient`, `group_key`, `threshold_sign`.
---
## Reading Hints: Identifying Protocol Patterns in Code
| Code pattern | Protocol signal |
|---|---|
| `send_msg` / `recv_msg` loop with round counter | Round-based MPC |
| Two `CipherState` after `split()` | Noise protocol completion |
| `transcript` accumulated via hash | TLS-style transcript MAC |
| `chain_key` / `root_key` updated per message | Double Ratchet |
| `verify_prekey_signature` | X3DH signal protocol |
| `lagrange` / `interpolate` | Shamir / threshold |
| `partial_sig` aggregated after broadcast | Threshold signature |
| `commitment = H(value || nonce)` followed by `open` | Commit-reveal |
| `challenge` sent, `Sign(sk, challenge)` response | Challenge-response |
| `g^a` sent, `g^b` received, `g^(ab)` computed | Classic DH |
plugins/trailmark/skills/crypto-protocol-diagram/references/spec-parsing-patterns.md
+320
View File
@@ -0,0 +1,320 @@
# Spec Parsing Patterns Reference
Extraction rules for turning protocol specifications into sequence diagram
content. Covers four spec formats. Read the section matching your input.
---
## RFC Format
RFCs follow a predictable structure. Use it to locate the right content fast.
### Locating the protocol description
1. **Find the handshake section**: search for "handshake", "key exchange",
"authentication", "message flow", or "overview" in section titles
2. **Find message definitions**: sections titled "Messages", "Record Layer",
"Handshake Protocol", or numbered `X.Y` subsections for each message type
3. **Find ASCII diagrams**: many RFCs embed sequence diagrams in code blocks
using `->` or `<-` arrows — use these as a starting point for message
ordering. If an ASCII diagram and the normative prose conflict, the prose
takes precedence — RFC ASCII diagrams are illustrative, not normative.
### Extracting parties
- Parties are usually named in the introduction or in a "Notation" / "Overview"
section: look for "client", "server", "initiator", "responder"
- Role names in RFCs are typically lowercase (`client`, `server`) — capitalise
them in the diagram
### Extracting message flow
Arrow patterns in RFC prose and ASCII diagrams:
```
Client Server
| |
|----------ClientHello------------------------->|
|<---------ServerHello + {EncryptedExtensions}--|
```
Also watch for:
- "The client sends a X message containing ..."
- "Upon receiving X, the server MUST ..."
- "The handshake proceeds as follows:" followed by a numbered list
`MUST`/`SHALL` clauses describe required steps; `MAY`/`SHOULD` describe
optional ones (use `opt` blocks in the diagram).
### Extracting crypto operations
RFCs typically define crypto in a "Cryptographic Computations" or "Key
Schedule" section. Look for:
- `HKDF-Extract`, `HKDF-Expand`, `Derive-Secret` — key derivation
- `Sign(sk, transcript)`, `Verify(pk, transcript, sig)` — signatures
- Encryption notation: `{...}` braces around a message mean it is encrypted
(TLS convention); note which key is used in the surrounding prose
- Transcript hash: running hash over all handshake messages — annotate as
`H(handshake_transcript)` at the point it is finalised
### ABNF grammars
ABNF defines message structure, not flow. Use it to populate arrow labels:
```
ClientHello = ProtocolVersion random [SessionID] CipherSuites Extensions
```
→ Arrow label: `ClientHello(version, random, session_id, cipher_suites, extensions)`
---
## Academic Paper / Pseudocode
Papers vary widely, but protocol descriptions follow common conventions.
### Locating the protocol description
- Look for boxes or figures labelled "Protocol X", "Figure X: Protocol name",
"Algorithm X"
- Section titles: "Protocol Description", "Construction", "Our Protocol",
"The Scheme", "Formal Description"
- Some papers give an informal description first, then a formal pseudocode box —
prefer the pseudocode box for message flow accuracy
### Extracting parties
- Header row of a protocol figure: `Alice | Bob`, `Client | Server`, `P | V`
- Pseudocode function names: `Client.KeyGen()`, `Server.Respond()`,
`Prover.Commit()`, `Verifier.Challenge()`
- Subscripts in mathematical notation: `pk_A`, `sk_B` — `A` and `B` are parties
### Extracting message flow
**Two-column layouts** (most common):
```
Alice Bob
--- ---
Compute x ← f(...)
Send x ──────────────►
Receive x
Compute y ← g(x, ...)
◄────────────── Send y
Receive y
```
Read left-to-right for Alice's column, right-to-left for Bob's. Arrows cross
the column boundary to indicate message sends.
**Numbered step lists**:
```
1. A generates (pk, sk) ← KeyGen(1^λ)
2. A sends pk to B
3. B computes c ← Enc(pk, m) and sends c to A
4. A decrypts m' ← Dec(sk, c)
```
Map step numbers to rounds. A step that says "X sends Y to Z" is a message
arrow. A step that says "X computes ..." is a `Note over X` annotation.
**Pseudocode with explicit send/receive**:
```
function Round1_Alice(sk_A, pk_B):
ek, epk = DH.KeyGen()
msg = epk
send(Bob, msg)
return ek
function Round1_Bob(pk_A):
epk_A = recv(Alice)
...
```
Treat `send(Party, msg)` as a message arrow, `recv(Party)` as the receiving
end of the previous arrow.
### Mathematical notation quick-reference
| Notation | Meaning |
|----------|---------|
| `←` or `:=` | assignment / output of a computation |
| `←$` or `←_R` | sample uniformly at random |
| `→` or `\leftarrow` between parties | message send |
| `\{m\}_k` or `Enc_k(m)` | encryption of `m` under key `k` |
| `[m]_sk` or `Sign_{sk}(m)` | signature on `m` with key `sk` |
| `H(m)` | hash |
| `\pi` or `Π` | protocol |
| `\lambda` | security parameter |
| `\bot` | reject / abort |
---
## Informal Prose
Informal descriptions vary the most. Apply these heuristics systematically.
### Locating the description
- Section headings: "Protocol Overview", "How It Works", "Flow", "Steps"
- Numbered or bulleted lists of protocol steps
- Diagrams embedded as images (describe what you can infer; note you cannot
read image content)
### Extracting parties
- Look for the first paragraph that names the participants: "Alice and Bob",
"the client and the server", "the initiator and responder"
- Use the first two prominent nouns that interact: if the text says "the user
authenticates to the service", parties are `User` and `Service`
### Extracting message flow — sentence patterns
Arrow syntax in the table below maps to Mermaid (`->>` solid, `-->>` dashed).
| Pattern | Arrow |
|---------|-------|
| "A sends [msg] to B" | `A->>B: msg` |
| "B receives [msg] from A" | `A->>B: msg` (same arrow, B's perspective) |
| "A transmits / delivers / forwards [msg]" | `A->>B: msg` (infer B from context) |
| "B responds with [msg]" | `B-->>A: msg` |
| "A and B exchange [msg]" | use two arrows if asymmetric, or `Note over A,B` if symmetric |
| "A computes / derives / generates [value]" | `Note over A: compute value` |
| "if [condition] then [action]" | `alt condition` block |
| "optionally, A sends [msg]" | `opt description` block |
### Handling vague crypto
If the prose says "encrypts" without specifying the scheme:
- Use `Enc(k, plaintext) → ct` in the note
- Add `⚠️ encryption scheme not specified in spec`
If the prose says "signs" without specifying the algorithm:
- Use `Sign(sk, msg) → σ`
- Add `⚠️ signature algorithm not specified`
---
## Formal Verification Models
### ProVerif (`.pv`)
ProVerif models processes, not a narrative sequence. Map process structure to
sequence diagram steps.
**Key constructs:**
```proverif
(* Channel declaration *)
free c: channel. (* public channel *)
free s: channel [private]. (* private / secure channel *)
(* Free names — constants known to attacker if not private *)
free pk_A: bitstring.
(* Process definition *)
let ClientProc(sk: bitstring, pk_S: bitstring) =
new nonce: bitstring; (* fresh random — Note over Client: nonce ← rand *)
out(c, nonce); (* send on channel c → arrow to Server *)
in(c, resp: bitstring); (* receive on channel c → arrow from Server *)
let (m1, sig) = resp in
if verify(m1, sig, pk_S) then (* conditional — alt block *)
...
else 0. (* abort path *)
(* Main process — composition of roles *)
process
( !ClientProc(sk_A, pk_S) | !ServerProc(sk_S, pk_A) )
```
**Extraction rules:**
| Construct | Diagram element |
|-----------|----------------|
| `let ProcName(params) =` | Defines a role; `ProcName` → participant |
| `new x: t` | `Note over Party: x ← fresh()` |
| `out(ch, msg)` | Arrow from this process to the process that `in`s on same `ch` |
| `in(ch, x)` | Receiving end of the matching `out` |
| `if cond then P else Q` | `alt cond` / `else` block |
| `let (a, b) = msg` | Destructuring — local computation, `Note over Party` |
| `!P` | Replication — this role handles multiple sessions; use `loop` annotation |
| `senc(m, k)` / `sdec(c, k)` | Symmetric enc/dec |
| `aenc(m, pk)` / `adec(c, sk)` | Asymmetric enc/dec |
| `sign(m, sk)` / `verify(m, sig, pk)` | Sign / verify |
| `hash(m)` | Hash |
| `pk(sk)` | Public key derivation — `Note over Party: pk = pk(sk)` |
**Channel matching:** Pair each `out(ch, msg)` with the `in(ch, x)` in another
process on the same channel. The sending process owns the arrow's tail; the
receiving process owns the arrow's head.
**Private channels** (`[private]` or declared with `new c`): represent
out-of-band communication — annotate: `Note over A,B: via private channel`.
**`phase N` construct:** ProVerif's `phase N` keyword sequences protocol steps
that cannot execute concurrently. Steps in phase N execute only after all phase
N-1 processes have terminated. If a model uses `phase`, use the phase numbers
to order the diagram: steps in phase 0 come before steps in phase 1, and so on.
Annotate phase boundaries: `Note over A,B: --- phase N begins ---`.
**Queries** (`query attacker(x)`, `query event(...)`) are security properties,
not protocol steps — omit from the diagram but mention in the Protocol Summary.
### Tamarin (`.spthy`)
**Important — Dolev-Yao attacker model:** Tamarin does not model direct
peer-to-peer channels. Every `Out(m)` delivers to the attacker network, and
every `In(m)` can be satisfied by any message the attacker knows (including
forwarded or replayed messages). For the diagram, treat `Out(m)` in one rule
and `In(m)` in another as a logical A→B message, but always add this note on
the diagram:
```
Note over A,B: ⚠️ Tamarin uses Dolev-Yao model — all messages transit adversary network
```
Tamarin models rules that fire when their premises are satisfied. Map rule
ordering to protocol steps.
**Key constructs:**
```tamarin
rule Register_pk:
[ Fr(~sk) ] (* fresh secret key generated *)
--[ Register($A, pk(~sk)) ]-> (* security annotation — not a message *)
[ !Ltk($A, ~sk) (* persistent fact — stored state *)
, !Pk($A, pk(~sk)) (* persistent fact — public key *)
, Out(pk(~sk)) ] (* send public key to network *)
rule Client_Send:
[ Fr(~n) (* fresh nonce *)
, !Pk($S, pk_S) ] (* lookup server's public key *)
--[ Send($C, $S, ~n) ]->
[ St_Client_1($C, $S, ~n) (* client state after round 1 *)
, Out(aenc(~n, pk_S)) ] (* send encrypted nonce *)
rule Server_Recv:
[ In(aenc(n, pk(~sk))) (* receive encrypted nonce *)
, !Ltk($S, ~sk) ] (* lookup server's secret key *)
--[ Recv($S, n) ]->
[ Out(n) ] (* echo decrypted nonce *)
```
**Extraction rules:**
| Construct | Diagram element |
|-----------|----------------|
| `Fr(~x)` in premise | `Note over Party: x ← fresh()` |
| `In(m)` in premise | Receive arrow — find matching `Out(m)` rule for sender |
| `Out(m)` in conclusion | Send arrow to network / other party |
| `!Fact($A, ...)` | Persistent state lookup — not a message |
| `St_Role_N(...)` | State fact — marks which round the party is in |
| `--[ Label ]->` | Security event annotation — omit from diagram |
| `$A` (public name) | Party / principal |
| `~x` (fresh name) | Freshly generated secret |
| `#i` (timepoint) | Ordering hint — earlier timepoint = earlier in diagram |
**Rule ordering:** Reconstruct order by following state facts: `St_Role_N`
consumed by a rule → `St_Role_{N+1}` produced → next rule for that role.
plugins/trailmark/skills/diagramming-code/SKILL.md
+181
View File
@@ -0,0 +1,181 @@
---
name: diagramming-code
description: >
Generates Mermaid diagrams from Trailmark code graphs. Produces call graphs,
class hierarchies, module dependency maps, containment diagrams, complexity
heatmaps, and attack surface data flow visualizations. Use when visualizing
code architecture, drawing call graphs, generating class diagrams, creating
dependency maps, producing complexity heatmaps, or visualizing data flow
and attack surface paths as Mermaid diagrams.
---
# Diagramming Code
Generates Mermaid diagrams from Trailmark's code graph. A pre-made script
handles Mermaid syntax generation; Claude selects the diagram type and
parameters.
## When to Use
- Visualizing call paths between functions
- Drawing class inheritance hierarchies
- Mapping module import dependencies
- Showing class structure with members
- Highlighting complexity hotspots with color coding
- Tracing data flow from entrypoints to sensitive functions
## When NOT to Use
- Querying the graph without visualization (use the `trailmark` skill)
- Mutation testing triage (use the `genotoxic` skill)
- Architecture diagrams not derived from code (draw by hand)
## Prerequisites
**trailmark** must be installed. If `uv run trailmark` fails, run:
```bash
uv pip install trailmark
```
**DO NOT** fall back to hand-writing Mermaid from source code reading. The
script uses Trailmark's parsed graph for accuracy. If installation fails,
report the error to the user.
---
## Quick Start
```bash
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type call-graph \
--focus main --depth 2
```
Output is raw Mermaid text. Wrap in a fenced code block:
````markdown
```mermaid
flowchart TB
...
```
````
---
## Diagram Types
```
├─ "Who calls what?" → --type call-graph
├─ "Class inheritance?" → --type class-hierarchy
├─ "Module dependencies?" → --type module-deps
├─ "Class members and structure?" → --type containment
├─ "Where is complexity highest?" → --type complexity
└─ "Path from input to function?" → --type data-flow
```
For detailed examples of each type, see
[references/diagram-types.md](references/diagram-types.md).
---
## Workflow
```
Diagram Progress:
- [ ] Step 1: Verify trailmark is installed
- [ ] Step 2: Identify diagram type from user request
- [ ] Step 3: Determine focus node and parameters
- [ ] Step 4: Run diagram.py script
- [ ] Step 5: Verify output is non-empty and well-formed
- [ ] Step 6: Embed diagram in response
```
**Step 1:** Run `uv run trailmark analyze --summary {targetDir}`. Install
if it fails. Then run pre-analysis via the programmatic API:
```python
from trailmark.query.api import QueryEngine
engine = QueryEngine.from_directory("{targetDir}", language="{lang}")
engine.preanalysis()
```
Pre-analysis enriches the graph with blast radius, taint propagation,
and privilege boundary data used by `data-flow` diagrams.
**Step 2:** Match the user's request to a `--type` using the decision tree
above.
**Step 3:** For `call-graph` and `data-flow`, identify the focus function.
Default `--depth 2`. Use `--direction LR` for dependency flows.
**Step 4:** Run the script and capture stdout.
**Step 5:** Check: output starts with `flowchart` or `classDiagram`,
contains at least one node. If empty or malformed, consult
[references/mermaid-syntax.md](references/mermaid-syntax.md).
**Step 6:** Wrap output in ` ```mermaid ``` ` code fence.
---
## Script Reference
```
uv run {baseDir}/scripts/diagram.py [OPTIONS]
```
| Argument | Short | Default | Description |
|---|---|---|---|
| `--target` | `-t` | required | Directory to analyze |
| `--language` | `-l` | `python` | Source language |
| `--type` | `-T` | required | Diagram type (see above) |
| `--focus` | `-f` | none | Center diagram on this node |
| `--depth` | `-d` | `2` | BFS traversal depth |
| `--direction` | | `TB` | Layout: `TB` (top-bottom) or `LR` (left-right) |
| `--threshold` | | `10` | Min complexity for `complexity` type |
### Examples
```bash
# Call graph centered on a function
uv run {baseDir}/scripts/diagram.py -t src/ -T call-graph -f parse_file
# Class hierarchy for a Rust project
uv run {baseDir}/scripts/diagram.py -t src/ -l rust -T class-hierarchy
# Module dependency map, left-to-right
uv run {baseDir}/scripts/diagram.py -t src/ -T module-deps --direction LR
# Class members
uv run {baseDir}/scripts/diagram.py -t src/ -T containment
# Complexity heatmap (threshold 5)
uv run {baseDir}/scripts/diagram.py -t src/ -T complexity --threshold 5
# Data flow from entrypoints to a specific function
uv run {baseDir}/scripts/diagram.py -t src/ -T data-flow -f execute_query
```
---
## Customization
**Direction:** Use `TB` (default) for hierarchical views, `LR` for
left-to-right flows like dependency chains.
**Depth:** Increase `--depth` to see more of the call graph. Decrease to
reduce clutter. The script warns if the diagram exceeds 100 nodes.
**Focus:** Always use `--focus` for `call-graph` on non-trivial codebases.
For `data-flow`, omitting focus auto-targets the top 10 complexity hotspots.
---
## Supporting Documentation
- **[references/diagram-types.md](references/diagram-types.md)** -
Detailed docs and Mermaid examples for each diagram type
- **[references/mermaid-syntax.md](references/mermaid-syntax.md)** -
ID sanitization, escaping, style definitions, and common pitfalls
plugins/trailmark/skills/diagramming-code/references/diagram-types.md
+206
View File
@@ -0,0 +1,206 @@
# Diagram Types
## Contents
- [Call graph](#call-graph)
- [Class hierarchy](#class-hierarchy)
- [Module dependencies](#module-dependencies)
- [Containment](#containment)
- [Complexity heatmap](#complexity-heatmap)
- [Attack surface / data flow](#attack-surface--data-flow)
---
## Call Graph
Shows which functions call which. Built from `callers_of` / `callees_of`
queries and `calls` edges.
**Mermaid type:** `flowchart`
**When to use `--focus`:** Almost always. Without focus, large codebases
produce unreadable diagrams. Start with `--depth 2` and increase if needed.
**Arrow styles reflect edge confidence:**
- Solid (`-->`) = certain (direct call)
- Dashed (`-.->`) = inferred (attribute access on non-self)
- Dotted (`..->`) = uncertain (dynamic dispatch)
**Example output:**
```mermaid
flowchart TB
query_api_QueryEngine_callers_of["callers_of, method"]
query_api_QueryEngine_callees_of["callees_of, method"]
query_api_QueryEngine_paths_between["paths_between, method"]
storage_graph_store_GraphStore_find_node_id["find_node_id, method"]
query_api_QueryEngine_callers_of --> storage_graph_store_GraphStore_find_node_id
query_api_QueryEngine_callees_of --> storage_graph_store_GraphStore_find_node_id
query_api_QueryEngine_paths_between --> storage_graph_store_GraphStore_find_node_id
```
**Script invocation:**
```bash
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type call-graph \
--focus QueryEngine --depth 2
```
---
## Class Hierarchy
Shows inheritance (`<|--`) and interface implementation (`<|..`)
relationships between classes, structs, interfaces, and traits.
**Mermaid type:** `classDiagram`
**Limitations:** Languages without class inheritance (e.g., Go, C) produce
empty diagrams. The script emits a note node in that case.
**Example output:**
```mermaid
classDiagram
class models_nodes_CodeUnit {
class
}
class models_edges_CodeEdge {
class
}
models_nodes_CodeUnit <|-- models_nodes_Parameter
```
**Script invocation:**
```bash
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type class-hierarchy
```
---
## Module Dependencies
Shows import relationships between modules. Built from `imports` edges.
**Mermaid type:** `flowchart`
**Best with `--direction LR`** for left-to-right dependency flow.
**Example output:**
```mermaid
flowchart LR
query_api["api, module"]
storage_graph_store["graph_store, module"]
models_nodes["nodes, module"]
query_api --> storage_graph_store
storage_graph_store --> models_nodes
```
**Script invocation:**
```bash
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type module-deps --direction LR
```
---
## Containment
Shows classes and their member functions/methods using `contains` edges.
**Mermaid type:** `classDiagram` (with member lists)
**Example output:**
```mermaid
classDiagram
class storage_graph_store_GraphStore {
+callers_of()
+callees_of()
+paths_between() list
+find_node() CodeUnit
}
```
**Script invocation:**
```bash
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type containment
```
---
## Complexity Heatmap
Shows functions color-coded by cyclomatic complexity with call edges
between them. Only nodes meeting `--threshold` are included.
**Mermaid type:** `flowchart` with `classDef` styles
**Color scale:**
- Green (`low`): CC < 5
- Yellow (`medium`): CC 5-10
- Red (`high`): CC > 10
**Example output:**
```mermaid
flowchart TB
parsers_python_parser_parse_file["parse_file, method, CC=15"]:::high
parsers_python_parser_visit_class["visit_class, method, CC=8"]:::medium
parsers_python_parser_parse_file --> parsers_python_parser_visit_class
classDef low fill:rgba(40,167,69,0.2),stroke:#28a745,color:#28a745
classDef medium fill:rgba(255,193,7,0.2),stroke:#e6a817,color:#e6a817
classDef high fill:rgba(220,53,69,0.2),stroke:#dc3545,color:#dc3545
```
**Script invocation:**
```bash
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type complexity --threshold 5
```
---
## Attack Surface / Data Flow
Shows paths from entrypoints (user input, API endpoints) to sensitive
functions. Entrypoints are styled distinctly (rounded rectangles, blue).
**Mermaid type:** `flowchart`
Without `--focus`, the script targets the top 10 complexity hotspots
reachable from entrypoints. With `--focus`, it shows all paths from
entrypoints to the specified function.
**Example output:**
```mermaid
flowchart TB
handle_request(["handle_request, function"]):::entrypoint
validate_input["validate_input, function"]
execute_query["execute_query, function"]
handle_request --> validate_input
validate_input --> execute_query
classDef entrypoint fill:rgba(0,123,255,0.2),stroke:#007bff,color:#007bff
```
**Script invocation:**
```bash
# Focus on a specific sensitive function
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type data-flow \
--focus execute_query
# Auto-detect: entrypoints to top complexity hotspots
uv run {baseDir}/scripts/diagram.py \
--target {targetDir} --type data-flow
```
plugins/trailmark/skills/diagramming-code/references/mermaid-syntax.md
+106
View File
@@ -0,0 +1,106 @@
# Mermaid Syntax Reference
Pitfalls and edge cases when generating Mermaid from code graph data.
## Contents
- [Node ID sanitization](#node-id-sanitization)
- [Label escaping](#label-escaping)
- [Style definitions](#style-definitions)
- [Edge confidence styling](#edge-confidence-styling)
- [Common pitfalls](#common-pitfalls)
---
## Node ID Sanitization
Trailmark node IDs use `module:Class.method` format. Mermaid node IDs
only allow `[a-zA-Z0-9_]`.
**Rules applied by `diagram.py`:**
- Replace any non-alphanumeric character (except `_`) with `_`
- Prefix with `n_` if the result starts with a digit
**Examples:**
| Trailmark ID | Mermaid ID |
|---|---|
| `query.api:QueryEngine.callers_of` | `query_api_QueryEngine_callers_of` |
| `3rdparty:init` | `n_3rdparty_init` |
---
## Label Escaping
Node labels are wrapped in double quotes to safely include special
characters:
```
node_id["label with (parens) and: colons"]
```
If the label itself contains double quotes, replace `"` with `#quot;`
(Mermaid's HTML entity escape).
---
## Style Definitions
Use `classDef` to define reusable styles and `:::` to apply them:
```mermaid
flowchart TB
A["Low complexity"]:::low
B["High complexity"]:::high
classDef low fill:rgba(40,167,69,0.2),stroke:#28a745,color:#28a745
classDef high fill:rgba(220,53,69,0.2),stroke:#dc3545,color:#dc3545
```
The script defines three classes for complexity heatmaps:
- `low` (green): CC < 5
- `medium` (yellow): CC 5-10
- `high` (red): CC > 10
And one for data flow:
- `entrypoint` (blue): marks untrusted input sources
---
## Edge Confidence Styling
Arrow syntax varies by edge confidence:
| Confidence | Arrow | Meaning |
|---|---|---|
| `certain` | `-->` | Direct call or `self.method()` |
| `inferred` | `-.->` | Attribute access on non-self object |
| `uncertain` | `..->` | Dynamic dispatch, reflection |
For class diagrams, arrows are different:
- `<\|--` = inherits
- `<\|..` = implements
---
## Common Pitfalls
**Reserved words as node IDs:** `end`, `graph`, `subgraph`, `style`,
`classDef`, `click` are reserved. The sanitization function avoids most
conflicts since it replaces special characters, but single-word function
names matching reserved words can still collide. Workaround: use the full
qualified ID which includes the module prefix.
**Leading digits:** Mermaid node IDs cannot start with a digit. The
script prefixes `n_` in this case.
**Diagram size:** Mermaid renderers struggle with >100 nodes. The script
warns when this limit is exceeded and suggests using `--focus` to scope
the diagram.
**Empty diagrams:** When no edges of the required type exist (e.g., no
`inherits` edges in a Go codebase), the script emits a single-node
diagram with an explanatory message rather than failing.
**Parentheses in labels:** Mermaid interprets `()` as rounded-rectangle
node shape. Always use quoted labels (`["label"]`) to avoid accidental
shape changes.
plugins/trailmark/skills/diagramming-code/scripts/diagram.py
+18
View File
@@ -0,0 +1,18 @@
# /// script
# requires-python = ">=3.12"
# dependencies = ["trailmark"]
# ///
"""Generate Mermaid diagrams from Trailmark code graphs.
Thin wrapper — all logic lives in ``trailmark.diagram``.
Run via ``uv run {this_file} --target ... --type ...``.
"""
from __future__ import annotations
import sys
from trailmark.diagram import main
if __name__ == "__main__":
sys.exit(main())
plugins/trailmark/skills/genotoxic/SKILL.md
+336
View File
@@ -0,0 +1,336 @@
---
name: genotoxic
description: "Graph-informed mutation testing triage. Parses codebases with Trailmark, runs mutation testing and necessist, then uses survived mutants, unnecessary test statements, and call graph data to identify false positives, missing test coverage, and fuzzing targets. Use when triaging survived mutants, analyzing mutation testing results, identifying test gaps, finding fuzzing targets from weak tests, running mutation frameworks (including circomvent and cairo-mutants), or using necessist."
---
# Genotoxic
Combines mutation testing and necessist (test statement removal) with
code graph analysis to triage findings into actionable categories:
false positives, missing unit tests, and fuzzing targets.
## When to Use
- After mutation testing reveals survived mutants that need triage
- Identifying where unit tests would have the highest impact
- Finding functions that need fuzz harnesses instead of unit tests
- Prioritizing test improvements using data flow context
- Filtering out harmless mutants from actionable ones
- Finding unnecessary test statements that indicate weak assertions (necessist)
## When NOT to Use
- Codebase has no existing test suite (write tests first)
- Pure documentation or configuration changes
- Single-file scripts with trivial logic
## Prerequisites
- **trailmark** installed — if `uv run trailmark` fails, run:
```bash
uv pip install trailmark
```
**DO NOT** fall back to "manual verification" or "manual analysis"
as a substitute for running trailmark. Install it first. If installation
fails, report the error instead of switching to manual analysis.
- A **mutation testing framework** for the target language — if the framework
command fails (not found, not installed), install it using the instructions
in [references/mutation-frameworks.md](references/mutation-frameworks.md).
**DO NOT** fall back to "manual mutation analysis" or skip mutation testing.
Install the framework first. If installation fails, report the error
instead of switching to manual mutation analysis.
- **necessist** (optional, recommended) — if the target language is
supported (Go, Rust, Solidity/Foundry, TypeScript/Hardhat,
TypeScript/Vitest, Rust/Anchor), install with `cargo install necessist`.
See [references/mutation-frameworks.md](references/mutation-frameworks.md)
for details.
- An existing test suite that passes
- **macOS environment**: Run `ulimit -n 1024` before any `mull-runner`
invocation. macOS Tahoe (26+) sets unlimited file descriptors by
default, which crashes Mull's subprocess spawning. See
[references/mutation-frameworks.md](references/mutation-frameworks.md)
for details.
---
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "All survived mutants need tests" | Many are harmless or equivalent | Triage before writing tests |
| "Mutation testing is too noisy" | Noise means you're not triaging | Use graph data to filter |
| "Unit tests cover everything" | Complex data flows need fuzzing | Check entrypoint reachability |
| "Dead code mutants don't matter" | Dead code should be removed | Flag for cleanup |
| "Low complexity = low risk" | Boundary bugs hide in simple code | Check mutant location |
| "Tool isn't installed, I'll do it manually" | Manual analysis misses what tooling catches | Install the tool first |
| "Necessist isn't mutation testing, skip it" | Necessist finds what mutation testing misses: weak tests | Run both when the language supports it |
---
## Quick Start
```bash
# 1. Build the code graph
uv run trailmark analyze --summary {targetDir}
# 2. Run mutation testing (language-dependent)
# Python:
uv run mutmut run --paths-to-mutate {targetDir}/src
uv run mutmut results
# 2b. Run necessist (if language supported)
necessist
# 3. Analyze results with this skill's workflow (Phase 3)
```
---
## Workflow Overview
```
Phase 1: Graph Build → Parse codebase with trailmark
↓
Phase 2: Mutation Run → Execute mutation testing framework
Phase 2b: Necessist Run → Remove test statements (optional, parallel)
↓
Phase 3: Triage → Classify findings using graph data
↓
Output: Categorized Report
├── Corroborated (both tools flag same function — highest value)
├── False Positives (harmless, skip)
├── Missing Tests (write unit tests)
└── Fuzzing Targets (set up fuzz harnesses)
```
---
## Decision Tree
```
├─ Need to set up mutation testing for a language?
│ └─ Read: references/mutation-frameworks.md
│
├─ Need to set up necessist or find weak test statements?
│ └─ Read: references/mutation-frameworks.md (Necessist section)
│
├─ Need to understand the triage criteria in depth?
│ └─ Read: references/triage-methodology.md
│
├─ Need to understand how graph data informs triage?
│ └─ Read: references/graph-analysis.md
│
└─ Already have results + graph? Use Phase 3 below.
```
---
## Phase 1: Build Code Graph and Run Pre-Analysis
Parse the target codebase with trailmark and run pre-analysis **before**
mutation testing. Pre-analysis computes blast radius, entry points, privilege
boundaries, and taint propagation, which Phase 3 uses for triage.
```bash
uv run trailmark analyze --summary {targetDir}
```
Use the `QueryEngine` API to build the graph and run pre-analysis:
1. `QueryEngine.from_directory("{targetDir}", language="{lang}")`
2. Call `engine.preanalysis()` — **mandatory** before triage
3. Export with `engine.to_json()` for cross-referencing with mutation results
See [references/graph-analysis.md](references/graph-analysis.md) for the
full API: node mapping, reachability queries, blast radius, and
pre-analysis subgraph lookups.
---
## Phase 2: Run Mutation Testing
Select and run the appropriate framework. See
[references/mutation-frameworks.md](references/mutation-frameworks.md) for
language-specific setup.
**Capture survived mutants.** Each framework reports differently, but
extract these fields per mutant:
| Field | Description |
|-------|-------------|
| File path | Source file containing the mutant |
| Line number | Line where mutation was applied |
| Mutation type | What was changed (operator, value, etc.) |
| Status | survived, killed, timeout, error |
Filter to **survived** mutants only for Phase 3.
---
## Phase 2b: Run Necessist (Optional)
If the target language is supported (Go, Rust, Solidity/Foundry,
TypeScript/Hardhat, TypeScript/Vitest, Rust/Anchor), run necessist to
find unnecessary test statements. This runs independently of Phase 2 and
can execute in parallel.
```bash
# Auto-detect framework
necessist
# Or target specific test files
necessist tests/test_parser.rs
# Export results
necessist --dump
```
Filter to findings where the test **passed after removal**. See
[references/mutation-frameworks.md](references/mutation-frameworks.md)
for framework-specific configuration and the normalized record format.
Map each removal to a production function using the algorithm in
[references/graph-analysis.md](references/graph-analysis.md).
---
## Phase 3: Triage Findings
For each survived mutant and each necessist removal, determine its
triage bucket using graph data. Necessist removals must first be mapped
to a production function (see
[references/graph-analysis.md](references/graph-analysis.md)).
### Quick Classification (Mutation Testing)
| Signal | Bucket | Reasoning |
|--------|--------|-----------|
| No callers in graph | **False Positive** | Dead code, mutant is unreachable |
| Only test callers | **False Positive** | Test infrastructure, not production |
| Logging/display string | **False Positive** | Cosmetic, no behavioral impact |
| Equivalent mutant | **False Positive** | Behavior unchanged despite mutation |
| Simple function, low CC, no entrypoint path | **Missing Tests** | Unit test is straightforward |
| Error handling path | **Missing Tests** | Should have negative test cases |
| Boundary condition (off-by-one) | **Missing Tests** | Property-based test candidate |
| Pure function, deterministic | **Missing Tests** | Easy to test, high value |
| High CC (>10), entrypoint reachable | **Fuzzing Target** | Complex + exposed = fuzz it |
| Parser/validator/deserializer | **Fuzzing Target** | Structured input handling |
| Many callers (>10) + moderate CC | **Fuzzing Target** | High blast radius |
| Binary/wire protocol handling | **Fuzzing Target** | Fuzzers excel at format testing |
### Quick Classification (Necessist)
| Signal | Bucket | Reasoning |
|--------|--------|-----------|
| Redundant setup or debug call | **False Positive** | Statement genuinely unnecessary |
| Cannot map to production function | **False Positive** | No graph context for triage |
| Call removed, no assertion checks its effect | **Missing Tests** | Test has weak assertions |
| Assertion removed, test still passes | **Missing Tests** | Redundant or insufficient coverage |
| Maps to high-CC entrypoint-reachable function | **Fuzzing Target** | Complex + exposed + weak test |
When both mutation testing and necessist flag the same production
function, mark as **corroborated** — highest confidence finding.
For detailed criteria, see
[references/triage-methodology.md](references/triage-methodology.md).
### Graph Queries for Triage
For each mutant, map it to its containing graph node and use pre-analysis
subgraphs (tainted, high_blast_radius, privilege_boundary) from Phase 1
to classify it. The classification logic checks: no callers → false
positive, privilege boundary → fuzzing, high CC + tainted → fuzzing,
high blast radius → fuzzing, otherwise → missing tests.
See [references/graph-analysis.md](references/graph-analysis.md) for
the `batch_triage` implementation and node mapping functions.
---
## Output Format
Generate a markdown report:
```markdown
# Genotoxic Triage Report
## Summary
- Total survived mutants: N
- Total necessist removals: N
- Corroborated findings: N
- False positives: N (N%)
- Missing test coverage: N (N%)
- Fuzzing targets: N (N%)
## Corroborated Findings
| File | Line | Function | Mutation Signal | Necessist Signal | Action |
|------|------|----------|----------------|------------------|--------|
## False Positives
| File | Line | Mutation | Reason | Source |
|------|------|----------|--------|--------|
## Missing Test Coverage
| File | Line | Function | CC | Callers | Suggested Test | Source |
|------|------|----------|----|---------|----------------|--------|
## Fuzzing Targets
| File | Line | Function | CC | Entrypoint Path | Blast Radius | Source |
|------|------|----------|----|-----------------|--------------|--------|
```
The `Source` column is `mutation`, `necessist`, or `corroborated`.
Write the report to `GENOTOXIC_REPORT.md` in the working directory.
---
## Quality Checklist
Before delivering:
- [ ] Trailmark graph built for target language
- [ ] Mutation framework ran to completion
- [ ] Necessist ran (if language supported) or noted as not applicable
- [ ] All survived mutants triaged (none unclassified)
- [ ] All necessist removals triaged (if applicable)
- [ ] Corroborated findings identified (if both tools ran)
- [ ] False positives have clear justifications
- [ ] Missing test items include suggested test type
- [ ] Fuzzing targets include entrypoint paths and blast radius
- [ ] Report file written to `GENOTOXIC_REPORT.md`
- [ ] User notified with summary statistics
---
## Integration
**trailmark skill:**
- Phase 1: Build code graph, query complexity and entrypoints
- Phase 3: Caller analysis, reachability, blast radius
**property-based-testing skill:**
- Missing test coverage items involving boundary conditions
- Roundtrip/idempotence properties for serialization mutants
**testing-handbook-skills (fuzzing):**
- Fuzzing target items: use `harness-writing`, `cargo-fuzz`, `atheris`
---
## Supporting Documentation
- **[references/mutation-frameworks.md](references/mutation-frameworks.md)** -
Language-specific framework setup, output parsing, and necessist configuration
- **[references/triage-methodology.md](references/triage-methodology.md)** -
Detailed triage criteria, edge cases, and worked examples for both
mutation testing and necessist
- **[references/graph-analysis.md](references/graph-analysis.md)** -
Graph query patterns, test-to-production mapping, and result merging
---
**First-time users:** Start with Phase 1 (graph build), then run mutations,
then use the Quick Classification table in Phase 3.
**Experienced users:** Jump to Phase 3 and use the Decision Tree to load
specific reference material.
plugins/trailmark/skills/genotoxic/references/graph-analysis.md
+453
View File
@@ -0,0 +1,453 @@
# Graph Analysis for Mutant Triage
How to use trailmark's code graph data to contextualize survived mutants
and assign them to the correct triage bucket.
## Contents
- Mapping mutants to graph nodes
- Reachability analysis
- Blast radius calculation
- Complexity correlation
- Annotation-driven triage
- Batch triage workflow
- Mapping necessist removals to graph nodes
- Merging mutation and necessist results
---
## Mapping Mutants to Graph Nodes
Each survived mutant has a `file_path` and `line` number. Map it to the
containing function in the trailmark graph:
```python
def find_containing_node(nodes: dict, file_path: str, line: int):
"""Find the graph node that contains a given source line."""
candidates = []
for node_id, node in nodes.items():
loc = node.get("location", {})
if not loc:
continue
if loc["file_path"] != file_path:
continue
if loc["start_line"] <= line <= loc["end_line"]:
candidates.append((node_id, node))
if not candidates:
return None
# Prefer the most specific (smallest range) containing node
candidates.sort(
key=lambda x: (
x[1]["location"]["end_line"]
- x[1]["location"]["start_line"]
)
)
return candidates[0][1]
```
**Why smallest range?** A line inside a method is also inside its
containing class. The method node is the more useful context for triage.
---
## Reachability Analysis
Determine whether a mutated function is reachable from untrusted input.
### From Entrypoints
```python
def is_entrypoint_reachable(engine, node_id: str) -> bool:
"""Check if any entrypoint can reach this node."""
for ep in engine.attack_surface():
paths = engine.paths_between(ep["node_id"], node_id)
if paths:
return True
return False
```
### Entrypoint Path Details
For fuzzing targets, include the specific entrypoint paths in the report:
```python
def entrypoint_paths(engine, node_id: str) -> list[dict]:
"""Get all entrypoint paths to this node with metadata."""
results = []
for ep in engine.attack_surface():
paths = engine.paths_between(ep["node_id"], node_id)
for path in paths:
results.append({
"entrypoint": ep["node_id"],
"trust_level": ep["trust_level"],
"kind": ep["kind"],
"path": path,
"hops": len(path),
})
return results
```
### Trust Level Weighting
Not all entrypoints are equally dangerous:
| Trust Level | Weight | Examples |
|-------------|--------|---------|
| `untrusted_external` | 3x | User input, network data |
| `semi_trusted_external` | 2x | Partner APIs, OAuth tokens |
| `trusted_internal` | 1x | Internal service calls |
Higher-weight entrypoints push mutants toward the fuzzing bucket.
---
## Blast Radius Calculation
Blast radius measures how many other functions depend on the mutated
function. Higher blast radius means a bug has wider impact.
### Direct Callers
```python
def blast_radius(engine, node_id: str) -> dict:
"""Calculate blast radius for a node."""
callers = engine.callers_of(node_id)
callees = engine.callees_of(node_id)
return {
"direct_callers": len(callers),
"direct_callees": len(callees),
"caller_ids": [c["id"] for c in callers],
}
```
### Transitive Impact
For critical functions, calculate transitive callers (all functions
that eventually call this one):
```python
from trailmark.storage.graph_store import GraphStore
# Build the store from the graph
store = GraphStore(graph)
# All nodes that can reach this function
# (predecessors in the call graph)
transitive = store.entrypoint_paths_to(node_id)
transitive_count = len(set(
node for path in transitive for node in path
))
```
### Blast Radius Classification
| Direct Callers | Transitive Callers | Classification |
|----------------|-------------------|----------------|
| 0 | 0 | Dead code (false positive) |
| 1-5 | 1-10 | LOW |
| 6-20 | 11-50 | MEDIUM |
| 21-50 | 51-100 | HIGH |
| 50+ | 100+ | CRITICAL |
---
## Complexity Correlation
Cross-reference survived mutants with complexity data to distinguish
"simple enough to unit test" from "complex enough to fuzz."
### Per-Function Complexity
```python
def complexity_context(engine, node_id: str) -> dict:
"""Get complexity context for triage decision."""
hotspots = engine.complexity_hotspots(threshold=1)
for h in hotspots:
if h["id"] == node_id:
return {
"cyclomatic_complexity": h["cyclomatic_complexity"],
"is_hotspot": h["cyclomatic_complexity"] >= 10,
}
return {"cyclomatic_complexity": 0, "is_hotspot": False}
```
### Decision Matrix
| CC | Entrypoint Reachable | Blast Radius | Bucket |
|----|---------------------|--------------|--------|
| <5 | No | Any | Missing Tests |
| <5 | Yes | LOW | Missing Tests |
| <5 | Yes | HIGH+ | Missing Tests (priority) |
| 5-10 | No | LOW | Missing Tests |
| 5-10 | No | HIGH+ | Missing Tests (priority) |
| 5-10 | Yes | Any | Fuzzing Target |
| >10 | Any | Any | Fuzzing Target |
---
## Annotation-Driven Triage
Use trailmark annotations to record triage decisions and refine
classification over time.
### Recording Decisions
```python
from trailmark.models import AnnotationKind
# Mark a function as triaged
engine.annotate(
node_id,
AnnotationKind.ASSUMPTION,
"genotoxic: false_positive (equivalent mutant in logging)",
source="llm",
)
# Mark a fuzzing target with rationale
engine.annotate(
node_id,
AnnotationKind.ASSUMPTION,
"genotoxic: fuzzing_target (CC=14, entrypoint-reachable via /api/parse)",
source="llm",
)
```
### Querying Previous Triage
```python
# Check if a function was previously triaged
annotations = engine.annotations_of(node_id)
genotoxic_annotations = [
a for a in annotations
if a["description"].startswith("genotoxic:")
]
```
This enables incremental triage across multiple mutation testing runs.
---
## Batch Triage Workflow
For large codebases with many survived mutants, process in batch:
```python
import json
def batch_triage(engine, survived_mutants: list[dict]) -> dict:
"""Classify all survived mutants."""
graph_json = json.loads(engine.to_json())
nodes = graph_json["nodes"]
results = {
"false_positives": [],
"missing_tests": [],
"fuzzing_targets": [],
}
for mutant in survived_mutants:
node = find_containing_node(
nodes, mutant["file_path"], mutant["line"]
)
if not node:
results["false_positives"].append({
**mutant,
"reason": "no containing function in graph",
})
continue
node_id = node["id"]
callers = engine.callers_of(node_id)
cc = node.get("cyclomatic_complexity", 0) or 0
# Dead code
if not callers:
results["false_positives"].append({
**mutant,
"reason": "no callers (dead code)",
"node_id": node_id,
})
continue
reachable = is_entrypoint_reachable(engine, node_id)
# Fuzzing criteria
if (cc > 10 and reachable) or (len(callers) > 10 and cc > 5):
ep_paths = entrypoint_paths(engine, node_id)
results["fuzzing_targets"].append({
**mutant,
"node_id": node_id,
"cyclomatic_complexity": cc,
"caller_count": len(callers),
"entrypoint_paths": ep_paths,
"blast_radius": blast_radius(engine, node_id),
})
continue
# Default: missing tests
results["missing_tests"].append({
**mutant,
"node_id": node_id,
"cyclomatic_complexity": cc,
"caller_count": len(callers),
"entrypoint_reachable": reachable,
})
return results
```
### Performance Considerations
- **Path queries are expensive.** Cache `paths_between` results when
checking multiple mutants against the same entrypoints.
- **Process by function, not by mutant.** Multiple mutants in the same
function share the same graph context. Group mutants by containing
function first, query graph once per function.
- **Use `complexity_hotspots` as a prefilter.** Functions with CC < 5
are almost never fuzzing targets. Skip reachability analysis for them
unless caller count is very high.
---
## Mapping Necessist Removals to Graph Nodes
Necessist findings reference **test code** locations, but triage requires
the **production function** that the removed statement exercises. Extract
the called function name from the removed statement and match it against
graph nodes.
```python
import re
def map_removal_to_production_node(
nodes: dict,
removed_statement: str,
test_file_path: str,
) -> dict | None:
"""Map a necessist removal to the production function it exercises."""
# Extract function/method name from the removed statement.
# Handles: obj.method(args), function(args), obj.method!(args)
match = re.search(
r"(?:(\w+)\.)?(\w+!?)\s*\(", removed_statement
)
if not match:
return None
func_name = match.group(2)
# Search graph nodes for matching function name
candidates = [
(nid, n) for nid, n in nodes.items()
if n.get("name") == func_name
and "test" not in n.get("location", {})
.get("file_path", "").lower()
]
if len(candidates) == 1:
return candidates[0][1]
# Disambiguate: prefer node in the production module
# that mirrors the test file path
prod_path = infer_production_path(test_file_path)
for nid, n in candidates:
if n.get("location", {}).get("file_path") == prod_path:
return n
# Fall back to first non-test candidate
return candidates[0][1] if candidates else None
def infer_production_path(test_file_path: str) -> str:
"""Heuristic: map test file to likely production file.
tests/test_parser.py → src/parser.py
test/parser_test.go → parser.go
tests/Parser.test.ts → src/Parser.ts
"""
path = test_file_path
# Strip test directory prefixes
path = re.sub(r"^tests?/", "src/", path)
# Strip test_ prefix or _test / .test suffix
path = re.sub(r"test_(\w+)", r"\1", path)
path = re.sub(r"(\w+)_test\.", r"\1.", path)
path = re.sub(r"(\w+)\.test\.", r"\1.", path)
return path
```
**When mapping fails:** If no production node matches, classify the
removal as a false positive with reason "unmappable to production code."
This is conservative — the removal may still be meaningful, but without
graph context triage cannot assign a confident bucket.
---
## Merging Mutation and Necessist Results
When both mutation testing and necessist produce findings for the same
production function, this is a **corroborated** finding: the function
has both uncaught production mutations and unnecessary test statements.
Corroborated findings are highest confidence.
```python
def merge_results(
mutation_results: dict,
necessist_results: dict,
) -> dict:
"""Merge mutation and necessist triage results.
Identifies corroborated findings where both tools flag
the same production function.
"""
merged = {
"corroborated": [],
"false_positives": (
mutation_results["false_positives"]
+ necessist_results["false_positives"]
),
"missing_tests": [],
"fuzzing_targets": [],
}
# Index necessist findings by production node_id
necessist_by_node = {}
for item in (
necessist_results["missing_tests"]
+ necessist_results["fuzzing_targets"]
):
nid = item.get("node_id")
if nid:
necessist_by_node.setdefault(nid, []).append(item)
# Check mutation findings for corroboration
for bucket in ("missing_tests", "fuzzing_targets"):
for item in mutation_results[bucket]:
nid = item.get("node_id")
if nid and nid in necessist_by_node:
merged["corroborated"].append({
"node_id": nid,
"mutation": item,
"necessist": necessist_by_node.pop(nid),
})
else:
merged[bucket].append(item)
# Add remaining non-corroborated necessist findings
for items in necessist_by_node.values():
for item in items:
bucket = (
"fuzzing_targets"
if item in necessist_results["fuzzing_targets"]
else "missing_tests"
)
merged[bucket].append(item)
return merged
```
Corroborated findings should appear in a dedicated report section
before the individual buckets, since they represent the highest-value
action items.
plugins/trailmark/skills/genotoxic/references/mutation-frameworks.md
+1026
View File
File diff suppressed because it is too large Load Diff
plugins/trailmark/skills/genotoxic/references/triage-methodology.md
+341
View File
@@ -0,0 +1,341 @@
# Triage Methodology
Detailed criteria for classifying survived mutants into actionable buckets.
## Contents
- False positive detection
- Missing test coverage identification
- Fuzzing target selection
- Edge cases and ambiguous mutants
- Worked examples
- Necessist removal triage
---
## False Positive Detection
A mutant is a false positive when killing it would not improve code
quality or catch real bugs. Classify as false positive when ANY of
these conditions hold:
### Dead Code
The mutated function has zero callers in the trailmark graph.
```python
callers = engine.callers_of(node_id)
if not callers:
# Dead code. The mutant is unreachable in production.
# Action: flag function for removal, not testing.
```
**Subtlety:** A function with no *direct* callers may still be reachable
via dynamic dispatch (reflection, callbacks, decorators). Check edge
confidence: if all edges to the function are `uncertain`, investigate
before dismissing.
### Test-Only Code
The function is only called from test files.
```python
callers = engine.callers_of(node_id)
prod_callers = [
c for c in callers
if "test" not in c["location"]["file_path"].lower()
]
if not prod_callers:
# Only tests call this. Mutant in test infrastructure.
```
### Equivalent Mutants
The mutation produces identical behavior. Common patterns:
| Mutation | Why Equivalent |
|----------|---------------|
| `x > 0` → `x >= 1` | Identical for integers |
| `x != 0` → `x > 0` | Identical for unsigned types |
| `return x` → `return +x` | Unary plus is a no-op |
| String literal change in log message | No behavioral impact |
| Reorder of commutative operations | `a + b` == `b + a` |
**Detection strategy:** Check if the mutation is in a logging call,
display string, comment-adjacent code, or assertion message. These
are cosmetic and do not affect program behavior.
### Redundant Checks
The mutation weakens a condition, but another check in the same call
path enforces the same constraint:
```python
# Caller validates x > 0 before calling this function.
# Mutating this function's own x > 0 check is redundant.
callers = engine.callers_of(node_id)
# Inspect caller source for equivalent preconditions.
```
Use trailmark annotations to track this:
```python
from trailmark.models import AnnotationKind
engine.annotate(
node_id,
AnnotationKind.PRECONDITION,
"x > 0 enforced by all callers",
source="llm",
)
```
---
## Missing Test Coverage
A mutant indicates missing test coverage when:
1. The function is reachable in production (has callers)
2. The mutated behavior *should* be caught by tests
3. A unit test is the appropriate testing strategy
### Criteria
| Signal | Why Unit Test | Priority |
|--------|--------------|----------|
| Pure function, no side effects | Deterministic, easy to test | HIGH |
| Low CC (<5) | Few paths to cover | HIGH |
| Error/exception handling path | Negative tests needed | HIGH |
| Boundary condition (off-by-one) | Property-based test | MEDIUM |
| Return value mutation | Assert on return values | MEDIUM |
| State transition logic | State machine tests | MEDIUM |
| Configuration/flag handling | Parameter variation tests | LOW |
### Suggested Test Types
Map the mutation type to a test strategy:
| Mutation Type | Suggested Test |
|---------------|---------------|
| Arithmetic operator (`+` → `-`) | Value assertion on known inputs |
| Comparison operator (`<` → `<=`) | Boundary value test |
| Boolean negation (`True` → `False`) | Branch coverage test |
| Return value (`return x` → `return None`) | Return value assertion |
| Removed statement | Side effect verification |
| Exception removal | Negative test (expect failure) |
### When to Prefer Property-Based Testing
If the survived mutant involves:
- Serialization/deserialization (roundtrip property)
- Idempotent operations (applying twice = applying once)
- Ordering invariants (sorted output)
- Numeric ranges or bounds
Use the **property-based-testing** skill for guidance.
---
## Fuzzing Target Selection
A survived mutant is a fuzzing target when unit testing alone is
insufficient due to complexity, input space, or exposure to untrusted
data.
### Criteria
| Signal | Threshold | Why Fuzzing |
|--------|-----------|-------------|
| Cyclomatic complexity | CC > 10 | Too many paths for manual tests |
| Entrypoint reachable | Any path from untrusted input | Attacker-controlled data |
| Caller count | > 10 callers | High blast radius |
| Input parsing | Handles structured data | Fuzzers generate diverse inputs |
| Binary/wire protocol | Processes byte sequences | Coverage-guided exploration |
| Recursive logic | Processes nested structures | Depth/stack exhaustion |
| State machine | Multiple state transitions | State space exploration |
### Prioritization
Combine signals for priority assignment:
```
CRITICAL: Entrypoint reachable + CC > 15 + parser/validator
HIGH: Entrypoint reachable + CC > 10
HIGH: CC > 10 + caller count > 20
MEDIUM: CC > 10 OR (entrypoint reachable + caller count > 10)
LOW: Moderate complexity, not entrypoint reachable
```
### Framework Selection
Based on target language, recommend the appropriate fuzzer:
| Language | Fuzzer | Skill Reference |
|----------|--------|-----------------|
| Python | Atheris | `testing-handbook-skills:atheris` |
| Rust | cargo-fuzz | `testing-handbook-skills:cargo-fuzz` |
| C/C++ | libFuzzer or AFL++ | `testing-handbook-skills:libfuzzer` |
| Go | go-fuzz (native) | Built-in `go test -fuzz` |
| Ruby | Ruzzy | `testing-handbook-skills:ruzzy` |
| Java | Jazzer | JUnit integration |
| JavaScript | jsfuzz | npm package |
---
## Edge Cases and Ambiguous Mutants
Some mutants don't cleanly fit one bucket. Resolution rules:
### Mutant in Validation Code
If the mutant weakens input validation:
- **Entrypoint reachable?** → Fuzzing target (attacker can exploit)
- **Internal only?** → Missing test (regression risk)
### Mutant in Error Path
If the mutant changes error handling behavior:
- **Error path tested?** → Check if test expects specific error
- **Error path untested?** → Missing test (negative test case)
- **Error in parser?** → Fuzzing target (malformed input testing)
### Mutant Straddles Complexity Threshold
CC is near the threshold (8-12 range):
- **Has entrypoint path?** → Fuzzing target (exposure wins)
- **No entrypoint path?** → Missing test (unit test is feasible)
### Tie-Breaking Rule
When signals conflict, prefer the higher-assurance category:
```
Fuzzing Target > Missing Test > False Positive
```
A function that *could* be unit tested but is also entrypoint-reachable
and complex should be fuzzed. Fuzzing subsumes the unit test goal while
providing broader coverage.
---
## Worked Example
**Scenario:** Python web application, `mutmut` reports 47 survived mutants.
**Graph context (from trailmark):**
- 312 nodes, 1,847 edges
- 8 entrypoints (Flask route handlers)
- 14 functions with CC > 10
**Triage results:**
| Category | Count | Examples |
|----------|-------|---------|
| False Positive | 12 | 5 logging strings, 3 dead utils, 4 equivalent |
| Missing Tests | 23 | 8 error paths, 7 return values, 5 boundary, 3 config |
| Fuzzing Targets | 12 | 4 request parsers, 3 validators, 3 query builders, 2 serializers |
**Key decisions:**
- `parse_query_params` (CC=14, entrypoint-reachable via `/search`) → **Fuzzing**
- `format_error_response` (CC=3, 2 callers, string formatting) → **False positive** (cosmetic)
- `validate_email` (CC=6, 4 callers, no entrypoint path) → **Missing test** (boundary cases)
- `build_sql_filter` (CC=12, entrypoint-reachable via `/api/filter`) → **Fuzzing** (injection risk)
---
## Necessist Removal Triage
Necessist findings differ from mutation testing: they identify test
statements whose removal doesn't cause test failure. Triage maps each
removal to a production function using the graph analysis algorithm
and then classifies it.
### False Positive Detection (Necessist)
Classify a necessist removal as false positive when:
| Signal | Reason |
| ------ | ------ |
| Redundant setup | Same call made elsewhere in the test or fixture |
| Debug/logging call | `println`, `console.log`, `dbg!` in test code |
| Teardown/cleanup | Removal of resource cleanup that doesn't affect assertions |
| Dead production code | Production function has no callers in graph |
| Unmappable statement | Cannot identify which production function is exercised |
### Missing Test Coverage (Necessist)
A removal indicates missing coverage when the test *should* fail but
doesn't — meaning the test has weak or missing assertions:
| Signal | Action |
| ------ | ------ |
| Function call removed, no assertion checks its effect | Add assertion on the function's return value or side effect |
| Assertion removed, remaining assertions still pass | The removed assertion covered unique behavior — restore and strengthen |
| Setup step removed with no downstream impact | Setup should affect test outcome; add assertions that depend on it |
| State mutation removed, test still passes | Test doesn't verify state changes — add state assertions |
### Fuzzing Target Selection (Necessist)
After mapping to a production function, apply the same graph-based
criteria as mutation testing:
- CC > 10 and entrypoint reachable → **Fuzzing Target**
- High blast radius and CC > 5 → **Fuzzing Target**
- On a privilege boundary → **Fuzzing Target**
The reasoning is identical: if a production function is complex, exposed,
and its test coverage is demonstrably weak (necessist proved a test
statement was unnecessary), fuzzing is the appropriate response.
### Edge Cases (Necessist)
**Async/await removals:** Removing an `await` may cause a test to pass
because the assertion runs before the async operation completes. This
is a genuine test weakness (race condition in test), not a false positive.
Classify as missing test coverage — the test needs to properly await
and assert.
**Macro expansions (Foundry/Anchor):** Cheatcodes like `vm.prank`,
`vm.expectRevert`, `vm.warp` are setup-critical. If removing one causes
the test to still pass, the test likely doesn't exercise the behavior
the cheatcode was supposed to enable. Classify as missing test coverage
unless the cheatcode is purely cosmetic (`vm.label`).
**Chained method calls:** `foo.bar().baz()` — necessist may remove
the entire chain. Map to the outermost call (`foo.bar`) for triage.
If the chain involves multiple production functions, triage against
the one with highest blast radius.
**Solidity `assert` vs `require`:** Removing a `require` check in a
test helper is different from removing an `assert` in a test body.
`require` removals in test helpers are usually false positives (guard
conditions). `assert` removals in test bodies are missing coverage.
### Worked Example: Foundry Project
**Scenario:** Foundry DeFi lending protocol, necessist reports 31
removals that passed.
**Graph context (from trailmark):**
- 89 nodes, 412 edges
- 5 entrypoints (external functions)
- 6 functions with CC > 10
**Triage results:**
| Category | Count | Examples |
| -------- | ----- | ------- |
| False Positive | 8 | 3 `vm.label` calls, 2 `console.log`, 3 redundant `vm.deal` |
| Missing Tests | 16 | 5 missing return value checks, 4 state assertions, 4 event assertions, 3 removed `assertEq` with redundant coverage |
| Fuzzing Targets | 7 | 3 liquidation path functions, 2 interest calculation, 2 oracle price handling |
**Key decisions:**
- `calculateInterest` (CC=11, reachable via `borrow()`) → **Fuzzing** — test removed `assertApproxEqRel` and still passed, meaning the interest calculation has untested edge cases in a complex, exposed function
- `vm.label(address(pool), "pool")` → **False positive** — cosmetic labeling for trace output
- `assertEq(token.balanceOf(user), expectedBalance)` removed and test passes → **Missing test** — the balance check was the only assertion verifying the transfer succeeded
plugins/trailmark/skills/graph-evolution/SKILL.md
+291
View File
@@ -0,0 +1,291 @@
---
name: graph-evolution
description: >
Compares Trailmark code graphs at two source code snapshots (git commits,
tags, or directories) to surface security-relevant structural changes.
Detects new attack paths, complexity shifts, blast radius growth, taint
propagation changes, and privilege boundary modifications that text diffs
miss. Use when comparing code between commits or tags, analyzing structural
evolution, detecting attack surface growth, reviewing what changed between
audit snapshots, or finding security-relevant changes that text diffs miss.
---
# Graph Evolution
Builds Trailmark code graphs at two source snapshots and computes a
structural diff. Surfaces security-relevant changes that text-level
diffs miss: new attack paths, complexity shifts, blast radius growth,
taint propagation changes, and privilege boundary modifications.
## When to Use
- Comparing two git refs to understand what structurally changed
- Auditing a range of commits for security-relevant evolution
- Detecting new attack paths created by code changes
- Finding functions whose blast radius or complexity grew silently
- Identifying taint propagation changes across refactors
- Pre-release structural comparison (tag-to-tag or branch-to-branch)
## When NOT to Use
- Line-level code review (use `differential-review` for text-diff analysis)
- Single-snapshot analysis (use the `trailmark` skill directly)
- Diagram generation from a single snapshot (use the `diagramming-code` skill)
- Mutation testing triage (use the `genotoxic` skill)
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "We just need the structural diff, skip pre-analysis" | Without pre-analysis, you miss taint changes, blast radius growth, and privilege boundary shifts | Run `engine.preanalysis()` on both snapshots |
| "Text diff covers what changed" | Text diffs miss new attack paths, transitive complexity shifts, and subgraph membership changes | Use structural diff to complement text diff |
| "Only added nodes matter" | Removed security functions and shifted privilege boundaries are equally dangerous | Review removals and modifications, not just additions |
| "Low-severity structural changes can be ignored" | INFO-level changes (dead code removal) can mask removed security checks | Classify every change, review removals for replaced functionality |
| "One snapshot's graph is enough for comparison" | Single-snapshot analysis can't detect evolution — you need both before and after | Always build and export both graphs |
| "Tool isn't installed, I'll compare manually" | Manual comparison misses what graph analysis catches | Install trailmark first |
---
## Prerequisites
**trailmark** must be installed. If `uv run trailmark` fails, run:
```bash
uv pip install trailmark
```
**DO NOT** fall back to "manual comparison" or reading source files as a
substitute for running trailmark. The tool must be installed and used
programmatically. If installation fails, report the error.
---
## Quick Start
```bash
# Compare two git refs (e.g., tags, branches, commits)
# 1. Build graphs at each snapshot
# 2. Run pre-analysis on both
# 3. Compute structural diff
# 4. Generate report
# Step-by-step: see Workflow below
```
---
## Decision Tree
```
├─ Need to understand what each metric means?
│ └─ Read: references/evolution-metrics.md
│
├─ Need the report output format?
│ └─ Read: references/report-format.md
│
├─ Already have two graph JSON exports?
│ └─ Jump to Phase 3 (run graph_diff.py directly)
│
└─ Starting from two git refs?
└─ Start at Phase 1
```
---
## Workflow
```
Graph Evolution Progress:
- [ ] Phase 1: Create snapshots (git worktrees)
- [ ] Phase 2: Build graphs + pre-analysis on both snapshots
- [ ] Phase 3: Compute structural diff
- [ ] Phase 4: Interpret diff and generate report
- [ ] Phase 5: Clean up worktrees
```
### Phase 1: Create Snapshots
Use git worktrees to get clean copies of each ref without disturbing
the working tree.
```bash
# Create temp directories for worktrees
BEFORE_DIR=$(mktemp -d)
AFTER_DIR=$(mktemp -d)
# Create worktrees (run from repo root)
git worktree add "$BEFORE_DIR" {before_ref}
git worktree add "$AFTER_DIR" {after_ref}
```
If comparing two directories instead of git refs, skip this phase and
use the directory paths directly in Phase 2.
### Phase 2: Build Graphs and Run Pre-Analysis
Build Trailmark graphs for both snapshots and run pre-analysis on each.
Pre-analysis computes blast radius, taint propagation, privilege
boundaries, and entrypoint enumeration.
```python
import json
from trailmark.query.api import QueryEngine
def build_and_export(target_dir, language, output_path):
"""Build graph, run pre-analysis, export JSON."""
engine = QueryEngine.from_directory(target_dir, language=language)
engine.preanalysis()
json_str = engine.to_json()
with open(output_path, "w") as f:
f.write(json_str)
return engine.summary()
import tempfile, os
work_dir = tempfile.mkdtemp(prefix="trailmark_evolution_")
before_json = os.path.join(work_dir, "before_graph.json")
after_json = os.path.join(work_dir, "after_graph.json")
before_summary = build_and_export(
"{before_dir}", "{lang}", before_json
)
after_summary = build_and_export(
"{after_dir}", "{lang}", after_json
)
```
Verify both graphs built successfully by checking the summary output.
If either fails, check that the language parameter matches the codebase
and that trailmark supports all file types present.
### Phase 3: Compute Structural Diff
Run the diff script on the two exported JSON files (using the same
`work_dir` from Phase 2):
```bash
uv run {baseDir}/scripts/graph_diff.py \
--before "{before_json}" \
--after "{after_json}" > "{work_dir}/evolution_diff.json"
```
The output JSON contains:
| Key | Contents |
|-----|----------|
| `summary_delta` | Changes in node/edge/entrypoint counts |
| `nodes.added` | New functions, classes, methods |
| `nodes.removed` | Deleted functions, classes, methods |
| `nodes.modified` | Functions with changed CC, params, return type, span |
| `edges.added` | New call/inheritance/import relationships |
| `edges.removed` | Deleted relationships |
| `subgraphs` | Per-subgraph membership changes (tainted, high_blast_radius, etc.) |
### Phase 4: Interpret Diff and Generate Report
Read the diff JSON and generate a security-focused markdown report.
See [references/report-format.md](references/report-format.md) for
the full template.
**Interpretation priorities (highest to lowest):**
1. **New tainted paths** — nodes entering the `tainted` subgraph,
especially if they also appear in added edges targeting sensitive
functions
2. **Privilege boundary changes** — new or removed trust transitions
3. **Attack surface growth** — new entrypoints, especially
`untrusted_external`
4. **Blast radius increases** — nodes entering `high_blast_radius`
5. **Complexity spikes** — CC increases > 3 on tainted or
entrypoint-reachable nodes
6. **Structural additions** — new nodes and edges (review needed)
7. **Structural removals** — verify removed security functions were
replaced
Cross-reference structural changes with `git diff {before_ref}..{after_ref}`
to add source-level context to findings.
**Severity classification:**
| Severity | Structural Signal |
|----------|------------------|
| CRITICAL | New tainted path to sensitive function, removed auth boundary |
| HIGH | New entrypoint + high blast radius, large CC increase on tainted node |
| MEDIUM | New trust-boundary-crossing edges, moderate CC increase |
| LOW | Added nodes without entrypoint reachability |
| INFO | Dead code removal, complexity reductions |
For detailed metric definitions, see
[references/evolution-metrics.md](references/evolution-metrics.md).
### Phase 5: Clean Up
Remove git worktrees after the report is written:
```bash
git worktree remove "{before_dir}"
git worktree remove "{after_dir}"
```
---
## Diff Script Reference
```
uv run {baseDir}/scripts/graph_diff.py [OPTIONS]
```
| Argument | Default | Description |
|----------|---------|-------------|
| `--before` | required | Path to the "before" graph JSON |
| `--after` | required | Path to the "after" graph JSON |
| `--indent` | `2` | JSON output indentation |
Input format: Trailmark JSON exports from `engine.to_json()`.
Output: JSON structural diff to stdout.
---
## Quality Checklist
Before delivering the report:
- [ ] Both graphs built successfully (check summaries)
- [ ] Pre-analysis ran on both snapshots
- [ ] Structural diff computed (non-empty diff JSON)
- [ ] All subgraph changes interpreted (tainted, blast radius, etc.)
- [ ] Critical findings include evidence (node IDs, edge diffs)
- [ ] Severity levels assigned to all findings
- [ ] Source-level context added via git diff cross-reference
- [ ] Worktrees cleaned up (or temp dirs removed)
- [ ] Report written to `GRAPH_EVOLUTION_*.md`
---
## Integration
**trailmark skill:**
Phase 2 uses the trailmark API for graph building and pre-analysis.
All trailmark query patterns work on either snapshot's engine.
**differential-review skill:**
Use graph-evolution for structural analysis, differential-review for
line-level code review. The two are complementary — graph-evolution
finds attack paths that text diffs miss, while differential-review
provides git blame context and micro-adversarial analysis.
**genotoxic skill:**
If graph-evolution reveals new high-CC tainted nodes, feed them to
genotoxic for mutation testing triage.
**diagramming-code skill:**
Generate before/after diagrams to visualize structural changes.
Use `call-graph` or `data-flow` diagrams focused on changed nodes.
---
## Supporting Documentation
- **[references/evolution-metrics.md](references/evolution-metrics.md)** —
What each structural metric means and why it matters for security
- **[references/report-format.md](references/report-format.md)** —
Report template, severity classification, and example findings
plugins/trailmark/skills/graph-evolution/references/evolution-metrics.md
+168
View File
@@ -0,0 +1,168 @@
# Evolution Metrics Reference
This document explains each structural metric the graph-evolution skill
tracks and why it matters for security analysis.
## Contents
- Node changes (added, removed, modified)
- Edge changes (added, removed)
- Complexity evolution
- Attack surface changes
- Blast radius shifts
- Taint propagation changes
- Privilege boundary changes
---
## Node Changes
### Added Nodes
New functions, methods, classes, or modules introduced between snapshots.
**Security relevance:**
- New code has no review history and may lack test coverage
- New public functions expand the attack surface
- New classes may introduce state management complexity
**Triage:** Cross-reference added nodes against the `after` graph's
`entrypoints` subgraph. Added nodes that are entrypoint-reachable get
highest review priority.
### Removed Nodes
Functions, methods, or classes deleted between snapshots.
**Security relevance:**
- Removed validation functions may indicate weakened security controls
- Removed error handlers can expose unhandled edge cases
- Dead code removal is generally positive (reduces attack surface)
**Triage:** Check if removed nodes had `privilege_boundary` or
`taint_propagation` annotations. If so, verify the security function
was replaced, not just deleted.
### Modified Nodes
Nodes present in both snapshots whose properties changed. Tracked
properties:
| Property | What Changed | Security Concern |
|----------|-------------|-----------------|
| `cyclomatic_complexity` | Control flow complexity | Higher CC = more paths to test |
| `parameters` | Function signature | New params may accept untrusted input |
| `return_type` | Return type annotation | Type changes can break callers |
| `line_span` | Lines of code | Significant growth may indicate added logic |
---
## Edge Changes
### Added Edges
New call relationships between functions.
**Security relevance:**
- New calls from untrusted entrypoints to sensitive functions create
attack paths that did not previously exist
- New `inherits` or `implements` edges can change polymorphic dispatch
- Cross-module calls may violate existing trust boundaries
**Triage:** For each added `calls` edge, check if `source` is in the
`tainted` subgraph and `target` handles sensitive operations.
### Removed Edges
Call relationships that no longer exist.
**Security relevance:**
- Removed validation calls may mean input is no longer checked
- Removed authorization calls can create privilege escalation
- Usually benign during refactoring, but verify removed edges
between security-relevant nodes
---
## Complexity Evolution
Tracks per-node cyclomatic complexity changes between snapshots.
**Thresholds:**
| CC Delta | Significance |
|----------|-------------|
| +1 to +3 | Minor — likely a new branch or error check |
| +4 to +9 | Moderate — new logic paths need test coverage |
| +10 or more | Major — function is becoming difficult to reason about |
| Negative | Positive — simplification usually reduces bug surface |
**Aggregate signals:**
- Mean CC increase across all modified nodes indicates codebase is
growing more complex
- Functions that crossed the CC > 10 threshold are new fuzzing
candidates (per the genotoxic skill's criteria)
---
## Attack Surface Changes
Derived from the `entrypoints` subgraph.
**New entrypoints:** Nodes that appear in the `after` entrypoints but
not `before`. Each new entrypoint is a new way external input reaches
the system.
**Removed entrypoints:** Nodes that were entrypoints in `before` but
not `after`. Usually positive (reduced surface), but verify the
functionality wasn't just moved.
**Trust level changes:** Compare entrypoint trust levels between
snapshots. A function changing from `trusted_internal` to
`untrusted_external` is a significant security event.
---
## Blast Radius Shifts
Derived from the `high_blast_radius` subgraph (nodes with 10+
downstream dependents).
**New high-blast nodes:** Nodes that entered `high_blast_radius` in
`after`. These now affect many downstream functions — bugs here have
wide impact.
**Reduced blast radius:** Nodes that left `high_blast_radius`. Usually
positive (decoupling), but verify the downstream functions weren't
orphaned.
---
## Taint Propagation Changes
Derived from the `tainted` subgraph (nodes reachable from untrusted
entrypoints).
**Newly tainted:** Nodes that entered `tainted` in `after`. These can
now be reached by untrusted input and must validate their inputs.
**De-tainted:** Nodes that left `tainted`. Usually means a trust
boundary was added or an entrypoint was removed.
**Critical combination:** Nodes that are both newly tainted AND had
their CC increase. These are the highest-priority review targets.
---
## Privilege Boundary Changes
Derived from the `privilege_boundary` subgraph (edges where trust
levels change).
**New boundary crossings:** Functions that appeared on a privilege
boundary. These are points where trust transitions happen — common
vulnerability locations.
**Removed boundaries:** Privilege boundaries that disappeared. Could
mean trust was flattened (potentially unsafe) or that the boundary
moved (needs verification).
plugins/trailmark/skills/graph-evolution/references/report-format.md
+171
View File
@@ -0,0 +1,171 @@
# Report Format Reference
Output format for graph-evolution reports. The report is a markdown file
summarizing structural changes between two code graph snapshots.
## Contents
- Report filename convention
- Section-by-section template
- Severity classification
- Example snippets
---
## Filename Convention
```
GRAPH_EVOLUTION_<project>_<before-ref>_<after-ref>.md
```
Example: `GRAPH_EVOLUTION_myapp_v1.2.0_v1.3.0.md`
---
## Report Template
```markdown
# Graph Evolution Report
**Project:** {project_name}
**Before:** {before_ref} ({before_date})
**After:** {after_ref} ({after_date})
**Language:** {language}
## Summary
| Metric | Before | After | Delta |
|--------|--------|-------|-------|
| Total nodes | N | N | +/-N |
| Functions | N | N | +/-N |
| Classes | N | N | +/-N |
| Call edges | N | N | +/-N |
| Entrypoints | N | N | +/-N |
## Critical Structural Changes
Changes with direct security implications. Each finding includes
the structural evidence and affected nodes.
### [SEVERITY] Finding title
**What changed:** Description of the structural change
**Evidence:** Node IDs, edge diffs, subgraph membership
**Security impact:** Why this matters
**Recommendation:** What to review or test
## Attack Surface Evolution
### New Entrypoints
| Node | Kind | Trust Level | File |
|------|------|------------|------|
### Removed Entrypoints
| Node | Kind | Trust Level | File |
|------|------|------------|------|
## Complexity Evolution
### Increased Complexity (CC delta > 0)
| Node | Before CC | After CC | Delta | File |
|------|-----------|----------|-------|------|
### Decreased Complexity (CC delta < 0)
| Node | Before CC | After CC | Delta | File |
|------|-----------|----------|-------|------|
## Taint Propagation Changes
### Newly Tainted Nodes
| Node | Kind | Tainted Via | File |
|------|------|-------------|------|
### De-Tainted Nodes
| Node | Kind | File |
|------|------|------|
## Blast Radius Shifts
### Nodes Entering high_blast_radius
| Node | Kind | Downstream Count | File |
|------|------|-----------------|------|
### Nodes Leaving high_blast_radius
| Node | Kind | File |
|------|------|------|
## Privilege Boundary Changes
### New Boundary Crossings
| Node | Trust Transition | File |
|------|-----------------|------|
### Removed Boundary Crossings
| Node | Trust Transition | File |
|------|-----------------|------|
## New Code (Added Nodes)
| Node | Kind | CC | File |
|------|------|----|------|
## Removed Code (Deleted Nodes)
| Node | Kind | CC | File |
|------|------|----|------|
## New Call Relationships (Added Edges)
| Source | Target | Kind |
|--------|--------|------|
## Removed Call Relationships (Deleted Edges)
| Source | Target | Kind |
|--------|--------|------|
## Methodology
- **Tool:** Trailmark graph-evolution
- **Before snapshot:** {before_ref}
- **After snapshot:** {after_ref}
- **Pre-analysis:** blast radius, taint, privilege boundaries,
entrypoints
- **Limitations:** {honest scope disclosure}
```
---
## Severity Classification
Classify structural findings by security impact:
| Severity | Criteria |
|----------|----------|
| **CRITICAL** | New tainted path to sensitive function, removed auth boundary |
| **HIGH** | New entrypoint + high blast radius, CC increase > 10 on tainted node |
| **MEDIUM** | New call edges crossing trust boundaries, moderate CC increase |
| **LOW** | Added nodes without entrypoint reachability, cosmetic changes |
| **INFO** | Dead code removal, complexity reductions, positive changes |
---
## Example: Critical Finding
```markdown
### [CRITICAL] New untrusted path to database query
**What changed:** Function `parse_user_input` (added) calls
`execute_query` (existing, tainted). This edge did not exist in the
before snapshot.
**Evidence:**
- Added edge: `parse_user_input` → `execute_query` (calls, certain)
- `execute_query` is in `high_blast_radius` (47 downstream nodes)
- `parse_user_input` is in `tainted` subgraph
- `parse_user_input` CC = 12 (above fuzzing threshold)
**Security impact:** Untrusted external input can now reach database
query execution through a complex, high-blast-radius path.
**Recommendation:**
1. Verify input validation on `parse_user_input`
2. Add parameterized query usage in `execute_query`
3. Write fuzz harness targeting `parse_user_input`
```
plugins/trailmark/skills/graph-evolution/scripts/graph_diff.py
+275
View File
@@ -0,0 +1,275 @@
# /// script
# requires-python = ">=3.12"
# ///
"""Compute structural diff between two Trailmark graph JSON exports.
Compares nodes, edges, complexity, subgraph membership, and
pre-analysis results to surface security-relevant structural changes.
"""
from __future__ import annotations
import argparse
import json
import sys
from pathlib import Path
from typing import Any
def load_graph(path: str) -> dict[str, Any]:
"""Load and validate a Trailmark JSON export."""
data = json.loads(Path(path).read_text())
for key in ("nodes", "edges"):
if key not in data:
print(f"ERROR: Missing '{key}' in {path}", file=sys.stderr)
sys.exit(1)
return data
def diff_nodes(
before: dict[str, Any],
after: dict[str, Any],
) -> dict[str, Any]:
"""Compute added, removed, and modified nodes."""
before_ids = set(before.keys())
after_ids = set(after.keys())
added = _summarize_nodes(after, after_ids - before_ids)
removed = _summarize_nodes(before, before_ids - after_ids)
modified = _find_modified(before, after, before_ids & after_ids)
return {"added": added, "removed": removed, "modified": modified}
def _summarize_nodes(
nodes: dict[str, Any],
ids: set[str],
) -> list[dict[str, Any]]:
"""Extract summary dicts for a set of node IDs."""
result = []
for nid in sorted(ids):
node = nodes[nid]
result.append(
{
"id": nid,
"name": node.get("name", ""),
"kind": node.get("kind", ""),
"file": _node_file(node),
"cyclomatic_complexity": node.get("cyclomatic_complexity"),
}
)
return result
def _node_file(node: dict[str, Any]) -> str:
"""Extract file path from a node's location."""
loc = node.get("location", {})
if isinstance(loc, dict):
return loc.get("file_path", "")
return ""
def _find_modified(
before: dict[str, Any],
after: dict[str, Any],
shared_ids: set[str],
) -> list[dict[str, Any]]:
"""Find nodes present in both with changed properties."""
modified = []
for nid in sorted(shared_ids):
b, a = before[nid], after[nid]
changes = _compare_node_properties(b, a)
if changes:
modified.append({"id": nid, "changes": changes})
return modified
def _compare_node_properties(
before: dict[str, Any],
after: dict[str, Any],
) -> dict[str, Any]:
"""Compare security-relevant properties of two node versions."""
changes: dict[str, Any] = {}
cc_b = before.get("cyclomatic_complexity")
cc_a = after.get("cyclomatic_complexity")
if cc_b != cc_a:
changes["cyclomatic_complexity"] = {
"before": cc_b,
"after": cc_a,
}
params_b = _param_signature(before)
params_a = _param_signature(after)
if params_b != params_a:
changes["parameters"] = {
"before": params_b,
"after": params_a,
}
ret_b = _return_type_str(before)
ret_a = _return_type_str(after)
if ret_b != ret_a:
changes["return_type"] = {"before": ret_b, "after": ret_a}
span_b = _line_span(before)
span_a = _line_span(after)
if span_b != span_a:
changes["line_span"] = {"before": span_b, "after": span_a}
return changes
def _param_signature(node: dict[str, Any]) -> list[str]:
"""Extract parameter names from a node."""
params = node.get("parameters", ())
if isinstance(params, (list, tuple)):
return [p.get("name", "") if isinstance(p, dict) else str(p) for p in params]
return []
def _return_type_str(node: dict[str, Any]) -> str | None:
"""Extract return type string from a node."""
rt = node.get("return_type")
if isinstance(rt, dict):
return rt.get("name")
return rt
def _line_span(node: dict[str, Any]) -> int:
"""Compute line count from a node's location."""
loc = node.get("location", {})
if isinstance(loc, dict):
start = loc.get("start_line", 0)
end = loc.get("end_line", 0)
return max(0, end - start + 1)
return 0
def diff_edges(
before: list[dict[str, Any]],
after: list[dict[str, Any]],
) -> dict[str, Any]:
"""Compute added and removed edges."""
before_set = {_edge_key(e) for e in before}
after_set = {_edge_key(e) for e in after}
added = sorted(after_set - before_set)
removed = sorted(before_set - after_set)
return {
"added": [_parse_edge_key(k) for k in added],
"removed": [_parse_edge_key(k) for k in removed],
}
def _edge_key(edge: dict[str, Any]) -> str:
"""Create a hashable key for an edge."""
src = edge.get("source", edge.get("source_id", ""))
tgt = edge.get("target", edge.get("target_id", ""))
kind = edge.get("kind", "")
return f"{src}|{tgt}|{kind}"
def _parse_edge_key(key: str) -> dict[str, str]:
"""Convert an edge key back to a dict."""
source, target, kind = key.split("|", 2)
return {"source": source, "target": target, "kind": kind}
def diff_subgraphs(
before: dict[str, list[str]],
after: dict[str, list[str]],
) -> dict[str, Any]:
"""Compute per-subgraph membership changes."""
all_names = sorted(set(before.keys()) | set(after.keys()))
changes: dict[str, Any] = {}
for name in all_names:
b_ids = set(before.get(name, []))
a_ids = set(after.get(name, []))
added = sorted(a_ids - b_ids)
removed = sorted(b_ids - a_ids)
if added or removed:
changes[name] = {"added": added, "removed": removed}
return changes
def compute_summary_delta(
before: dict[str, Any],
after: dict[str, Any],
) -> dict[str, Any]:
"""Compute deltas for summary statistics."""
b_sum = before.get("summary", {})
a_sum = after.get("summary", {})
delta: dict[str, Any] = {}
for key in ("total_nodes", "functions", "classes", "call_edges", "entrypoints"):
b_val = b_sum.get(key, 0)
a_val = a_sum.get(key, 0)
if b_val != a_val:
delta[key] = {
"before": b_val,
"after": a_val,
"delta": a_val - b_val,
}
return delta
def compute_diff(
before: dict[str, Any],
after: dict[str, Any],
) -> dict[str, Any]:
"""Compute the full structural diff between two graphs."""
return {
"summary_delta": compute_summary_delta(before, after),
"nodes": diff_nodes(
before.get("nodes", {}),
after.get("nodes", {}),
),
"edges": diff_edges(
before.get("edges", []),
after.get("edges", []),
),
"subgraphs": diff_subgraphs(
before.get("subgraphs", {}),
after.get("subgraphs", {}),
),
}
def parse_args(argv: list[str] | None = None) -> argparse.Namespace:
"""Parse command-line arguments."""
parser = argparse.ArgumentParser(
description="Structural diff between Trailmark graphs",
)
parser.add_argument(
"--before",
required=True,
help="Path to the 'before' graph JSON export",
)
parser.add_argument(
"--after",
required=True,
help="Path to the 'after' graph JSON export",
)
parser.add_argument(
"--indent",
type=int,
default=2,
help="JSON output indentation (default: 2)",
)
return parser.parse_args(argv)
def main(argv: list[str] | None = None) -> None:
"""Entry point: load graphs, compute diff, print JSON."""
args = parse_args(argv)
before = load_graph(args.before)
after = load_graph(args.after)
diff = compute_diff(before, after)
print(json.dumps(diff, indent=args.indent))
if __name__ == "__main__":
main()
plugins/trailmark/skills/mermaid-to-proverif/SKILL.md
+461
View File
@@ -0,0 +1,461 @@
---
name: mermaid-to-proverif
description: "Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif formal verification models (.pv files). Use when generating a ProVerif model, formally verifying a protocol, converting a Mermaid diagram to ProVerif, verifying protocol security properties (secrecy, authentication, forward secrecy), checking for replay attacks, or producing a .pv file from a sequence diagram."
---
# Mermaid to ProVerif
Reads a Mermaid `sequenceDiagram` describing a cryptographic protocol and
produces a ProVerif model (`.pv` file) that can be passed directly to the
ProVerif verifier.
**Tools used:** Read, Write, Grep, Glob.
The typical input is the output of the `crypto-protocol-diagram` skill — a
Mermaid `sequenceDiagram` annotated with cryptographic operations (`Sign`,
`Verify`, `DH`, `HKDF`, `Enc`, `Dec`, etc.) and message arrows.
## When to Use
- User asks to formally verify a cryptographic protocol described as a Mermaid sequenceDiagram
- User wants to generate a ProVerif model (.pv file) from a protocol diagram
- User wants to prove secrecy, authentication, or forward secrecy properties
- Input is the output of the `crypto-protocol-diagram` skill
## When NOT to Use
- No Mermaid sequenceDiagram exists yet — use `crypto-protocol-diagram` first to generate one
- User wants to verify properties of non-cryptographic systems (state machines, access control)
- User wants to run ProVerif on an existing .pv file — just run `proverif model.pv` directly
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "Reachability queries are just busywork" | If events aren't reachable, all other query results are meaningless | Always add reachability queries first as a sanity check |
| "Public channels are fine for all messages" | Private channels for internal state prevent false attacks | Use private channels for intra-process state threading |
| "I'll skip the forward secrecy test" | Ephemeral keys demand forward secrecy verification | Add the ForwardSecrecyTest process whenever the diagram shows ephemeral keys |
| "Unused declarations are harmless" | ProVerif may report spurious results from orphan declarations | Clean up all unused types, functions, and events |
| "The model compiles, so it's correct" | A compiling model can have dead receives, type mismatches, or impossible guards that make queries vacuously true | Validate reachability before trusting any security query |
| "I don't need to check the example first" | The example defines the expected output quality bar | Study `examples/simple-handshake/` before working on unfamiliar protocols |
---
## Workflow
```
ProVerif Model Progress:
- [ ] Step 1: Parse participants and channels
- [ ] Step 2: Inventory cryptographic operations
- [ ] Step 3: Declare types, functions, and equations
- [ ] Step 4: Identify and declare events
- [ ] Step 5: Formulate security queries
- [ ] Step 6: Write participant processes
- [ ] Step 7: Write main process and finalize
- [ ] Step 8: Verify and deliver
```
### Step 1: Parse Participants and Channels
From the Mermaid diagram:
1. Extract every `participant` or `actor` declaration. Each becomes a
ProVerif process.
2. Count message arrows (`->>`, `-->>`, `-x`, `--x`). Each distinct
`A ->> B: label` creates a communication step on a channel.
3. Decide channel model:
- **Public channel** for any message sent over the network before a
secure channel is established (e.g., ClientHello, ephemeral keys,
ciphertext to be decrypted by the peer).
- **Private channel** only for internal state threading within a single
party process (not for cross-party messages).
- Default: declare one shared public channel `c` for all cross-party
messages. Add per-flow channels only when two distinct parallel sessions
must be independent.
```proverif
free c: channel.
```
### Step 2: Inventory Cryptographic Operations
Walk through every `Note over` annotation and message label. Build a list of
all distinct operations used. Map each to a ProVerif declaration category:
| Mermaid annotation | ProVerif category |
|--------------------|-------------------|
| `keygen() → sk, pk` | New name (`new sk`), public key derived via function |
| `DH(sk_A, pk_B)` | DH function or `exp` with group |
| `Sign(sk, msg) → σ` | Signature function |
| `Verify(pk, msg, σ)` | Equation or destructor |
| `Enc(key, msg) → ct` | Symmetric or asymmetric encryption function |
| `Dec(key, ct) → msg` | Destructor (equation) |
| `HKDF(ikm, info) → k` | PRF/KDF function |
| `HMAC(key, msg) → tag` | MAC function |
| `H(msg) → digest` | Hash function |
| `Commit(v, r) → C` | Commitment function |
| `Open(C, v, r)` | Commitment equation |
Consult [references/crypto-to-proverif-mapping.md](references/crypto-to-proverif-mapping.md)
for exact ProVerif syntax for each.
### Step 3: Declare Types, Functions, and Equations
Build the cryptographic preamble in this order:
1. **Types** — declare custom types used to distinguish key material:
```proverif
type key.
type pkey. (* public key *)
type skey. (* secret key *)
type nonce.
```
2. **Constants** — for fixed strings used as domain separators or labels:
```proverif
const msg1_label: bitstring.
const msg2_label: bitstring.
const info_session_key: bitstring.
```
3. **Functions** — constructors and destructors. Destructors use inline `reduc`
so that the process aborts on verification or decryption failure:
```proverif
(* Asymmetric encryption *)
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring
reduc forall m: bitstring, k: skey;
adec(aenc(m, pk(k)), k) = m.
fun pk(skey): pkey.
(* Symmetric encryption / AEAD *)
fun aead_enc(bitstring, key): bitstring.
fun aead_dec(bitstring, key): bitstring
reduc forall m: bitstring, k: key;
aead_dec(aead_enc(m, k), k) = m.
(* Digital signatures — verify returns the message on success, aborts on failure *)
fun sign(bitstring, skey): bitstring.
fun verify(bitstring, bitstring, pkey): bitstring
reduc forall m: bitstring, k: skey;
verify(sign(m, k), m, pk(k)) = m.
(* KDF — first arg is key (from DH), second is bitstring (info/context) *)
fun hkdf(key, bitstring): key.
(* MAC *)
fun mac(bitstring, key): bitstring.
(* Hash *)
fun hash(bitstring): bitstring.
(* DH *)
fun dh(skey, pkey): key.
fun dhpk(skey): pkey.
(* Serialization — ProVerif is strongly typed: pkey cannot appear
* where bitstring is expected. Use these to build signed payloads. *)
fun pkey2bs(pkey): bitstring.
fun concat(bitstring, bitstring): bitstring.
```
4. **Equations** — algebraic identities on constructors only (not on destructors,
which already have their rewrite rules inline):
```proverif
equation forall sk_a: skey, sk_b: skey;
dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a)).
```
Only declare what the diagram actually uses. Do not add functions for
operations not present.
### Step 4: Identify and Declare Events
Events mark security-relevant moments in the protocol execution. Extract them
by identifying:
- **Begin events** (`event beginRole(params)`): triggered immediately before a
party sends a message that depends on a long-term identity commitment (e.g.,
right before sending a signed message or a MAC'd message).
- **End events** (`event endRole(params)`): triggered immediately after a party
successfully verifies the peer's identity (e.g., after `Verify(...)` or MAC
check passes, session key confirmed).
- **Secrecy markers**: any key or nonce that should remain unknown to the
attacker after the handshake.
```proverif
event beginI(pkey, pkey). (* pk_I, pk_R — fired before sending the signed message *)
event endI(pkey, pkey, key). (* pk_I, pk_R, session_key — fired after accepting *)
event beginR(pkey, pkey).
event endR(pkey, pkey, key).
```
Parameters should uniquely identify the session: the parties' public keys,
plus the session key or a transcript hash.
### Step 5: Formulate Security Queries
Write one query per security property. Choose from:
**Reachability (always add first — structural sanity check):**
Verify that the success events are actually reachable. If ProVerif reports any
of these as `false`, the model has a structural bug (dead receive, type mismatch,
impossible guard) and no other query result should be trusted. Once the model
is validated, comment them out if they slow down the main property checks:
```proverif
(* Sanity: both endpoints must be reachable — comment out once validated. *)
(*
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).
*)
```
**Secrecy** (key not derivable by attacker):
Declare a private free name and encrypt it under the session key. The attacker
knowing `private_I` is equivalent to breaking the session key:
```proverif
free private_I: bitstring [private].
(* In process, after deriving sk_session: *)
out(c, aead_enc(private_I, sk_session));
(* Query: *)
query attacker(private_I).
```
**Weak authentication** (if B accepted, A ran at some point with matching
params — does not prevent replay):
```proverif
query pk_i: pkey, pk_r: pkey, k: key;
event(endR(pk_i, pk_r, k)) ==> event(beginI(pk_i, pk_r)).
```
**Injective authentication** (prevents replay — each B-accept corresponds to
a distinct A-run):
```proverif
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endR(pk_i, pk_r, k)) ==>
inj-event(beginI(pk_i, pk_r)).
```
**Forward secrecy**: add a `ForwardSecrecyTest` process to the main process
that leaks both long-term secret keys to the attacker, then check that a past
session key remains secret. Pair it with a `free fs_witness: key [private]`
declaration and `query attacker(fs_witness)`. See
[references/security-properties.md](references/security-properties.md) →
Forward Secrecy, and the worked example in
`examples/simple-handshake/sample-output.pv`.
Choose the strongest applicable query for each property. See
[references/security-properties.md](references/security-properties.md) for
the full decision tree.
### Step 6: Write Participant Processes
Write one `let` process per participant. Structure each process to mirror the
Mermaid diagram step-by-step, in order.
**Template for a two-party protocol:**
```proverif
let Initiator(sk_I: skey, pk_R: pkey) =
(* Step: generate ephemeral key *)
new ek_I: skey;
let epk_I = dhpk(ek_I) in
(* Step: sign and send msg1 — pkey2bs casts pkey to bitstring *)
let sig_I = sign(concat(msg1_label, pkey2bs(epk_I)), sk_I) in
event beginI(pk(sk_I), pk_R);
out(c, (epk_I, sig_I));
(* Step: receive msg2 *)
in(c, (epk_R: pkey, sig_R: bitstring));
(* Step: verify responder signature — destructor aborts on failure *)
let transcript = concat(pkey2bs(epk_I), pkey2bs(epk_R)) in
let _ = verify(sig_R, concat(msg2_label, transcript), pk_R) in
(* Step: derive session key *)
let dh_val = dh(ek_I, epk_R) in
let sk_session = hkdf(dh_val, concat(info_session_key, transcript)) in
event endI(pk(sk_I), pk_R, sk_session);
(* Secrecy witness: encrypt private_I under the session key.
* Declared as: free private_I: bitstring [private].
* The query attacker(private_I) checks the attacker cannot derive it. *)
out(c, aead_enc(private_I, sk_session)).
```
**Rules for writing processes:**
- Each `A ->> B: msg_contents` in the diagram becomes:
- `out(c, msg_contents)` in A's process
- `in(c, x)` (with matching destructuring) in B's process
- Each `Note over A: op → result` becomes a `let result = op in` binding
- Each `Note over A: Verify(...)` becomes a `let _ = verify(...) in`
binding (the destructor aborts on failure — no explicit else needed,
modeling abort)
- Use `alt` blocks in the diagram as `if/then/else` in the process
- Long-term keys are process parameters; ephemeral values use `new`
**N-party or MPC protocols:** write one process per distinct role. For
threshold protocols, write a single role process and replicate it `!N` times
in the main process.
### Step 7: Write Main Process and Finalize
The main process:
1. Generates long-term keys with `new`
2. Publishes public keys to the attacker via `out(c, pk(sk))`
3. Runs participant processes in parallel under replication (`!`) to allow
multiple sessions
4. Optionally leaks long-term keys for forward-secrecy analysis
```proverif
process
new sk_I: skey; let pk_I = pk(sk_I) in out(c, pk_I);
new sk_R: skey; let pk_R = pk(sk_R) in out(c, pk_R);
(
!Initiator(sk_I, pk_R)
| !Responder(sk_R, pk_I)
)
```
Place the full file in this order:
```
(* 1. Channel declarations (free c: channel. / free ch: channel [private].) *)
(* 2. noselect directives (if needed for termination) *)
(* 3. Type declarations *)
(* 4. Constants *)
(* 5. Function declarations *)
(* 6. Equations (algebraic identities on constructors only) *)
(* 7. Table declarations *)
(* 8. Events *)
(* 9. Queries *)
(* 10. Let processes *)
(* 11. Main process *)
```
### Step 8: Verify and Deliver
Before writing the file:
- [ ] Every participant in the diagram has a matching `let` process
- [ ] Every `out(c, ...)` has a matching `in(c, ...)` on the other side with
compatible types
- [ ] Every function used in a process is declared in the preamble
- [ ] Every destructor uses inline `reduc` (not a separate `equation` block)
- [ ] Every event in a query is declared and triggered in a process
- [ ] Long-term public keys are output to channel `c` in the main process
(attacker can see them — that is the Dolev-Yao model)
- [ ] No unused declarations (clean up anything added speculatively)
- [ ] If `table` declarations are present: every `insert T(...)` has a
corresponding `get T(...)` with compatible column types and matching
pattern constraints (`=key` vs bare name)
- [ ] If `noselect` is used: its tuple structure matches the actual message
shapes sent on `c` (e.g., pairs → `mess(c, (x, y))`)
- [ ] If the Key Exposure Oracle pattern is used: `event key_exposed(sk_type)`
is declared, the oracle `in(c, guess: sk_type); if pk(guess) = pk_new then
event key_exposed(guess)` appears at the end of the process that holds the
secret, and the query is `query x: sk_type; event(key_exposed(x))`
**Write the model to a `.pv` file.** Choose a filename from the protocol name,
e.g. `noise-xx-handshake.pv` or `x3dh-key-agreement.pv`.
After writing, print a brief summary:
```
Protocol: <Name>
Output: <filename>
Queries: <list each query and what property it tests>
Assumptions: <list modeling decisions and simplifications>
```
---
## Decision Tree
```
├─ No Mermaid diagram provided?
│ └─ Ask the user: "Please provide the Mermaid sequenceDiagram,
│ or run the crypto-protocol-diagram skill first."
│
├─ Diagram uses DH (not just symmetric crypto)?
│ └─ Use dh/dhpk with commutativity equation
│ See references/crypto-to-proverif-mapping.md → DH section
│
├─ Diagram uses asymmetric signatures (Sign/Verify)?
│ └─ Use sign/verify with inline reduc (not equation)
│ verify returns the message on success; let _ = verify(...) in to abort on failure
│ Distinguish signing key (skey) from verification key (pkey)
│
├─ Diagram has an "alt" block (abort path)?
│ └─ Model as if/then only — the else branch aborts (process terminates)
│ Do NOT add out(c, error_message) unless the diagram shows it
│
├─ Protocol has N > 2 parties?
│ └─ Write one process per role, use ! for replication
│ Pass participant index as a parameter if roles differ by index only
│
├─ Forward secrecy requested?
│ └─ Add a ForwardSecrecy variant in the main process that leaks
│ long-term sk after session; add secrecy query for past session_key
│ See references/security-properties.md → Forward Secrecy
│
├─ Type-checker rejects the model?
│ └─ ProVerif is typed: check every function arg type matches declaration.
│ bitstring is the catch-all; key/pkey/skey/nonce are stricter.
│ Cast with explicit constructors when needed.
│
├─ Protocol has cross-process state coordination (e.g., one process must wait
│ for another to record acceptance before proceeding)?
│ └─ Use ProVerif tables (table/insert/get)
│ See references/proverif-syntax.md → Tables
│
├─ Verification does not terminate after several minutes?
│ └─ Add noselect directive matching the message tuple structure on c
│ See references/proverif-syntax.md → noselect
│
├─ Protocol generates a private-type key (type sk [private]) that is never
│ output directly but whose secrecy should be verified?
│ └─ Use the Key Exposure Oracle pattern instead of query attacker(sk)
│ See references/security-properties.md → Key Exposure Oracle
│
└─ Unsure which security properties to verify?
└─ Default set: secrecy of session key + injective authentication
(both directions). Add forward secrecy if diagram shows ephemeral keys.
```
---
## Example
`examples/simple-handshake/` contains a worked example:
- **`diagram.md`** — Mermaid sequenceDiagram for a two-party authenticated key
exchange (X25519 DH + Ed25519 signing + HKDF)
- **`sample-output.pv`** — exact ProVerif model the skill should produce,
with secrecy and injective authentication queries
Study this before working on an unfamiliar protocol.
---
## Supporting Documentation
- **[references/crypto-to-proverif-mapping.md](references/crypto-to-proverif-mapping.md)** —
Mapping table from Mermaid cryptographic annotations to ProVerif function
declarations, equations, and process patterns
- **[references/proverif-syntax.md](references/proverif-syntax.md)** —
ProVerif language reference: types, functions, equations, processes, events,
queries, and common pitfalls
- **[references/security-properties.md](references/security-properties.md)** —
Decision guide for choosing the right queries: secrecy, authentication
(weak vs injective), forward secrecy, unlinkability, and how to model them
plugins/trailmark/skills/mermaid-to-proverif/examples/simple-handshake/diagram.md
+48
View File
@@ -0,0 +1,48 @@
# Simple Authenticated Key Exchange Sequence Diagram
```mermaid
sequenceDiagram
participant I as Initiator
participant R as Responder
rect rgb(230, 240, 255)
Note over I,R: Setup (out-of-band key registration)
Note over I: keygen() → sk_I, pk_I
Note over R: keygen() → sk_R, pk_R
end
rect rgb(230, 255, 230)
Note over I,R: Handshake
Note over I: keygen() → ek_I, epk_I
Note over I: sig_I = Sign(sk_I, "msg1" || epk_I)
I->>R: epk_I || sig_I
Note over R: Verify(pk_I, "msg1" || epk_I, sig_I)
Note over R: keygen() → ek_R, epk_R
Note over R: transcript = epk_I || epk_R
Note over R: sig_R = Sign(sk_R, "msg2" || transcript)
Note over R: dh = DH(ek_R, epk_I)
Note over R: sk_R = HKDF(dh || transcript, info="session-key-v1")
R-->>I: epk_R || sig_R
Note over I: Verify(pk_R, "msg2" || epk_I || epk_R, sig_R)
Note over I: dh = DH(ek_I, epk_R)
Note over I: sk_I = HKDF(dh || transcript, info="session-key-v1")
end
rect rgb(255, 240, 200)
Note over I,R: Application Data
I->>R: ChaCha20Poly1305(sk, nonce, plaintext)
end
alt signature verification failure
R-->>I: abort(INVALID_SIGNATURE)
end
```
## Protocol Summary
- **Parties:** Initiator (I), Responder (R)
- **Round complexity:** 2 messages (1 round-trip)
- **Key primitives:** X25519 (DH), Ed25519 (Sign/Verify), HKDF-SHA256, ChaCha20-Poly1305
- **Authentication:** Mutual — both parties sign their ephemeral key; both verify the peer's signature
- **Forward secrecy:** Yes — session key derived exclusively from ephemeral DH; long-term keys only used for authentication
- **Notable:** Long-term keys registered out-of-band; no PKI or certificate exchange in-protocol
plugins/trailmark/skills/mermaid-to-proverif/examples/simple-handshake/sample-output.pv
+229
View File
@@ -0,0 +1,229 @@
(* Simple Authenticated Key Exchange — ProVerif Model
*
* Protocol: Two-party authenticated key exchange
* Parties: Initiator (I), Responder (R)
* Crypto: X25519 DH, Ed25519 signatures, HKDF, AEAD
*
* Generated from: examples/simple-handshake/diagram.md
*
* Security queries verified:
* Q1 Reachability: both end events are reachable
* Q2 Session key secrecy: attacker cannot learn the session key
* Q3 Injective auth (R): each R-accept maps to a unique I-run
* Q4 Injective auth (I): each I-accept maps to a unique R-run
*
* Note on forward secrecy: model a Compromise process that outputs sk_I
* and sk_R on c, add it to the main process, and re-run Q2. If Q2 still
* holds, the session key depends only on ephemeral DH material.
*)
(* ── Types ─────────────────────────────────────────────────────────────── *)
type key. (* symmetric session key *)
type skey. (* secret key (signing / DH scalar) *)
type pkey. (* public key (DH point / verification key) *)
(* ── Channel ────────────────────────────────────────────────────────────── *)
free c: channel. (* public network — Dolev-Yao attacker reads and writes freely *)
(* ── Domain-separation constants ────────────────────────────────────────── *)
const msg1_label: bitstring. (* bound into Initiator's signature *)
const msg2_label: bitstring. (* bound into Responder's signature *)
const info_session_key: bitstring. (* HKDF info tag *)
(* ── Functions ──────────────────────────────────────────────────────────── *)
(* DH key derivation and shared-secret computation *)
fun dhpk(skey): pkey.
fun dh(skey, pkey): key.
(* Public/verification key derivation from secret key *)
fun pk(skey): pkey.
(* Signatures.
* sign is a constructor (always succeeds).
* verify is a destructor: verify(sig, msg, vk) returns msg if sig = sign(msg, sk)
* and vk = pk(sk); otherwise the binding fails and the process aborts.
* This models the "abort on invalid signature" behaviour. *)
fun sign(bitstring, skey): bitstring.
fun verify(bitstring, bitstring, pkey): bitstring
reduc forall m: bitstring, k: skey;
verify(sign(m, k), m, pk(k)) = m.
(* HKDF: keying material (key) + context (bitstring) → derived key *)
fun hkdf(key, bitstring): key.
(* AEAD (ChaCha20-Poly1305 abstracted).
* aead_enc is a constructor; aead_dec is a destructor that only succeeds
* when the ciphertext was produced with the same key. *)
fun aead_enc(bitstring, key): bitstring.
fun aead_dec(bitstring, key): bitstring
reduc forall m: bitstring, k: key;
aead_dec(aead_enc(m, k), k) = m.
(* Serialization helpers.
* ProVerif is strongly typed: pkey cannot be passed directly where bitstring
* is expected. pkey2bs() casts a public key to bitstring for use in signed
* payloads and KDF input. concat() builds a single bitstring from two. *)
fun pkey2bs(pkey): bitstring.
fun concat(bitstring, bitstring): bitstring.
(* ── Equations ──────────────────────────────────────────────────────────── *)
(* DH commutativity: both parties derive the same shared secret *)
equation forall a: skey, b: skey;
dh(a, dhpk(b)) = dh(b, dhpk(a)).
(* ── Events ─────────────────────────────────────────────────────────────── *)
(* beginI: Initiator commits to a session before sending the signed msg1.
* Parameters: (pk_I, pk_R) — party identities for this session. *)
event beginI(pkey, pkey).
(* endI: Initiator accepted — verified R's signature, derived session key.
* Parameters: (pk_I, pk_R, session_key) *)
event endI(pkey, pkey, key).
(* beginR: Responder commits after verifying msg1, before sending msg2.
* Parameters: (pk_I, pk_R) *)
event beginR(pkey, pkey).
(* endR: Responder accepted — sent signed reply, derived session key.
* Parameters: (pk_I, pk_R, session_key) *)
event endR(pkey, pkey, key).
(* ── Secrecy witnesses ───────────────────────────────────────────────────── *)
(* Each party encrypts a private constant under the session key.
* query attacker(private_I/R) checks the attacker cannot derive the
* session key (since decrypting the ciphertext requires it). *)
free private_I: bitstring [private].
free private_R: bitstring [private].
(* ── Queries ────────────────────────────────────────────────────────────── *)
(* Q1: Reachability — both end events must be reachable.
* If either returns FALSE, the model has a structural bug. *)
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).
(* Q2: Session key secrecy — attacker cannot learn private data encrypted
* under the session key, which is equivalent to key secrecy. *)
query attacker(private_I).
query attacker(private_R).
(* Q3: Injective authentication (R's view) — replay prevention.
* Each time R accepts with (pk_I, pk_R, k), a unique I-run with those
* same parameters preceded it. *)
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endR(pk_i, pk_r, k)) ==> inj-event(beginI(pk_i, pk_r)).
(* Q4: Injective authentication (I's view) *)
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endI(pk_i, pk_r, k)) ==> inj-event(beginR(pk_i, pk_r)).
(* ── Processes ──────────────────────────────────────────────────────────── *)
(* Initiator
* sk_I : long-term signing/DH secret key
* pk_R : Responder's public key (registered out-of-band)
*)
let Initiator(sk_I: skey, pk_R: pkey) =
(* Handshake: generate fresh ephemeral keypair *)
new ek_I: skey;
let epk_I = dhpk(ek_I) in
(* Sign: Sign(sk_I, "msg1" || epk_I) *)
let sig_I = sign(concat(msg1_label, pkey2bs(epk_I)), sk_I) in
(* Commit before sending the authenticated message *)
event beginI(pk(sk_I), pk_R);
(* msg1 → Responder: epk_I || sig_I *)
out(c, (epk_I, sig_I));
(* msg2 ← Responder: epk_R || sig_R *)
in(c, (epk_R: pkey, sig_R: bitstring));
(* Verify: Verify(pk_R, "msg2" || epk_I || epk_R, sig_R)
* Destructor returns the message on success; process aborts on failure. *)
let transcript = concat(pkey2bs(epk_I), pkey2bs(epk_R)) in
let _ = verify(sig_R, concat(msg2_label, transcript), pk_R) in
(* Derive session key: HKDF(DH(ek_I, epk_R), info || transcript) *)
let dh_val = dh(ek_I, epk_R) in
let sk_session = hkdf(dh_val, concat(info_session_key, transcript)) in
(* Accept *)
event endI(pk(sk_I), pk_R, sk_session);
(* Secrecy witness: encrypt private_I under the session key *)
out(c, aead_enc(private_I, sk_session));
(* Application data phase *)
new plaintext: bitstring;
out(c, aead_enc(plaintext, sk_session)).
(* Responder
* sk_R : long-term signing/DH secret key
* pk_I : Initiator's public key (registered out-of-band)
*)
let Responder(sk_R: skey, pk_I: pkey) =
(* msg1 ← Initiator: epk_I || sig_I *)
in(c, (epk_I: pkey, sig_I: bitstring));
(* Verify: Verify(pk_I, "msg1" || epk_I, sig_I) *)
let _ = verify(sig_I, concat(msg1_label, pkey2bs(epk_I)), pk_I) in
(* Generate ephemeral keypair *)
new ek_R: skey;
let epk_R = dhpk(ek_R) in
(* Compute transcript and sign: Sign(sk_R, "msg2" || epk_I || epk_R) *)
let transcript = concat(pkey2bs(epk_I), pkey2bs(epk_R)) in
let sig_R = sign(concat(msg2_label, transcript), sk_R) in
(* Commit before sending the authenticated reply *)
event beginR(pk_I, pk(sk_R));
(* Derive session key: HKDF(DH(ek_R, epk_I), info || transcript) *)
let dh_val = dh(ek_R, epk_I) in
let sk_session = hkdf(dh_val, concat(info_session_key, transcript)) in
(* msg2 → Initiator: epk_R || sig_R *)
out(c, (epk_R, sig_R));
(* Accept *)
event endR(pk_I, pk(sk_R), sk_session);
(* Secrecy witness *)
out(c, aead_enc(private_R, sk_session));
(* Receive and verify application data *)
in(c, ct: bitstring);
let _ = aead_dec(ct, sk_session) in
0.
(* ── Main Process ───────────────────────────────────────────────────────── *)
process
(* Generate long-term keypairs *)
new sk_I: skey; let pk_I = pk(sk_I) in
new sk_R: skey; let pk_R = pk(sk_R) in
(* Publish public keys — Dolev-Yao attacker knows them *)
out(c, pk_I);
out(c, pk_R);
(* Run unbounded concurrent sessions *)
(
!Initiator(sk_I, pk_R)
| !Responder(sk_R, pk_I)
)
plugins/trailmark/skills/mermaid-to-proverif/references/crypto-to-proverif-mapping.md
+387
View File
@@ -0,0 +1,387 @@
# Cryptographic Operation to ProVerif Mapping
Maps every Mermaid annotation produced by the `crypto-protocol-diagram` skill
to the corresponding ProVerif declarations and process patterns.
Use this table to build the preamble (types, functions, equations) and the
per-step process code for each participant.
---
## Key Generation
### Long-term asymmetric keypair
**Mermaid:** `Note over A: keygen() → sk_A, pk_A`
**Meaning:** Party A has a long-term signing or asymmetric encryption keypair.
**ProVerif:**
- Long-term keys are inputs to the participant process (not `new` inside).
- The secret key is a process parameter; the public key is derived.
- The main process generates the keypair and publishes the public key.
```proverif
(* Function declaration *)
fun pk(skey): pkey.
(* In main process *)
new sk_A: skey; let pk_A = pk(sk_A) in out(c, pk_A);
(* In participant process signature *)
let PartyA(sk_A: skey, pk_B: pkey) = ...
```
### Ephemeral keypair
**Mermaid:** `Note over A: keygen() → ek_A, epk_A`
**Meaning:** Party A generates a fresh single-use keypair for this session.
**ProVerif:**
- Generate with `new` inside the participant process.
- Derive the public ephemeral key from the secret ephemeral key.
```proverif
(* Function declaration *)
fun dhpk(skey): pkey.
(* In participant process *)
new ek_A: skey;
let epk_A = dhpk(ek_A) in
```
---
## Diffie-Hellman
### Two-party DH
**Mermaid:** `Note over A: dh = DH(ek_A, epk_B)`
**Meaning:** Party A computes the DH shared secret using their ephemeral
secret key and the peer's ephemeral public key.
**ProVerif:**
```proverif
(* Function declarations *)
fun dhpk(skey): pkey.
fun dh(skey, pkey): key.
(* Equation — DH commutativity *)
equation forall a: skey, b: skey;
dh(a, dhpk(b)) = dh(b, dhpk(a)).
(* In process *)
let dh_val = dh(ek_A, epk_B) in
```
**Note:** ProVerif's equation engine handles the commutativity — you only
write `dh(ek_A, epk_B)` in A's process and `dh(ek_B, epk_A)` in B's process;
the equation unifies them.
### Static-ephemeral DH (e.g., for authentication)
**Mermaid:** `Note over A: dh_se = DH(sk_A, epk_B)`
Same declaration — `dh` accepts any `skey` regardless of whether it is
long-term or ephemeral. The typing is structural.
---
## Key Derivation (KDF / HKDF / PRF)
**Mermaid:** `Note over A: sk = HKDF(dh || transcript, info="...")`
**Meaning:** Party A derives a session key from keying material and
domain-separation info.
**ProVerif:**
```proverif
(* Function declaration *)
fun hkdf(key, bitstring): key.
(* Constants for domain separation labels *)
const info_session_key: bitstring.
const info_handshake: bitstring.
(* In process — concatenate IKM and call hkdf *)
let sk_session = hkdf(dh_val, concat(info_session_key, concat(pkey2bs(epk_A), pkey2bs(epk_B)))) in
```
**Tuple vs concatenation:** Use tuples `(a, b, c)` rather than a `concat`
function when the protocol only extracts keys from HKDF (not when it computes
a MAC over the same bytes). Tuples are simpler and keep the model readable.
If the protocol chains two HKDF calls (e.g., TLS 1.3's `HKDF-Extract` +
`HKDF-Expand`), model them as two separate function applications:
```proverif
let prk = hkdf_extract(salt, ikm) in
let okm = hkdf_expand(prk, info, length_tag) in
```
---
## Digital Signatures
### Signing
**Mermaid:** `Note over A: σ = Sign(sk_A, msg)`
**ProVerif:**
```proverif
(* Function declarations *)
fun sign(bitstring, skey): bitstring.
fun pk(skey): pkey. (* verification key derived from signing key *)
(* In process *)
let sig = sign(msg, sk_A) in
```
### Verification
**Mermaid:** `Note over B: Verify(pk_A, msg, σ)`
**ProVerif:**
```proverif
(* Function declaration — returns the message on success, aborts on failure *)
fun verify(bitstring, bitstring, pkey): bitstring
reduc forall m: bitstring, k: skey;
verify(sign(m, k), m, pk(k)) = m.
(* In process — let _ = ... in aborts the branch if the signature is invalid *)
let _ = verify(sig, msg, pk_A) in
```
**Signing key vs verification key:** In ProVerif it is idiomatic to use a
single `skey` as the signing key and derive the verification key with `pk`.
Do not create a separate `vk` type unless the diagram explicitly uses
different keys for signing and verification (rare).
---
## Symmetric Encryption / AEAD
### Encryption
**Mermaid:** `Note over A: ct = Enc(key, plaintext)` or
`A ->> B: AEAD(sk, nonce, plaintext)`
**ProVerif:**
```proverif
(* Function declarations *)
fun aead_enc(bitstring, key): bitstring.
fun aead_dec(bitstring, key): bitstring
reduc forall m: bitstring, k: key;
aead_dec(aead_enc(m, k), k) = m.
(* In process *)
let ct = aead_enc(plaintext, sk_session) in
out(c, ct);
```
### Decryption
**Mermaid:** `Note over B: plaintext = Dec(key, ct)`
```proverif
(* In process *)
in(c, ct: bitstring);
let plaintext = aead_dec(ct, sk_session) in
```
**AEAD vs unauthenticated encryption:** ProVerif does not distinguish AEAD
from unauthenticated encryption at the equational level — both use `aead_enc`/`aead_dec`.
Authentication is modeled implicitly: if decryption succeeds (the equation
fires), the ciphertext was produced with the correct key. This is a standard
simplification in symbolic models.
---
## Message Authentication Codes (MAC)
**Mermaid:** `Note over A: tag = MAC(key, msg)` /
`Note over B: VerifyMAC(key, msg, tag)`
**ProVerif:**
```proverif
(* Function declaration *)
fun mac(bitstring, key): bitstring.
(* Verification: check tag equals recomputed mac *)
if mac(msg, key) = received_tag then
```
**Note:** Unlike signatures, MACs do not have a dedicated verify function.
Verification is equality-checking the recomputed value. This means:
- Both parties must hold the key (symmetric — no public-key exposure).
- Do not output the MAC key to channel `c` in the main process.
---
## Asymmetric Encryption
**Mermaid:** `Note over A: ct = AEnc(pk_B, msg)` /
`Note over B: plaintext = ADec(sk_B, ct)`
**ProVerif:**
```proverif
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring
reduc forall m: bitstring, k: skey;
adec(aenc(m, pk(k)), k) = m.
(* Encrypt *)
let ct = aenc(msg, pk_B) in out(c, ct);
(* Decrypt *)
in(c, ct: bitstring);
let msg = adec(ct, sk_B) in
```
---
## Hash Functions
**Mermaid:** `Note over A: h = H(data)` or `h = SHA256(data)`
**ProVerif:**
```proverif
fun hash(bitstring): bitstring.
(* In process *)
let h = hash(data) in
```
Hash functions are modeled as free constructors — the attacker can compute
them on any input. This is the standard symbolic model (random oracle is not
needed for most authentication properties).
---
## Commitments
**Mermaid:** `Note over A: C = Commit(value, rand)` /
`Note over B: Open(C, value, rand)` or `Verify(C, value, rand)`
**ProVerif:**
```proverif
fun commit(bitstring, bitstring): bitstring.
(* Binding: equational model — no equation needed;
opening is modeled by sending value and rand and letting
the verifier recompute the commitment *)
(* Committer *)
new r: bitstring;
let com = commit(value, r) in
out(c, com); (* send commitment *)
...
out(c, (value, r)); (* reveal *)
(* Verifier *)
in(c, (v: bitstring, r2: bitstring));
if commit(v, r2) = received_com then
```
**Hiding:** This symbolic model does not prove computational hiding. For
formal hiding proofs, use a computational tool (CryptoVerif, EasyCrypt).
---
## Nonces
**Mermaid:** `Note over A: nonce_A = random()` or `A ->> B: nonce_A`
**ProVerif:**
```proverif
new nonce_A: bitstring. (* type can also be nonce *)
out(c, nonce_A);
```
Nonces are just fresh bitstrings. Use `type nonce.` if you want to prevent
accidental type confusion, but `bitstring` is fine for simple protocols.
---
## Message Concatenation and Transcripts
**Mermaid:** `transcript = epk_I || epk_R` or `msg = A || B || C`
**ProVerif approach:**
Prefer **tuples** over a concat function:
```proverif
(* Send: pack into tuple *)
out(c, (epk_I, epk_R));
(* Receive: destructure tuple *)
in(c, (epk_I: pkey, epk_R: pkey));
```
Use a `concat` function only when the protocol computes over the raw
concatenated bytes in a way that matters (e.g., the transcript is fed to a
MAC or HKDF as a single blob, and the parts are also available separately).
In that case:
```proverif
fun concat2(bitstring, bitstring): bitstring.
fun concat3(bitstring, bitstring, bitstring): bitstring.
```
There are no equations on `concat` — it is a free constructor, which is
correct: the attacker cannot split a concatenation unless they know the
length boundaries (length-prefix models are usually out of scope for symbolic
proofs).
---
## Key Agreement Summary Table
| Mermaid annotation | ProVerif function | Equation needed? |
|-------------------|-------------------|------------------|
| `keygen() → sk, pk` | `pk(skey): pkey` | No |
| `keygen() → ek, epk` | `dhpk(skey): pkey` | No |
| `DH(ek, epk)` | `dh(skey, pkey): key` | Yes — commutativity |
| `HKDF(ikm, info)` | `hkdf(key, bitstring): key` | No |
| `Sign(sk, msg)` | `sign(bitstring, skey): bitstring` | No |
| `Verify(pk, msg, σ)` | `verify(bitstring, bitstring, pkey): bitstring` | Yes — inline `reduc` |
| `Enc(k, m)` / `Dec(k, ct)` | `aead_enc` / `aead_dec` | Yes — correctness |
| `AEnc(pk, m)` / `ADec(sk, ct)` | `aenc` / `adec` | Yes — correctness |
| `MAC(k, m)` | `mac(bitstring, key): bitstring` | No |
| `H(data)` | `hash(bitstring): bitstring` | No |
| `Commit(v, r)` | `commit(bitstring, bitstring): bitstring` | No |
| `nonce = random()` | `new nonce: bitstring` | No |
---
## Modeling Notes
### What the symbolic model captures
- Perfect correctness of cryptographic functions (equations hold exactly)
- Dolev-Yao attacker: controls the network, can read/write all public channel
messages, knows all published public keys
- Unbounded sessions via replication `!`
### What the symbolic model does NOT capture
- Computational hardness (e.g., discrete log, AES key recovery)
- Timing side-channels
- Nonce/IV reuse in AEAD (model assumes nonces are always fresh)
- Key material leakage through implementation bugs
- Computational binding/hiding of commitment schemes
For these properties, use CryptoVerif (computational) or EasyCrypt (proofs).
plugins/trailmark/skills/mermaid-to-proverif/references/proverif-syntax.md
+486
View File
@@ -0,0 +1,486 @@
# ProVerif Syntax Reference
ProVerif models cryptographic protocols in the applied pi-calculus. This
reference covers the constructs needed to translate a Mermaid sequence diagram
into a verifiable `.pv` file.
---
## File Structure
A `.pv` file must follow this order:
```
1. Channel declarations (free c: channel. / free ch: channel [private].)
2. noselect directives (if needed for termination)
3. Type declarations
4. Constants
5. Function declarations
6. Equations / Reduction rules
7. Table declarations
8. Event declarations
9. Query declarations
10. Let process definitions
11. Main process (process ...)
```
Comments: `(* this is a comment *)` — no inline `//`.
---
## Types
ProVerif is strongly typed. The base type for any untyped byte sequence is
`bitstring`. Declare custom types to prevent confusing distinct key roles:
```proverif
type key. (* symmetric key *)
type pkey. (* public key (for enc or verify) *)
type skey. (* secret key (for dec or sign) *)
type nonce. (* random nonce *)
type tag. (* MAC tag or signature *)
```
Types are structural — ProVerif does not enforce physical separation, but
type mismatches cause type errors that prevent verification.
---
## Constants
Declare fixed domain-separation labels or protocol identifiers:
```proverif
const msg1: bitstring.
const msg2: bitstring.
const info_session: bitstring.
const info_handshake: bitstring.
const info_app: bitstring.
```
---
## Functions
### Declaring Functions
```proverif
fun name(arg_type1, arg_type2, ...): return_type.
```
Functions are **constructors** by default — the attacker can apply them freely.
```proverif
fun pk(skey): pkey. (* derive public key *)
fun sign(bitstring, skey): bitstring.
fun aenc(bitstring, pkey): bitstring.
fun aead_enc(bitstring, key): bitstring.
fun mac(bitstring, key): bitstring.
fun hash(bitstring): bitstring.
fun hkdf(key, bitstring): key.
fun pkey2bs(pkey): bitstring. (* cast pkey to bitstring *)
fun concat2(bitstring, bitstring): bitstring.
fun concat3(bitstring, bitstring, bitstring): bitstring.
```
For DH:
```proverif
fun dhpk(skey): pkey. (* g^x given x *)
fun dh(skey, pkey): key. (* g^(xy) given x and g^y *)
```
### Destructors
Destructors **can fail** — they extract values only when the rewrite rule
matches. Declare them with an inline `reduc` block:
```proverif
fun adec(bitstring, skey): bitstring
reduc forall m: bitstring, k: skey;
adec(aenc(m, pk(k)), k) = m.
fun aead_dec(bitstring, key): bitstring
reduc forall m: bitstring, k: key;
aead_dec(aead_enc(m, k), k) = m.
fun verify(bitstring, bitstring, pkey): bitstring
reduc forall m: bitstring, k: skey;
verify(sign(m, k), m, pk(k)) = m.
```
`verify` returns the verified message on success; the process **aborts** (that
branch is pruned) on failure. Use it as an abort-on-failure guard:
```proverif
let _ = verify(sig_R, msg, pk_R) in
(* reaches here only if sig_R is a valid signature under pk_R *)
```
**`equation` vs `reduc` — critical distinction:**
- A standalone `equation` block applies to **constructors** — functions
declared with `fun` that the attacker can apply freely. Adding an equation
does not make the function fail on mismatch; it only enables rewriting.
- An inline `reduc` block declares the function as a **destructor** that
fails when no rewrite rule matches. This is what you want for `verify`,
`adec`, `sdec`, and any check that must abort the process on failure.
Use `equation` only for algebraic identities on constructors (e.g., DH
commutativity). Use `reduc` for all cryptographic verification and decryption.
```proverif
(* Constructor + algebraic identity — equation is correct here *)
fun dh(skey, pkey): key.
equation forall a: skey, b: skey;
dh(a, dhpk(b)) = dh(b, dhpk(a)).
```
**Note:** `bool` is not a valid return type for `fun` declarations in ProVerif.
Use `bitstring` (and return the message on success) or a custom type.
---
## Channels
All cross-party communication happens on channels:
```proverif
free c: channel. (* public channel — attacker can read and write *)
free priv_c: channel [private]. (* private channel — only declared code can use *)
```
The `free name: channel.` form declares `name` as a globally accessible
channel name. The `[private]` attribute prevents the attacker from learning
or using the channel.
For most protocol models, one public channel `c` is sufficient.
---
## Events
Events mark security-relevant points for use in authentication queries.
**Declaration:**
```proverif
event beginI(pkey, pkey). (* pk_I, pk_R — before session key is known *)
event endI(pkey, pkey, key). (* pk_I, pk_R, session_key *)
event beginR(pkey, pkey).
event endR(pkey, pkey, key).
```
**Use in process:**
```proverif
event beginI(pk(sk_I), pk_R); (* fired before sending authenticated msg *)
event endI(pk(sk_I), pk_R, sk_session); (* fired after deriving session key *)
```
---
## Queries
### Secrecy
```proverif
query attacker(session_key).
```
Succeeds (i.e., ProVerif proves the protocol secure) if the attacker cannot
derive `session_key` in any execution.
For named secrets inside a process, use `query secret session_key.` inside the
process — but `query attacker(x)` at top level is cleaner for most use cases.
### Authentication (Correspondence)
**Weak**: A ran ==> B ran (allows replay):
```proverif
query x: pkey, y: pkey, k: key;
event(endR(x, y, k)) ==> event(beginI(x, y)).
```
**Injective**: each B-accept corresponds to a unique A-run (prevents replay):
```proverif
query x: pkey, y: pkey, k: key;
inj-event(endR(x, y, k)) ==> inj-event(beginI(x, y)).
```
### Reachability (sanity check)
Verify that the "success" point of the protocol is actually reachable (rules out
vacuously true results from trivially blocked processes):
```proverif
query x: pkey, y: pkey, k: key; event(endR(x, y, k)).
```
If this query returns `false` (unreachable), the protocol model is broken —
the endpoint never executes. Note: ProVerif does not support `_` wildcards in
`query` declarations; all parameters must be bound to typed variables.
---
## Processes
### Basic Syntax
```proverif
let ProcessName(param1: type1, param2: type2) =
(* body *).
```
### Core Constructs
| Construct | Meaning |
|-----------|---------|
| `new x: T` | Generate fresh random value of type T |
| `out(c, term)` | Send term on channel c |
| `in(c, x: T)` | Receive a term of type T from channel c |
| `in(c, (x: T, y: U))` | Receive and destructure a tuple |
| `let x = term in P` | Bind term to x, continue with P |
| `let (x, y) = term in P` | Destructure tuple |
| `if t = u then P else Q` | Conditional |
| `if f(t) = true then P` | Destructor check |
| `event e(args)` | Trigger event |
| `P \| Q` | Parallel composition |
| `!P` | Replicate P (unbounded concurrent sessions) |
| `0` | Terminated process |
### Receiving and Destructuring
When a message contains multiple components separated by a comma in the
Mermaid diagram, receive as a tuple:
```proverif
in(c, (epk_R: pkey, sig_R: bitstring));
```
For concatenated values (e.g., `A || B`), model as a tuple `(a, b)` unless the
protocol computes over the concatenated bytes specifically:
```proverif
(* sender *)
out(c, (epk_R_bytes, sig_R));
(* receiver *)
in(c, (epk_R_bytes: pkey, sig_R: bitstring));
```
If the protocol requires an explicit concat (e.g., hashing a concatenation),
declare a constructor:
```proverif
fun concat(bitstring, bitstring): bitstring.
out(c, concat(epk_R_bytes, sig_R));
```
### Verification Checks
Map each `Verify(pk, msg, sig)` annotation to a `let _ = ... in` destructor
call. The destructor fails and aborts the branch when the signature is invalid:
```proverif
let _ = verify(sig_R, concat2(msg2, concat2(pkey2bs(epk_I), pkey2bs(epk_R))), pk_R) in
(* reaches here only if sig_R is a valid signature under pk_R *)
(* else: branch is pruned — models abort on invalid signature *)
```
The `else` branch is implicit; ProVerif prunes the branch on destructor failure.
### Example: Two-Party Process
```proverif
let Initiator(sk_I: skey, pk_R: pkey) =
new ek_I: skey;
let epk_I = dhpk(ek_I) in
let sig_I = sign(concat2(msg1, pkey2bs(epk_I)), sk_I) in
event beginI(pk(sk_I), pk_R); (* session key not yet known *)
out(c, (epk_I, sig_I));
in(c, (epk_R: pkey, sig_R: bitstring));
let transcript = concat2(pkey2bs(epk_I), pkey2bs(epk_R)) in
let _ = verify(sig_R, concat2(msg2, transcript), pk_R) in
let dh_val = dh(ek_I, epk_R) in
let sk_session = hkdf(dh_val, concat2(info_session, transcript)) in
event endI(pk(sk_I), pk_R, sk_session).
```
---
## Main Process
```proverif
process
new sk_I: skey; let pk_I = pk(sk_I) in out(c, pk_I);
new sk_R: skey; let pk_R = pk(sk_R) in out(c, pk_R);
(
!Initiator(sk_I, pk_R)
| !Responder(sk_R, pk_I)
)
```
**Replication `!`** allows arbitrarily many concurrent sessions — essential
for ProVerif to detect replay and man-in-the-middle attacks.
**Long-term key publication** (`out(c, pk_I)`) is mandatory: the Dolev-Yao
attacker must know public keys to attempt attacks.
---
## Tables
ProVerif tables provide shared mutable state across parallel processes — the
only built-in mechanism for synchronizing information between two `let`
processes that run concurrently.
### Declaration
```proverif
table myTable(bitstring, bitstring). (* two bitstring columns *)
table accepted(bitstring, bitstring). (* e.g. (session_id, sas) *)
table sessionKeys(bitstring, key). (* (nonce, derived_key) *)
```
### Insert a row
```proverif
insert myTable(key1, value1);
```
### Read a row
```proverif
get myTable(=key1, x: bitstring) in
(* x is bound to value1 when the first column equals key1 *)
...
```
`=key1` is a pattern-match constraint (first column must equal `key1`).
Bare names like `x: bitstring` capture the column value for use in the body.
**Semantics:** `get T(...) in P` succeeds for every matching row. If no row
matches, the process terminates (that branch is pruned). If multiple rows
match, ProVerif considers all branches.
### When to use tables
| Use tables | Use private channels |
|------------|----------------------|
| Reader determines the lookup key | Writer pushes to a known recipient |
| Fan-in: wait for multiple writers | Point-to-point signal |
| Cross-check: two processes verify agreement on a value | Callback: one-shot reply |
**Typical pattern — coordination between parallel processes:**
```proverif
table accepted(bitstring, bitstring). (* (nonce, sas) *)
(* Party A: records user acceptance *)
insert accepted(nonce_new, sas);
(* Party B: checks that A recorded acceptance before proceeding *)
get accepted(=nonce_new, =sas) in
event partyB_accept(...);
...
```
---
## `noselect` — Termination Hints
ProVerif's Horn clause solver may not terminate on models with complex tuple
patterns on the public channel. The `noselect` directive restricts which
clauses the solver selects during proof search. It is a **performance hint
only** — it does not restrict what the attacker can send or receive.
### Syntax
```proverif
noselect x: bitstring, y: bitstring; mess(c, (x, y)).
```
This tells ProVerif: "do not select clauses that derive a pair `(x, y)` from
channel `c`." The `mess(c, t)` predicate means "term `t` is on channel `c`."
### When to add
If ProVerif runs for several minutes without terminating on a model with:
- Many concurrent sessions (`!` replication on multiple processes)
- Pair-typed messages on the public channel (tuples sent over `c`)
Then add a `noselect` hint matching the tuple structure of messages on `c`.
For a protocol where all messages are pairs, use:
```proverif
noselect x: bitstring, y: bitstring; mess(c, (x, y)).
```
For triple-element messages:
```proverif
noselect x: bitstring, y: bitstring, z: bitstring; mess(c, (x, y, z)).
```
### Placement
Add immediately after channel declarations, before type and function
declarations. `noselect` is parsed as a query-level directive and must appear
before the `process` block. Placing it early (after channels) keeps it
visible alongside the declarations it constrains.
---
## Common Pitfalls
### Pitfall 1: Type Mismatch
`dh(ek_I, epk_R)` requires `ek_I: skey` and `epk_R: pkey`. If you declared
both as `bitstring`, the equation `dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a))`
cannot fire. Keep types strict.
### Pitfall 2: Missing Replication
Without `!` in the main process, ProVerif only checks single-session security.
Always use `!Initiator(...)` and `!Responder(...)` to allow multiple sessions.
### Pitfall 3: Attacker Cannot Reach End Event
If the reachability query `query event(endR(...))` returns false, the protocol
process is stuck — usually due to a type error in `in(c, ...)` destructuring
or an `if` condition that never holds. Debug by simplifying the process to just
the `out`/`in` steps without guards, confirm reachability, then add guards
back one at a time.
### Pitfall 4: Equations Cause Non-Termination
The DH commutativity equation `dh(sk_a, dhpk(sk_b)) = dh(sk_b, dhpk(sk_a))`
is convergent. Arbitrary equations with cycles (e.g., `f(f(x)) = x`) can
cause ProVerif to loop. Stick to the standard primitives in the mapping table.
### Pitfall 5: Secrets Must Be `new` Inside Process
Do not use `new` in the main process for values that should be per-session
secrets — they would be shared across all replications. Generate per-session
secrets inside the participant `let` process.
```proverif
(* WRONG — shared across all sessions *)
new sk_session: key;
!Initiator(sk_session, ...)
(* RIGHT — fresh per session *)
let Initiator(...) =
...
let sk_session = hkdf(...) in (* derived, not new *)
...
```
### Pitfall 6: Queries Reference Undeclared Events
Every event name used in a `query` must be declared with `event name(types).`.
Missing declarations cause a parse error.
plugins/trailmark/skills/mermaid-to-proverif/references/security-properties.md
+348
View File
@@ -0,0 +1,348 @@
# Security Properties in ProVerif
A guide to choosing and expressing the right security queries for a given
Mermaid sequence diagram.
---
## Decision Tree: Which Queries to Include
```
Start here for every protocol
│
├─ Does the protocol establish a shared key?
│ └─ YES → Add secrecy query for that key
│
├─ Does a party verify the peer's identity (Verify/MAC check)?
│ └─ YES → Add authentication queries (both directions if mutual auth)
│ ├─ Does the verification cover a fresh session value (nonce, epk)?
│ │ └─ YES → Use injective authentication (prevents replay)
│ └─ NO (only verifies static identity, no freshness) → Use weak auth
│
├─ Does the protocol use ephemeral keys (keygen inside the session)?
│ └─ YES → Add forward secrecy query (compromise long-term key after session)
│
├─ Does the protocol have a "challenge-response" nonce exchange?
│ └─ YES → Add injective authentication to capture that freshness
│
└─ Always add: reachability sanity check query
```
---
## 1. Secrecy
### Goal
The session key (or any sensitive value) is not learnable by the attacker,
even after observing all network traffic.
### When to add
Add whenever the Mermaid diagram contains a derived session key label (e.g.,
`sk_session`, `sk_I`, `key_data`) that should remain private.
### Query
The canonical pattern: declare a private free name and encrypt it under the
session key. The attacker learning `private_I` is equivalent to breaking the
session key, because decrypting the ciphertext requires it.
```proverif
(* Top-level declarations *)
free private_I: bitstring [private].
free private_R: bitstring [private].
(* In the Initiator process, after deriving sk_session: *)
out(c, aead_enc(private_I, sk_session));
(* In the Responder process, after deriving sk_session: *)
out(c, aead_enc(private_R, sk_session));
(* Queries *)
query attacker(private_I).
query attacker(private_R).
```
ProVerif proves `attacker(private_I)` by verifying that no derivation path
for `private_I` exists. Since `private_I` is encrypted and decryption requires
`sk_session`, this is equivalent to session key secrecy.
**Important:** `attacker(k)` cannot appear as the consequent of a
correspondence query (`event(...) ==> attacker(k)` is not valid ProVerif
syntax). Use the witness pattern above instead.
---
## 2. Authentication
### Weak Authentication
**Goal:** If B completed accepting a session with A, then A ran at some point.
Does NOT prevent replay (attacker can replay A's messages to create a second
session where B accepts).
**When to use:** Protocol has identity verification but no per-session
freshness binding (e.g., only verifies a static certificate, no nonce or
ephemeral key in the signature).
```proverif
query pk_i: pkey, pk_r: pkey, k: key;
event(endR(pk_i, pk_r, k)) ==> event(beginI(pk_i, pk_r)).
```
Note: `beginI` fires before the session key is known, so it typically
has fewer parameters than `endR`. Match the parameter list to what the
`begin` event actually receives when it fires.
### Injective Authentication
**Goal:** Each B-accept corresponds to a distinct, unique A-run. Prevents
replay attacks.
**When to use:** The signature (or MAC) covers a fresh value unique to this
session — an ephemeral key, a nonce, or a transcript hash. This is the
default for most modern protocols.
```proverif
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endR(pk_i, pk_r, k)) ==>
inj-event(beginI(pk_i, pk_r)).
```
**Note on `inj-event`:** ProVerif will report this as `true` if there is a
one-to-one correspondence. If it reports `false`, the protocol is vulnerable
to replay — investigate whether nonces or ephemeral keys are correctly bound
in the signatures.
### Mutual Authentication
For protocols where both parties authenticate each other, add queries in both
directions:
```proverif
(* Responder accepts => Initiator ran *)
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endR(pk_i, pk_r, k)) ==>
inj-event(beginI(pk_i, pk_r)).
(* Initiator accepts => Responder ran *)
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endI(pk_i, pk_r, k)) ==>
inj-event(beginR(pk_i, pk_r)).
```
### Placing Events in the Process
| Event | Where to trigger |
|-------|-----------------|
| `beginI(pk_I, pk_R)` | Just before Initiator sends the first authenticated message (the one signed with sk_I) |
| `endI(pk_I, pk_R, sk)` | Just after Initiator successfully verifies Responder's identity AND derives session key |
| `beginR(pk_I, pk_R)` | Just before Responder sends its signed reply |
| `endR(pk_I, pk_R, sk)` | Just after Responder successfully verifies Initiator's identity AND derives session key |
The session key `sk` in the event parameters binds authentication to the
specific key material established — preventing cross-session confusion attacks.
---
## 3. Forward Secrecy
### Goal
Compromise of a long-term key AFTER a session completes does not allow the
attacker to decrypt past session traffic.
### When to add
Add when:
- The Mermaid diagram shows ephemeral key generation inside the session
(e.g., `keygen() → ek_I, epk_I`)
- The session key derivation uses DH over ephemeral keys (not just static ones)
### Modeling Pattern
Leak long-term keys to the attacker and check that session key secrecy
still holds. If it does, forward secrecy is achieved because the session
key depends only on ephemeral material.
```proverif
(* In main process — leak long-term keys immediately *)
new sk_I: skey; out(c, pk(sk_I)); out(c, sk_I); (* attacker knows sk_I *)
new sk_R: skey; out(c, pk(sk_R)); out(c, sk_R); (* attacker knows sk_R *)
(!Initiator(sk_I, pk(sk_R)) | !Responder(sk_R, pk(sk_I)))
```
The existing session key secrecy query (`query attacker(private_I).`) now
tests forward secrecy: if the attacker knows both long-term keys but still
cannot derive the session key, the protocol has forward secrecy. If the
query fails, the session key depended on a long-term key.
---
## 4. Reachability (Sanity Check)
### Goal
Confirm that the success path of the protocol actually executes. A ProVerif
model with a bug (e.g., a type error causing a dead receive) may trivially
prove all security properties because the end event is never reached.
### Always add
```proverif
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).
```
Note: ProVerif does not support `_` wildcards in `query` declarations; every
parameter must be bound to a typed variable.
If ProVerif reports these as `false` (unreachable), the model has a structural
bug. Fix it before trusting any other query result.
---
## 5. Key Exposure Oracle (for `[private]` type secrets)
### Goal
Prove that the attacker cannot learn a secret key `sk` that is declared with a
private type (`type sk [private]`) and never directly output on the public
channel.
### Why `query attacker(sk)` doesn't work here
`query attacker(sk)` checks whether the attacker can derive the term `sk` from
public channel traffic. A value of a private type is never synthesised by the
attacker (the type prevents it), and if `sk` is never output, ProVerif cannot
prove the query — it would return `cannot be proved`, not `true`. The property
needs a different formulation.
### The oracle pattern
Give the attacker an explicit "guess oracle": receive an arbitrary value of
type `sk` from the public channel, then fire a `key_exposed` event if that
guess matches the known public key:
```proverif
(* Declare the sentinel event — use whatever secret key type the protocol uses *)
event key_exposed(skey).
(* Secrecy query: key_exposed must be unreachable *)
query x: skey; event(key_exposed(x)).
(* At the end of the process that generated sk_new — place after all other
* protocol steps so the oracle is only reachable on a complete run: *)
in(c, guess: skey);
if pk(guess) = pk_new then event key_exposed(guess)
else 0.
```
**How it works:**
1. The attacker submits its best guess for `sk_new` via `c`.
2. The process checks whether `pk(guess)` matches the known `pk_new`.
3. If the check succeeds, `key_exposed` fires.
4. ProVerif proves `event(key_exposed(x))` unreachable → no guess can match
the public key → `sk_new` is secret.
### When to use
Use the oracle pattern when all of these hold:
- The secret key is of a `[private]` type (e.g., `type skey [private]`) and
never output directly.
- The corresponding public key IS observable on `c` (e.g., sent in a signed
message or after key exchange).
- `query attacker(sk_new)` would return `cannot be proved` (not meaningful).
### Placement in process
Put the oracle at the very end of the process that generated `sk_new`,
**after** all other steps that depend on the secret are complete (typically
after the signature is sent). This ensures `key_exposed` is only reachable
upon protocol completion, not on every intermediate step.
---
## 6. Query Checklist by Protocol Type
### Two-party key exchange (e.g., DH-based handshake)
```proverif
(* Sanity — all parameters must be bound to typed variables *)
query pk_i: pkey, pk_r: pkey, k: key; event(endI(pk_i, pk_r, k)).
query pk_i: pkey, pk_r: pkey, k: key; event(endR(pk_i, pk_r, k)).
(* Session key secrecy — use the witness pattern, not correspondence *)
query attacker(private_I).
query attacker(private_R).
(* Mutual injective authentication *)
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endR(pk_i, pk_r, k)) ==> inj-event(beginI(pk_i, pk_r)).
query pk_i: pkey, pk_r: pkey, k: key;
inj-event(endI(pk_i, pk_r, k)) ==> inj-event(beginR(pk_i, pk_r)).
```
### Unilateral authentication (server authenticates, client does not)
```proverif
(* Sanity *)
query pk_s: pkey, k: key; event(endC(pk_s, k)).
(* Session key secrecy — use the witness pattern *)
query attacker(private_C).
(* Server authentication only — client to server direction *)
query pk_s: pkey, k: key;
inj-event(endC(pk_s, k)) ==> inj-event(beginS(pk_s, k)).
```
### Commit-reveal protocol
```proverif
(* Binding: verifier accepts only the committed value *)
query v: bitstring, r: bitstring;
event(accepted(v)) ==> event(committed(v, r)).
(* Hiding: attacker cannot learn committed value before reveal *)
query attacker(committed_value).
```
### Challenge-response authentication
```proverif
(* Freshness: each successful auth used a distinct challenge *)
query id: pkey, ch: bitstring;
inj-event(authSuccess(id, ch)) ==> inj-event(challengeSent(id, ch)).
```
---
## 7. Interpreting ProVerif Output
| ProVerif result | Meaning |
|----------------|---------|
| `RESULT ... is true.` | Property holds for all executions (proof found) |
| `RESULT ... is false.` | Attack found — ProVerif prints a trace |
| `RESULT ... cannot be proved.` | Proof search timed out or approximation too coarse; does not mean the property is false |
When a result is `false`, read the attack trace carefully:
1. Identify the event sequence ProVerif found
2. Map it back to the Mermaid diagram steps
3. Determine if the attack is a real flaw or a modeling artifact
Common false attacks from modeling artifacts:
- **Type confusion**: Two bitstrings with compatible types where the model
should use distinct types
- **Missing replication**: Single-session model allows trivial "man-in-middle"
because the attacker is the only other party
- **Missing freshness binding**: Signature does not include the nonce/epk,
so replay is possible at the model level even if the spec would bind it
When a result is `cannot be proved`, consider:
- Adding more specific type annotations
- Splitting the `!` replication into bounded sessions
- Switching to a weaker query first to establish partial results
plugins/trailmark/skills/trailmark-structural/SKILL.md
+107
View File
@@ -0,0 +1,107 @@
---
name: trailmark-structural
description: "Runs full trailmark structural analysis with all pre-analysis passes (blast radius, taint propagation, privilege boundaries, complexity hotspots). Use when vivisect needs detailed structural data for a target. Triggers: structural analysis, blast radius, taint analysis, complexity hotspots."
allowed-tools:
- Bash
- Read
- Grep
- Glob
---
# Trailmark Structural Analysis
Runs `trailmark analyze` with all four pre-analysis passes.
## When to Use
- Vivisect Phase 1 needs full structural data (hotspots, taint, blast radius, privilege boundaries)
- Detailed pre-analysis passes for a specific target scope
- Generating complexity and taint data for audit prioritization
## When NOT to Use
- Quick overview only (use `trailmark-summary` instead)
- Ad-hoc code graph queries (use the main `trailmark` skill directly)
- Target is a single small file where structural analysis adds no value
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "Summary analysis is enough" | Summary skips taint, blast radius, and privilege boundary data | Run full structural analysis when detailed data is needed |
| "One pass is sufficient" | Passes cross-reference each other — taint without blast radius misses critical nodes | Run all four passes |
| "Tool isn't installed, I'll analyze manually" | Manual analysis misses what tooling catches | Report "trailmark is not installed" and return |
| "Empty pass output means the pass failed" | Some passes produce no data for some codebases (e.g., no privilege boundaries) | Return full output regardless |
## Usage
The target directory is passed via the `args` parameter.
## Execution
**Step 1: Check that trailmark is available.**
```bash
trailmark analyze --help 2>/dev/null || \
uv run trailmark analyze --help 2>/dev/null
```
If neither command works, report "trailmark is not installed"
and return. Do NOT run `pip install`, `uv pip install`,
`git clone`, or any install command. The user must install
trailmark themselves.
**Step 2: Detect the primary language.**
```bash
find {args} -type f \( -name '*.rs' -o -name '*.py' \
-o -name '*.go' -o -name '*.js' -o -name '*.jsx' \
-o -name '*.ts' -o -name '*.tsx' -o -name '*.sol' \
-o -name '*.c' -o -name '*.h' -o -name '*.cpp' \
-o -name '*.hpp' -o -name '*.hh' -o -name '*.cc' \
-o -name '*.cxx' -o -name '*.hxx' \
-o -name '*.rb' -o -name '*.php' -o -name '*.cs' \
-o -name '*.java' -o -name '*.hs' -o -name '*.erl' \
-o -name '*.cairo' -o -name '*.circom' \) 2>/dev/null | \
sed 's/.*\.//' | sort | uniq -c | sort -rn | head -5
```
Map the most common extension to a language flag:
- `.rs` -> `--language rust`
- `.py` -> (no flag, Python is default)
- `.go` -> `--language go`
- `.js`/`.jsx` -> `--language javascript`
- `.ts`/`.tsx` -> `--language typescript`
- `.sol` -> `--language solidity`
- `.c`/`.h` -> `--language c`
- `.cpp`/`.hpp`/`.hh`/`.cc`/`.cxx`/`.hxx` -> `--language cpp`
- `.rb` -> `--language ruby`
- `.php` -> `--language php`
- `.cs` -> `--language c_sharp`
- `.java` -> `--language java`
- `.hs` -> `--language haskell`
- `.erl` -> `--language erlang`
- `.cairo` -> `--language cairo`
- `.circom` -> `--language circom`
**Step 3: Run the full structural analysis.**
```bash
trailmark analyze \
--passes blast_radius,taint,privilege_boundary,complexity \
{language_flag} {args} 2>&1 || \
uv run trailmark analyze \
--passes blast_radius,taint,privilege_boundary,complexity \
{language_flag} {args} 2>&1
```
**Step 4: Verify the output.**
The output should include:
- Hotspot scores (complexity data)
- Tainted node list (taint propagation data)
- Blast radius data
- Privilege boundary information
Some passes may produce no data for some codebases (this is
normal). Return the full output regardless.
plugins/trailmark/skills/trailmark-summary/SKILL.md
+103
View File
@@ -0,0 +1,103 @@
---
name: trailmark-summary
description: "Runs a trailmark summary analysis on a codebase. Returns language detection, entry point count, and dependency graph shape. Use when vivisect or galvanize needs a quick structural overview. Triggers: trailmark summary, code summary, structural overview."
allowed-tools:
- Bash
- Read
- Grep
- Glob
---
# Trailmark Summary
Runs `trailmark analyze --summary` on a target directory.
## When to Use
- Vivisect Phase 0 needs a quick structural overview before decomposition
- Galvanize Phase 1 needs language detection and entry point count
- Quick orientation on an unfamiliar codebase before deeper analysis
## When NOT to Use
- Full structural analysis with all passes needed (use `trailmark-structural`)
- Detailed code graph queries (use the main `trailmark` skill directly)
- You need hotspot scores or taint data (use `trailmark-structural`)
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "I can read the code manually instead" | Manual reading misses dependency graph shape and entry point enumeration | Install and run trailmark |
| "Language detection doesn't matter" | Wrong language flag produces empty or incorrect analysis | Detect language from file extensions first |
| "Partial output is good enough" | Missing any of the three required outputs (language, entry points, dependencies) means incomplete analysis | Verify all three are present |
| "Tool isn't installed, I'll skip it" | This skill exists specifically to run trailmark | Report the installation gap instead of skipping |
## Usage
The target directory is passed via the `args` parameter.
## Execution
**Step 1: Check that trailmark is available.**
```bash
trailmark analyze --help 2>/dev/null || \
uv run trailmark analyze --help 2>/dev/null
```
If neither command works, report "trailmark is not installed"
and return. Do NOT run `pip install`, `uv pip install`,
`git clone`, or any install command. The user must install
trailmark themselves.
**Step 2: Detect the primary language.**
```bash
find {args} -type f \( -name '*.rs' -o -name '*.py' \
-o -name '*.go' -o -name '*.js' -o -name '*.jsx' \
-o -name '*.ts' -o -name '*.tsx' -o -name '*.sol' \
-o -name '*.c' -o -name '*.h' -o -name '*.cpp' \
-o -name '*.hpp' -o -name '*.hh' -o -name '*.cc' \
-o -name '*.cxx' -o -name '*.hxx' \
-o -name '*.rb' -o -name '*.php' -o -name '*.cs' \
-o -name '*.java' -o -name '*.hs' -o -name '*.erl' \
-o -name '*.cairo' -o -name '*.circom' \) 2>/dev/null | \
sed 's/.*\.//' | sort | uniq -c | sort -rn | head -5
```
Map the most common extension to a language flag:
- `.rs` -> `--language rust`
- `.py` -> (no flag, Python is default)
- `.go` -> `--language go`
- `.js`/`.jsx` -> `--language javascript`
- `.ts`/`.tsx` -> `--language typescript`
- `.sol` -> `--language solidity`
- `.c`/`.h` -> `--language c`
- `.cpp`/`.hpp`/`.hh`/`.cc`/`.cxx`/`.hxx` -> `--language cpp`
- `.rb` -> `--language ruby`
- `.php` -> `--language php`
- `.cs` -> `--language c_sharp`
- `.java` -> `--language java`
- `.hs` -> `--language haskell`
- `.erl` -> `--language erlang`
- `.cairo` -> `--language cairo`
- `.circom` -> `--language circom`
**Step 3: Run the summary.**
```bash
trailmark analyze --summary {language_flag} {args} 2>&1 || \
uv run trailmark analyze --summary {language_flag} {args} 2>&1
```
**Step 4: Verify the output.**
The output must include ALL THREE of:
1. Language detection (at least one language name)
2. Entry point count (or "no entry points found")
3. Dependency graph shape (module count or "single module")
If any are missing, report the gap. Do not fabricate output.
Return the full trailmark output.
plugins/trailmark/skills/trailmark/SKILL.md
+196
View File
@@ -0,0 +1,196 @@
---
name: trailmark
description: "Builds and queries multi-language source code graphs for security analysis. Includes pre-analysis passes for blast radius, taint propagation, privilege boundaries, and entry point enumeration. Use when analyzing call paths, mapping attack surface, finding complexity hotspots, enumerating entry points, tracing taint propagation, measuring blast radius, or building a code graph for audit prioritization. Supports 16 languages including Solidity, Cairo, Circom, Rust, Go, Python, C/C++, TypeScript."
---
# Trailmark
Parses source code into a directed graph of functions, classes, calls, and
semantic metadata for security analysis. Supports 16 languages.
## When to Use
- Mapping call paths from user input to sensitive functions
- Finding complexity hotspots for audit prioritization
- Identifying attack surface and entrypoints
- Understanding call relationships in unfamiliar codebases
- Security review or audit preparation across polyglot projects
- Adding LLM-inferred annotations (assumptions, preconditions) to code units
- Pre-analysis before mutation testing (genotoxic skill) or diagramming
## When NOT to Use
- Single-file scripts where call graph adds no value (read the file directly)
- Architecture diagrams not derived from code (use the `diagramming-code` skill or draw by hand)
- Mutation testing triage (use the genotoxic skill, which calls trailmark internally)
- Runtime behavior analysis (trailmark is static, not dynamic)
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "I'll just read the source files manually" | Manual reading misses call paths, blast radius, and taint data | Install trailmark and use the API |
| "Pre-analysis isn't needed for a quick query" | Blast radius, taint, and privilege data are only available after `preanalysis()` | Always run `engine.preanalysis()` before handing off to other skills |
| "The graph is too large, I'll sample" | Sampling misses cross-module attack paths | Build the full graph; use subgraph queries to focus |
| "Uncertain edges don't matter" | Dynamic dispatch is where type confusion bugs hide | Account for `uncertain` edges in security claims |
| "Single-language analysis is enough" | Polyglot repos have FFI boundaries where bugs cluster | Use the correct `--language` flag per component |
| "Complexity hotspots are the only thing worth checking" | Low-complexity functions on tainted paths are high-value targets | Combine complexity with taint and blast radius data |
---
## Installation
**MANDATORY:** If `uv run trailmark` fails (command not found, import error,
ModuleNotFoundError), install trailmark before doing anything else:
```bash
uv pip install trailmark
```
**DO NOT** fall back to "manual verification", "manual analysis", or reading
source files by hand as a substitute for running trailmark. The tool must be
installed and used programmatically. If installation fails, report the error
to the user instead of silently switching to manual code reading.
## Quick Start
```bash
# Python (default)
uv run trailmark analyze --summary {targetDir}
# Other languages
uv run trailmark analyze --language rust {targetDir}
uv run trailmark analyze --language javascript {targetDir}
uv run trailmark analyze --language go --summary {targetDir}
# Complexity hotspots
uv run trailmark analyze --complexity 10 {targetDir}
```
### Programmatic API
```python
from trailmark.query.api import QueryEngine
# Specify language (defaults to "python")
engine = QueryEngine.from_directory("{targetDir}", language="rust")
engine.callers_of("function_name")
engine.callees_of("function_name")
engine.paths_between("entry_func", "db_query")
engine.complexity_hotspots(threshold=10)
engine.attack_surface()
engine.summary()
engine.to_json()
# Run pre-analysis (blast radius, entrypoints, privilege
# boundaries, taint propagation)
result = engine.preanalysis()
# Query subgraphs created by pre-analysis
engine.subgraph_names()
engine.subgraph("tainted")
engine.subgraph("high_blast_radius")
engine.subgraph("privilege_boundary")
engine.subgraph("entrypoint_reachable")
# Add LLM-inferred annotations
from trailmark.models import AnnotationKind
engine.annotate("function_name", AnnotationKind.ASSUMPTION,
"input is URL-encoded", source="llm")
# Query annotations (including pre-analysis results)
engine.annotations_of("function_name")
engine.annotations_of("function_name",
kind=AnnotationKind.BLAST_RADIUS)
engine.annotations_of("function_name",
kind=AnnotationKind.TAINT_PROPAGATION)
```
## Pre-Analysis Passes
**Always run `engine.preanalysis()` before handing off to genotoxic or
`diagramming-code` skills.** Pre-analysis enriches the graph with four passes:
1. **Blast radius estimation** — counts downstream and upstream nodes per
function, identifies critical high-complexity descendants
2. **Entry point enumeration** — maps entrypoints by trust level, computes
reachable node sets
3. **Privilege boundary detection** — finds call edges where trust levels
change (untrusted -> trusted)
4. **Taint propagation** — marks all nodes reachable from untrusted
entrypoints
Results are stored as annotations and named subgraphs on the graph.
For detailed documentation, see
[references/preanalysis-passes.md](references/preanalysis-passes.md).
## Supported Languages
| Language | `--language` value | Extensions |
| --- | --- | --- |
| Python | `python` | `.py` |
| JavaScript | `javascript` | `.js`, `.jsx` |
| TypeScript | `typescript` | `.ts`, `.tsx` |
| PHP | `php` | `.php` |
| Ruby | `ruby` | `.rb` |
| C | `c` | `.c`, `.h` |
| C++ | `cpp` | `.cpp`, `.hpp`, `.cc`, `.hh`, `.cxx`, `.hxx` |
| C# | `c_sharp` | `.cs` |
| Java | `java` | `.java` |
| Go | `go` | `.go` |
| Rust | `rust` | `.rs` |
| Solidity | `solidity` | `.sol` |
| Cairo | `cairo` | `.cairo` |
| Haskell | `haskell` | `.hs` |
| Circom | `circom` | `.circom` |
| Erlang | `erlang` | `.erl` |
## Graph Model
**Node kinds:** `function`, `method`, `class`, `module`, `struct`,
`interface`, `trait`, `enum`, `namespace`, `contract`, `library`
**Edge kinds:** `calls`, `inherits`, `implements`, `contains`, `imports`
**Edge confidence:** `certain` (direct call, `self.method()`), `inferred`
(attribute access on non-self object), `uncertain` (dynamic dispatch)
### Per Code Unit
- Parameters with types, return types, exception types
- Cyclomatic complexity and branch metadata
- Docstrings
- Annotations: `assumption`, `precondition`, `postcondition`, `invariant`,
`blast_radius`, `privilege_boundary`, `taint_propagation`
### Per Edge
- Source/target node IDs, edge kind, confidence level
### Project Level
- Dependencies (imported packages)
- Entrypoints with trust levels and asset values
- Named subgraphs (populated by pre-analysis)
## Key Concepts
**Declared contract vs. effective input domain:** Trailmark separates what a
function *declares* it accepts from what can *actually reach* it via call
paths. Mismatches are where vulnerabilities hide:
- **Widening**: Unconstrained data reaches a function that assumes validation
- **Safe by coincidence**: No validation, but only safe callers exist today
**Edge confidence:** Dynamic dispatch produces `uncertain` edges. Account for
confidence when making security claims.
**Subgraphs:** Named collections of node IDs produced by pre-analysis.
Query with `engine.subgraph("name")`. Available after `engine.preanalysis()`.
## Query Patterns
See [references/query-patterns.md](references/query-patterns.md) for common
security analysis patterns.
See [references/preanalysis-passes.md](references/preanalysis-passes.md) for
pre-analysis pass documentation.
plugins/trailmark/skills/trailmark/references/preanalysis-passes.md
+165
View File
@@ -0,0 +1,165 @@
# Pre-Analysis Passes
Four passes that enrich the code graph before downstream skills (genotoxic,
diagramming-code) consume it. Run via `engine.preanalysis()`.
## Contents
- Blast radius estimation
- Entry point enumeration
- Privilege boundary detection
- Taint propagation
- Subgraph reference
- Annotation reference
---
## 1. Blast Radius Estimation
Counts how many nodes are reachable downstream (descendants) and upstream
(ancestors) from each function. High blast radius means a bug in that
function affects many others.
**Annotation:** `AnnotationKind.BLAST_RADIUS` on every node.
```
"12 downstream, 3 upstream; critical: db_query, auth_check"
```
**Subgraph:** `high_blast_radius` — nodes with >= 10 downstream descendants.
```python
engine.preanalysis()
# All high-blast-radius nodes
high = engine.subgraph("high_blast_radius")
for node in high:
print(f"{node['id']}: CC={node['cyclomatic_complexity']}")
# Per-node annotation
for ann in engine.annotations_of("handler",
kind=AnnotationKind.BLAST_RADIUS):
print(ann["description"])
```
---
## 2. Entry Point Enumeration
Collects all entrypoints, groups them by trust level, and computes the
full set of reachable nodes from any entrypoint.
**Subgraphs:**
| Name | Contents |
|------|----------|
| `entrypoints` | All entrypoint nodes |
| `entrypoint_reachable` | Every node reachable from any entrypoint |
| `entrypoints:untrusted_external` | Entrypoints at untrusted level |
| `entrypoints:semi_trusted_external` | Entrypoints at semi-trusted level |
| `entrypoints:trusted_internal` | Entrypoints at trusted level |
```python
engine.preanalysis()
# Nodes NOT reachable from any entrypoint (potential dead code)
all_ids = {n["id"] for n in engine.subgraph("entrypoint_reachable")}
# Compare with full node set from engine.summary()
```
---
## 3. Privilege Boundary Detection
Finds call edges where the source and target are reachable from entrypoints
at different trust levels. These boundaries are where untrusted data crosses
into trusted zones.
**Annotation:** `AnnotationKind.PRIVILEGE_BOUNDARY` on boundary nodes.
```
"trust transition across call: untrusted_external -> trusted_internal"
```
**Subgraph:** `privilege_boundary` — all nodes sitting on a trust boundary.
```python
engine.preanalysis()
boundary = engine.subgraph("privilege_boundary")
for node in boundary:
anns = engine.annotations_of(
node["id"], kind=AnnotationKind.PRIVILEGE_BOUNDARY)
for a in anns:
print(f"{node['id']}: {a['description']}")
```
---
## 4. Taint Propagation
Propagates taint from every untrusted and semi-trusted entrypoint through
call edges. Trusted entrypoints do not generate taint. Each tainted node
is annotated with the entrypoint(s) that reach it.
**Annotation:** `AnnotationKind.TAINT_PROPAGATION` on tainted nodes.
```
"tainted via: handle_request, parse_input"
```
**Subgraph:** `tainted` — all nodes reachable from any non-trusted entrypoint.
```python
engine.preanalysis()
tainted = engine.subgraph("tainted")
for node in tainted:
anns = engine.annotations_of(
node["id"], kind=AnnotationKind.TAINT_PROPAGATION)
print(f"{node['id']}: {anns[0]['description']}")
```
---
## Subgraph Reference
All subgraphs created by `engine.preanalysis()`:
| Subgraph | Pass | Description |
|----------|------|-------------|
| `high_blast_radius` | Blast radius | Nodes with >= 10 downstream descendants |
| `entrypoints` | Entry point enum | All entrypoint nodes |
| `entrypoint_reachable` | Entry point enum | Union of all entrypoint-reachable nodes |
| `entrypoints:{trust_level}` | Entry point enum | Entrypoints grouped by trust level |
| `privilege_boundary` | Privilege boundary | Nodes on trust-level transitions |
| `tainted` | Taint propagation | All nodes reachable from non-trusted entrypoints |
Query any subgraph:
```python
nodes = engine.subgraph("tainted")
names = engine.subgraph_names()
```
---
## Annotation Reference
Annotations added by pre-analysis (source = `"preanalysis"`):
| Kind | Pass | Description format |
|------|------|--------------------|
| `blast_radius` | Blast radius | `"N downstream, M upstream; critical: ..."` |
| `privilege_boundary` | Privilege boundary | `"trust transition across call: X -> Y"` |
| `taint_propagation` | Taint propagation | `"tainted via: ep1, ep2"` |
Query annotations:
```python
from trailmark.models import AnnotationKind
engine.annotations_of("func", kind=AnnotationKind.BLAST_RADIUS)
engine.annotations_of("func", kind=AnnotationKind.PRIVILEGE_BOUNDARY)
engine.annotations_of("func", kind=AnnotationKind.TAINT_PROPAGATION)
```
plugins/trailmark/skills/trailmark/references/query-patterns.md
+137
View File
@@ -0,0 +1,137 @@
# Trailmark Query Patterns for Security Analysis
Common patterns for using Trailmark in security reviews.
## 1. Mapping Attack Surface
Find all entrypoints and trace what they can reach:
```python
from trailmark.query.api import QueryEngine
engine = QueryEngine.from_directory("{targetDir}")
# All entrypoints
for ep in engine.attack_surface():
print(f"{ep['node_id']}: {ep['trust_level']} ({ep['kind']})")
```
## 2. Complexity Hotspots
High-complexity functions are more likely to contain bugs:
```python
for hotspot in engine.complexity_hotspots(threshold=10):
loc = hotspot["location"]
print(
f"{hotspot['id']} "
f"complexity={hotspot['cyclomatic_complexity']} "
f"{loc['file_path']}:{loc['start_line']}"
)
```
## 3. Call Path Analysis
Find how user input reaches a sensitive function:
```python
paths = engine.paths_between("handle_request", "execute_query")
for path in paths:
print(" -> ".join(path))
```
## 4. Caller Analysis
Find all callers of a security-sensitive function to check if they
all validate input properly:
```python
callers = engine.callers_of("execute_query")
for caller in callers:
print(f"{caller['id']} at {caller['location']['file_path']}:{caller['location']['start_line']}")
```
## 5. Reachability from Entrypoints
Check if a function is reachable from any entrypoint:
```python
surface = engine.attack_surface()
paths = engine.paths_between("main", "sensitive_function_id")
if paths:
print(f"Reachable via {len(paths)} path(s)")
else:
print("Not reachable from any entrypoint")
```
## 6. Full Graph Export
Export for use with other tools:
```python
import json
json_str = engine.to_json()
with open("graph.json", "w") as f:
f.write(json_str)
```
## 7. Multi-Language Analysis
Analyze non-Python projects by specifying the language:
```python
from trailmark.query.api import QueryEngine
engine = QueryEngine.from_directory("{targetDir}", language="rust")
engine = QueryEngine.from_directory("{targetDir}", language="go")
engine = QueryEngine.from_directory("{targetDir}", language="typescript")
```
Supported `--language` values: `python`, `javascript`, `typescript`, `php`,
`ruby`, `c`, `cpp`, `c_sharp`, `java`, `go`, `rust`, `solidity`, `cairo`,
`haskell`, `circom`, `erlang`.
## 8. CLI Patterns
```bash
# Quick summary (Python, default)
uv run trailmark analyze --summary {targetDir}
# Analyze other languages
uv run trailmark analyze --language rust --summary {targetDir}
uv run trailmark analyze --language go --complexity 8 {targetDir}
# Full JSON output for piping to other tools
uv run trailmark analyze {targetDir} | jq '.nodes | to_entries[] | select(.value.cyclomatic_complexity > 10)'
```
## 9. Annotation Workflow
Add semantic annotations after analyzing code with an LLM. Annotations
persist on the in-memory graph and can be queried later:
```python
from trailmark.models import AnnotationKind
# Add annotations (returns False if node not found)
engine.annotate("handle_request", AnnotationKind.ASSUMPTION, "input is URL-encoded", source="llm")
engine.annotate("validate_token", AnnotationKind.PRECONDITION, "token is non-empty string", source="llm")
# Query annotations on a specific function
for ann in engine.annotations_of("handle_request"):
print(f"[{ann['kind']}] {ann['description']} (source: {ann['source']})")
# Filter by kind
assumptions = engine.annotations_of("handle_request", kind=AnnotationKind.ASSUMPTION)
# Clear annotations (all, or by kind)
engine.clear_annotations("handle_request", kind=AnnotationKind.ASSUMPTION)
engine.clear_annotations("handle_request")
```
**Annotation kinds:** `ASSUMPTION`, `PRECONDITION`, `POSTCONDITION`, `INVARIANT`.
Pre-analysis adds: `BLAST_RADIUS`, `PRIVILEGE_BOUNDARY`, `TAINT_PROPAGATION`.
**Source convention:** Use `"llm"` for LLM-inferred annotations, `"docstring"`
for annotations extracted from source, `"manual"` for human-added annotations.
plugins/trailmark/skills/vector-forge/SKILL.md
+478
View File
@@ -0,0 +1,478 @@
---
name: vector-forge
description: "Mutation-driven test vector generation. Finds implementations of a cryptographic algorithm or protocol, runs mutation testing to identify escaped mutants, then generates new test vectors that deliberately exercise the uncovered code paths. Compares before/after mutation kill rates to prove vector effectiveness. Use when generating cryptographic test vectors, measuring Wycheproof coverage gaps, finding escaped mutants via mutation testing, creating cross-implementation test suites, or improving test vector coverage for crypto primitives."
---
# Vector Forge
Uses mutation testing to systematically identify gaps in test vector
coverage, then generates new test vectors that close those gaps.
Measures effectiveness by comparing mutation kill rates before and after.
## When to Use
- Generating test vectors for cryptographic algorithms or protocols
- Evaluating how well existing test vectors cover an implementation
- Finding implementation code paths that no test vector exercises
- Creating Wycheproof-style cross-implementation test vectors
- Measuring the concrete coverage value of a test vector suite
## When NOT to Use
- No implementations exist yet (need code to mutate)
- Single trivial implementation with no edge cases
- Testing application logic rather than algorithm implementations
- The algorithm has no public test vectors to compare against
## Prerequisites
- **trailmark** installed — if `uv run trailmark` fails, run:
```bash
uv pip install trailmark
```
- At least one implementation of the target algorithm in a
language with mutation testing support
- A test harness that consumes test vectors and exercises
the implementation
- A mutation testing framework for the target language
---
## Rationalizations to Reject
| Rationalization | Why It's Wrong | Required Action |
|-----------------|----------------|-----------------|
| "We have enough test vectors" | Mutation testing proves otherwise | Run the baseline first |
| "The implementation's own tests are sufficient" | Own tests often share blind spots with the impl | Cross-impl vectors catch different bugs |
| "FFI crates can be mutation tested at the binding layer" | Mutations to wrappers don't affect the underlying impl | Mutate the actual implementation language |
| "Timeouts mean the mutation was caught" | Timeouts are ambiguous — could be killed or alive | Resolve timeouts before drawing conclusions |
| "All mutants are equivalent" | Most aren't — verify by reading the mutation | Classify each escaped mutant individually |
| "Checking valid vectors is enough" | Permissive mutations survive without negative assertions | Assert rejection for every invalid vector |
| "Manual analysis is fine" | Manual analysis misses what tooling catches | Install and run the tools |
---
## Workflow Overview
```
Phase 1: Discovery → Find implementations to test
↓
Phase 2: Harness → Write/adapt test vector harness for each impl
↓
Phase 3: Baseline → Run mutation testing with existing vectors
↓
Phase 4: Escape Analysis → Classify escaped mutants by code path
↓
Phase 5: Vector Gen → Create test vectors targeting escapes
↓
Phase 6: Validation → Re-run mutation testing, compare before/after
↓
Output: Coverage Report + New Test Vectors
```
---
## Phase 1: Discovery
Find implementations of the target algorithm. Look for:
1. **Pure implementations** in high-level languages (Go, Rust, Python)
— these are the best mutation testing targets
2. **FFI wrapper crates** — identify these early so you don't waste
time mutating wrapper glue code
3. **Reference implementations** — useful for cross-verification but
may not be the best mutation targets
For each implementation, note:
- Language and mutation testing framework
- Whether it's pure code or FFI wrappers
- Existing test suite size and coverage
- Which API surface the test vectors will exercise
### Implementation Type Classification
| Type | Mutation Value | Example |
|------|---------------|---------|
| Pure implementation | High | zkcrypto/bls12_381 (Rust), gnark-crypto (Go) |
| FFI bindings to C/asm | Low at binding layer | blst Rust crate |
| C/C++ implementation | High (use Mull) | blst C library |
| Generated code | Medium (mutations may be equivalent) | gnark-crypto generated field arithmetic |
**Key insight:** If an implementation delegates to another language
via FFI, you must mutate the *underlying* implementation, not the
bindings. For C/C++ underneath Rust/Go/Python, use Mull or similar.
---
## Phase 2: Harness
For each implementation, create a test harness that:
1. Reads test vectors from JSON files (Wycheproof format recommended)
2. Exercises the implementation's API for each vector
3. Asserts **both acceptance and rejection**:
- Valid vectors: deserialization succeeds, output matches expected
- Invalid vectors: deserialization fails or verification rejects
4. Adds **roundtrip assertions** for valid deserialization vectors:
`serialize(deserialize(bytes)) == bytes`
5. Reports pass/fail per vector with test IDs
**Critical:** A harness that only checks valid vectors will miss all
permissive mutations (e.g., `&` → `|` in validation). See
[references/lessons-learned.md](references/lessons-learned.md) §7.
The harness must be runnable by the mutation testing framework.
For most frameworks this means:
- **Go:** A `_test.go` file in the same package as the implementation
- **Rust:** An integration test in `tests/` or inline `#[test]` functions
- **Python:** A pytest test file
- **C/C++:** A test binary linked against the implementation
### Harness Placement
The harness must live *inside the implementation's package* so the
mutation framework can see it. This usually means:
```bash
# Go: add test file to the package being mutated
cp wycheproof_test.go /path/to/impl/package/
# Rust: add integration test
cp wycheproof.rs /path/to/crate/tests/
# Python: add test to the test directory
cp test_wycheproof.py /path/to/package/tests/
```
### Handling Existing Vectors
If the implementation already has test vectors:
1. Run mutation testing with ONLY the existing vectors (baseline)
2. Run mutation testing with ONLY your new vectors
3. Run mutation testing with BOTH combined
4. The delta between (1) and (3) shows the new vectors' value
---
## Phase 3: Baseline
Run mutation testing with existing test vectors only.
### Framework Selection
See [references/mutation-frameworks.md](references/mutation-frameworks.md)
for language-specific setup.
| Language | Framework | Command |
|----------|-----------|---------|
| Go | gremlins | `gremlins unleash ./path/to/package` |
| Rust | cargo-mutants | `cargo mutants -j N --timeout T` |
| Python | mutmut | `mutmut run --paths-to-mutate src/` |
| C/C++ | Mull | `mull-runner -test-framework=GoogleTest binary` |
### Parallelism
Always use parallel execution for large codebases:
- `cargo mutants -j 8` (Rust, 8 parallel workers)
- `gremlins unleash --timeout-coefficient 3` (Go, increase timeouts)
- `mutmut run --runner "pytest -x -q"` (Python, fail-fast)
### Recording Baseline Results
Capture these metrics per implementation:
| Metric | Description |
|--------|-------------|
| Total mutants | Number of mutations generated |
| Killed | Mutants caught by tests |
| Survived/Lived | Mutants NOT caught (these are the targets) |
| Not covered | Code paths no test reaches at all |
| Timed out | Ambiguous — resolve before comparing |
| Efficacy % | Killed / (Killed + Survived) |
| Coverage % | (Total - Not covered) / Total |
Save the full mutation log for Phase 4 analysis.
---
## Phase 4: Escape Analysis (Graph-Informed Triage)
Classify each escaped (survived + not covered) mutant using the
Trailmark call graph for reachability and blast radius analysis.
**This phase MUST use the genotoxic skill's triage methodology.**
The call graph transforms mutation results from a flat list of
survived mutants into an actionable, prioritized set of vector
targets.
### Step 1: Build the Call Graph
Build a Trailmark code graph for each implementation before
triaging mutations:
```bash
# Go
uv run trailmark analyze --language go --summary {targetDir}
# Rust
uv run trailmark analyze --language rust --summary {targetDir}
```
The graph provides:
- **Caller chains** — trace from public API entry points to
mutated functions to determine reachability
- **Cyclomatic complexity** — prioritize high-CC functions
- **Blast radius** — functions with many callers have wider
impact if their mutations survive
### Step 2: Filter to Relevant Code
Mutation frameworks test the entire package. Filter results to
only the files/functions that test vectors should exercise:
```bash
# Go (gremlins)
grep -E "(LIVED|NOT COVERED)" baseline.log \
| grep -E " at (relevant|files)" \
| sort
# Rust (cargo-mutants)
cat mutants.out/missed.txt | grep "src/relevant"
```
### Step 3: Graph-Informed Classification
For each escaped mutant, map it to its containing function in the
call graph and apply the genotoxic triage criteria:
| Graph Signal | Classification | Action |
|--------------|----------------|--------|
| No callers in graph | **False Positive** | Dead code, skip |
| Only test callers | **False Positive** | Test infrastructure |
| Logging/display/formatting | **False Positive** | Cosmetic |
| Cross-package callers but NOT COVERED | **Cross-Package Gap** | See below |
| Reachable from public API, low CC | **Missing Vector** | Design targeted vector |
| Reachable from public API, high CC (>10) | **Fuzzing Target** | Both vector + fuzz harness |
| Validation/error-handling path | **Negative Vector** | Craft invalid input that triggers path |
| Optimization path (GLV, SIMD, batch) | **Edge-Case Vector** | Input that triggers optimization threshold |
| `\|`→`^` after left shift (e.g. `(t<<1) \| carry`) | **Equivalent Mutant** | Skip — bit 0 always 0, OR=XOR |
| ct_eq `&`→`\|` on Montgomery limbs | **API-Unreachable** | Needs library-internal tests, not vectors |
| Equivalent mutation (behavior unchanged) | **False Positive** | Skip |
### Step 4: Identify Cross-Package Test Gaps
**Critical pitfall:** Mutation frameworks often only run tests
within the same package as the mutation. For Go (gremlins) and
Rust (cargo-mutants), this means:
- A mutation in `hash_to_curve/g2.go` only runs tests in the
`hash_to_curve` package, NOT tests in the parent `bls12381`
package that imports it
- Functions that are fully exercised by cross-package tests
will appear as NOT COVERED — these are **false positives**
- To confirm: check if the mutated function is called from a
test in a *different* package that wouldn't be run
To resolve cross-package gaps:
1. Add a thin test in the sub-package that calls through the
same code path as the cross-package test
2. Or run gremlins with `--test-pkg ./...` (if supported)
3. Or document as a framework limitation in the report
### Step 5: Prioritize by Security Impact
Using the call graph, rank surviving mutants by impact:
| Priority | Criteria | Example |
|----------|----------|---------|
| **P0 — Critical** | Mutant weakens validation/equality/authentication | `ct_eq`: `&` → `\|` makes equality permissive |
| **P1 — High** | Mutant in deserialization flag parsing | `from_compressed`: `&` → `\|` accepts invalid flags |
| **P2 — Medium** | Mutant in field arithmetic internals | `Fp::square`: `\|` → `^` corrupts computation |
| **P3 — Low** | Mutant in optimization path | `phi` endomorphism: only affects performance path |
| **Skip** | Formatting, display, equivalent mutation | `Debug::fmt` return value replacement |
### Step 6: Group by Vector Strategy
Group escaped mutants by the code path they represent and the
type of test vector needed:
```
Deserialization flag validation (P1):
- g1.rs:339,363-365,384 — from_compressed_unchecked flags
→ Need: valid-point-wrong-flag vectors
Field arithmetic (P2):
- fp.rs:371-376,406,635-643 — subtract_p, neg, square
→ Need: field arithmetic KATs with edge-case values
Optimization thresholds (P3):
- g1.go:68, g2.go:75 — GLV vs windowed multiplication
→ Need: scalar multiplication with large scalars
Cross-package (framework limitation):
- hash_to_curve/g2.go:242-278 — isogeny, sgn0
→ Document as false positive or add sub-package test
```
Each group becomes a target for new test vectors in Phase 5.
---
## Phase 5: Vector Generation
For each escaped code path group, design test vectors that
force execution through that path.
### Vector Design Patterns
| Code Path Type | Vector Strategy |
|----------------|----------------|
| Point deserialization | Malformed points: wrong length, invalid field elements, off-curve, wrong subgroup, identity point |
| Signature verification | Valid sig + all single-bit corruptions of sig, pk, msg |
| Hash-to-curve | Known answer tests (KATs) with edge-case inputs: empty, single byte, max length |
| Aggregate operations | 1 signer, many signers, duplicate signers, mixed valid/invalid |
| Error handling | Every error path should have a vector that triggers it |
| Arithmetic edge cases | Zero, one, field modulus - 1, points at infinity |
| Serialization flags | Every valid flag combination + every invalid flag combination |
| Roundtrip integrity | For every valid deser vector, assert `serialize(deserialize(b)) == b` |
| Carry/reduction faults | Reimplement at reduced limb widths, inject faults, extract distinguishing inputs |
### Single-Fault Negative Vectors
Each negative vector should have **exactly one defect** with
everything else valid — this isolates which validation check is
being tested. See [references/vector-patterns.md](references/vector-patterns.md)
for per-flag construction examples.
### Fault Simulation (Limb-Width Reimplementation)
When mutation testing only applies local operator swaps, deeper
architectural bugs (carry propagation, reduction overflow) go
untested. To close this gap, reimplement the target algorithm
at reduced limb widths (8, 16, 25, 32 bits) and deliberately
inject faults — then generate vectors that catch them.
See [references/fault-simulation.md](references/fault-simulation.md)
for the full methodology: limb-width selection, fault injection
catalog, vector extraction, and validation workflow.
### Cross-Implementation Verification
Every new test vector MUST be verified against at least two
independent implementations before being added to the suite:
1. Generate the vector using implementation A
2. Verify with implementation B (different codebase, ideally different language)
3. If B disagrees, investigate — one implementation has a bug
### Vector Format
Use Wycheproof JSON format (`algorithm`, `testGroups[].tests[]`
with `tcId`, `comment`, `result`, `flags`). See
[references/vector-patterns.md](references/vector-patterns.md)
for the full schema.
**JSON encoding:** Wycheproof canonicalizes vectors with
`reformat_json.py`, which unescapes HTML entities. Generate vectors
with literal characters, not HTML-escaped sequences:
- **Go:** Use `json.NewEncoder` + `enc.SetEscapeHTML(false)` —
never `json.Marshal`/`json.MarshalIndent`, which silently escape
`>` → `\u003e`, `<` → `\u003c`, `&` → `\u0026`
- **Python:** `json.dumps` is safe by default
- **Node.js:** `JSON.stringify` is safe by default
See [references/lessons-learned.md](references/lessons-learned.md)
§14 for details.
---
## Phase 6: Validation
Re-run mutation testing with the new test vectors included.
**Tip:** Use per-file mutation testing for fast iteration during
vector development (see [references/lessons-learned.md](references/lessons-learned.md) §12).
Only run full-crate tests for the final comparison.
### Before/After Comparison
| Metric | Baseline | With New Vectors | Delta |
|--------|----------|------------------|-------|
| Killed | X | Y | Y - X |
| Survived | A | B | A - B (should decrease) |
| Not Covered | C | D | C - D (should decrease) |
| Efficacy % | E% | F% | F - E |
### Success Criteria
Vectors have both **retroactive** value (killing mutants in
existing code) and **proactive** value (catching bugs in future
implementations). Generate both kinds — boundary-condition vectors
may not improve kill rates in mature libraries but will catch bugs
in new implementations. See
[references/lessons-learned.md](references/lessons-learned.md) §13.
**Retroactive (measurable):** previously survived/uncovered mutants
become killed, no regressions.
**If kill rates don't change:** the implementation's own tests
likely already cover those paths. The vectors still add
cross-implementation verification value. Document which case
applies.
---
## Output Format
Write `VECTOR_FORGE_REPORT.md` covering: target algorithm,
implementations tested, baseline results, escape analysis,
new vectors generated, after results, before/after delta, and
conclusions. See
[references/report-template.md](references/report-template.md)
for the full template.
---
## Quality Checklist
Before delivering:
- [ ] At least one pure implementation mutation-tested (not just FFI wrappers)
- [ ] Baseline run completed with existing vectors
- [ ] Trailmark call graph built for each implementation
- [ ] All escaped mutants triaged using graph-informed classification
- [ ] Cross-package false positives identified and documented
- [ ] Security-critical mutations (ct_eq, validation, auth) prioritized as P0/P1
- [ ] Fault simulation and mutation-derived vectors cross-verified against 2+ implementations
- [ ] After run completed with new vectors included
- [ ] Before/after delta computed and explained
- [ ] Report written to `VECTOR_FORGE_REPORT.md`
- [ ] New test vectors saved in standard format (Wycheproof JSON)
---
## Integration
| Skill | Relationship |
|-------|-------------|
| **genotoxic** (required for Phase 4) | Provides graph-informed triage — call graph cuts actionable mutants by 30-50% |
| **mutation-testing** (mewt/muton) | Use for Solidity; Vector Forge is language-agnostic |
| **property-based-testing** | Better than hand-crafted vectors for bitwise mutations in field arithmetic |
| **testing-handbook-skills** (fuzzing) | Functions with CC > 10 and surviving mutants need both vectors and fuzz harnesses |
---
## Supporting Documentation
- **[references/mutation-frameworks.md](references/mutation-frameworks.md)** -
Language-specific mutation testing framework setup
- **[references/vector-patterns.md](references/vector-patterns.md)** -
Common test vector patterns for cryptographic primitives
- **[references/fault-simulation.md](references/fault-simulation.md)** -
Limb-width reimplementation for carry, reduction, and overflow faults
- **[references/report-template.md](references/report-template.md)** -
Full markdown template for the Vector Forge report
- **[references/lessons-learned.md](references/lessons-learned.md)** -
BLS12-381 case study: FFI kill rates, timeout masking, cross-package
false positives, bitwise mutation gaps, and security-critical priorities
plugins/trailmark/skills/vector-forge/references/fault-simulation.md
+151
View File
@@ -0,0 +1,151 @@
# Fault Simulation via Limb-Width Reimplementation
Generate test vectors that catch carry propagation, modular
reduction, and overflow bugs by reimplementing the target
algorithm at non-standard limb widths and deliberately injecting
architectural faults.
## Why Mutation Testing Misses These
Mutation testing frameworks apply local operator swaps (`+` → `-`,
`&` → `|`, `<` → `<=`). They cannot:
- Change the number of limbs in a multi-precision integer
- Alter carry propagation logic across limb boundaries
- Modify reduction strategies (Barrett vs Montgomery vs schoolbook)
- Introduce off-by-one errors in limb iteration bounds
These are exactly the bugs that cause real-world cryptographic
vulnerabilities (e.g., carry bugs in OpenSSL, Go's P-256).
## Methodology
### Step 1: Select Limb Widths
Reimplement the target operation at multiple limb widths to
exercise different carry propagation patterns:
| Limb Width | Why |
|-----------|-----|
| 8-bit | Maximum carries per operation, exposes propagation bugs |
| 16-bit | Intermediate carry frequency, different overflow boundary |
| 25-bit | Non-power-of-2 — exercises radix-2^25 representations (common in constant-time code) |
| 32-bit | Standard width, catches 64-bit-specific assumptions |
| 51-bit | Radix-2^51 (used in curve25519 implementations) |
Choose widths that differ from the production implementation.
If the production code uses 64-bit limbs, test at 8, 25, and
32 bits. If it uses radix-2^25.5 (like ref10), test at 8, 16,
and 32 bits.
### Step 2: Implement a Minimal Reference
You do NOT need a full cryptographic library. Implement only
the specific operation under test:
- **Field arithmetic:** add, subtract, multiply, square, reduce
- **Scalar arithmetic:** multiply, reduce mod group order
- **Point operations:** add, double, scalar multiply
The implementation must:
1. Produce correct results for known test vectors
2. Be simple enough to manually verify (schoolbook algorithms)
3. Use the chosen limb width throughout
### Step 3: Inject Faults
For each reimplementation, introduce ONE fault at a time from
this catalog:
| Fault Category | Specific Fault | What It Catches |
|---------------|----------------|-----------------|
| **Carry propagation** | Drop carry on limb N-1 → N | Missing final carry |
| **Carry propagation** | Off-by-one in carry shift | Carry to wrong bit position |
| **Carry propagation** | Skip carry in multiplication inner loop | Accumulator overflow |
| **Reduction** | Reduce modulo (p+1) instead of p | Wrong modulus |
| **Reduction** | Skip final conditional subtraction | Non-canonical output |
| **Reduction** | Off-by-one in reduction loop bound | Incomplete reduction |
| **Overflow** | Truncate intermediate to limb width before carry | Silent overflow |
| **Overflow** | Use signed instead of unsigned limbs | Sign extension corruption |
| **Boundary** | Return 0 for input = p-1 | Fence-post on modulus boundary |
| **Boundary** | Accept p as valid field element | Off-by-one in validation |
### Step 4: Extract Distinguishing Vectors
For each injected fault:
1. Run the faulted implementation against a broad input set
(random values + boundary values from the edge-case table)
2. Find inputs where `faulted_output != correct_output`
3. These inputs become test vectors — any correct implementation
must produce the correct output, and the faulted implementation
must diverge
**Key insight:** The distinguishing inputs often cluster around
specific value patterns:
| Fault Type | Likely Distinguishing Inputs |
|-----------|----------------------------|
| Carry propagation | Values where limb N-1 is at max (all bits set) |
| Reduction | Values near the modulus: p-1, p-2, 2p-1 |
| Overflow | Products of large values: (p-1) * (p-1) |
| Boundary | Exact modulus, modulus ± 1, zero, one |
### Step 5: Validate Against Production
Run the extracted vectors against the production implementation:
1. If production passes → vector validates production correctness
for that fault class
2. If production fails → you found a real bug (the production
implementation has the same fault class)
Both outcomes are valuable. Outcome 2 is a finding.
## Example: Field Multiplication Carry Bug
Target: 256-bit prime field multiplication (4×64-bit limbs in
production).
Reimplementation: 8×32-bit limbs, schoolbook multiplication.
Injected fault: Drop carry from limb 3 → limb 4 in the
multiplication accumulator.
```
Input A: 0xFFFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF (limbs 0-3 maxed)
Input B: 0x00000000_00000000_00000000_00000002 (simple multiplier)
Correct: A * B mod p = <correct value>
Faulted: A * B mod p = <wrong value, carry lost at limb boundary>
```
The pair (A, B, correct_result) becomes a test vector. Any
implementation that drops the carry at that boundary will fail.
## Integration with Phase 5
Fault simulation vectors complement mutation-derived vectors:
| Source | Catches |
|--------|---------|
| Mutation testing escapes | Local operator bugs in existing code |
| Fault simulation | Architectural bugs in carry/reduce/overflow logic |
Run fault simulation AFTER mutation testing baseline (Phase 3)
but BEFORE the final validation run (Phase 6). Add fault
simulation vectors to the same test suite as mutation-derived
vectors for the combined before/after comparison.
## Limb-Width Selection Heuristic
For a production implementation with W-bit limbs and N limbs:
1. Always include 8-bit (maximum carry stress)
2. Include at least one non-power-of-2 width (25 or 51 bits)
3. Include a width that is exactly half of production (W/2)
4. If production uses a non-standard radix, include the nearest
power-of-2 width
This ensures carry boundaries fall at different positions than
production, exposing width-specific assumptions.
plugins/trailmark/skills/vector-forge/references/lessons-learned.md
+190
View File
@@ -0,0 +1,190 @@
# Lessons Learned (BLS12-381 Case Study)
Patterns observed during mutation testing of gnark-crypto (Go),
blst (Rust FFI), and zkcrypto/bls12_381 (Rust):
## 1. FFI Wrappers Have 0% Kill Rate
Mutating blst's Rust bindings produced 0 kills across 79 mutants.
The Rust layer is thin wrappers around C/assembly — mutations to
`PartialEq`, `miller_loop_n`, `finalverify` all survive because
the real logic is in C. **Always identify FFI crates in Phase 1
and skip them for Rust/Go mutation testing. Use Mull for the C layer.**
## 2. Timeouts Mask Surviving Mutants
Adding Wycheproof tests to gnark-crypto changed gremlins' timeout
calibration, converting 3,144 timeouts into 2,533 killed + 476
lived. The 476 LIVED mutants were previously hidden. **Always
resolve timeouts before comparing baselines. Increase timeout
coefficients (`--timeout-coefficient 3`) for the first run.**
## 3. Cross-Package NOT COVERED ≠ Dead Code
In gnark-crypto, `hash_to_curve/g2.go` functions appeared as NOT
COVERED even though `HashToG2()` in the parent package calls them.
Gremlins only runs same-package tests for each mutated file.
**Use the call graph to identify cross-package false positives
before generating vectors for NOT COVERED mutants.**
## 4. Comprehensive Test Suites Resist Vector Coverage
gnark-crypto's own test suite already kills every mutant that
Wycheproof vectors can reach. The 53 NOT COVERED BLS mutants are
identical between baseline and Wycheproof runs. **The value of
Wycheproof vectors for well-tested libraries is cross-implementation
semantic validation, not code coverage improvement.**
## 5. Bitwise Operator Mutations Reveal Precision Gaps
In zkcrypto, 164 mutants survived — mostly `&` → `|` and `|` → `^`
in field arithmetic (`Fp::square`, `Fp::neg`, `Scalar::ct_eq`).
These mutations corrupt specific bits in multi-precision arithmetic.
**Killing bitwise mutations requires test vectors that exercise
every limb of the field representation, not just the "happy path"
with small values.** Vectors needed:
- Field element = modulus - 1 (all limbs active)
- Field element with alternating 0/1 limb patterns
- Scalar values near the group order boundary
## 6. Security-Critical Mutations Need Priority
`Scalar::ct_eq` with `&` → `|` makes equality permissive — more
values compare as equal. This could cause signature verification
to accept invalid signatures. **Always prioritize mutations in
equality checks, validation logic, and authentication paths.**
## 7. Test Harnesses Must Assert Rejection, Not Just Acceptance
The initial zkcrypto Wycheproof harness only checked that valid
vectors deserialized successfully. It never checked that invalid
vectors were *rejected*. This meant all flag-permissive mutations
(`&` → `|` in `from_compressed_unchecked`) survived — the mutated
code accepted invalid flags, but no test asserted rejection.
Adding `else if result == "invalid" { assert!(deser.is_none()) }`
killed ALL P1 flag mutations in both G1 and G2. **Every test
harness needs both positive assertions (valid accepted) AND
negative assertions (invalid rejected). Without negative
assertions, permissive mutations are invisible.**
## 8. Roundtrip Assertions Catch Field Arithmetic Corruption
`compress(decompress(bytes)) == bytes` is a powerful generic
assertion that catches carry propagation, square root, negation,
and modular reduction bugs without knowing the internal field
representation. If `Fp::square` or `Fp::subtract_p` has a carry
bug, the recovered y-coordinate will be wrong, changing the sort
bit in the re-compressed encoding.
This killed 15 previously-missed fp.rs mutations. **Add roundtrip
assertions to every deserialization test that handles valid
vectors. It's cheap and catches deep arithmetic bugs.**
## 9. Equivalent Mutant Pattern: Shift-then-OR
In `Fp::square` and `Scalar::square`, the doubling step uses
`(t << 1) | (prev >> 63)`. The mutation `|` → `^` survives
because `(t << 1)` always clears bit 0 (left shift), and
`(prev >> 63)` only affects bit 0. Since `0 | x == 0 ^ x` for
any `x`, these mutations are provably equivalent — they cannot
change behavior regardless of input.
14 of the "survived" mutations across scalar.rs and fp.rs are
this pattern. **When triaging `|` → `^` mutations in shift-based
expressions, check if the OR'd bit position is always 0 after the
shift. If so, classify as equivalent and skip.**
## 10. Montgomery Representation Creates an API Testing Boundary
`Scalar::ct_eq` computes `limb[0].ct_eq & limb[1].ct_eq & ...`.
With `&` → `|`, it returns equal if ANY limb matches. To kill
this, you need two different scalars that share at least one
internal Montgomery limb value. But `Scalar::from_raw` applies
Montgomery reduction (multiply by R), spreading the value across
all limbs unpredictably.
You cannot construct Montgomery-limb-aware test values through the
public API. **Mutations in internal representation comparisons
(ct_eq on limb arrays) require library-internal property-based
tests, not external test vectors. Document these as "not reachable
via API" rather than wasting time on vector design.**
## 11. Single-Fault Negative Vectors Isolate Validation Checks
The most effective flag vectors had exactly ONE defect — e.g.,
a valid G2 point with only the compression flag cleared. This
isolates the specific flag check: if `from_compressed` accepts
the vector, that particular validation is broken.
Multi-fault vectors (wrong flag AND wrong length AND off-curve)
are less useful because multiple checks reject them — you can't
tell which check is doing the work. **Design negative vectors with
the minimum number of defects to target a single validation check.
Keep the rest of the encoding valid.**
## 12. Per-File Mutation Testing for Fast Iteration
Full-crate mutation testing takes 30+ minutes. Per-file runs
(`cargo mutants -f src/scalar.rs`) take 2-5 minutes. When
iterating on test design for a specific file's mutations, use
per-file mode for rapid feedback:
```bash
# Fast iteration loop:
# 1. Edit test
# 2. Run per-file mutation test
# 3. Check missed.txt
# 4. Repeat
cargo mutants -j 8 --timeout 120 -f src/scalar.rs
cat mutants.out/missed.txt
```
**Use per-file mode during Phase 5 (vector generation) and
Phase 6 (validation). Only run full-crate tests for the final
before/after comparison.**
## 13. Vectors Have Retroactive and Proactive Value
Mutation testing measures retroactive value: which vectors kill
mutants in existing implementations. But test vectors also have
proactive value: catching bugs in future implementations that
haven't been written yet.
Not-on-curve, wrong-subgroup, and field-boundary vectors killed
zero additional mutants in mature zkcrypto code — the library
already validates these cases. But a new BLS12-381 implementation
that skips a subgroup check or mishandles x ≈ p will fail these
vectors immediately.
**Generate boundary-condition vectors even when they don't improve
mutation kill rates. They're a net for the implementations that
will be written tomorrow, not just the ones that exist today.**
## 14. Go's json.Marshal HTML-Escapes Characters in JSON Output
Go's `json.Marshal` and `json.MarshalIndent` silently HTML-escape
`>`, `<`, and `&` as `\u003e`, `\u003c`, `\u0026` in string values.
This is the default behavior and applies to comment fields, notes,
and any other string in the generated JSON.
Wycheproof's `reformat_json.py` canonicalizes vector files and
unescapes these sequences back to literal characters. The result:
generated vectors fail the `reformat_json.py && git diff --exit-code`
CI check immediately after generation.
**Use `json.NewEncoder` with `SetEscapeHTML(false)` in every Go
vector generator — never `json.Marshal` or `json.MarshalIndent`:**
```go
var buf bytes.Buffer
enc := json.NewEncoder(&buf)
enc.SetEscapeHTML(false)
enc.SetIndent("", " ")
if err := enc.Encode(data); err != nil { ... }
```
This applies to any string that might contain `>`, `<`, or `&` —
comments like "x >= field prime", notes with HTML, CVE descriptions,
URLs, etc. The same bug will recur silently whenever a new comment
or note uses these characters.
plugins/trailmark/skills/vector-forge/references/mutation-frameworks.md
+778
View File
@@ -0,0 +1,778 @@
# Mutation Testing Frameworks
Language-specific setup, execution, and output parsing for mutation testing.
## Contents
- Language detection
- Framework reference table
- Per-language setup and commands
- Parsing survived mutants
- Necessist (test statement removal)
---
## Installation Policy
**Every mutation testing framework listed below MUST be installed before
proceeding.** If a framework command is not found or fails to install:
1. Try the primary install method for the platform
2. Try the alternative install methods listed in the language section
3. If all methods fail, **report the error to the user** — do NOT fall
back to "manual mutation analysis", "manual verification", or any
other substitute that skips running the tool
Manual analysis is not a replacement for mutation testing. Mutation
testing tools systematically apply hundreds or thousands of mutations
that manual review cannot replicate. Skipping installation and doing
manual analysis produces false confidence with minimal actual coverage.
---
## Language Detection
Use file extensions to determine the target language, then select the
appropriate mutation framework:
| Extensions | Language | Framework |
|-----------|----------|-----------|
| `.py` | Python | pytest-gremlins or mutmut |
| `.js`, `.jsx`, `.ts`, `.tsx` | JavaScript/TypeScript | Stryker |
| `.rs` | Rust | cargo-mutants |
| `.go` | Go | gremlins or go-mutesting |
| `.java` | Java | PITest |
| `.c`, `.h`, `.cpp`, `.hpp`, `.cc` | C/C++ | Mull |
| `.cs` | C# | Stryker.NET |
| `.rb` | Ruby | mutant |
| `.php` | PHP | Infection |
| `.hs` | Haskell | MuCheck or Hedgehog |
---
## Python: pytest-gremlins (preferred) or mutmut
### pytest-gremlins
Faster alternative to mutmut. Uses mutation switching (no file I/O or
module reloads), coverage-guided test selection, and parallel execution.
Requires Python 3.11+.
**Install:**
```bash
uv add --dev pytest-gremlins
```
**Run:**
```bash
uv run pytest --gremlins
```
No configuration needed — it integrates directly with pytest.
**Parse survived mutants:** pytest-gremlins reports survived gremlins
in its test output. Each entry includes the file, line, mutation type,
and original/replacement values.
### mutmut
**Install:**
```bash
uv add --dev mutmut
```
**Configure** in `pyproject.toml`:
```toml
[tool.mutmut]
paths_to_mutate = "src/"
tests_dir = "tests/"
runner = "python -m pytest -x -q"
```
**Run:**
```bash
uv run mutmut run
uv run mutmut results
```
**Parse survived mutants:**
```bash
# List survived mutant IDs
uv run mutmut results | grep "Survived"
# Show specific mutant
uv run mutmut show <id>
# Export all results as JSON (mutmut 3.x+)
uv run mutmut junitxml > mutmut-results.xml
```
**Extract from results output:**
Each survived mutant line contains the file path, line number, and
mutation description. Parse with:
```bash
uv run mutmut results 2>&1 | grep "Survived" | \
sed 's/.*Survived: //'
```
**macOS note:** If using rustworkx or other Rust extensions, set:
```bash
export OBJC_DISABLE_INITIALIZE_FORK_SAFETY=YES
```
---
## JavaScript/TypeScript: Stryker
**Install:**
```bash
pnpm add -D @stryker-mutator/core
pnpm dlx stryker init
```
**Configure** `stryker.config.json`:
```json
{
"mutate": ["src/**/*.ts", "!src/**/*.test.ts"],
"testRunner": "vitest",
"reporters": ["json", "clear-text"],
"jsonReporter": { "fileName": "stryker-report.json" }
}
```
**Run:**
```bash
pnpm dlx stryker run
```
**Parse survived mutants:**
```bash
# JSON report at reports/mutation/stryker-report.json
# Filter survived:
cat reports/mutation/stryker-report.json | \
jq '.files | to_entries[] | .value.mutants[] | select(.status == "Survived")'
```
**Output fields:** `mutatorName`, `replacement`, `location.start.line`,
`location.start.column`, `fileName`.
---
## Rust: cargo-mutants
**Install:**
```bash
cargo install cargo-mutants
```
**Run:**
```bash
cargo mutants --json
```
**Parse survived mutants:**
```bash
# Results in mutants.out/outcomes.json
cat mutants.out/outcomes.json | \
jq '.[] | select(.outcome == "survived")'
```
**Output fields:** `scenario.function`, `scenario.file`, `scenario.line`,
`scenario.replacement`, `outcome`.
**Filtering by module:**
```bash
cargo mutants --file src/parser.rs --json
```
---
## Go: gremlins (preferred) or go-mutesting
### gremlins
Actively maintained mutation testing tool for Go. Works best on
small-to-medium Go modules (microservices, libraries).
**Install:**
```bash
# macOS
brew tap go-gremlins/tap && brew install gremlins
# Any platform with Go
go install github.com/go-gremlins/gremlins/cmd/gremlins@latest
```
**Run:**
```bash
gremlins unleash .
```
**Parse results:** gremlins reports survived mutants to stdout with
file path, line number, and mutation type.
### go-mutesting
**Install:**
```bash
go install github.com/zimmski/go-mutesting/cmd/go-mutesting@latest
```
**Run:**
```bash
go-mutesting ./...
```
**Parse results:** go-mutesting prints survived mutants to stdout.
Each line contains the file, line number, and mutation operator.
### Alternative: native fuzzing (Go 1.18+)
```bash
go test -fuzz=FuzzTarget -fuzztime=60s ./pkg/...
```
---
## Java: PITest
**Configure** in `pom.xml`:
```xml
<plugin>
<groupId>org.pitest</groupId>
<artifactId>pitest-maven</artifactId>
<configuration>
<targetClasses>com.example.*</targetClasses>
<outputFormats>XML,CSV</outputFormats>
</configuration>
</plugin>
```
**Run:**
```bash
mvn org.pitest:pitest-maven:mutationCoverage
```
**Parse survived mutants:**
```bash
# Results in target/pit-reports/mutations.xml
# Filter SURVIVED status
grep 'status="SURVIVED"' target/pit-reports/*/mutations.xml
```
**Output fields:** `mutatedClass`, `mutatedMethod`, `lineNumber`,
`mutator`, `status`.
---
## C/C++: Mull
Mull is an LLVM-based mutation testing tool for C and C++. It works as a
compiler plugin — it instruments the compiled test binary with mutations,
then selectively activates them during test execution.
**Mull requires a specific LLVM version.** Check the Mull releases page
for the LLVM version supported by the latest release. The project must
compile with the matching Clang version.
### Install
Mull is distributed as prebuilt binaries on GitHub Releases. Each
binary targets a specific LLVM version — **you must match the Mull
binary's LLVM version to the Clang version installed on the system.**
**Step 1: Determine your Clang/LLVM version:**
```bash
clang --version
# Look for the major version number (e.g., 19, 20)
```
If Clang is not installed, install it first. On macOS, use
`brew install llvm@<version>`. On Ubuntu, use
`sudo apt-get install clang-<version>`.
**Step 2: Download the matching Mull binary.**
Go to the [Mull releases page](https://github.com/mull-project/mull/releases/latest)
and download the asset matching your LLVM version, platform, and
architecture. Asset naming convention:
```text
Mull-<LLVM_MAJOR>-<MULL_VERSION>-LLVM-<LLVM_FULL>-<OS>-<ARCH>.<ext>
```
Examples (Mull 0.29.0):
| Platform | LLVM | Asset |
| -------- | ---- | ----- |
| macOS arm64 | 19 | `Mull-19-0.29.0-LLVM-19.1.7-macOS-aarch64-*.zip` |
| macOS arm64 | 20 | `Mull-20-0.29.0-LLVM-20.1.8-macOS-aarch64-*.zip` |
| Ubuntu 24.04 amd64 | 19 | `Mull-19-0.29.0-LLVM-19.1.1-ubuntu-amd64-24.04.deb` |
| Ubuntu 24.04 amd64 | 20 | `Mull-20-0.29.0-LLVM-20.1.2-ubuntu-amd64-24.04.deb` |
| RHEL 9 amd64 | 20 | `Mull-20-0.29.0-LLVM-20.1.8-rhel-amd64-9.6.rpm` |
**Step 3: Install.**
**macOS:**
```bash
# 1. Install the matching LLVM/Clang version via Homebrew
# Check Mull releases for which LLVM versions are available
brew install llvm@18 # or llvm@19, llvm@20
# 2. Download the matching Mull binary
gh release download --repo mull-project/mull \
--pattern 'Mull-18-*-macOS-aarch64-*.zip' # match LLVM version
unzip Mull-18-*.zip
# 3. Install binaries to a known location
sudo mkdir -p /usr/local/bin /usr/local/lib
sudo cp usr/local/bin/mull-runner-* /usr/local/bin/
sudo cp usr/local/bin/mull-reporter-* /usr/local/bin/
sudo cp usr/local/lib/mull-ir-frontend-* /usr/local/lib/
# 4. Verify
mull-runner-18 --version
/opt/homebrew/opt/llvm@18/bin/clang --version
```
**Important macOS notes:**
- The Mull binary's LLVM version must **exactly match** the installed
Clang. Using `brew install llvm@18` with `Mull-19-*` will not work.
- Use the Homebrew Clang, not Apple's system Clang (which is a
different LLVM version and lacks plugin support).
- Set `ulimit -n 1024` before running `mull-runner` (see Environment
Setup section below).
**Ubuntu/Debian:**
```bash
# Option A: Cloudsmith APT repository
curl -1sLf \
'https://dl.cloudsmith.io/public/mull-project/mull-stable/setup.deb.sh' \
| sudo -E bash
sudo apt-get update
sudo apt-get install mull-19 # match your LLVM version
# Option B: Direct .deb from GitHub
gh release download --repo mull-project/mull \
--pattern 'Mull-19-*-ubuntu-amd64-24.04.deb'
sudo dpkg -i Mull-19-*.deb
```
**RHEL/Fedora:**
```bash
# Option A: Cloudsmith RPM repository
curl -1sLf \
'https://dl.cloudsmith.io/public/mull-project/mull-stable/setup.rpm.sh' \
| sudo -E bash
sudo dnf install mull-20 # match your LLVM version
# Option B: Direct .rpm from GitHub
gh release download --repo mull-project/mull \
--pattern 'Mull-20-*-rhel-amd64-*.rpm'
sudo rpm -i Mull-20-*.rpm
```
**Verify installation:**
```bash
mull-runner --version
```
If `mull-runner` is not found after installation, check that the
install prefix is on `$PATH`. **DO NOT** fall back to "manual mutation
analysis" — fix the installation or report the error.
### Configure and Build
Mull requires the project to be compiled with Clang and the Mull
compiler plugin. The plugin injects mutations at the LLVM IR level.
**Key build requirements:**
- Use the **same Clang version** that matches your Mull release
- Pass `-fpass-plugin=<path-to-mull-ir-frontend>` to the compiler
- Use `-g -O0` (debug info required, no optimization)
- **Disable assembly** (`--disable-asm`) — Mull can only mutate
LLVM IR, not hand-written assembly
- Disable hardening flags that interfere: `--disable-ssp --disable-pie`
**Find the plugin path:**
```bash
# The plugin is typically installed alongside mull-runner:
# Linux: /usr/lib/mull-ir-frontend-<N> (or mull-ir-frontend.so)
# macOS: <install-prefix>/lib/mull-ir-frontend-<N>
# Use `find` or `locate` if unsure:
find /usr/local /opt/homebrew /tmp -name "mull-ir-frontend*" 2>/dev/null
```
**Simple projects:**
```bash
MULL_PLUGIN=$(find /usr/local /opt/homebrew -name "mull-ir-frontend*" 2>/dev/null | head -1)
clang -fpass-plugin=$MULL_PLUGIN -g -O0 \
-o test_binary test_main.c src/*.c
```
**Autotools projects (configure/make):**
```bash
MULL_PLUGIN=$(find /usr/local /opt/homebrew -name "mull-ir-frontend*" 2>/dev/null | head -1)
LLVM_BIN=$(dirname $(which clang)) # or /opt/homebrew/opt/llvm@18/bin
CC=$LLVM_BIN/clang \
CFLAGS="-fpass-plugin=$MULL_PLUGIN -g -grecord-command-line -O0" \
./configure --disable-shared --enable-static --disable-asm \
--disable-ssp --disable-pie
make clean && make -j$(nproc)
```
**CMake projects:**
```cmake
set(CMAKE_C_COMPILER clang)
set(CMAKE_CXX_COMPILER clang++)
set(MULL_PLUGIN_PATH "" CACHE STRING "Path to Mull plugin")
if(MULL_PLUGIN_PATH)
add_compile_options(-fpass-plugin=${MULL_PLUGIN_PATH} -g -O0)
endif()
```
```bash
MULL_PLUGIN=$(find /usr/local /opt/homebrew -name "mull-ir-frontend*" 2>/dev/null | head -1)
cmake -B build -DMULL_PLUGIN_PATH=$MULL_PLUGIN
cmake --build build
```
### Run
```bash
# Set FD limit (required on macOS, see Environment Setup)
ulimit -n 1024
# Run with GoogleTest binary
mull-runner --allow-surviving --no-output --timeout=5000 \
--reporters=Elements --report-dir=mull-report ./build/tests
# Run with custom test command
mull-runner --test-program=ctest ./build/tests
# Generate report
mull-runner --report-dir=mull-report ./build/tests
```
**Recommended flags:**
- `--allow-surviving` — don't treat survived mutants as errors
- `--no-output` — suppress stdout/stderr from mutant runs
- `--timeout=5000` — 5 second timeout per mutant (adjust based on
baseline test runtime; use 1000ms for tests completing in <100ms)
- `--reporters=Elements` — JSON output in Mutation Testing Elements
format (machine-parseable for triage)
- `--report-dir=DIR` — write JSON reports to this directory
- `--report-name=NAME` — control output filename (useful when
running multiple test binaries)
- `--workers=N` — parallelism for mutant execution (defaults to
CPU count)
### Parse survived mutants
Mull outputs results to stdout and optionally to report files. Each
survived mutant includes the file path, line number, and mutation type.
```bash
# JSON report (if --report-dir used)
cat mull-report/mutation-testing-report.json | \
jq '.files | to_entries[] | .value.mutants[] |
select(.status == "Survived")'
```
### Environment Setup (Required)
**Before running `mull-runner`, always set a bounded file descriptor
limit.** On macOS (especially Tahoe / macOS 26+), the default
`ulimit -n` is `unlimited`, which causes Mull's subprocess library
(reproc) to fail with `EINVAL` when it tries to close inherited file
descriptors in the forked child process. The fix:
```bash
# REQUIRED before any mull-runner invocation
ulimit -n 1024
```
Add this to your Mull runner scripts or shell session. Without it,
you will see:
```
[error] Cannot run executable: Invalid argument
```
**Root cause:** reproc calls `getrlimit(RLIMIT_NOFILE)` to determine
the max FD to close. When the soft limit is `RLIM_INFINITY`, reproc
computes `max_fd = INT_MAX`, which exceeds its internal
`MAX_FD_LIMIT` (1048576) safety check, causing the child to exit
with `EMFILE`.
### Troubleshooting
| Problem | Solution |
| ------- | -------- |
| `mull-runner: command not found` | Install Mull using the instructions above |
| `Cannot run executable: Invalid argument` | Run `ulimit -n 1024` before `mull-runner` (see Environment Setup above) |
| LLVM version mismatch | Install the LLVM version matching your Mull release |
| Plugin load error | Recompile with matching Clang version |
| No mutants generated | Ensure `-g -O0` flags and Mull plugin are active |
| Tests fail without mutations | Fix test suite first — Mull needs a green baseline |
| Original test failed (timeout) | Increase `--timeout` or skip tests with long baseline runtimes |
---
## C#: Stryker.NET
**Install:**
```bash
dotnet tool install -g dotnet-stryker
```
**Run:**
```bash
dotnet stryker --reporter json
```
**Parse survived mutants:**
```bash
cat StrykerOutput/*/reports/mutation-report.json | \
jq '.files | to_entries[] | .value.mutants[] | select(.status == "Survived")'
```
---
## Ruby: mutant
**Install:**
```bash
gem install mutant
```
**Run:**
```bash
bundle exec mutant run --include lib --require mylib 'MyLib*'
```
**Parse results:** mutant outputs surviving mutations to stdout with
file paths, line numbers, and mutation descriptions.
---
## PHP: Infection
**Install:**
```bash
composer require --dev infection/infection
```
**Run:**
```bash
vendor/bin/infection --show-mutations --min-msi=0
```
**Parse survived mutants:**
```bash
# JSON log at infection-log.json
cat infection-log.json | jq '.survived[]'
```
---
## Haskell: MuCheck or Hedgehog
MuCheck is the primary mutation testing tool for Haskell. For projects
without MuCheck support, property-based testing with Hedgehog or
QuickCheck serves as a mutation-resistant alternative.
### MuCheck
**Install:**
```bash
cabal install MuCheck
```
**Run:**
```bash
mucheck -t "cabal test" src/MyModule.hs
```
MuCheck applies standard mutation operators (negate guards, swap
operators, replace patterns) to the target module and runs the test
suite against each mutant.
**Parse survived mutants:** MuCheck prints results to stdout. Each
survived mutant includes the file path, line number, and mutation
description (e.g., "Negated guard on line 42").
**Limitations:** MuCheck requires the project to build with cabal and
has limited support for large multi-module projects. For Stack-based
projects, wrap the test command: `mucheck -t "stack test" src/Module.hs`.
### Alternative: property-based testing as mutation proxy
For projects where MuCheck is impractical, strong property-based tests
provide equivalent mutation resistance. Properties that assert invariants
over all inputs catch most mutations that MuCheck would surface.
**Hedgehog (preferred):**
```bash
cabal install hedgehog
```
Write properties in `test/` that cover arithmetic, branching, and
boundary behavior. A comprehensive property suite catches the same
classes of defects as mutation testing.
**QuickCheck:**
```bash
cabal install QuickCheck
```
QuickCheck properties work similarly. Use `forAll` with custom generators
to target the input domain of each function under test.
---
## Universal Mutant Record Format
Regardless of framework, normalize each survived mutant to this schema
before feeding into Phase 3 triage:
```json
{
"file_path": "src/parser.py",
"line": 42,
"mutation_type": "arithmetic_operator",
"original": "+",
"replacement": "-",
"function_name": "parse_header",
"status": "survived"
}
```
Map the containing function name by matching `file_path:line` against
trailmark graph nodes using their `location.start_line` and
`location.end_line` ranges.
---
## Necessist: Test Statement Removal
Necessist complements mutation testing by removing statements and method
calls from **test code** and re-running the tests. If a test still passes
after a statement is removed, that statement may be unnecessary —
indicating weak assertions or missing coverage.
Mutation testing mutates production code to check if tests detect changes.
Necessist mutates test code to check if each test statement is actually
needed. Run both when the language supports it.
### Supported Frameworks
| Framework | Language | Auto-detected |
| --------- | -------- | ------------- |
| Anchor | Rust (Solana) | Yes |
| Foundry | Solidity | Yes |
| Go | Go | Yes |
| Hardhat (TypeScript) | TypeScript | Yes |
| Rust | Rust | Yes |
| Vitest | JavaScript/TypeScript | Yes |
Necessist auto-detects the framework from project files. Use `--framework`
to override when auto-detection fails.
### Install
```bash
cargo install necessist
```
### Run
```bash
# Auto-detect framework, run on all test files
necessist
# Explicit framework selection
necessist --framework foundry
# Target specific test files
necessist tests/test_parser.rs tests/test_validator.rs
# Set timeout per test (default 60s, 0 = no timeout)
necessist --timeout 120
# Resume a previous run (results stored in SQLite)
necessist --resume
```
### Parse Results
Necessist stores results in a SQLite database by default. Use `--dump`
to export:
```bash
necessist --dump
```
Each result line contains the test file, line number, the removed
statement, and whether the test passed or failed after removal. Filter
to **passed after removal** entries — these are the findings to triage.
### Configuration
Create `necessist.toml` in the project root (`necessist --default-config`
generates a template):
```toml
ignored_functions = ["println", "eprintln", "dbg"]
ignored_methods = ["clone", "to_string", "unwrap"]
ignored_macros = ["debug_assert", "trace"]
```
- `ignored_functions` — Skip removals of these function calls
- `ignored_methods` — Skip removals of these method calls
- `ignored_macros` — Skip removals of these macro invocations
For Foundry projects, consider ignoring common cheatcodes that are
setup-only (e.g., `vm.label`, `vm.deal` for labeling/funding).
### Normalized Necessist Record Format
Normalize each finding before feeding into Phase 3 triage:
```json
{
"test_file_path": "tests/test_parser.rs",
"test_line": 42,
"removed_statement": "parser.validate(&input)",
"test_function": "test_parse_header",
"status": "passed_after_removal",
"source": "necessist"
}
```
The `source` field distinguishes necessist findings from mutation testing
results during triage and reporting. Map the removed statement to a
production function using the graph analysis algorithm described in the
`genotoxic` skill.
plugins/trailmark/skills/vector-forge/references/report-template.md
+43
View File
@@ -0,0 +1,43 @@
# Vector Forge Report Template
Write the report to `VECTOR_FORGE_REPORT.md` in the working directory.
```markdown
# Vector Forge Report
## Target Algorithm
[Algorithm name and specification reference]
## Implementations Tested
| Library | Language | Type | Mutation Framework |
|---------|----------|------|--------------------|
## Baseline Results (Existing Vectors Only)
[Per-implementation baseline table]
## Escape Analysis
### [Implementation Name]
- Total escaped: N
- By code path:
- [Path 1]: N mutants — [description]
- [Path 2]: N mutants — [description]
## New Vectors Generated
| Vector ID | Target Code Path | Expected Kill |
|-----------|-----------------|---------------|
## After Results (With New Vectors)
[Per-implementation after table]
## Before/After Comparison
[Delta table per implementation]
## Conclusions
[What the vectors caught, what they missed, and why]
```
plugins/trailmark/skills/vector-forge/references/vector-patterns.md
+251
View File
@@ -0,0 +1,251 @@
# Test Vector Patterns for Cryptographic Primitives
Patterns for designing test vectors that target specific code paths
identified through mutation testing escape analysis.
## Contents
- General principles
- Serialization / deserialization vectors
- Signature scheme vectors
- Hash-to-curve vectors
- Pairing-based cryptography vectors
- Aggregate / threshold scheme vectors
- Key encapsulation vectors
- Symmetric cipher vectors
- Mapping escaped mutants to vector patterns
---
## General Principles
### Every Vector Needs a Purpose
Each test vector should target a specific code path or validation
check. Document the purpose in the vector's `comment` field:
```json
{
"tcId": 5,
"comment": "signature with flipped sign bit in G2 y-coordinate",
"result": "invalid",
"flags": ["ModifiedSignature"]
}
```
### Cross-Implementation Verification is Mandatory
A test vector is only trustworthy if two independent implementations
agree on its result. If they disagree, one has a bug — and that
disagreement is itself a valuable finding.
### Negative Vectors are More Valuable Than Positive Ones
Valid-case vectors verify basic correctness. Invalid-case vectors
exercise error handling, validation, and rejection logic — the code
paths where security bugs hide.
### Edge Cases Over Random Cases
Random test vectors exercise the "happy path." Edge cases exercise
boundary conditions where off-by-one errors, overflow, and
validation gaps lurk.
---
## Serialization / Deserialization Vectors
Target: `SetBytes`, `FromCompressed`, `Decode`, `Unmarshal`,
`from_bytes`, `deserialize` and similar functions.
### Point Encoding Vectors (Elliptic Curves)
| Vector Type | Purpose | Expected Result |
|-------------|---------|-----------------|
| Valid compressed point | Baseline correctness | valid |
| Valid uncompressed point | Baseline for uncompressed path | valid |
| Identity / point at infinity | Special case handling | valid or invalid (spec-dependent) |
| Wrong length (truncated) | Length validation | invalid |
| Wrong length (extra bytes) | Length validation | invalid |
| All-zero bytes | Zero-check handling | invalid |
| Field element >= modulus | Field validation | invalid |
| Point not on curve | Curve check | invalid |
| Point on curve but wrong subgroup | Subgroup check | invalid |
| Flipped compression flag bit | Flag parsing | invalid |
| Flipped sign bit | Sign selection | invalid or different point |
| Maximum valid field element | Boundary condition | valid |
| Modulus - 1 as field element | Boundary condition | valid |
| Mixed compressed/uncompressed flags | Flag consistency | invalid |
### Roundtrip Assertions
For every valid deserialization vector, add a roundtrip check:
`serialize(deserialize(bytes)) == bytes`. This catches field
arithmetic corruption (carry propagation, modular reduction,
square root, negation bugs) that produces a valid-looking but
incorrect point — the wrong y-coordinate changes the sort bit
in the re-compressed encoding.
This technique killed 15 previously-missed `Fp` mutations in
the BLS12-381 campaign without requiring knowledge of the
internal field representation.
### Single-Fault Negative Vectors
Each negative vector should isolate ONE validation check by
having exactly one defect. For flag parsing mutations:
| Defect | Construction | Validates |
|--------|-------------|-----------|
| Compression flag cleared | `bytes[0] &= 0x7f` on valid point | Flag bit 7 check |
| Infinity flag set | `bytes[0] \|= 0x40` on non-identity | Flag bit 6 check |
| Sort flag on identity | `bytes = [0xe0, 0, ...]` | Identity + flag consistency |
| Compression cleared on identity | `bytes = [0x40, 0, ...]` | Identity encoding check |
| Both infinity + sort | `bytes[0] \|= 0x60` on valid point | Multi-flag validation |
| Wrong length | 192 bytes with compression flag | Length vs flag consistency |
Keep the underlying field element valid so the ONLY reason for
rejection is the flag. This is what kills `&` → `|` mutations
in `from_compressed_unchecked`.
### Scalar Encoding Vectors
| Vector Type | Purpose | Expected Result |
|-------------|---------|-----------------|
| Zero scalar | Zero handling | valid (context-dependent) |
| One scalar | Identity element | valid |
| Group order - 1 | Maximum valid | valid |
| Group order | Reduction check | invalid or reduced to zero |
| Group order + 1 | Overflow handling | invalid or reduced to one |
| All-ones bytes | Large value handling | invalid (usually > order) |
| Non-canonical encoding | Reduction behavior | depends on spec |
---
## Signature Scheme Vectors
Target: `Verify`, `Sign`, `verify`, `core_verify` and similar.
### Single Signature Vectors
| Vector Type | Purpose | Expected Result |
|-------------|---------|-----------------|
| Valid signature on empty message | Empty input handling | valid |
| Valid signature on single byte | Minimal input | valid |
| Valid signature on large message | No length limits | valid |
| Wrong message (1 bit flip) | Verification correctness | invalid |
| Wrong public key | Key binding | invalid |
| Truncated signature | Length check | invalid |
| Signature with extra bytes | Strict parsing | invalid |
| Identity point as signature | Identity rejection | invalid |
| Identity point as public key | Identity rejection | invalid |
| Negated signature | Sign check | invalid |
| Signature from wrong scheme/DST | Cross-scheme isolation | invalid |
| All-zero signature bytes | Degenerate input | invalid |
| Signature with field overflow | Field validation | invalid |
### Multi-Signature / Aggregate Vectors
| Vector Type | Purpose | Expected Result |
|-------------|---------|-----------------|
| 1 signer, valid | Minimal aggregate | valid |
| N signers, all valid | Standard case | valid |
| N signers, one wrong message | Detects per-message binding | invalid |
| Mismatched pubkey/message count | Input validation | invalid |
| Empty signer list | Empty input handling | invalid |
| Duplicate messages (rogue key attack) | See spec requirements | invalid |
| Identity key in aggregate | Identity rejection | invalid |
| Identity signature in aggregate | Identity rejection | invalid |
---
## Hash-to-Curve Vectors
Target: `HashToG1`, `HashToG2`, `hash_to_curve`, `encode_to_curve`.
### Known Answer Tests (KATs)
| Vector Type | Purpose | Expected Result |
|-------------|---------|-----------------|
| Empty message | Empty input handling | known point |
| Single byte 0x00 | Minimal non-empty | known point |
| ASCII string "abc" | Standard test | known point |
| Long message (128+ bytes) | No length restrictions | known point |
| Very long message (256+ bytes) | Large input handling | known point |
| RFC test vectors | Spec compliance | known point |
Hash-to-curve vectors must use a specific DST (domain separation
tag) and the expected output must be computed by a reference
implementation.
---
## Pairing-Based Cryptography Vectors
Target: `PairingCheck`, `MillerLoop`, `FinalExponentiation`,
`multi_miller_loop`, `pairing`.
### Pairing Check Vectors
| Vector Type | Purpose | Expected Result |
|-------------|---------|-----------------|
| e(P, Q) == e(P, Q) | Reflexivity | pass |
| e(aP, Q) == e(P, aQ) | Bilinearity | pass |
| e(P, O) == 1 | Identity handling (O = point at infinity) | pass |
| e(O, Q) == 1 | Identity handling | pass |
| e(P, Q) with P not in G1 | Subgroup check | fail or undefined |
| e(P, Q) with Q not in G2 | Subgroup check | fail or undefined |
| Multi-pairing with n=1 | Minimal multi-pairing | matches single pairing |
| Multi-pairing with n=0 | Empty input | implementation-defined |
---
## Key Encapsulation Vectors (KEM)
Target: `Encapsulate`, `Decapsulate`, `encaps`, `decaps`.
| Vector Type | Purpose | Expected Result |
|-------------|---------|-----------------|
| Valid encaps/decaps roundtrip | Correctness | shared secrets match |
| Modified ciphertext (1 bit flip) | Ciphertext integrity | decaps fails or different secret |
| Wrong secret key | Key binding | decaps fails or different secret |
| Truncated ciphertext | Length validation | error |
| All-zero ciphertext | Degenerate input | error |
| Known-answer test (deterministic encaps) | Spec compliance | known ciphertext + secret |
---
## Mapping Escaped Mutants to Vector Patterns
When escape analysis (Phase 4) identifies survived mutants, use
this mapping to select appropriate vector patterns:
| Mutant Location | Mutant Type | Vector Pattern |
|-----------------|-------------|----------------|
| Length check (`len != N`) | CONDITIONALS_BOUNDARY | Truncated / extended inputs |
| Field validation (`>= modulus`) | CONDITIONALS_NEGATION | Field overflow values |
| Subgroup check | CONDITIONALS_NEGATION | Wrong-subgroup points |
| Identity check (`IsInfinity`) | CONDITIONALS_NEGATION | Identity point inputs |
| Sign bit handling | ARITHMETIC_BASE | Negated / flipped-sign inputs |
| Error return path | CONDITIONALS_NEGATION | Input triggering that error |
| Serialization flag parsing | ARITHMETIC_BASE | All flag combinations |
| Loop bound (`i < n`) | INCREMENT_DECREMENT | Boundary-length inputs |
| Arithmetic operation | INVERT_NEGATIVES | KATs verifying exact output |
### Example: Mapping gnark-crypto BLS12-381 Escapes
```
marshal.go:117-352 (streaming encoder, NOT COVERED)
→ Not reachable via SetBytes/Bytes API
→ Need vectors exercising io.Writer-based Encode/Decode
→ Pattern: Serialization vectors via streaming API
pairing.go:352-394 (Miller loop internals, NOT COVERED)
→ Reachable via PairingCheck but specific arithmetic lines
don't have distinguishing inputs
→ Pattern: Pairing bilinearity KATs with edge-case points
g1.go:184, g2.go:191 (endomorphism, NOT COVERED)
→ Only used in multi-scalar multiplication optimization
→ Pattern: Large-scalar multiplication with known answers
```