mirror of https://github.com/trailofbits/skills synced 2026-06-21 14:12:00 +00:00

Files

T

Scott Arciszewski 6b79b5e879 feat(trailmark): skills that reason about code as graphs (#133 )

* 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>

2026-03-31 17:31:30 -04:00

.claude-plugin

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

2026-03-31 17:31:30 -04:00

skills

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

2026-03-31 17:31:30 -04:00

README.md

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

2026-03-31 17:31:30 -04:00

README.md

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 (source) must be installed:

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

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

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

README.md

trailmark

Prerequisites

Skills

Directory Structure

Related Skills