stave-lib.md

gistfile1.txt

Organize the 30 HackerOne reports by **attack stage**.
That gives you two useful outputs:

1. **End-to-end fixtures** for Stave
2. **Article series** that explains real risk patterns clearly

Use this pipeline:

```text
report → incident pattern → attack stage → invariant → fixture → article
```

The report is raw evidence.
The incident pattern is the reusable lesson.
The attack stage shows where it fits in the attacker path.
The invariant turns it into something Stave can evaluate.
The fixture proves the invariant works.
The article explains business value.

## Attack-stage buckets

| Stage                 | Meaning                                       | Example Stave angle                                                |
| --------------------- | --------------------------------------------- | ------------------------------------------------------------------ |
| Discovery             | Attacker finds exposed asset                  | Public bucket, guessable object paths, exposed website endpoint    |
| Access                | Attacker can read/list/write                  | Public read, public list, authenticated-users grant                |
| Expansion             | Attacker moves from one exposure to more data | Wildcard policy, broad prefix access, cross-account trust          |
| Persistence           | Exposure survives because controls are weak   | PAB masking latent public policy, stale config, missing guardrail  |
| Exfiltration Evidence | Data could be pulled or was pulled            | Readable sensitive objects, missing logging, anonymous access gaps |
| Prevention            | Control that would have stopped recurrence    | SCP, Terraform PAB, invariant policy, CI check                     |

This is simple enough for articles and precise enough for fixtures.

## Fixture layout

Use one fixture folder per reusable scenario.

```text
fixtures/e2e/hackerone/
  001-public-read-policy/
    report.md
    metadata.yaml
    before.obs.json
    invariant.yaml
    expected.out.json
    after.obs.json
    remediation.md

  002-public-list-enabled/
    report.md
    metadata.yaml
    before.obs.json
    invariant.yaml
    expected.out.json
    after.obs.json
    remediation.md
```

Avoid naming folders after the company.
Use the vulnerability pattern instead.

## Metadata schema

```yaml
id: H1-S3-001
title: Public read through bucket policy
source_type: hackerone_report
source_url: "..."
attack_stage: access
cloud: aws
service: s3
pattern: public-read-policy
stave_invariant: INV.S3.PUBLIC.001
article_status: draft
fixture_status: implemented
sensitive_data_type:
  - customer_data
  - documents
business_risk:
  - data_disclosure
  - compliance_exposure
```

This metadata becomes your publishing index later.

## Article mapping

Each fixture can produce one article.

```text
Article title:
How a Public S3 Bucket Policy Creates a Data Disclosure Risk

Article structure:
1. The misconfiguration
2. What the HackerOne report showed
3. Why this matters
4. The AWS configuration state
5. The Stave invariant
6. The failing fixture
7. The remediation
8. The passing fixture
9. The prevention lesson
```

Do not create 30 totally unique categories.
Group them into 6–10 reusable patterns.

Example:

| Pattern                        |            Attack stage | Fixture count |
| ------------------------------ | ----------------------: | ------------: |
| Public read                    |                  Access |             6 |
| Public list                    |      Discovery / Access |             4 |
| Public write                   |      Access / Expansion |             3 |
| Sensitive object path exposure |               Discovery |             4 |
| Wildcard bucket policy         |               Expansion |             3 |
| Cross-account access           |               Expansion |             3 |
| Missing logging                |   Exfiltration Evidence |             2 |
| PAB masks latent exposure      |             Persistence |             2 |
| Website hosting exposure       |      Discovery / Access |             2 |
| Dangling origin / takeover     | Discovery / Persistence |             1 |

This gives you article clusters instead of isolated posts.

A HackerOne report should not become the fixture.

The **reusable configuration defect** should become the fixture.

Bad:

```text
fixtures/hackerone/shopify-report-12345/
```

Better:

```text
fixtures/e2e/s3-public-read-policy/
```

Stave is about preventing a class of bugs.

## Suggested first 10 fixtures

Start with the most article-friendly cases.

