Skip to content

AGENTS.md

Latest commit

 

History

History
336 lines (268 loc) · 16.4 KB

AGENTS.md

File metadata and controls

336 lines (268 loc) · 16.4 KB

AGENTS.md — Sigil Project Instructions

This is the canonical AI-instruction file for this repository. Cursor, OpenCode, Claude Code, and other coding agents should all read this first. CLAUDE.md mandates reading this file.

Rivet Artifact Reference

This project uses Rivet for SDLC artifact traceability.

  • Config: rivet.yaml
  • Schemas: common, dev, stpa, stpa-sec, cybersecurity
  • Artifacts: 452 across 23 types
  • Validation: rivet validate (current status: 9 errors)

Available Commands

Command Purpose Example
rivet validate Check link integrity, coverage, required fields rivet validate --format json
rivet list List artifacts with filters rivet list --type requirement --format json
rivet stats Show artifact counts by type rivet stats --format json
rivet add Create a new artifact rivet add -t requirement --title "..." --link "satisfies:SC-1"
rivet link Add a link between artifacts rivet link SOURCE -t satisfies --target TARGET
rivet serve Start the dashboard rivet serve --port 3000
rivet export Generate HTML reports rivet export --format html --output ./dist
rivet impact Show change impact rivet impact --since HEAD~1
rivet coverage Show traceability coverage rivet coverage --format json
rivet diff Compare artifact versions rivet diff --base path/old --head path/new

Artifact Types

Type Count Description
asset 25 An item of value requiring protection — data, function, or component. Identified during TARA (ISO 21434 clause 8).
attack-scenario 33 A security-specific causal pathway describing how a threat agent could cause an unsecure control action or exploit a data flow. Extends STPA loss scenarios with attacker intent, attack feasibility scoring (ISO 21434 Annex H), and links to threat agents.
control-action 14 An action issued by a controller to a controlled process or another controller.
controlled-process 8 A process being controlled — the physical or data transformation acted upon by controllers.
controller 13 A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process.
controller-constraint 26 A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do.
cybersecurity-design 27 Architecture or design element addressing cybersecurity requirements. SEC.2 outcome — security mechanisms, protocols, algorithms.
cybersecurity-goal 13 A top-level cybersecurity requirement derived from TARA results. Equivalent to a cybersecurity goal in ISO 21434 clause 9.
cybersecurity-implementation 3 Implementation artifact for a cybersecurity design element. SEC.3 outcome — code, configuration, key management.
cybersecurity-req 24 A detailed cybersecurity requirement derived from cybersecurity goals. SEC.1 outcome (ISO 21434 clause 9).
cybersecurity-verification 34 Verification measure for cybersecurity requirements. SEC.4 outcome — includes penetration testing, fuzzing, code review, static analysis, vulnerability scanning.
data-flow 22 A flow of data between controllers, controlled processes, or external entities. Data flows are first-class objects in STPA-DFSec, enabling analysis of confidentiality, integrity, and availability properties on data in transit — not just control actions. Critical for reasoning about key material, tokens, certificates, and trust bundles moving through the system.
design-decision 7 An architectural or design decision with rationale
feature 11 A user-visible capability or feature
hazard 35 A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss.
loss 10 An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent.
requirement 14 A functional or non-functional requirement
risk-assessment 24 Combined risk level from threat feasibility and impact. Determines whether a cybersecurity goal is needed (ISO 21434 clause 8).
security-property 12 A security property (CIA + authenticity + non-repudiation) required on a controlled process, data flow, or controller. Annotates the STPA control structure with security-specific requirements that drive the identification of unsecure control actions.
system-constraint 33 A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard.
threat-agent 5 An entity (person, organization, or automated system) that could intentionally or unintentionally cause an unsecure control action. Models attacker capability, motivation, and access level for feasibility assessment aligned with ISO/SAE 21434 Annex H.
threat-scenario 24 A potential attack scenario against an asset. Part of TARA (ISO 21434 clause 8).
uca 35 An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long
loss-scenario 0 A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard.
sub-hazard 0 A refinement of a hazard into a more specific unsafe condition.

Working with Artifacts

File Structure

  • Artifacts are stored as YAML files in: artifacts
  • Schema definitions: schemas/ directory
  • Documents: docs, docs/security, .

Creating Artifacts

rivet add -t requirement --title "New requirement" --status draft --link "satisfies:SC-1"

Validating Changes

Always run rivet validate after modifying artifact YAML files. Use rivet validate --format json for machine-readable output.

Link Types

