Files
trailofbits-skills/.codex/skills/graph-evolution
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

Symbolic link
1 line
46 B
Plaintext

../../plugins/trailmark/skills/graph-evolution