| Order | Fixture                          | Why first                                 |
| ----: | -------------------------------- | ----------------------------------------- |
|     1 | Public read bucket policy        | easiest to explain                        |
|     2 | Public list bucket policy        | clear discovery risk                      |
|     3 | Public ACL read                  | common legacy issue                       |
|     4 | AuthenticatedUsers grant         | non-obvious public-ish exposure           |
|     5 | Public website hosting           | easy for readers to visualize             |
|     6 | Wildcard `s3:*` action           | strong policy lesson                      |
|     7 | Prefix-level sensitive exposure  | more realistic than whole-bucket exposure |
|     8 | Missing full Public Access Block | strong prevention angle                   |
|     9 | PAB masking latent public policy | strong Stave differentiator               |
|    10 | Missing access logging           | evidence and audit angle                  |

## Publishing strategy

Publish by attack stage.

Suggested sequence:

```text
Series 1: Discovery
Series 2: Access
Series 3: Expansion
Series 4: Persistence
Series 5: Evidence
Series 6: Prevention
```

implement fixtures by invariant.

```text
engineering organization = by invariant
article organization = by attack stage
```

Use this structure:

```text
/fixtures/e2e/by-invariant/
/content/articles/by-attack-stage/
/data/cases/hackerone-index.yaml
```

One source index connects everything.

```text
HackerOne report
  → case index entry
  → invariant fixture
  → article
```

This gives you traceability, reusable tests, and a clean publishing system.

Do not force each HackerOne report into only one stage.

A real case can touch multiple stages:

```text
public bucket listing
→ discovery

public object read
→ access

sensitive files exposed
→ exfiltration risk

missing guardrail
→ prevention failure
```

So use **one primary stage** and optional secondary stages.

## Better model

```yaml
id: H1-S3-001
pattern: public-list-and-read
primary_stage: access
secondary_stages:
  - discovery
  - exfiltration_evidence
  - prevention
invariants:
  - INV.S3.PUBLIC.LIST.001
  - INV.S3.PUBLIC.READ.001
```

Use the **primary stage** for article placement.
Use **all relevant stages** for analysis.

Example:

| Report                    | Primary stage | Secondary stages    |
| ------------------------- | ------------- | ------------------- |
| Public bucket list + read | Access        | Discovery, Evidence |
| Public website bucket     | Discovery     | Access, Prevention  |
| Wildcard S3 policy        | Expansion     | Access, Prevention  |
| PAB masks public policy   | Persistence   | Access, Prevention  |
| Missing S3 logging        | Evidence      | Prevention          |

A **report** may overlap.
A **fixture** should be narrow.

Bad fixture:

```text
public-list-read-sensitive-data-missing-logging/
```

Better fixtures:

```text
s3-public-list/
s3-public-read/
s3-sensitive-prefix-readable/
s3-server-access-logging-missing/
```

Then one HackerOne case can reference multiple fixtures.

```text
Report = messy real-world story
Fixture = one precise defect
Article = one teaching angle
Invariant = one enforceable rule
```

So the overlap belongs in the **case index**, not inside the fixture.

You should expect **repeating cases** across different HackerOne reports.
The goal is not 30 unique vulnerability types.
The goal is to show that the **same configuration defect repeats across companies**.

```text
many reports → one reusable defect pattern → one Stave invariant
```

Example:

```text
HackerOne report A: public S3 read
HackerOne report B: public S3 read
HackerOne report C: public S3 read

→ Pattern: public object read
→ Invariant: S3 buckets must not allow public read
→ Fixture: s3-public-read-policy
```

## Do not create duplicate fixtures

Bad:

```text
fixtures/h1-report-001-public-read/
fixtures/h1-report-014-public-read/
fixtures/h1-report-022-public-read/
```

Better:

```text
fixtures/e2e/s3-public-read-policy/
```

Then reference all related reports in metadata:

```yaml
pattern: s3-public-read-policy
invariant: INV.S3.PUBLIC.READ.001
related_reports:
  - h1_report_001
  - h1_report_014
  - h1_report_022
frequency: 3
```

## Repetition becomes evidence

In the article, repetition gives you a stronger claim:

```text
This is not a one-off bug.
The same S3 exposure pattern appears across multiple HackerOne reports.
That means the risk is systemic.
```

That supports Stave’s message:

```text
Do not fix one bucket.
Prevent the configuration state from existing again.
```

## Practical organization

Use three layers:

```text
/cases/hackerone/
  h1-001.yaml
  h1-002.yaml
  h1-003.yaml

/patterns/
  s3-public-read-policy.yaml
  s3-public-list-policy.yaml
  s3-public-write-acl.yaml

/fixtures/e2e/
  s3-public-read-policy/
  s3-public-list-policy/
  s3-public-write-acl/
```