Link Type Description Inverse
acts-on Control action acts on a process or controller acted-on-by
allocated-to Source is allocated to the target (e.g. requirement to architecture component) allocated-from
assesses Risk assessment evaluates a threat scenario assessed-by
carries Control action or feedback carries a data flow carried-by
caused-by-uca Loss scenario is caused by an unsafe control action causes-scenario
constrained-by Source is constrained by the target constrains
constrains-controller Constraint applies to a specific controller controller-constrained-by
depends-on Source depends on target being completed first depended-on-by
derives-from Source is derived from the target derived-into
executed-by Attack scenario is executed by a threat agent executes
exploits Attack scenario exploits an unsecure control action or data flow exploited-by
flows-from Data flow originates from a controller or process sends-flow
flows-to Data flow is received by a controller or process receives-flow
implements Source implements the target implemented-by
inverts-uca Controller constraint inverts (is derived from) an UCA inverted-by
issued-by Control action or UCA is issued by a controller issues
leads-to-hazard UCA or loss scenario leads to a hazard hazard-caused-by
leads-to-loss Hazard leads to a specific loss loss-caused-by
mitigates Source mitigates or prevents the target mitigated-by
prevents Constraint prevents a hazard prevented-by
property-of Security property applies to a process, flow, or controller has-property
protects System constraint or controller constraint protects a security property protected-by
refines Source is a refinement or decomposition of the target refined-by
satisfies Source satisfies or fulfils the target satisfied-by
threatens Threat scenario threatens an asset threatened-by
traces-to General traceability link between any two artifacts traced-from
verifies Source verifies or validates the target verified-by
violates-property UCA or loss scenario violates a security property property-violated-by

Conventions

  • Artifact IDs follow the pattern: PREFIX-NNN (e.g., REQ-001, FEAT-042)
  • Use rivet add to create artifacts (auto-generates next ID)
  • Always include traceability links when creating artifacts
  • Run rivet validate before committing

Commit Traceability

This project enforces commit-to-artifact traceability.

Required git trailers:

  • Fixes -> maps to link type fixes
  • Implements -> maps to link type implements
  • Refs -> maps to link type traces-to
  • Satisfies -> maps to link type satisfies
  • Verifies -> maps to link type verifies

Exempt artifact types (no trailer required): chore, style, ci, docs, build

To skip traceability for a commit, add: Trace: skip

Project Guidance (Manually Maintained)

The content below is NOT auto-generated by rivet. Preserve it during rivet init --agents regeneration. If the tool overwrites this section, restore it from git history.

Project Overview

sigil (wsc — WebAssembly Signature Component) is a security-critical cryptographic signing tool for WebAssembly modules. It handles:

  • Ed25519 signatures
  • Sigstore keyless signing (OIDC → Fulcio → Rekor)
  • Air-gapped verification for embedded devices
  • Trust bundle management

Formal Verification

Follow the PulseEngine Verification Guide for all proof work. Key rules:

  1. Get the spec right before attempting proofs
  2. Try the simple thing first — let the solver attempt it
  3. Generate multiple candidates (3–5 strategies before concluding hard)
  4. Code must satisfy all verification tracks simultaneously (Rust + Verus + coq-of-rust + Kani)
  5. No Vec in Verus specs — use Seq; no trait objects in verified code

Kani scope limitation

Kani/CBMC runs out of memory on code that exercises std::io (BufReader, BorrowedBuf), rich Vec manipulation, or deep generic trait dispatch. When a Kani harness OOMs, that is NOT evidence the property holds — it is evidence the tool cannot reach the property. Fall back to the nearest lower-level Kani proof on the primitives the code composes (see existing proofs in src/lib/src/wasm_module/varint.rs for examples), and document the limitation in the finding report.

Mythos Bug-Hunt Pipeline

Mythos-style agentic bug hunting is wired into this repo. Prompts, rubric, and the portable HOWTO live in scripts/mythos/:

  • rank.md — file ranking (1–5) by bug likelihood, sigil-specific rubric
  • discover.md — per-file discovery prompt with oracle requirement
  • validate.md — fresh-session confirmation (rejects hallucinations)
  • emit.md — converts confirmed findings to draft AS-N entries in artifacts/stpa/attack-scenarios.yaml, grouped under existing UCAs
  • HOWTO.md — portable pipeline documentation (same across all PulseEngine repos)

Oracle requirement (invariant)

