Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
212 changes: 207 additions & 5 deletions AGENTS.md
Original file line number Diff line number Diff line change
@@ -1,10 +1,18 @@
<!-- Auto-generated by `rivet init --agents`. Re-run to update after artifact changes. -->
# AGENTS.md — Rivet Project Instructions
<!--
MIXED FILE:
- Sections under "## Rivet Artifact Reference" below are auto-generated by
`rivet init --agents`. Re-run that command after artifact changes.
- Sections under "## Project Guidance (Manually Maintained)" are NOT
auto-generated. Preserve them during regeneration. If `rivet init --agents`
overwrites this file without preserving them, restore from git history.
-->
# AGENTS.md — Sigil Project Instructions

> This file was generated by `rivet init --agents`. Re-run the command
> any time artifacts change to keep this file current.
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.

## Project Overview
## Rivet Artifact Reference

This project uses **Rivet** for SDLC artifact traceability.
- Config: `rivet.yaml`
Expand Down Expand Up @@ -127,3 +135,197 @@ Required git trailers:
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](https://pulseengine.eu/guides/VERIFICATION-GUIDE.md) 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:

```bash
# 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**:
```bash
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
```bash
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
```bash
gh pr merge <PR#> --squash
```

5. **Create release**: Only after merge and main CI passes
```bash
# 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

```bash
# 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
121 changes: 12 additions & 109 deletions CLAUDE.md
Original file line number Diff line number Diff line change
@@ -1,113 +1,16 @@
# Claude Code Instructions for wsc
# CLAUDE.md

## Project Overview
**IMPORTANT — Read [`AGENTS.md`](AGENTS.md) first.** It is the canonical
AI-instruction file for this repository. Cursor, OpenCode, Claude Code, and
other coding agents all read AGENTS.md; keeping project guidance there
avoids drift.

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
All substantive project guidance — overview, formal-verification rules,
Mythos bug-hunt pipeline, release process, build commands, repository
structure, CI workflows — lives in `AGENTS.md`. Do not duplicate it here.

## Formal Verification
## Claude Code-specific notes

Follow the [PulseEngine Verification Guide](https://pulseengine.eu/guides/VERIFICATION-GUIDE.md) 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

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

### Release Process

1. **Create version bump PR**:
```bash
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
```bash
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
```bash
gh pr merge <PR#> --squash
```

5. **Create release**: Only after merge and main CI passes
```bash
# 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

```bash
# 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

## 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
Currently none. Add Claude-Code-only settings (hook configurations, skill
invocations, etc.) below this line if and when they diverge from the
cross-tool guidance.
Loading
Loading