A HackerOne report is **evidence**.
A pattern is **the reusable lesson**.
A fixture is **the executable proof**.

So repeating cases should not repeat fixtures.
They should increase the confidence score for the pattern.

Use your **Stave Go library** as the domain layer.
Use **Z3** as the reasoning engine.

Do not put Z3 everywhere.

Use this boundary:

```text
AWS snapshot JSON
→ Stave domain model
→ Stave facts
→ Z3 constraints
→ solver result
→ Stave finding/report
```

Z3 has official Go bindings, but they use CGO and require the Z3 native library/toolchain. The Z3 repo documents Go bindings, Go 1.20+, and `-DZ3_BUILD_GO_BINDINGS=ON` for CMake builds.

Stave should own the cloud/security language.

Examples:

```text
Bucket
BucketPolicy
Principal
Action
Resource
PublicAccessBlock
Finding
Invariant
Evidence
```

This code should not know much about Z3.

## What Z3 should own

Z3 should answer logic questions.

Examples:

```text
Can any public principal read this bucket?
Can any principal write outside the allowed prefix?
Is there any counterexample to this invariant?
Can this policy ever allow public access?
```

Think of Z3 as a **counterexample finder**.

Stave asks:

```text
Is unsafe state possible?
```

Z3 answers:

```text
sat     → yes, here is a counterexample
unsat   → no, the invariant holds
unknown → solver could not prove it
```

## First program to write

Start with a tiny program outside the main CLI.

```text
cmd/stave-z3-lab/
  main.go
```

Goal:

```text
load one Stave observation
encode one S3 rule into Z3
print sat / unsat
```

Example question:

```text
Can a public principal perform s3:GetObject on this bucket?
```

Input:

```json
{
  "bucket": "patient-records",
  "policy_allows_public_read": true,
  "public_access_block_enabled": false
}
```

Z3 model:

```text
publicPrincipal = true
action = GetObject
policyAllows = true
pabBlocks = false

unsafe = publicPrincipal AND actionIsRead AND policyAllows AND NOT pabBlocks
```

Expected result:

```text
sat
```

Meaning:

```text
An unsafe access path exists.
```

## Better first set of programs

Write 5 small programs before integrating into Stave.

| Program             | Purpose                                |
| ------------------- | -------------------------------------- |
| `z3-hello`          | Learn `sat`, `unsat`, model output     |
| `z3-public-read`    | Check public S3 read                   |
| `z3-public-write`   | Check public S3 write                  |
| `z3-prefix-scope`   | Check write outside allowed prefix     |
| `z3-counterexample` | Print why the unsafe state is possible |

## Best first Stave use case

Start with **policy reachability**, not compliance reporting.

Good first question:

```text
Is there any principal/action/resource combination that violates the invariant?
```

Example invariant:

```text
No public principal may read objects from a bucket containing PHI.
```

Z3 formulation:

```text
exists principal, action, resource:
  isPublic(principal)
  AND isRead(action)
  AND isPHIBucket(resource)
  AND policyAllows(principal, action, resource)
```

If Z3 returns `sat`, Stave creates a finding.

## Keep the architecture clean

Use an interface:

```go
type Solver interface {
    Check(ctx context.Context, facts Facts, invariant Invariant) (Result, error)
}
```

Then create:

```text
internal/solver/cel
internal/solver/z3
```

CEL remains good for direct evaluation.

Z3 is for deeper reasoning:

| Use CEL                   | Use Z3                       |
| ------------------------- | ---------------------------- |
| Direct snapshot checks    | Existence questions          |
| Simple predicates         | Counterexamples              |
| Known fields              | Unknown combinations         |
| Fast deterministic checks | Reachability-style reasoning |
| Reporting rules           | Policy satisfiability        |

Do not make Stave depend on Z3 at the core.
It also avoids forcing every Stave user to install native Z3 dependencies.

## Suggested package structure

```text
/stave
  /pkg/stave
    observation.go
    invariant.go
    finding.go

  /internal/reason
    facts.go
    solver.go
    result.go

  /internal/reason/z3
    encoder.go
    solver.go
    model.go

  /cmd/stave-z3-lab
    main.go
```

Start by writing small Go programs that use:

```text
Stave library → extract facts
Z3 library → answer one logic question
```

Then integrate only the useful patterns back into Stave.