A failing PoC test is ALWAYS required for a confirmed finding — this is the deterministic oracle. A failing Kani harness is required unless the subject code exercises a symbolic surface CBMC cannot handle (see Kani scope limitation above); in that case, cite the nearest primitive-layer Kani proof and document the limitation. Hallucinations are more expensive than silence. If neither oracle can be produced, the finding does not count — do not report it.

Pre-Release Mythos delta pass (MANDATORY)

Before creating a release tag, run a Mythos delta pass scoped by release type:

Release Scope
Patch (x.y.Z) Tier-5 files changed since last tag
Minor (x.Y.z) Tier-5 + tier-4 files changed since last tag
Major / LTS Full tier-5 sweep regardless of diff

Procedure:

# Identify changed tier-5 files
git diff --name-only v<last>..HEAD -- \
  src/lib/src/wasm_module/ \
  src/lib/src/signature/keys.rs \
  src/lib/src/signature/sig_sections.rs \
  src/lib/src/airgapped/bundle.rs \
  src/lib/src/airgapped/tuf.rs \
  src/lib/src/secure_file.rs \
  src/lib/src/dsse.rs \
  src/lib/src/platform/ \
  src/lib/src/provisioning/ca.rs

For each file, in a fresh Claude Code session:

Read scripts/mythos/discover.md and apply it to <file>. Do not relax the
oracle requirement.

For each finding, fresh session: Read scripts/mythos/validate.md and apply it to the report above.

Block the release if any confirmed finding lacks an approved AS-N in artifacts/stpa/attack-scenarios.yaml with a shipped fix or an explicit risk-acceptance note.

Security-Critical Release Process

THIS IS A CRYPTOGRAPHIC SECURITY TOOL. RELEASES MUST FOLLOW THIS PROCESS:

Pre-Release Checklist (MANDATORY)

  1. All changes via PR: Never push directly to main for any code changes
  2. CI must pass completely: Wait for ALL CI jobs to succeed before merging
  3. Watch the full CI run: Do not assume CI passes - verify it
  4. Sign & Verify workflow must succeed: The wasm-signing.yml workflow must demonstrate end-to-end signing and verification works
  5. Mythos delta pass: Run per ### Pre-Release Mythos delta pass above. Zero confirmed findings, OR every confirmed finding maps to an approved AS-N in artifacts/stpa/attack-scenarios.yaml with a shipped fix

Release Process

  1. Create version bump PR:

    git checkout -b release/vX.Y.Z
# Update version in Cargo.toml
# Update internal dependency versions
git commit -m "chore: bump version to X.Y.Z"
git push -u origin release/vX.Y.Z
gh pr create

  2. Wait for CI to complete: Watch ALL checks pass

    gh pr checks <PR#> --watch

  3. Verify signing workflow: Ensure the Sign WASM Module workflow succeeds and produces valid artifacts

  4. Merge PR: Only after all checks pass

    gh pr merge <PR#> --squash

  5. Create release: Only after merge and main CI passes

    # Pull latest main
git checkout main && git pull

# Verify main CI passed
gh run list --branch main --limit 1

# Create and push tag
git tag -a vX.Y.Z -m "Release vX.Y.Z"
git push origin vX.Y.Z

# Create GitHub release
gh release create vX.Y.Z --generate-notes

What NOT to do

  • NEVER release without CI verification
  • NEVER push tags before PR is merged and CI passes
  • NEVER assume CI will pass - always watch it complete
  • NEVER skip the signing workflow verification
  • NEVER release if any security-related test fails

Build Commands

# Build
cargo build --release

# Test (all tests)
cargo test

# Test specific module
cargo test --test airgapped_e2e
cargo test --test keyless_integration -- --ignored  # Requires OIDC

# Bazel build
bazel build //src/lib:wsc
bazel build //src/component:signing_lib
bazel build //src/cli:wasmsign_cli

Repository Structure

  • src/lib/ - Core signing library
  • src/cli/ - Command-line interface
  • src/component/ - WASM component (WASI)
  • src/lib/src/airgapped/ - Air-gapped verification
  • src/lib/src/keyless/ - Sigstore keyless signing
  • fuzz/ - Fuzz testing targets
  • scripts/mythos/ - Mythos bug-hunt pipeline prompts

CI Workflows

  • rust.yml - Main CI (cargo + bazel builds, tests)
  • wasm-signing.yml - End-to-end signing demonstration
  • fuzz.yml - Fuzz testing
  • memory.yml - Memory profiling

Memory profiling reproducibility note: Memory profiling via Dockerfile.bytehound is not in the hermetic build path. The bytehound image clones upstream and builds with cargo +nightly, so reproducibility is best-effort, not bit-exact (unlike the Nix flake).