DEV Community: Bala Paranj

Visual Regression Testing for CLIs with VHS

Bala Paranj — Mon, 18 May 2026 12:06:31 +0000

How to use Charm's VHS to create GIF-based visual regression tests for your CLI's terminal output — catching formatting bugs that unit tests miss.

Your CLI's unit tests verify that the right data comes out. But they don't test what the user actually sees.

A missing newline. A table column that wraps at 80 characters. A progress spinner that bleeds into the output. An ANSI color code that renders as garbage on a light terminal theme. These are visual bugs that pass every unit test but make your CLI look broken.

VHS by Charm solves this by recording your terminal as a GIF from a script — and you can use those GIFs as visual regression tests.

Using VHS

VHS reads a .tape file that describes terminal interactions:

# demo.tape
Output demo.gif
Set Width 120
Set Height 40
Set Theme "Monokai"

Type "stave apply --controls ./controls --observations ./obs --format text"
Enter
Sleep 2s

Run it:

vhs demo.tape

Output: demo.gif — a pixel-perfect recording of what the terminal looks like when that command runs.

How This Differs from Asciinema

	Asciinema (.cast)	VHS (.gif/.png)
Output	Text-based replay (NDJSON)	Pixel-based image (GIF/PNG/WebM)
Renders	In a JavaScript player	As a static image anywhere
Tests	Text content correctness	Visual formatting correctness
Use case	Documentation, interactive replay	README badges, visual regression
File size	Small (text)	Large (image)
Searchable	Yes (it's text)	No (it's pixels)

Asciinema answers: "What text does the CLI produce?"
VHS answers: "What does the CLI look like?"

Both are useful. They test different things.

Visual Regression Testing Pattern

Step 1: Create a `.tape` file per workflow

# tapes/apply-violation.tape
Output testdata/screenshots/apply-violation.gif
Set Width 120
Set Height 40
Set FontSize 14
Set Theme "Catppuccin Mocha"

Type "stave apply --controls controls/s3 --observations observations --now 2026-01-15T00:00:00Z --format text"
Enter
Sleep 3s

Step 2: Generate the baseline

vhs tapes/apply-violation.tape

Commit testdata/screenshots/apply-violation.gif as the golden file.

Step 3: Compare in CI

# .github/workflows/visual.yml
- name: Generate screenshots
  run: |
    for tape in tapes/*.tape; do
      vhs "$tape"
    done

- name: Check for visual changes
  run: |
    git diff --exit-code testdata/screenshots/

If any GIF changes, the diff catches it. The developer reviews the visual change and either updates the golden file or fixes the formatting bug.

Step 4: Review with PR comments

For GitHub PRs, you can post the before/after GIF directly in a comment:

- name: Post visual diff
  if: failure()
  run: |
    echo "Visual regression detected. See the updated screenshots below."
    # Upload artifacts or post to PR

What Visual Tests Catch That Unit Tests Miss

Table alignment

CONTROL_ID          ASSET_ID              STATUS
CTL.S3.PUBLIC.001   my-very-long-bucket   NON_COMPLIANT
                    -name-that-wraps

A unit test checks that the data is correct. A visual test catches that the column wraps and breaks the alignment.

Color and formatting

[PASS] CTL.S3.ENCRYPT.001 — Server-Side Encryption
[FAIL] CTL.S3.PUBLIC.001 — No Public Read Access

A unit test sees [PASS] and [FAIL]. A visual test sees whether the ANSI color codes render correctly — green for pass, red for fail — or whether they produce \033[32m[PASS]\033[0m garbage.

Progress indicators

Running: evaluating controls... ⠋

A spinner that works in a real terminal but bleeds into piped output. A visual test with a fixed terminal size catches this.

Help text layout

Usage:
  stave apply [flags]

Flags:
  -i, --controls string   Path to control definitions (default "controls/s3")
  -o, --observations string
                          Path to observation snapshots (default "observations")

Does the flag help wrap correctly? Are the defaults aligned? Is the long description properly indented? Unit tests don't check layout. VHS checks layout.

VHS `.tape` Cheat Sheet

Output file.gif              # Output file (gif, png, webm, mp4)
Set Width 120                # Terminal width
Set Height 40                # Terminal height
Set FontSize 14              # Font size in pixels
Set Theme "Dracula"          # Terminal theme
Set TypingSpeed 50ms         # Delay between keystrokes

Type "command"               # Type text (simulated keystrokes)
Enter                        # Press Enter
Sleep 2s                     # Wait for output
Ctrl+C                       # Send interrupt
Tab                          # Press Tab (for completion testing)
Backspace 5                  # Delete 5 characters

Hide                         # Stop recording (for setup commands)
Show                         # Resume recording

Combining Both Tools

For a complete CLI testing strategy:

Layer	Tool	Tests
Unit tests	`go test`	Data correctness, error handling, exit codes
E2E golden files	`go test` + JSON comparison	Full output correctness, determinism
Text recordings	Custom asciicast generator	Documentation accuracy, demo freshness
Visual regression	VHS	Formatting, alignment, colors, layout

Each layer catches different bugs. Unit tests catch logic errors. Golden files catch output regressions. Asciicast recordings catch documentation drift. VHS catches visual formatting bugs.

Getting Started

# Install VHS (macOS)
brew install charmbracelet/tap/vhs

# Install VHS (Linux)
go install github.com/charmbracelet/vhs@latest

# Create your first tape
cat > hello.tape << 'EOF'
Output hello.gif
Set Width 80
Set Height 24
Type "echo 'Hello from VHS'"
Enter
Sleep 1s
EOF

# Record
vhs hello.tape

The GIF is your visual test. Commit it, compare it in CI, review it in PRs.

Stave uses programmatic asciicast generation for documentation recordings and Go-based golden file testing for output correctness. VHS is the natural next step for visual regression testing of the text-formatted output.

Z3 Can Prove Your Cloud is Unsafe. It Can't Tell You Why.

Bala Paranj — Sun, 17 May 2026 11:35:08 +0000

Z3 is one of the most powerful reasoning engines ever built. Microsoft Research created it to verify chip designs and flight software. It can take your cloud configuration, model it as a set of logical assertions, and mathematically prove whether an attack path exists.

Z3 says when it finds one:

sat

Three letters. No context. No explanation. No link to the configuration property that caused it. No fix. Just "sat" — which means "satisfiable," which means "the unsafe state you asked about is reachable," which means your cloud is vulnerable. Probably. If you encoded the question correctly. Which you can't verify from the output.

This is the gap between a powerful engine and a useful tool. The engine answers the question. The tool explains the answer. This article explains why the explanation layer matters more than the engine, and what it looks like in practice.

What Z3 outputs

Let's say you want to check whether an anonymous internet user can read PHI data from an S3 bucket through a Cognito identity pool. You model the configuration as SMT-LIB assertions, write a query, and run it through Z3.

The input Z3 sees:

(set-logic ALL)
(declare-fun allows_unauthenticated (String String) Bool)
(declare-fun maps_unauth_to (String String) Bool)
(declare-fun has_action (String String) Bool)
(declare-fun has_tag (String String) Bool)

(assert (allows_unauthenticated "pool-abc" "true"))
(assert (maps_unauth_to "pool-abc" "role/AppUnauthRole"))
(assert (has_action "role/AppUnauthRole" "s3:GetObject"))
(assert (has_tag "bucket-prod-phi" "data_classification:phi"))

(declare-const principal String)
(declare-const action String)
(declare-const resource String)

(assert (allows_unauthenticated principal "true"))
(assert (has_action principal action))
(assert (has_tag resource "data_classification:phi"))

(check-sat)
(get-model)

The output Z3 produces:

sat
(
  (define-fun principal () String "pool-abc")
  (define-fun action () String "s3:GetObject")
  (define-fun resource () String "bucket-prod-phi")
)

In SMT-LIB, sat means the forbidden state is reachable. The model names the specific pool, action, and bucket. The proof is mathematically sound.

If you're a security engineer who just wants to know whether your Cognito configuration is safe, this output is useless. You have three questions:

Is this result correct? Did the input assertions match your configuration, or did the translation introduce a bug?
What does it mean? Which specific settings in which specific files create the vulnerability?
What do I do about it? What's the fix, what does it cost, and how do I verify it worked?

Z3 answers none of these. It answered the math question. The security question is still open.

The two translation boundaries

Between your cloud configuration and Z3's answer, there are two translation steps. Each can introduce bugs. Each is invisible if you only look at the solver's output.

YOUR CLOUD CONFIG          THE MATH              YOUR ANSWER

  S3 bucket policy    →    SMT-LIB assertions    →    "sat"
  IAM role policy          (was the translation        (was the translation
  Cognito settings          correct?)                   back to cloud
                                                        terms correct?)

  ENCODING BOUNDARY        Z3 SOLVER              DECODING BOUNDARY
  (can have bugs)          (trusted)              (can have bugs)

Encoding bugs: Your S3 bucket has PublicAccessBlock.BlockPublicPolicy = true, but the translation emits has_public_read "bucket" "true". The assertion is wrong — the bucket is private, but Z3 thinks it's public. Z3 faithfully returns sat based on the wrong input. The "vulnerability" doesn't exist. You can't tell from sat that the encoding was wrong.

Decoding bugs: Z3 returns sat with a model. You read the model and conclude "the bucket is directly accessible from the internet." But the actual path is through the Cognito identity pool, not direct access. The model told you which variables were assigned, but the interpretation of those variables — what they mean in cloud terms — is your responsibility. Misread the model, misunderstand the vulnerability.

The solver is the most reliable component in the pipeline. The translation layers are where the bugs hide. And they're the layers that get the least attention because everyone focuses on the solver.

What an orchestration layer provides

An orchestration layer wraps the solver with five capabilities that make the answer trustworthy, traceable, and actionable:

1. Encoding explanation — "Did the tool understand my configuration?"

Before the solver runs, you see what the tool extracted from your configuration, in your language:

Configuration Summary: 7 assets, 43 facts extracted

Asset: arn:aws:s3:::prod-phi (S3 Bucket)
  ├── Public read access: ENABLED
  │   Source: prod-phi-bucket.obs.json → access.public_read
  │   Fact: a3f8c2e91b04
  │
  ├── Encryption: AES256 (SSE-S3, not KMS)
  │   Source: prod-phi-bucket.obs.json → encryption.algorithm
  │   Fact: b7d1e4f03c89
  │
  └── Data classification: PHI
      Source: prod-phi-bucket.obs.json → tags.data_classification
      Fact: c9e2a1f04d77

Asset: arn:aws:cognito-identity:...:identitypool/abc (Identity Pool)
  ├── Unauthenticated access: ALLOWED
  │   Source: cognito-pool.obs.json → identity.access.allow_unauthenticated
  │   Fact: d4e5f6a7b8c9
  │
  └── Maps unauthenticated users to: arn:aws:iam::111122223333:role/AppUnauthRole
      Source: cognito-pool.obs.json → identity.cognito.unauth_role_arn
      Fact: e5f6a7b8c9d0

No SMT-LIB. No predicate names. "Public read access: ENABLED" — the security engineer compares this to their mental model of the bucket. If the bucket is private, the encoding is wrong and the engineer knows before the solver runs.

Every fact has a unique identifier and a traceable source showing which file and which property path produced it. This is the audit trail. When the solver's answer doesn't match expectations, the engineer traces the identifier back to the source and checks whether the encoding was correct.

2. Human verdict — "What does the result mean?"

After the solver runs, you see the answer in security language:

VERDICT: UNSAFE

An anonymous internet user can read PHI data from the prod-phi
bucket through the Cognito identity pool.

The forbidden state is reachable because:
  1. Identity pool allows unauthenticated access
     (cognito-pool.obs.json → identity.access.allow_unauthenticated = true)
  2. Unauthenticated users receive credentials for AppUnauthRole
     (cognito-pool.obs.json → identity.cognito.unauth_role_arn)
  3. AppUnauthRole has s3:GetObject permission
     (iam-role.obs.json → policies.attached_policies[0].Action)
  4. Target bucket contains PHI
     (prod-phi-bucket.obs.json → tags.data_classification = phi)

Not sat. Not a model with define-fun expressions. A four-step chain in plain English, each step linked to a specific file and property path. The security engineer reads it and knows exactly which settings create the vulnerability and where they live.

3. Fix guidance — "What do I do about it?"

FIX: Disable unauthenticated access on the identity pool.

  aws cognito-identity update-identity-pool \
    --identity-pool-id us-east-1:abc123 \
    --no-allow-unauthenticated-identities

  Cost: $0. Time: 30 seconds.
  Effect: Breaks the chain at step 1.

VERIFICATION: After applying the fix, re-run the analysis.
  Expected result: SAFE
  (Z3 returns UNSAT — no assignment of principals, actions,
  and resources can satisfy the attack path conditions.)

The fix is a shell command. The cost is quantified. The effect names the specific chain step that breaks. The verification tells the engineer what to expect and explains the solver's output in cloud terms.

4. Traceability — "Which property caused this?"

Every step in the verdict traces back to a specific property in a specific file through a unique identifier:

# The verdict says step 1 caused the chain.
# Trace identifier d4e5f6a7b8c9:

grep "d4e5f6a7b8c9" facts.jsonl

# Returns:
# fact_id: d4e5f6a7b8c9
# subject: pool-abc
# predicate: allows_unauthenticated = true
# source: cognito-pool.obs.json
# property: identity.access.allow_unauthenticated
# captured: 2026-05-01T00:00:00Z

One identifier. One grep. Full trace from the verdict to the configuration property, including when the snapshot was taken. No manual correlation across output files.

5. Encoding verification — "Can I trust the translation?"

The orchestration layer verifies its own encoding by comparing each extracted fact against the raw configuration:

Encoding verification: 43/43 facts verified ✓

Every extracted fact matches the corresponding property
in the observation file. The solver's input is consistent
with the configuration snapshot.

Or, when there's a bug:

Encoding verification: 41/43 facts verified

MISMATCH:
  Fact d4e5f6a7b8c9:
    Extracted: allows_unauthenticated = "true"
    Observation: identity.access.allow_unauthenticated = "false"
    File: cognito-pool.obs.json
    → ENCODING BUG: fact says unauthenticated is allowed,
      but the configuration says it's disabled.
      The UNSAFE verdict may be incorrect.

No other tool in the market verifies its own translation layer. The security engineer doesn't need to read SMT-LIB to trust the result — the tool proves its encoding is correct, or reports where it is wrong.

What you get without orchestration vs. with it

Capability	Z3 alone	With orchestration
Prove an attack path exists	`sat`	UNSAFE: anonymous user can read PHI data
Explain which settings cause it	Read the SMT-LIB model	Four-step chain with file names and property paths
Verify the encoding is correct	Manually review assertions	Automated: 43/43 facts match observations
Trace the finding to a file	Grep through comments	One identifier, one grep, full trace
Get the fix	Derive it from the model	Shell command, cost, time, expected result
Run multiple solvers	Reformat per solver	Same input, three solvers, consensus
Explain to an auditor	Show them SMT-LIB	Show them the chain in English with evidence

The right column is the product. The left column is a math library. Security engineers don't need a math library — they need trustworthy answers in their language.

Why this matters more for compound detection

The orchestration layer is most valuable when the analysis spans multiple services. A single-service check ("is this bucket public?") is simple enough to verify manually. A cross-service check ("can an anonymous user reach PHI data through a chain of Cognito → IAM → S3?") involves three services, three configuration files, and dozens of properties.

The encoding has more places to be wrong. The verdict has more steps to explain. The traceability has more links to follow.

This is where raw solver output becomes dangerous. If Z3 returns sat on a three-service chain and the encoding has a bug in the IAM layer, the finding is a false positive. The security team triages it as critical, burns two sprints investigating, and discovers it was caused by a property path error in the translation code. The encoding verification catches that error before the solver runs.

If Z3 returns unsat and the encoding has a bug — a property that should be true was encoded as false — the finding is a false negative. The team thinks they're safe. They're not. The encoding verification catches that too.

The more complex the analysis, the more valuable the translation layer. Single-service checks can tolerate raw solver output. Cross-service compound detection cannot.

The bottom line

Don't evaluate formal verification tools by which solver they use. Z3, cvc5, and Yices all produce correct answers to the questions they're asked. The question is whether the question was asked correctly and whether the answer is translated back to your language.

Don't accept sat as an answer. Accept "UNSAFE: an anonymous internet user can read PHI data from the prod-phi bucket through the Cognito identity pool, caused by these four settings in these three files, fixable with this one command for $0 in 30 seconds, verified by three independent solvers, encoding confirmed correct against 43 observation properties."

That's an answer. sat is a data point.

The orchestration layer described in this article is implemented in Stave, an open-source static analysis tool that evaluates cloud configurations via CEL predicates and exports standardized facts for consumption by nine independent reasoning engines. The encoding explanation, verdict translation, traceability, and encoding verification are built on Stave's fact_id provenance chain — every fact carries a deterministic identifier linking the solver's input to the specific observation file and property path that produced it. All analysis runs on air-gapped snapshots with no cloud credentials required.

Proof, not prediction: where formal verification beats AI in cloud security

Bala Paranj — Sat, 16 May 2026 11:33:09 +0000

An AI scanner says 'this configuration looks unsafe' with 87% confidence. A formal verifier says 'this configuration IS unsafe, here is the exact principal, action, and resource that proves it.' One is a prediction. The other is evidence. The difference matters for insurance, for audits, and for the 80% of cloud security questions that have exact answers.

A CISO walks into a renewal meeting with the cyber-insurance underwriter. The underwriter asks one question:

Can your most sensitive S3 bucket be accessed by an unauthorized principal?

There are two ways to answer. An AI-powered cloud security tool gives you a something like "this bucket appears to have appropriate controls based on similar configurations in our training data, confidence: 92%." A formal verifier gives you a yes/no with a witness: "no — UNSAT against the following 17 constraints over the bucket policy, identity federation, IAM, and account-level Public Access Block."

One is a prediction. The other is a proof. The underwriter knows which one survives a subrogation suit.

What is a proof

When a solver like Z3 says UNSAT, it has shown that no assignment of the free variables in the model satisfies the constraints. There is no principal, no action, no resource, no role assumption, no trust path, no policy condition — within the model — that violates the property. The answer is mathematically complete relative to the model.

When the same solver says SAT, it returns a witness: the concrete assignment that satisfies the constraints. The witness names the exact principal, action, and resource that constitute the violation. The output is constructive. You didn't just learn the property is false; you got the counterexample that proves it.

There is no confidence score. There is no probability. There is no temperature setting. There is no false-positive rate. There is no training data. There is no "this might be similar to a known bad pattern." There is a function from facts to verdicts, and the verdict is correct relative to the inputs it was given.

The qualification relative to the model is critical. If your model doesn't include SCP evaluation, the solver won't catch SCP issues. If your model doesn't include Cognito identity-pool trust, the solver won't catch identity-federation chains. But the model's limitations are enumerable. You can list them. Operators know exactly what the verifier covers and what it doesn't.

An AI tool's limitations are statistical and unknowable. You can't enumerate what the training data didn't cover. A configuration that doesn't match any training pattern gets missed silently. A configuration that superficially resembles a bad pattern gets flagged incorrectly. The miss is invisible until the breach.

Proof vs prediction

Dimension	Formal verification (Z3 / cvc5 / Yices)	AI-based cloud-security tools
Output shape	Proof or counterexample	Prediction with confidence score
Correctness guarantee	Mathematically complete relative to the model	Statistically approximate relative to the training data
False positives	Zero relative to the model	Non-zero, tunable via threshold
False negatives	Zero relative to the model	Non-zero, depends on training coverage
Explainability	Exact witness — "principal P, action A, resource R"	This configuration resembles known-bad patterns
Novel attack paths	Discovers paths nobody has seen before, if the model captures them	Recognises only patterns similar to training data
Reproducibility	Deterministic — same input always produces the same answer	Varies across model versions, temperatures, prompts

The deterministic property makes the verifier auditable. Run it today, get UNSAT. Run it tomorrow against the same fact base, get UNSAT. Run it in three years when the auditor asks for evidence, get UNSAT with the same fact base. The proof is the artifact. It does not decay.

An AI prediction at 92% confidence today is a 87% confidence prediction tomorrow because the model was updated, or a 79% confidence prediction next week because the prompt template changed. The prediction is not an artifact. It is an output of a service. The service can be re-priced, re-trained, or shut down. Your audit evidence cannot.

The cost structure that nobody mentions

The accuracy story is the visible one. The cost story is the one that bends adoption.

Z3 runs on a single CPU core. The binary is ~10 MB. Running it on Stave's full SMT-LIB export — 5,000 facts plus 90 closed-world axioms — completes in milliseconds:

$ time z3 facts.smt2
sat

real    0m0.131s
user    0m0.123s
sys     0m0.009s

130 milliseconds. No GPU. No API call. No usage tier.

An AI-based tool pays for every query. Inference cost, GPU hours, API fees, token pricing. The cost scales linearly with usage: more assets, more policies, more frequent runs, higher bill. Enterprise customers with thousands of resources across multiple AWS accounts pay proportionally.

The cost ratio shows up most starkly in continuous-assessment scenarios. A cyber-insurance underwriter might require posture verification on every configuration change. For a company making hundreds of changes daily across multiple accounts, the AI-based tool runs hundreds of times per day per account. The formal verifier runs the same number of times — at a marginal cost of zero. The CPU was already paid for.

	AI-based tools	Stave + Z3/cvc5
Per-query cost	API inference fee	Zero
Infrastructure	GPU clusters	Single CPU core
Scaling cost	Linear with usage	Flat
Offline capability	Requires API connectivity	Runs fully offline (`STAVE_NO_NETWORK=1`)
Predictability	Variable pricing, usage-based	Fixed — it's a binary

The offline guarantee compounds with the cost guarantee. Air-gapped environments — defence, classified workloads, certain financial verticals — cannot ship configuration data to a third-party AI API. They must analyse locally. A formal verifier was designed for this constraint. AI-powered SaaS tools were designed for the opposite constraint. The trade-off is structural, not a UX choice.

Why this matters for insurance and evidence

Cyber-insurance underwriting is the canary for this entire shift. Underwriters today read CSPM-tool screenshots and trust the vendor's narrative. The narrative is statistical: "our customers have 92% lower breach rates." The screenshot is an opinion: "this bucket appears compliant."

Underwriters are moving toward evidence. They want artifacts they can hand to legal, archive in their underwriting file, and produce in a subrogation suit if the breach happens anyway. A formal proof — (check-sat) returning unsat against a specific fact base on a specific date — is an artifact. It can be archived. It can be re-run. It can be independently verified by Z3, cvc5, or Yices to confirm the answer.

The proof and the fact base are the audit evidence. The fact base is obs.v0.1 JSON, schema-validated, with provenance for every property. The proof is whatever the solver returns. Together they reconstruct the verdict exactly. The auditor does not need to trust the security vendor's model — they can run the solver themselves against the committed fact base and verify the verdict independently.

A Z3 proof is evidence. An AI prediction is an opinion.

This is also Stave's strongest positioning. When an insurer asks "prove your S3 bucket can't be accessed by unauthenticated principals," the formal answer is the artifact the underwriter is starting to demand.

Where AI genuinely belongs

Roughly 80–90% of cloud-security questions have exact answers:

Is MFA enabled on the root account?
Does this bucket policy allow Principal: *?
Can an unauthenticated Cognito identity assume this role?
Is CloudTrail logging multi-region?
Are these three controls all violated on the same asset?

None of these requires a language model. None of them benefits from a confidence score. They are predicates over structured facts. The deterministic verifier answers them in milliseconds with mathematical completeness relative to the model. Paying AI pricing for "is MFA enabled?" is a category error.

The remaining 10–20% genuinely needs AI:

Natural-language policy interpretation: parsing a vendor's English SOC 2 attestation and asking "does this commit them to encrypting backups?" The text is ambiguous; the intent must be inferred.
Anomaly detection in behavioural data: "is this CloudTrail access pattern unusual for this principal?" The baseline is statistical, the answer is probabilistic.
Intent inference from incomplete documentation: "does the team that owns this bucket consider its contents public-by-design, or did the public ACL get added by mistake?" The signal is in commit messages, ticket history, and Slack threads; the answer is judgment.

AI tools are valuable on those. They are also expensive on those. The cost is justified because the alternative is human review at twice the price.

The foundation-layer architecture

The right shape is composition. Deterministic verification at the bottom; AI judgement at the top:

+-------------------------------------------------------+
|  AI tools (10-20% of work)                            |
|    Policy interpretation, anomaly detection,          |
|    intent inference from English / behavioural data   |
+-------------------------------------------------------+
|  Stave + Z3/cvc5 (80-90% of work)                     |
|    Compound chain detection, formal proofs,           |
|    deterministic verdicts on structured facts         |
+-------------------------------------------------------+
|  Snapshot facts (obs.v0.1)                            |
|    Schema-validated, provenance-tracked, offline      |
+-------------------------------------------------------+

The AI bill drops 80–90% because trivial deterministic checks no longer route through an inference endpoint. The remaining AI workload has a much better signal-to-noise ratio because it sees only the hard cases — the ones where human judgement is the alternative. The AI tool gets better, not worse, when the deterministic layer is in place underneath it.

This is also the partnership angle. An AI-powered cloud-security vendor benefits from Stave handling the deterministic layer: their costs drop because the volume drops, their accuracy improves because the inputs are cleaner, and their pricing model survives the next round of GPU price increases because they're no longer paying inference cost for questions like "is encryption enabled?"

Stave does not replace AI tools. It makes them economically viable by removing the work they shouldn't be doing.

A 130-millisecond demo

The repository ships a working pipeline. Clone, build, and run:

git clone https://github.com/sufield/stave
cd stave && make build

# Pick a real fixture — HackerOne #1021906, the Shopify "tag says internal,
# policy says everyone" case. The fixture is a reconstructed snapshot from
# the public disclosure.
FIXTURE=testdata/e2e/e2e-h1-shopify-1021906

# Export the snapshot as SMT-LIB v2 — facts only, no query.
./stave export-sir --format smt2 \
  --controls $FIXTURE/controls \
  --observations $FIXTURE/observations \
  --now 2026-01-15T00:00:00Z > /tmp/facts.smt2

# Append the satisfiability query.
echo "(check-sat)" >> /tmp/facts.smt2

# Two independent solvers.
z3 /tmp/facts.smt2
cvc5 --lang smt2 /tmp/facts.smt2

z3 returns sat on 302 lines of SMT-LIB in 132 milliseconds. cvc5 runs over the same input as an independent cross-check; on this particular fact base it returns unknown, which is itself an honest verdict — the second solver could not establish the answer with its default tactic. Two engines returning the same sat/unsat is the strongest possible cross-validation; one returning unknown is the signal to either widen the timeout, switch tactics, or refine the model. The point is that the protocol — facts plus query plus solver — is reproducible. The verdict is auditable regardless of which solver produced it.

No GPU, no API key, no per-query cost. The binary that produced the export does not call any cloud API. The solver runs locally. The audit evidence is the file at /tmp/facts.smt2 plus the verdict — both reproducible byte-for-byte at any point in the future against the same obs.v0.1 snapshot.

What this is not

It is not "AI is bad for security." AI is excellent for the 10–20% of problems that genuinely require judgement, anomaly detection, or natural-language interpretation. The framing is use the right tool for each class of problem.

It is not "formal verification solves everything." The verifier is correct relative to the model. If your model doesn't include the Cognito identity-pool trust pattern, the solver will not flag a Cognito identity-pool attack. But model coverage is enumerable; you can list what is and isn't covered. AI coverage is statistical; you cannot.

It is not "Z3 replaces your CSPM." CSPM and formal verification are complementary. CSPM tells you what's in the cloud right now. Formal verification tells you whether what's there satisfies your stated invariants. The CSPM dashboard is the inventory; the formal verifier is the auditor with the proof.

The structural shift

Cloud security has spent a decade paying language-model prices for boolean questions. The market matured around AI because no deterministic alternative existed that handled compound risk across services. That gap is closed. Stave's open-source policy library plus the SMT-LIB export plus a $0 solver replaces the deterministic-check layer at zero marginal cost.

The AI vendors who survive will be the ones who specialise in genuinely judgemental questions and welcome a free, deterministic foundation beneath them. The CSPM vendors who survive will be the ones who emit obs.v0.1-compatible inventories and let any open-source verifier consume them. The customers who survive are the ones who stop paying API fees for Principal: * checks.

When the insurance underwriter asks for proof, the customer hands them the SMT-LIB file and the solver verdict. The verifier ran on a laptop. The cost was zero. The evidence is independently reproducible.

That is what formal verification looks like in cloud security in 2026. The technique has been validated at scale by Microsoft Research (SecGuru, 2015) on Azure's datacentre network. Applying it to cloud service configurations is the only step that was missing. It is no longer missing.

Stave is an open-source intent verification engine for cloud infrastructure with 2,650+ controls, compound risk detection, and nine independent reasoning engines.

Zero-cost abstractions in Go: deleting your way to better code

Bala Paranj — Fri, 15 May 2026 12:09:37 +0000

The most impactful refactoring in a Go CLI wasn't adding code — it was deleting pass-through layers, thin wrappers, and premature frameworks. Here's how to recognize abstractions that cost more than they save.

Over 60 refactorings on a security CLI, the highest-ROI changes were deletions. Deletions of abstractions that existed "just in case" and cost every reader cognitive overhead with zero runtime benefit.

Here are the abstractions we removed and why.

1. Pass-through packages

A package that exists only to forward calls to another package:

// internal/app/workflow/evaluate.go
package workflow

func Evaluate(input EvalInput) (Result, error) {
    return eval.Evaluate(input) // just forwards
}

Every command imported workflow instead of eval directly. The package had no logic, no transformation, no error handling. It was a phantom layer — it appeared in import paths, confused grep results, and added one more package to understand.

The fix: Delete the package. Rewire all callers to import eval directly. One commit, zero behavior change.

The rule: If a package only forwards calls, it shouldn't exist.

2. Thin wrapper functions

func RenderJSON(w io.Writer, v any) error {
    return jsonutil.WriteIndented(w, v)
}

func RenderText(w io.Writer, report Report) error {
    return textReporter.Render(w, report)
}

These wrappers added names but no behavior. Every caller could call the underlying function directly. The wrappers existed because "we might add logging later" — but we never did.

The fix: Inline the call at every call site. Delete the wrapper.

The principle: Don't create a function to wrap a single function call. The call itself is already readable.

3. Anemic files

25 Go files with fewer than 20 lines of logic. Each contained a single type or a single function that belonged in its neighboring file.

types.go          → 1 type, 0 methods
constants.go      → 3 constants
helpers.go        → 1 helper function

Every file is a navigation decision. 25 anemic files means 25 wrong guesses when searching for code. Merging types.go into policy.go means the type lives next to the logic that uses it.

The fix: Merge into the logical neighbor. 25 files became 0 additional files — the types moved into the files that used them.

The rule: Name files after the primary type they contain. Don't create types.go, utils.go, or helpers.go.

4. Premature generic frameworks

The most expensive deletion: a 500-line Pipeline[T] generic framework.

type Pipeline[T any] struct {
    stages []Stage[T]
}

func (p *Pipeline[T]) Run(ctx context.Context, input T) (T, error) {
    for _, stage := range p.stages {
        var err error
        input, err = stage.Execute(ctx, input)
        if err != nil {
            return input, err
        }
    }
    return input, nil
}

This was used in only one place — the evaluation pipeline. The stages were three sequential function calls. The framework added generics, interfaces, registration, and error handling for a problem that looked like this:

controls, err := loadControls(ctx, dir)
if err != nil { return err }

result, err := evaluate(controls, snapshots)
if err != nil { return err }

return writeOutput(result)

Three lines of sequential Go. No generics. No interfaces. No framework.

The fix: Delete the pipeline package. Replace with three sequential calls.

The principle: Three lines of sequential Go beats a 500-line generic fluent API. Every time.

5. Backward-compatibility aliases

After renaming invariant to control across 60 files, we kept type aliases for safety:

// Deprecated: use ControlID.
type InvariantID = ControlID

The aliases created confusion about which name was canonical. Grep returned both. Autocompletion showed both. New code used both names randomly.

The fix: Delete all aliases in the same commit as the rename. No transition period. The codebase has no external consumers — there is nobody to break.

The rule: If you have no external consumers, backward compatibility is debt.

6. Dead methods

After the hexagonal migration, deadcode analysis found 207 unreachable functions:

$ deadcode -test ./...
internal/core/controldef.(*Operand).AsBool
internal/core/controldef.(*Operand).AsString
internal/core/controldef.(*Operand).AsNumber
internal/core/controldef.(*Operand).IsZero
internal/core/evaluation.(*EvalContext).GetLogger
...

Methods that were written speculatively, methods left behind after a refactoring, methods duplicated across packages during a migration. All dead. All deleted.

The fix: Run deadcode -test ./... after every structural change. Delete what it finds. No exceptions.

The cost model

Every abstraction has a cost:

Abstraction	Cost per reader	Runtime benefit
Pass-through package	Import confusion, grep noise	Zero
Thin wrapper	Extra indirection to read	Zero
Anemic file	Navigation overhead	Zero
Unused generic framework	500 lines to understand	Zero
Type alias	Namespace pollution	Zero
Dead method	"Is this used?" investigation	Zero

If the runtime benefit column is zero, the abstraction is not zero-cost. It's negative-cost.

When to delete

After every structural refactoring, ask:

Does this package forward calls without adding logic? Delete it.
Does this function wrap a single function call? Inline it.
Does this file contain fewer than 20 lines? Merge it.
Does this framework serve one use case? Replace with sequential code.
Does this type alias exist for transition safety? Delete it now.
Does deadcode find anything? Delete it all.

The Real Zero Cost Abstraction

Go doesn't have zero-cost abstractions in the Rust sense. Every interface adds a vtable lookup. Every package adds compile time. Every file adds navigation cost. Every line adds reading time.

The only truly zero-cost abstraction in Go is the one you deleted.

Stave is an open-source intent verification engine for cloud infrastructure with 2,650+ controls, compound risk detection, and nine independent reasoning engines.

The $0 cloud infrastructure security stack

Bala Paranj — Thu, 14 May 2026 11:02:07 +0000

Maya Kaczorowski documented Oblique's $0 security stack for code, email, logs, and devices. This is the companion piece: the $0 stack for cloud infrastructure — intent verification, compound risk detection, and formal safety proofs for AWS configurations, with nine independent reasoning engines.

Inspired by a $0 stack

Maya Kaczorowski recently wrote about Oblique's $0 security stack — world-class security tooling at zero cost. Semgrep for code analysis, TruffleHog for secret scanning, RunReveal for SIEM, Sublime for email, Apple Business for device management. All free or free-tier. All solving real problems. Her point is important: the excuse that security costs too much no longer holds.

Her article covers application security, email security, log aggregation, and device management. This article covers a different domain: cloud infrastructure security — verifying whether your AWS resources are configured safely, not just correctly.

The distinction matters. A configuration can be correct by every checklist and still be unsafe. Three individually-correct settings — an unauthenticated identity pool, a scoped IAM role, and a private PHI-tagged bucket — can compose into a path that lets anonymous users reach patient data. No individual check catches it because the vulnerability exists in the composition, not in any single setting. This stack solves that problem.

The infrastructure security pipeline

Commercial cloud security posture management — Wiz, Orca, Prisma Cloud — starts at five figures annually. The open-source alternative costs nothing, and it does something commercial tools structurally cannot: verify that your configurations don't contradict your own declared intent, with mathematical proofs from engines built to verify flight software.

Input              Evaluation           Reasoning              Downstream
─────              ──────────           ─────────              ──────────
Steampipe    →     Stave          →     9 External Engines →   Neo4j GDS
(cloud SQL)        (CEL predicates      Z3 / cvc5 / Yices      SIEM
                    + compound chains)  Soufflé / Clingo       SARIF
                                        Prolog / PySAT         Evidence bundles
                                        Risk / Game Theory

Each layer is independent. Replace any piece without touching the others.

Steampipe is the input layer. It queries your cloud APIs like a database — AWS, Azure, and GCP resources become SQL tables. Steampipe produces the inventory. It doesn't evaluate it.

Stave is the evaluation layer. It reads observation snapshots and evaluates them against 2,650+ controls across 74 AWS service domains. CEL predicates detect individual misconfigurations. Compound chains compose multiple findings into named attack paths. The evaluation is deterministic — same snapshot, same findings, every time.

Nine reasoning engines consume Stave's fact export independently. Z3 proves whether forbidden states are mathematically reachable. Soufflé enumerates blast radius and reachability paths. Clingo fires declarative violation rules. Each engine adds a reasoning dimension that CEL predicates structurally cannot express — quantification, graph traversal, satisfiability. The engines are external consumers, not internal components. Stave exports facts as JSONL triples or SMT-LIB assertions. The engines read them.

Downstream systems consume what Stave and the engines produce. Neo4j Community Edition provides graph analysis — centrality, shortest paths, choke points. SARIF output feeds IDEs. JSONL output feeds SIEMs. Signed evidence bundles feed compliance audits.

What scanners check vs. what Stave verifies

A scanner asks: "Is this setting correct?" It checks attributes on individual resources — encryption enabled, public access blocked, MFA enforced. These are necessary checks. They verify that individual nodes meet a baseline.

Stave asks a different question: "Do your configurations contradict what you declared?"

When you tag a bucket data_classification: phi, you're declaring intent: this contains patient records. When a Bedrock knowledge base indexes that bucket and a customer-facing agent serves the results without a guardrail, your infrastructure contradicts your declaration. Three individually-correct configurations compose into a violation of your own stated intent.

Scanners check 10 attributes per resource. With five layers of AWS security — IAM, SCPs, resource policies, VPC endpoints, trust relationships — a single bucket can exist in over 200 possible effective-access states. The other 190 stay unexamined. Stave collapses that state space through invariants: define which states are forbidden, prove they're unreachable.

The findings reflect this difference:

A scanner says: "S3 bucket is publicly accessible. Severity: High."

Stave says:

CHAIN: bedrock_rag_phi_exposure (CRITICAL)

  CTL.COGNITO.UNAUTH.ACCESS.001
    Identity pool allows unauthenticated access

  CTL.IAM.ROLE.MAPPED.BROAD.001
    Mapped role has s3:GetObject on PHI bucket

  CTL.BEDROCK.AGENT.GUARDRAIL.001
    Agent has no content-filtering guardrail

  Compound: anonymous internet user can reach
  patient health records through the RAG pipeline.
  Three settings, three clean individual checks,
  one CRITICAL attack path.

The scanner found zero issues. Stave found the composition that makes the system unsafe.

What 2,650 controls cover

The catalog spans 74 AWS service domains. The controls that matter most are the families that detect structural patterns no individual check can see.

32 AI agent identity controls cover Bedrock agents, SageMaker pipelines, and Lambda tool chains. Agent execution role overprivilege, missing guardrails, ghost action groups referencing deleted Lambda functions, shadow agents created outside IaC, knowledge base data boundary violations. Five compound chains compose these into attack paths: agent-to-PHI exposure through RAG pipelines, cross-account training data access, shadow agent credential theft.

Shadow admin detection catches IAM roles that accumulated permissions beyond their declared scope. A role named S3-ReadOnly that can retrieve secrets, invoke Lambda functions, and enumerate the full IAM inventory. Five controls check permission drift (unused service ratio via Access Advisor), category mixing (data access combined with IAM write), and intent mismatch (permissions contradict the declared role-type tag). Two compound chains fire when the pattern is systemic.

Vendor delegation governance checks whether vendors with access to your S3 buckets have exceeded their declared scope, whether their access review is overdue, whether they can make your bucket public, and whether you can revoke their access. Five controls, one compound chain at threshold 3-of-5 — a single overdue review is a reminder, three concurrent failures is a systemic governance breakdown.

23 ghost reference controls detect policies that reference resources absent from the snapshot — dangling IAM trust policies pointing at deleted accounts, Cognito triggers referencing deleted Lambda functions, S3 policies granting access to buckets that no longer exist. An attacker who recreates the deleted resource under the same name inherits every permission the dangling policy still grants.

47 credential TTL controls across IAM rotation, token expiry, certificate lifecycle, Secrets Manager rotation, and KMS key management. The Time-Bound Credential Invariant checks not just that a TTL is declared, but that the TTL hasn't elapsed — the difference between "rotation is configured" and "rotation actually happened."

Temporal analysis treats time as a built-in dimension. Drift detection compares snapshots and flags configuration changes. Duration tracking measures how long a misconfiguration has persisted — the same public bucket at 6 hours and 6 months tells different stories. Observation freshness detects stale snapshots — findings based on data that's 90 days old need different urgency than findings based on data from today.

Nine engines, one fact export

Stave evaluates controls with CEL predicates — the primary detection mechanism. But CEL has expressivity limits: it can't quantify over lists, traverse reachability graphs, or prove satisfiability of combined assertions. The nine external engines fill those gaps.

The fact export is the interface. Stave projects observation properties into JSONL triples (subject-predicate-object) and SMT-LIB assertions. 44 scalar predicates and 6 per-element array projectors cover AI agents, VPC peering, EC2 instance profiles, IAM role drift, and S3 delegation. Every engine reads the same facts and produces independent analysis.

Z3 / cvc5 / Yices (SMT solvers) prove whether forbidden states are reachable. "Can an anonymous user reach PHI data through any combination of identity pool, role mapping, and bucket policy?" The answer is sat (reachable — unsafe) or unsat (mathematically impossible — proven safe). These are the solvers Microsoft Research built for verifying flight control software and CPU designs. The proof is deterministic and independently reproducible. Microsoft has used the same approach to solve firewall rules verification for Azure.

Soufflé (Datalog) enumerates reachability paths and counts blast radius. "How many resources can this compromised role reach?" "Which vendor principals have excessive delegation reach on this bucket?" Per-element facts — has_unused_service(role, "lambda"), has_delegated_principal(bucket, principal_arn) — enable queries that name specific services and specific principals, not just booleans.

Clingo (Answer Set Programming) fires declarative violation rules. Shipped rules cover AI agent patterns (broad Lambda + no guardrail), delegation violations (unknown principal, scope exceeded, irrevocable access), shadow admin signals (incompatible categories + unused services), VPC peering exposure, and shadow EC2 lateral movement. Every remediated fixture produces zero violations — verified end-to-end.

Prolog derives proof trees showing step-by-step reasoning: attacker → shadow account → trusted role → production data. PySAT checks boolean satisfiability on multi-control compounds. Risk model computes exploitation probability. Game theory quantifies attacker cost vs. defender remediation ROI. TLA+ checks temporal safety — how many configuration changes separate the current state from an unsafe state.

Each engine finds a different class of issue on the same fact set. That's breadth without tool sprawl — nine reasoning dimensions from one data export.

Where this fits in a security program

A security program has multiple layers. Each addresses a different domain. Each can be $0 independently:

Layer                    Domain                  $0 tools
─────                    ──────                  ────────
Application security     Code + dependencies     Semgrep, TruffleHog
Infrastructure security  Cloud configuration     Steampipe, Stave, Neo4j CE
Detection & response     Logs + runtime events   RunReveal
Email security           Phishing + BEC          Sublime Security
Device management        Endpoints               Apple Business

The infrastructure layer is the one most startups skip because commercial CSPM starts at five figures. The pipeline above is $0 and covers 2,650+ controls with formal verification from engines designed for safety-critical systems.

Setting it up

Step 1: Install Steampipe and the AWS plugin.

brew install turbot/tap/steampipe
steampipe plugin install aws

Steampipe reads your AWS credentials from the standard locations. No additional configuration needed.

Step 2: Verify your inventory.

select name, region, bucket_policy_is_public
from aws_s3_bucket
where bucket_policy_is_public = true;

If this returns results, you have public S3 buckets. Steampipe makes cloud inventory queryable in seconds.

Step 3: Try the demo (30 seconds, no AWS account needed).

git clone https://github.com/sufield/stave.git
cd stave
bash examples/demo-ai-security/run.sh

The demo shows the full pipeline on built-in fixtures: 5 AI agent findings → 3 CRITICAL compound chains → remediation → clean. No cloud credentials required.

Step 4: Run against your own snapshots.

stave apply --observations ./my-snapshots

Stave evaluates every observation against 2,650+ controls. Compound chains fire when multiple findings compose into attack paths on the same resource.

Step 5: Export to reasoning engines.

# JSONL triples for Soufflé / Clingo
stave export-sir --format jsonl --observations ./my-snapshots > facts.jsonl

# SMT-LIB assertions for Z3 / cvc5
stave export-sir --format smt2 --observations ./my-snapshots > facts.smt2

Step 6: Track drift over time.

stave diff --before ./snapshot-march --after ./snapshot-april

Compares snapshots and flags configuration changes with before-and-after state.

Step 7: Export graph for Neo4j.

stave graph export --format graphml --observations ./my-snapshots > graph.graphml

Load into Neo4j Community Edition for centrality analysis, shortest-path computation, and effective permission reasoning.

What you get for $0

The input layer (Steampipe)

SQL queries over AWS, Azure, and GCP resources
150+ plugins covering every major cloud provider and SaaS service

The evaluation layer (Stave)

2,650+ controls across 74 AWS service domains
30+ compound chains composing individual findings into named attack paths
32 AI agent identity controls (Bedrock, SageMaker, Lambda tool chains)
Shadow admin detection (permission drift + category mixing + intent mismatch)
Vendor delegation governance (scope, lifecycle, revocability, escalation)
23 ghost reference controls detecting dangling policies after resource deletion
47 credential TTL controls with elapsed-TTL verification
Temporal analysis: drift detection, duration tracking, observation freshness
Intent verification: findings fire when configurations contradict declared tags, role-type taxonomies, and vendor registries

The reasoning layer (9 engines)

Z3 / cvc5 / Yices: mathematical proofs of safety or reachability
Soufflé: blast radius enumeration and reachability path counting
Clingo: declarative violation rules across 5 attack pattern families
Prolog: step-by-step proof trees for attack path derivation
PySAT / Risk / Game Theory / TLA+: satisfiability, probability, cost, temporal safety

The insights layer (downstream)

Neo4j GDS: graph centrality, shortest paths, choke point identification
SARIF: IDE integration for developer-visible findings in pull requests
JSONL: SIEM ingestion for correlation with runtime events
Evidence bundles: signed compliance archives

The commercial equivalent of this pipeline costs $25,000–$100,000+ annually. The open-source version costs nothing, includes formal verification from SMT solvers designed for flight software, and verifies intent — not just configuration — across 74 service domains.

Infrastructure security doesn't have to cost anything

The reason most startups skip cloud security posture management is that the tools cost more than their entire infrastructure spend. A startup paying $500/month for AWS can't justify $50,000/year for a CSPM tool. So they don't. Their S3 buckets stay public, their IAM roles accumulate permissions nobody reviews, their deleted resources leave ghost references nobody detects, and their AI agents serve PHI through RAG pipelines nobody verified.

The open-source pipeline removes this barrier. Steampipe + Stave + nine reasoning engines + Neo4j costs nothing and provides capabilities commercial CSPM tools structurally cannot: intent verification against operator declarations, compound risk detection across service boundaries, mathematical safety proofs from SMT solvers, and temporal analysis that tracks how configurations evolve over time.

Maya Kaczorowski showed that application security, email security, log aggregation, and device management can all be $0. This article shows the same is true for cloud infrastructure security — and that the $0 version doesn't just match the commercial tools. On compound risk detection, intent verification, and formal safety proofs, it goes beyond them.

Three tools. Nine engines. Zero dollars. A pipeline, not a product.

Stave is an open-source intent verification engine for cloud infrastructure with 2,650+ controls, compound risk detection, and nine independent reasoning engines. Steampipe is an open-source tool for querying cloud APIs via SQL. Together with Neo4j for graph insights, they form the $0 infrastructure security pipeline.

Your Go Golden Tests Don't Need to Regenerate Everything

Bala Paranj — Wed, 13 May 2026 10:55:51 +0000

A practical pattern for targeted golden file regeneration in Go projects — from minutes to 0.27 seconds.

I have 5,810 golden files in my project. Every time I changed one test, I was regenerating all of them. It took minutes. Now it takes 0.27 seconds.

The fix was just organizing the regeneration path so you could aim it at one file instead of firing at everything.

The problem with regenerate everything

Golden tests are great. You capture known-good output, save it to a file, and compare against it on every run. When the output changes intentionally, you regenerate the golden file.

Most Go projects start with a simple approach: a Makefile target that regenerates all golden files at once.

make regenerate-goldens

This works when you have 20 golden files. When you have 5,810, it doesn't. You change one test, you wait for the tool to process every fixture directory, and most of the time nothing else changed. You're wasting time to update one file.

Two kinds of golden tests

Before fixing anything, I audited how golden files worked in the codebase. I found two completely different mechanisms hiding behind the same word.

In-process goldens — a test function renders output, compares it against a .golden or golden.json file in testdata/. The test itself can write the file if you ask it to. I had 3 of these.

E2e fixture goldens — an external tool runs the compiled binary against fixture directories and captures stdout into expected.* files. The test reads those files and compares. I had 5,807 of these.

These need different regeneration strategies. Trying to unify them under one mechanism would either duplicate the external tool inside the test (pointless) or force the external tool to understand in-process test output (brittle).

The in-process pattern: UPDATE_GOLDEN env var

For the 3 in-process golden tests, I added a small helper to the existing test utilities package.

package testutil

import (
    "bytes"
    "os"
    "path/filepath"
    "testing"

    "github.com/google/go-cmp/cmp"
)

func UpdateGolden() bool {
    return os.Getenv("UPDATE_GOLDEN") != ""
}

func AssertGolden(t *testing.T, path string, got []byte) {
    t.Helper()

    if UpdateGolden() {
        writeIfChanged(t, path, got)
    }

    want, err := os.ReadFile(path)
    if err != nil {
        t.Fatalf("read golden file %s: %v\nRun with UPDATE_GOLDEN=1 to create it", path, err)
    }

    if diff := cmp.Diff(string(want), string(got)); diff != "" {
        t.Fatalf("golden mismatch %s (-want +got):\n%s\nRun with UPDATE_GOLDEN=1 to update", path, diff)
    }
}

func writeIfChanged(t *testing.T, path string, data []byte) {
    t.Helper()

    old, err := os.ReadFile(path)
    if err == nil && bytes.Equal(old, data) {
        return
    }

    if err := os.MkdirAll(filepath.Dir(path), 0755); err != nil {
        t.Fatalf("create golden dir: %v", err)
    }
    if err := os.WriteFile(path, data, 0644); err != nil {
        t.Fatalf("write golden file %s: %v", path, err)
    }
    t.Logf("updated golden file: %s", path)
}

Usage in a test:

func TestTextReporter_Golden(t *testing.T) {
    got := renderReport(buildFixture())
    testutil.AssertGolden(t, "testdata/reports/hipaa_golden.txt", []byte(got))
}

Regenerate just that one test:

UPDATE_GOLDEN=1 go test ./internal/profile/reporter -run TestTextReporter_Golden

0.27 seconds.

Why an env var instead of a flag

My first version used flag.Bool("update", ...). The problem: Go test flags are per-package. If you define -update in one package and run go test ./... -update, every other package fails because it doesn't recognize the flag.

An environment variable works across all packages without any registration.

# This works for any package, any test
UPDATE_GOLDEN=1 go test ./path/to/package -run TestWhatever

Why writeIfChanged matters

Without it, every UPDATE_GOLDEN=1 go test ./... run touches every golden file's timestamp, even if the content didn't change. Your git status fills up with phantom changes. writeIfChanged reads the file first, compares bytes, and skips the write if nothing changed. Five lines that keep your diffs clean.

The e2e pattern: wrap what already exists

For the 5,807 fixture goldens, I already had a regeneration tool (regengoldens) that accepted a -filter regex. The problem was discoverability. Nobody remembered the flag syntax.

I added a Makefile target:

.PHONY: golden-fixture
golden-fixture:
    @test -n "$(FILTER)" || (echo "Usage: make golden-fixture FILTER=<regex>" && exit 1)
    $(MAKE) regenerate-goldens ARGS='-filter $(FILTER)'

Now regenerating one fixture set:

make golden-fixture FILTER=hipaa

No syntax to remember. Tab-completable.

The full Makefile surface

# In-process goldens
.PHONY: golden-update-all
golden-update-all:
    UPDATE_GOLDEN=1 go test ./...

.PHONY: golden-update
golden-update:
    @test -n "$(PKG)" || (echo "Usage: make golden-update PKG=./path/to/pkg/..." && exit 1)
    UPDATE_GOLDEN=1 go test $(PKG)

.PHONY: golden-one
golden-one:
    @test -n "$(PKG)" || (echo "Usage: make golden-one PKG=./path/to/pkg/... RUN=TestName" && exit 1)
    @test -n "$(RUN)" || (echo "Usage: make golden-one PKG=./path/to/pkg/... RUN=TestName" && exit 1)
    UPDATE_GOLDEN=1 go test $(PKG) -run '$(RUN)'

# E2e fixture goldens
.PHONY: golden-fixture
golden-fixture:
    @test -n "$(FILTER)" || (echo "Usage: make golden-fixture FILTER=<regex>" && exit 1)
    $(MAKE) regenerate-goldens ARGS='-filter $(FILTER)'

Two mechanisms, one discoverable surface. grep golden Makefile tells you everything.

What I didn't do

I didn't unify the two mechanisms. The in-process tests and e2e fixture tests have different architectures. Forcing them into one pattern would mean either duplicating the external regeneration tool inside Go tests or making the tool understand in-process rendering. Both are worse than having two clear paths.

I didn't add subtests where they weren't needed. The original plan called for converting flat tests to subtests for -run targeting. In practice, my 3 in-process golden tests were either single-case or already subtested. Converting for the sake of a pattern would have been churn.

I didn't migrate one test that would have changed golden content. One golden file was a hand-ordered JSON map. json.MarshalIndent sorts keys alphabetically, so running AssertGolden with UPDATE_GOLDEN=1 would have silently reordered the file. The rule I set was: the migration changes the mechanism, not the content. If any golden file changes, something is wrong. I left that test alone and documented why.

The verification that matters

After the migration, this is the check:

UPDATE_GOLDEN=1 go test ./...
git diff --name-only -- '*.golden' '*.golden.*'

The diff must be empty. If any golden file changed during migration, the helper introduced a difference — a trailing newline, an encoding change, a key reordering. That's a bug in the migration, not a legitimate update.

Results

Before: change one test, run make regenerate-goldens, wait minutes.

After: change one test, run UPDATE_GOLDEN=1 go test ./pkg/foo -run TestBar, wait 0.27 seconds.

The approach is boring. Env var, a 40-line helper, a few Makefile targets. Nothing novel. But the development loop went from avoid touching golden tests to golden tests are free to change.

This speed up was applied to Stave codebase, an offline configuration safety evaluator.

9 Go Performance Patterns That Don't Need a Profiler to Find

Bala Paranj — Tue, 12 May 2026 11:26:16 +0000

Pre-allocated slices, bitmask operations, index-based iteration, strings.Builder with Grow, switch-over-map hot paths, defensive cloning, sync. Once caching, WalkDir over Walk, and defined types avoiding string conversion — patterns visible in code review.

Most performance advice starts with run a profiler. That's correct for micro-optimization. But the patterns in this article are visible in code review. You don't need a flamegraph to know that copying a 408-byte struct in a loop 10,000 times is slower than taking a pointer to it.

These are the patterns we applied across a 50,000-line Go security CLI. Each one has a reason that doesn't require benchmarks to justify.

1. Pre-Allocate Slices and Maps

The Cost of Growth

// BAD: append grows the backing array 5+ times for 100 elements
var results []Finding
for _, asset := range assets {
    if isViolation(asset) {
        results = append(results, buildFinding(asset))
    }
}

Each time append exceeds the slice capacity, Go allocates a new backing array (typically 2x the current size), copies all existing elements, and lets the old array be garbage collected. For 100 elements starting from zero, that's approximately 7 allocations and 7 copies.

The Fix

// GOOD: one allocation, zero copies
results := make([]Finding, 0, len(assets))  // cap = upper bound
for _, asset := range assets {
    if isViolation(asset) {
        results = append(results, buildFinding(asset))
    }
}

Same pattern for maps:

// BAD: map grows through multiple rehashes
baseMap := make(map[string]Finding)

// GOOD: pre-sized to avoid rehashing
baseMap := make(map[string]Finding, len(baseline))

The capacity hint doesn't need to be exact. It's an upper bound. make([]T, 0, len(input)) is correct even if the filter removes 90% of elements. The wasted capacity (a few KB of pointers) is cheaper than the allocation churn.

Where to Apply

Pre-allocate when:

You know the upper bound (input length, map size)
The collection is built in a loop
The collection survives the function (returned, stored in a struct)

Skip when:

The collection is tiny (< 8 elements — Go's small-object optimization handles it)
The upper bound is unknown or enormous
You're building a result from streaming data

2. Index-Based Iteration for Large Structs

The Cost of Range-Value Copy

// BAD: copies 408 bytes per iteration
for _, f := range findings {
    process(f)
}

Go's for _, v := range copies the element into v on every iteration. For a Finding struct (408 bytes), iterating over 1,000 findings copies 408 KB of data — just to read each element.

The Fix

// GOOD: zero copy — pointer to element in existing slice memory
for i := range findings {
    f := &findings[i]
    process(f)
}

&findings[i] takes a pointer to the element in the slice's backing array. No copy. The pointer is 8 bytes regardless of struct size.

When It Matters

The Go compiler may optimize small structs (< 64 bytes) to registers. For structs above 128 bytes, the copy is measurable. We set the rangeValCopy gocritic threshold to 128 bytes and fixed 70 loops across the codebase.

Types we fixed:

Type	Size	Loop Count
`remediation.Finding`	408B	15 loops
`policy.ControlDefinition`	304B	12 loops
`remediation.RemediationFinding`	352B	8 loops
`securityaudit.Finding`	160B	5 loops
`risk.Item`	152B	4 loops
`s3/policy.Statement`	128B	3 loops

Do NOT change []T to []*T. Pointer slices destroy cache locality — each element is a separate heap allocation that the CPU prefetcher can't predict. Keep contiguous []T memory; access individual elements by index.

3. Switch Over Map for Hot-Path Dispatch

The Cost of Map + Closures

// BAD: map lookup + closure allocation on every call
var operators = map[Operator]operatorFunc{
    OpEq:  handled(func(exists bool, f, m any) bool { return exists && EqualValues(f, m) }),
    OpNe:  handled(func(exists bool, f, m any) bool { return !exists || !EqualValues(f, m) }),
    // ... 14 operators
}

func EvaluateOperator(op Operator, exists bool, val, compare any) (bool, bool) {
    fn, ok := operators[op]
    if !ok { return false, false }
    return fn(exists, val, compare)  // 2 levels of function indirection
}

Three costs: (1) hash the operator string and probe the map, (2) call through a handled() wrapper that allocates a closure, (3) call through the inner closure. On the hot path (43 controls × 50 assets × 10 snapshots), that's 21,500 map lookups with closure calls.

The Fix

// GOOD: compiler-generated jump table, zero allocation
func EvaluateOperator(op Operator, exists bool, val, compare any) (res bool, handled bool) {
    handled = true
    switch op {
    case OpEq:
        res = exists && EqualValues(val, compare)
    case OpNe:
        res = !exists || !EqualValues(val, compare)
    case OpGt:
        res = exists && GreaterThan(val, compare)
    // ... 14 cases
    default:
        return false, false
    }
    return res, true
}

The switch compiles to a jump table — same O(1) dispatch as the map, but without hashing, without closure allocation, and without function pointer indirection. The CPU branch predictor can optimize switch patterns better than indirect function calls.

4. Bitmask Operations for Permission Analysis

The Cost of Slice-Based Tracking

// BAD: O(n) contains check for each permission
type Permissions []string

func (p Permissions) HasRead() bool {
    return slices.Contains(p, "s3:GetObject") || slices.Contains(p, "s3:*") || slices.Contains(p, "*")
}

Three linear scans per check. For a policy with 20 actions, that's 60 string comparisons to answer "does this grant read access?"

The Fix

// GOOD: O(1) bitmask check
type ActionMask uint8

const (
    ActionRead    ActionMask = 1 << iota  // s3:GetObject
    ActionWrite                           // s3:PutObject
    ActionDelete                          // s3:DeleteObject
    ActionList                            // s3:ListBucket
    actionACLWrite                        // s3:PutBucketAcl (unexported)
)

func (m ActionMask) has(flag ActionMask) bool {
    return m&flag != 0
}

func (s Statement) ResolveActions() (ActionMask, int) {
    var mask ActionMask
    for _, action := range s.Action {
        a := strings.ToLower(action)
        switch {
        case a == "*" || a == "s3:*":
            mask |= ActionRead | ActionWrite | ActionDelete | ActionList | actionACLWrite
        case a == "s3:getobject":
            mask |= ActionRead
        case a == "s3:putobject":
            mask |= ActionWrite
        // ...
        }
    }
    return mask, bits.OnesCount8(uint8(mask))
}

// Check: one bitwise AND, constant time
func (s Statement) GrantsReadAccess() bool {
    mask, _ := s.ResolveActions()
    return mask.has(ActionRead)
}

Parse the action list once into a bitmask. Every subsequent permission check is a single bitwise AND — constant time, zero allocation, fits in a register.

5. strings.Builder with Pre-Allocation

The Cost of String Concatenation

// BAD: each += allocates a new string
result := ""
for _, finding := range findings {
    result += finding.ControlID.String() + ": " + finding.Evidence.TemporalRisk + "\n"
}

Go strings are immutable. Each += allocates a new backing array and copies the accumulated string. For 100 findings with 50-character lines, that's 100 allocations copying an average of 2.5 KB each.

The Fix

// GOOD: one allocation, zero copies
var b strings.Builder
b.Grow(len(findings) * 64)  // estimate: 64 bytes per finding

for i := range findings {
    f := &findings[i]
    b.WriteString(f.ControlID.String())
    b.WriteString(": ")
    b.WriteString(f.Evidence.TemporalRisk)
    b.WriteByte('\n')
}
result := b.String()

strings.Builder writes to a growing byte buffer. Grow(n) pre-allocates n bytes so the buffer never needs to resize if your estimate is close. The final String() converts the buffer to a string without copying (Go 1.10+).

WriteString over fmt.Fprintf: WriteString is a direct memcpy. Fprintf parses a format string, allocates for the format args, and calls reflection for %v. For simple concatenation, WriteString is 5-10x faster.

The Grow Estimate

b.Grow(5 * 1024)  // 5 KB for a markdown report
b.Grow(256)        // 256 bytes for a diagnostic error message
b.Grow(len(items) * 80)  // 80 bytes per line estimate

Over-estimating is fine — the wasted capacity is a few KB. Under-estimating triggers a reallocation (still better than +=). The rule: estimate the total output size from the input size and allocate once.

6. strings.Cut Over Split+Index

The Cost of Split

// BAD: allocates a []string, splits entire string
parts := strings.Split(line, "=")
if len(parts) >= 2 {
    key = parts[0]
    value = parts[1]
}

strings.Split allocates a slice and all the substrings. For "KEY=value=with=equals", it allocates 4 strings when you only need 2.

The Fix

// GOOD: zero allocation, stops at first separator
key, value, ok := strings.Cut(line, "=")
if ok {
    // key = "KEY", value = "value=with=equals"
}

strings.Cut (Go 1.18+) returns substrings of the original string — no allocation. It stops at the first separator, so "KEY=value=with=equals" correctly splits into "KEY" and "value=with=equals".

For prefix checking:

// BAD: allocates trimmed string
if strings.HasPrefix(s, "severity:") {
    rest := s[len("severity:"):]
}

// GOOD: CutPrefix returns substring, no allocation
if rest, ok := strings.CutPrefix(s, "severity:"); ok {
    // rest is a substring, zero allocation
}

7. Defined Types Avoiding Conversion

The Cost of String Conversion

// BAD: string() creates a new string from the typed value
assetID := asset.ID("bucket-1")
history[assetID.String()] = observations  // allocates new string on every call

assetID.String() returns string(assetID) — which in Go allocates a new string and copies the bytes. In a loop over 1,000 assets × 10 snapshots, that's 10,000 string allocations.

The Fix

// GOOD: use the typed value directly as map key
history[assetID] = observations  // asset.ID IS a string — no conversion

asset.ID is type ID string. Go allows defined string types as map keys. The map uses the underlying string bytes directly. No conversion, no allocation.

The same principle applies to function parameters:

// BAD: convert to string for a function that accepts string
fmt.Println(string(controlID))

// GOOD: use the String() method (or let fmt call it)
fmt.Println(controlID)  // fmt calls String() automatically

When Conversion is Needed

Sometimes you need string():

// String conversion required: joining typed values into a single string
joinedPath := string(vendor) + "/" + string(assetType)

But within the same type system — passing ControlID to a function that accepts ControlID, using it as a map key, comparing it — no conversion is needed.

8. sync.Once and sync.Map for Initialization

The Cost of Repeated Initialization

// BAD: check-then-init has a race condition
type ExemptionConfig struct {
    prepared bool
    exactMap map[string]*Rule
}

func (c *ExemptionConfig) Prepare() {
    if c.prepared { return }  // RACE: two goroutines can both see false
    c.exactMap = buildIndex(c.Assets)
    c.prepared = true
}

The Fix

// GOOD: sync.Once is atomic and runs exactly once
type ExemptionConfig struct {
    once     sync.Once
    exactMap map[string]*Rule
}

func (c *ExemptionConfig) Prepare() {
    c.once.Do(func() {
        c.exactMap = buildIndex(c.Assets)
    })
}

For caching values keyed by pointer identity (TTY detection results):

// Cache TTY detection result per file descriptor
var ttyCache sync.Map

func CanColor(out io.Writer) bool {
    f, ok := out.(*os.File)
    if !ok { return false }

    key := reflect.ValueOf(f).Pointer()
    if cached, ok := ttyCache.Load(key); ok {
        v, _ := cached.(bool)
        return v
    }

    enabled := detectTTY(f)
    ttyCache.Store(key, enabled)
    return enabled
}

sync.Map is optimized for the "write-once, read-many" pattern — exactly what caching needs. No mutex contention on the read path after the first call.

9. WalkDir Over Walk

The Cost of Extra Syscalls

// BAD: filepath.Walk calls Lstat on every entry
filepath.Walk(dir, func(path string, info os.FileInfo, err error) error {
    // info is from Lstat — an extra syscall per entry
})

filepath.Walk calls os.Lstat on every directory entry to populate os.FileInfo. For a directory with 10,000 files, that's 10,000 extra syscalls — each one a kernel context switch.

The Fix

// GOOD: filepath.WalkDir uses cached DirEntry
filepath.WalkDir(dir, func(path string, d fs.DirEntry, err error) error {
    // d.IsDir() and d.Name() are cached from readdir — no extra syscall
    // Only call d.Info() when you actually need size/mode/modtime
})

filepath.WalkDir (Go 1.16+) uses fs.DirEntry, which caches the entry type from the readdir syscall. d.IsDir() and d.Name() are free. d.Info() calls Lstat only when you explicitly need it — most filters don't (skip hidden dirs, match extensions).

The Checklist

Pattern	Cost of Not Doing It	Fix Effort
Pre-allocate slices	O(log n) allocations + copies	One `make()` parameter
Index-based iteration	128-408B copy per iteration	Change `_, v` to `i := range`
Switch over map	Hash + closure + indirect call per dispatch	Replace map with switch
Bitmask operations	O(n) contains per check	One-time parse + O(1) checks
strings.Builder + Grow	O(n²) concatenation	Replace `+=` with `WriteString`
strings.Cut	Allocate full split slice	Replace `Split` with `Cut`
Defined type as key	String conversion per use	Remove `string()` casts
sync.Once / sync.Map	Race condition or mutex contention	Replace bool flag with Once
WalkDir over Walk	Extra Lstat syscall per entry	Change `Walk` to `WalkDir`

None of these require benchmarks to justify. They're visible in code review, mechanical to apply, and eliminate entire categories of unnecessary work. The profiler is for finding the 1% improvements after these 9 patterns are already in place.

These 9 performance patterns were applied across Stave, a Go CLI for offline security evaluation. The index-based iteration alone fixed 70 loops copying structs up to 408 bytes. The switch-over-map change eliminated closure allocations on the predicate evaluation hot path.

Two Problems, Two Tools: Why AI-Assisted Scanning and Configuration Verification Solve Different Things

Bala Paranj — Mon, 11 May 2026 14:00:56 +0000

There's growing confusion in cloud security about what AI-assisted tools can do. Some of the confusion comes from inflated claims about AI-powered vulnerability discovery. Some comes from genuine uncertainty about where different tools fit. But most of it comes from treating security as one problem when it's actually two. The two problems require fundamentally different approaches.

Before evaluating any tool, separate the problems.

Two classes of security problems

Class 1: Pattern Recognizable Problems

SQL injection is a vulnerability regardless of the operator. Unsanitized user input concatenated into a SQL query is dangerous in every application, every deployment, every organization. The operator's intent doesn't change the verdict. Nobody intends for their application to be injectable.

The same applies to XSS, buffer overflows, command injection, insecure deserialization, and most of the OWASP Top 10 for web applications. These are universal patterns. The vulnerability exists because of how the code works, not because of what the operator intended. A function that passes user input to eval() is unsafe whether the application is a healthcare portal or a recipe blog.

Key property: The verdict is independent of the operator's intent. The pattern generalizes across deployments. If you've seen one SQL injection, you can recognize the next one.

Class 2: Intent Dependent Problems

A public S3 bucket is correct for a static website hosting CSS files. The same configuration is a HIPAA violation when the bucket contains patient records. The bucket settings are identical. The verdict depends entirely on what the operator declared about the data inside.

A Bedrock agent with lambda:InvokeFunction on Resource: * is appropriate for an internal developer tool that needs to orchestrate arbitrary workflows. The same permission is catastrophic when the agent serves customer-facing queries and one of those Lambda functions reads from a PHI-tagged bucket. The IAM policy is identical. The verdict depends on the interaction between the policy, the agent's purpose, and the data classification of the resources the tool chain can reach.

Key property: The verdict depends on the operator's declared intent. The pattern does not generalize across deployments. Every organization's tags, policies, and trust relationships are unique. Seeing a thousand examples of "this configuration is unsafe" doesn't tell you whether the next configuration is unsafe — because the next operator's intent is different.

Why this distinction matters

Mixing the two classes leads to the wrong tool for the problem, and the wrong expectations for the results.

Using an AI-trained scanner on Class 2 problems produces the IDOR false positive: the scanner flags a critical IDOR on a public endpoint because it doesn't know the endpoint is supposed to be open. It's applying pattern recognition to a problem where the pattern doesn't generalize. Because the verdict depends on intent that only this operator knows.

Using a configuration consistency checker on Class 1 problems is equally wrong. It can't find SQL injection because SQL injection isn't a configuration contradiction — it's a code defect that exists regardless of what the operator declared.

The tools aren't interchangeable. They solve different problem classes.

What solves each class

Class 1: Pattern recognition

AI-assisted vulnerability discovery — LLM-powered pen testing, fuzzing, SAST, agentic security scanners — excels at Class 1 problems. The scanner learns patterns from training data: "this code shape leads to injection," "this API behavior indicates a broken access control." The patterns generalize because the vulnerabilities are universal.

The growing critique that AI-assisted scanning produces inflated findings is valid within Class 1. Some findings are in low-tier targets, some bugs aren't exploitable, some results are source-assisted. The community is right to demand validation. But the approach itself is sound: pattern recognition works when patterns generalize.

Where the approach breaks down is at the boundary between Class 1 and Class 2. The IDOR example sits on that boundary. Some IDORs are universal (accessing another user's private data is always wrong). Some are intent-dependent (accessing a public record through a predictable ID is by design). When the scanner can't distinguish the two, it produces noise. The fix isn't better AI. It's recognizing that the problem has crossed into Class 2, where the operator's intent determines the verdict.

Why more training doesn't fix Class 2

The reason is structural. In Class 1, the verdict is a function of the code: verdict = f(code). The function is the same for every deployment. Train on enough examples and the model approximates it well.

In Class 2, intent is a variable: verdict = f(configuration, intent). The configuration is visible. It's the IAM policy, the S3 tag, the Bedrock agent setup. But intent is supplied by the operator, and its value changes for every scenario. A public bucket is correct when intent is "serve static assets." The same public bucket is a violation when intent is "store patient records." The configuration is identical. The intent is different. The verdict flips.

Because intent is a variable in that function, it cannot be baked into a model during training. It is unknown before training — no dataset contains this operator's future decisions. It is unknown during training — the model learns patterns from other operators' configurations, none of which carry this operator's intent. And it is unknown after training — when the model encounters a new deployment, the intent variable has a value it has never seen because that value was created when this specific operator tagged this specific bucket and configured this specific agent. The variable doesn't exist yet when the model is trained. It comes into existence when the operator makes a deployment decision.

An AI scanner sees the configuration. It does not see the intent. It's solving an equation with a variable that has no value at any stage of the model's lifecycle. No amount of training data fills that gap because the gap isn't a data problem — it's a timing problem. The value is created after the model is deployed, by an operator the model has never observed, for a purpose the model cannot infer from the configuration alone.

This is why the false-positive IDOR is unfixable by training: the scanner sees the endpoint and the response. It cannot see whether the operator intended that data to be public. That intent didn't exist when the model was trained. It came into existence when this operator designed this application. The model will encounter this value for the first time at inference — with no prior example to generalize from.

Class 2: Constraint satisfaction

Configuration consistency checking asks: "Given what the operator declared — what's sensitive, what's public, who can reach what — do those declarations contradict each other?"

This is a constraint satisfaction problem. The operator's declarations are constraints: "this bucket contains PHI," "this agent serves public queries," "this knowledge base indexes this bucket." The tool checks whether those constraints are simultaneously satisfiable without creating a forbidden state. That's a satisfiability query — the exact problem SMT solvers like Z3 have been solving since 2007 for flight software, CPU verification, and compiler correctness.

The solver doesn't need training data. It doesn't need to generalize across organizations. It reads THIS operator's assertions and checks whether THEY contradict each other. The logic is the same for every deployment. The facts are different. That's what constraint solvers are built for — same engine, different inputs, deterministic answers.

A trained model answering the same question would need thousands of labeled examples of "this configuration is safe" and "this configuration is unsafe." It would produce a probability, not a proof. It would struggle with novel compositions it hadn't seen in training. And crucially, it would fail on intent — because every organization's tags, policies, and classifications are unique. You can show a model a thousand IDOR findings and it still can't determine whether endpoint /api/records/123 is supposed to be open, because that depends on what THIS operator intended for THIS application, and that intent isn't in any training corpus. It's in the tags, policies, and configurations that only this operator controls.

The right tool for each class

Property	Class 1 (universal patterns)	Class 2 (intent-dependent)
Example	SQL injection, XSS, buffer overflow	PHI bucket indexed by public RAG pipeline
Verdict depends on operator intent?	No — always a vulnerability	Yes — depends on declared data classification
Pattern generalizes?	Yes — one SQLi resembles the next	No — every operator's intent is different
Training data helps?	Yes — more examples improve detection	No — each deployment's intent is unique
Right approach	Pattern recognition (AI/ML)	Constraint satisfaction (SMT solvers)
Right tool	SAST, DAST, fuzzing, AI scanners	Configuration consistency verification

What the scanner sees vs. what consistency verification sees

Now that the classes are separated, the gap becomes visible.

Consider a Bedrock agent in AWS. A component-level scanner checks each resource individually:

Bedrock encryption:     ✅ PASS
Bedrock VPC:            ✅ PASS
Bedrock model access:   ✅ PASS
S3 encryption:          ✅ PASS
S3 public access:       ✅ PASS
Lambda encryption:      ✅ PASS

6 checks. 6 passes. COMPLIANT.

These are Class 1 checks applied to configuration: "is encryption on?" is a universal pattern. The answer doesn't depend on the operator's intent. Encryption should be on.

But the agent's execution role has lambda:InvokeFunction on Resource: *. It can invoke any Lambda in the account. One of those Lambda functions reads from a bucket tagged data_classification: phi. The knowledge base indexes the same PHI bucket for RAG retrieval. These are Class 2 problems — the verdict depends on the interaction between the agent's permissions, the Lambda's access, and the bucket's data classification. All three are intentional configurations. The contradiction is in their composition.

Consistency verification extracts facts from all three services, checks whether they compose into a forbidden state, and reports: "Your customer-facing chatbot can return patient records through its Lambda tool chain." Five individual findings compose into three CRITICAL compound chains. The scanner's 6/6 PASS and the consistency checker's 3 CRITICAL chains are both correct — they're answering different questions about different problem classes.

What consistency verification provides

Compound detection across services. Individual checks can't find cross-service compositions. When the agent's role is overpermissioned AND the Lambda reads PHI AND the knowledge base indexes PHI, the compound fires as a single chain with a description naming the specific attack path.

Intent-aware evaluation. The IDOR problem doesn't exist here because the operator's intent is encoded in the configuration. Tags declare sensitivity. Policies declare access. The tool doesn't guess whether data is sensitive — the operator tagged it. "Your PHI-tagged bucket is indexed by your public-facing knowledge base" isn't a guess. Both the tag and the configuration are explicit operator decisions. The finding resolves into a concrete decision (remove the tag or change the data source), not a triage exercise.

Mathematical proof. Z3 returns sat (the forbidden state is reachable) or unsat (mathematically impossible). Not a confidence score. Not a probability. A proof that can be verified by running the same query again, or by a different solver. For compliance evidence, proofs beat confidence scores.

Traceability. Every step in the compound chain traces back to a specific property in a specific configuration file through a deterministic identifier. One grep returns the observation file, the property path, and the timestamp. The team doesn't search for the root cause — the tool names it.

Air-gapped operation. No credentials, no API calls, no network access. Static snapshot analysis on a laptop. For organizations under GDPR, HIPAA, or FedRAMP, this isn't a feature — it's a prerequisite.

What consistency verification does NOT do

It doesn't find SQL injection. It doesn't discover XSS. It doesn't fuzz API endpoints. It doesn't scan dependencies for CVEs. It doesn't evaluate models for prompt injection. These are Class 1 problems. They need Class 1 tools.

Consistency verification catches what sits between the Class 1 tools: the compound configuration errors that exist in the interaction between services, where every individual check passes and the aggregate state is unsafe.

What's missing: your intent

There's a prerequisite that consistency verification cannot work without: the tool cannot read the security engineer's mind. It reads configurations. If the engineer's intent isn't expressed in the configuration, the tool has nothing to reason about.

If your PHI buckets aren't tagged data_classification: phi, the compound chain "knowledge base indexes PHI data" cannot fire. No tag, no finding. The engineer has to declare what's sensitive before the tool can check whether the declaration is violated.

Tags are intent declarations. data_classification: phi is not metadata for a dashboard. It's a machine-readable statement: "this bucket contains patient records." Without it, the tool treats the bucket like any other bucket. The compound detection that joins "this knowledge base indexes this bucket" with "this bucket contains PHI" requires both declarations to exist.

Policy absence is an intent signal. When a Bedrock agent has no guardrail configured, the tool reads that absence as a fact: "guardrail is not present." The configuration is the expressed state — the tool reads what's there and what's missing.

Chain definitions encode security judgment. When a control author writes a compound chain that says "if the agent's role is overpermissioned AND the knowledge base indexes PHI AND there's no guardrail, that's CRITICAL" — they're encoding a security team's judgment about which interactions matter. The engine doesn't decide what's dangerous. The control author decides.

This is similar to how you write a unit test: You know the expected value of the right result for a given input, you encode that human judgment in the unit test.

Tagging discipline is the prerequisite. An organization that doesn't tag its sensitive data, doesn't classify its environments, and doesn't label its IAM roles by purpose will get fewer findings — not because their infrastructure is safer, but because they haven't expressed enough intent for the tool to reason about.

That's the correct design. The alternative is guessing. Guessing produces inflated findings, false-positive IDORs, and the critical-severity noise that the security community is rightly pushing back on. Consistency verification doesn't guess. It requires the engineer to say what matters, and then checks whether the infrastructure respects what they said.

How to think about your tooling stack

Question	Problem class	Right tool
"Does my code have bugs?"	Class 1 — universal	SAST, DAST, fuzzing, AI-assisted pen testing
"Does my model have vulnerabilities?"	Class 1 — universal	Model security scanners, red teaming
"Are my components configured correctly?"	Class 1 — universal	CSPM, CIS benchmarks, component scanners
"Do my configurations contradict each other?"	Class 2 — intent-dependent	Compound risk / consistency verification

The first three rows are mature. The fourth is new. It doesn't replace the others — it catches what they structurally cannot.

The critical mindset the security community applies to AI-assisted scanner findings — "is this finding real? is the bug exploitable? is the target meaningful?" — is right. Apply it to consistency verification too. But ask the Class 2 version: "does this configuration really say what the tool claims?" (every fact is verified against the raw configuration file). "Is the compound really a risk?" (the chain description names specific services and data classifications from the operator's own declarations). "Can I verify it independently?" (the solver is open source — run the query yourself).

The findings aren't inflated because they aren't heuristic. They're logical consequences of the operator's own declarations. The operator said "this is PHI." The operator said "this agent can invoke any Lambda." The tool says "those two facts compose into a breach path." That's not an opinion. That's arithmetic on expressed intent.

The consistency verification approach described in this article is implemented in Stave, an open-source static analysis tool for cloud infrastructure configurations. Stave evaluates 2,650+ controls across 74 AWS service domains, exports facts to nine independent reasoning engines — including SMT solvers used to verify flight software — and detects compound risk chains across services. 32 AI agent identity controls and 5 AI-specific compound chains cover Bedrock, SageMaker, and Lambda. All analysis runs on air-gapped snapshots with no cloud credentials required.

go:embed in a CLI: Schemas, Controls, Templates, and Pack Registries

Bala Paranj — Sun, 10 May 2026 13:59:23 +0000

How embedding JSON schemas, YAML controls, Go templates, and a pack registry index into the binary eliminates external file dependencies — critical for air-gapped deployment and deterministic evaluation.

A security CLI that depends on external schema files to validate input is a CLI that breaks when deployed to a Docker container, a CI runner, or an air-gapped server where those files don't exist.

go:embed solves this by compiling files into the binary at build time. The binary carries its own schemas, controls, templates, and registry index. No installation step. No file path configuration. No "schema file not found" errors in production.

Here are four ways to use, each solving a different embed problem.

1. JSON Schemas — Validation Without a Registry

//go:embed embedded/*/*/*.json
var embeddedFS embed.FS

The directory structure:

internal/contracts/schema/embedded/
├── control/v1/control.schema.json
├── diagnose/v1/diagnose.schema.json
└── output/v1/output.schema.json

The validator loads schemas from the embedded filesystem:

func (v *Validator) getSchema(kind Kind, version string) (*jsonschema.Schema, error) {
    v.mu.RLock()
    if cached, ok := v.compiled[cacheKey]; ok {
        v.mu.RUnlock()
        return cached, nil
    }
    v.mu.RUnlock()

    // Load from embedded FS — no disk access
    data, err := embeddedFS.ReadFile(schemaPath(kind, version))
    if err != nil {
        return nil, fmt.Errorf("load schema %s/%s: %w", kind, version, err)
    }

    v.mu.Lock()
    defer v.mu.Unlock()
    // ... compile and cache
}

Why embed, not bundle separately: The schema version must match the binary version. If schemas are external files, a user could upgrade the binary but keep old schemas — leading to validation that passes when it shouldn't or fails when it should pass. Embedding guarantees schema-binary consistency.

2. YAML Controls — Built-In Security Policies

//go:embed embedded/s3/**/*.yaml
var controlFS embed.FS

43 S3 security controls embedded in the binary:

internal/controldata/embedded/s3/
├── access/
│   ├── CTL.S3.PUBLIC.001.yaml
│   ├── CTL.S3.ACL.001.yaml
│   └── ...
├── encryption/
│   ├── CTL.S3.ENC.001.yaml
│   └── ...
└── governance/
    └── ...

The loader accepts any fs.FS — embedded for production, fstest.MapFS for tests:

type BuiltinLoader struct {
    fsys fs.FS
    mu   sync.RWMutex
    once sync.Once
    controls []policy.ControlDefinition
}

// Production: uses embedded FS
func EmbeddedFS() fs.FS { return controlFS }

// Tests: use any fs.FS
func NewBuiltinLoader(fsys fs.FS) *BuiltinLoader {
    return &BuiltinLoader{fsys: fsys}
}

Why embed controls: Users can run stave apply --controls controls/s3 to use the built-in controls without copying YAML files to their project. The controls ship with the binary. For custom controls, users point --controls at their own directory — the built-in ones are a starting point, not a lock-in.

3. Go Templates — Customizable Output

//go:embed templates/prompt_default.tmpl
var DefaultTemplate string

The LLM prompt template is embedded as a string (not embed.FS — it's a single file):

func RenderPrompt(data Data, tmpl string) (string, error) {
    return ui.ExecuteTemplate(tmpl, data)
}

For the default template, tmpl is DefaultTemplate (the embedded string). For custom templates, the user provides a path:

# Default embedded template
stave prompt from-finding --evaluation-file eval.json

# Custom template from disk
stave prompt from-finding --evaluation-file eval.json --prompt-template ./my-template.tmpl

Why string, not embed.FS: A single template doesn't need a filesystem abstraction. string is simpler — it can be passed directly to template.Parse(). The embed.FS pattern is for collections of files.

4. Pack Registry — Index of Built-In Control Packs

//go:embed embedded/index.yaml
var embeddedRegistryFS embed.FS

The registry index maps pack names to control IDs:

# embedded/index.yaml
packs:
  s3:
    description: "AWS S3 bucket security controls"
    controls:
      - CTL.S3.PUBLIC.001
      - CTL.S3.ACL.001
      - CTL.S3.ENC.001
      # ... 43 controls

The registry validates its own integrity at startup:

func (r *Index) ValidateStrict(fsys embed.FS) error {
    // Verify every control referenced in index.yaml exists as a YAML file
    // Verify every YAML file in the embedded FS is referenced in index.yaml
    // No orphans. No phantom references.
}

This catches build-time mistakes: adding a control YAML file but forgetting to register it in the index, or removing a file but leaving the index entry.

The Build Pipeline

sync-schemas:
    @mkdir -p $(SCHEMA_DST)
    rm -rf $(SCHEMA_DST)/*
    cp -R $(SCHEMA_SRC)/* $(SCHEMA_DST)/

build: sync-schemas
    go build -o stave ./cmd/stave

Schemas are synced from a canonical source directory into the embed directory before building. The canonical schemas are human-editable; the embedded copies are build artifacts. This means go build alone won't work after a fresh clone — make build is required (documented in CLAUDE.md).

When NOT to Embed

User-authored files (observations, custom controls): these change per project — don't embed
Large binary assets (images, videos): bloats the binary unnecessarily
Files that change between deployments (config, secrets): must be external
Files > 10MB: Go's embed has no compression — large files inflate the binary

Embed when the file is part of the tool's identity (schemas, built-in policies, default templates) and must be available in every deployment environment including air-gapped.

These 4 embed patterns are used in Stave, a Go CLI for offline security evaluation. The embedded schemas, controls, templates, and pack registry ensure the binary is self-contained — deployable to air-gapped environments with no external file dependencies.

Your Private API is Currently Safe. One Developer Change Away From Unsafe.

Bala Paranj — Sat, 09 May 2026 11:44:13 +0000

A 2023 Medium tutorial walks through restricting a private API Gateway to a single EC2 host in a single VPC. The author's intent — read literally — is correct: make the API reachable only from inside the VPC, only through the VPC endpoint they create, only by the EC2 they specify. The configuration they publish does this almost. It also has two active gaps and one latent gap. The active gaps are visible to a careful reader of AWS documentation. The latent gap is invisible until a future change activates it.

Z3 from Microsoft Research runs four queries against the published configuration and proves all three. The two active gaps return SAT with concrete witnesses. The latent gap returns UNSAT on the published configuration but SAT on a one-line variant — the kind of variant a developer would introduce while adding a new method or stage. That asymmetry is the article's central argument: a configuration's current safety status and its structural fragility are different questions. Heuristic scanners only check the first. Formal verification can answer both.

The configuration

The author's resource policy:

{
  "Version": "2012-10-17",
  "Statement": [
    {
      "Effect": "Deny",
      "Principal": "*",
      "Action": "execute-api:Invoke",
      "Resource": "execute-api:/prod/GET/*",
      "Condition": {
        "StringNotEquals": {
          "aws:sourceVpc": "vpc-0b52ca08e7db8531f"
        }
      }
    },
    {
      "Effect": "Allow",
      "Principal": "*",
      "Action": "execute-api:Invoke",
      "Resource": "execute-api:/prod/GET/*"
    }
  ]
}

The API uses --authorization-type NONE. The resource policy is the only access control on the API itself.

Three claims, three Z3 queries

Claim 1: Allow/Deny resource pattern alignment

Both statements scope to execute-api:/prod/GET/*. Today, that means every request the Allow admits is also covered by the Deny condition. The Deny applies whenever the request comes from a VPC other than vpc-0b52ca08e7db8531f; the Allow is unconditional but scoped to the same resource pattern. The two statements together restrict /prod/GET/* to traffic from the VPC.

Z3 query: is there a (stage, method, resource) witness that the Allow admits but the Deny does not?

Verdict on the published config: UNSAT. Every witness the Allow admits is also blocked by the Deny. The current design is aligned.

But the design is fragile: there's no structural guarantee that the Allow and Deny patterns stay aligned under future edits. To demonstrate, consider what a developer would do when asked to "add a dev stage so QA can test against it." The natural change is to broaden the Allow:

 {
   "Effect": "Allow",
   "Principal": "*",
   "Action": "execute-api:Invoke",
-  "Resource": "execute-api:/prod/GET/*"
+  "Resource": "execute-api:/*"
 }

The Deny stays at /prod/GET/* because nobody noticed it needed to change too. Re-run Z3 against this variant:

Verdict on the broadened-allow variant: SAT.

verdict: SAT — witness: stage=prod method=POST resource=execute-api:/prod/POST/users
         (Allow widened to execute-api:/* — Deny still scoped to
          /prod/GET/*, so this resource is allowed without any VPC
          restriction)

The witness is concrete. execute-api:/prod/POST/users is admitted by the broadened Allow (matches execute-api:/*) and not blocked by the Deny (does not match execute-api:/prod/GET/*). The Deny condition's VPC restriction does not apply to this resource at all. The new POST endpoint is publicly invocable — without any VPC restriction — even though the API is still configured as a private REST API.

The published configuration is currently safe because the Allow and Deny patterns happen to be identical. That equality is structural. It depends on a human remembering, every time either pattern changes, to update the other. Z3 can detect when that invariant breaks.

Claim 2: aws:sourceVpc admits every endpoint in the VPC

The Deny condition uses aws:sourceVpc:

"Condition": {
  "StringNotEquals": {
    "aws:sourceVpc": "vpc-0b52ca08e7db8531f"
  }
}

This restricts to traffic from any source in vpc-0b52ca08e7db8531f. The author's narrative says "restrict to the VPC endpoint we created" — but the condition restricts to the entire VPC, not the specific endpoint.

In a shared enterprise VPC, multiple teams create multiple VPC endpoints. Each endpoint is a separate network path; each has its own security group and its own service. The author's intended endpoint (vpce-0abc123def456789) is one of them. Any other interface endpoint in the same VPC, with permissive security-group rules, is a path to this private API that the author did not intend.

Z3 query: is there a VPC endpoint in vpc-0b52ca08e7db8531f that is not vpce-0abc123def456789, but reaches the API anyway?

Verdict on the published config: SAT.

verdict: SAT — witness: vpce-0999888777666555
         (in vpc-0b52ca08e7db8531f, NOT vpce-0abc123def456789)
         (Deny condition uses aws:sourceVpc which matches every
          endpoint in the VPC, not just the intended one)

The witness is the exact failure mode: a different VPC endpoint in the same VPC, created by another team for another service, can route traffic to this API. The security group on the intended endpoint restricts to one EC2 IP, but the resource policy doesn't care which endpoint a request came through — it only checks the source VPC.

The fix is one word in the condition key:

 "Condition": {
   "StringNotEquals": {
-    "aws:sourceVpc": "vpc-0b52ca08e7db8531f"
+    "aws:sourceVpce": "vpce-0abc123def456789"
   }
 }

aws:sourceVpce matches the specific endpoint ID, not the entire VPC. After this change, the Deny applies to every endpoint except the named one; the witness from above is denied.

Claim 3: No authorization compounds the gap

The API method uses --authorization-type NONE. There is no IAM authorization, no Cognito user pool, no Lambda authorizer. The resource policy is the only gate. If the resource policy has a gap (claim 2: it does), no second layer catches it.

Z3 query: is there a request that reaches the API with auth_type=NONE AND a non-intended VPC endpoint?

Verdict on the published config: SAT — the same witness as claim 2, plus auth_type: NONE. Any workload in the VPC, on any endpoint, with any identity (or no identity), can invoke the API.

This is not a discrete vulnerability so much as a defense-in-depth failure. AWS provides four authorization options at the method level (NONE, AWS_IAM, COGNITO_USER_POOLS, CUSTOM). Three of the four require the request be authenticated by some mechanism; the resource policy is then a second layer that further restricts based on source. With NONE, the resource policy is the only layer.

 aws apigateway put-method \
   --rest-api-id timegateway-id \
   --resource-id root-id \
   --http-method GET \
-  --authorization-type NONE
+  --authorization-type AWS_IAM

After this change, requests must be SigV4-signed by an authorized IAM principal. The resource policy still applies; the IAM check is a second layer that catches resource-policy gaps that creep in over time.

Why this is a logic question

CEL evaluates a state predicate. Stave's existing CTL.APIGATEWAY.NETWORK.PRIVATE.POLICY.001 checks one boolean: resource_policy_restricts_vpc. The published configuration sets this to true (the policy does restrict by VPC, just by the wrong condition key). The control reports clean.

Z3 doesn't pattern-match. It runs SAT searches over witness sets:

exists witness:
  resource_policy_admits(witness)
  AND witness != intended

For Claim 1, the witness set is a few stage/method tuples. The query asks whether any tuple is admitted by the Allow but not blocked by the Deny. On the published config: no — the patterns happen to match. On the broadened-allow variant: yes — prod/POST/users is admitted but not blocked.

For Claim 2, the witness set is several VPC endpoint ARNs in the same VPC. The query asks whether the Deny fails to apply for any non-intended endpoint. On the published config: yes for every non-intended endpoint — the condition's StringNotEquals on aws:sourceVpc
is false (the source IS in the VPC), so the Deny doesn't fire, so the Allow takes over.

For Claim 3, the query compounds Claim 2 with the auth_type=NONE field. On the published config: yes — same witness as Claim 2 plus no auth check.

CEL's predicate vocabulary doesn't include "find a witness." Z3's does.

The reframe

Earlier version of this example series refuted a suspicion about KMS Resource: "*" — the pattern looked unsafe to a heuristic scanner; Z3 proved it was correctly scoped because of KMS-specific semantics. The lesson was: formal verification is right when you expect it to be right and right when you expect it to be wrong.

Later it demonstrates the converse case. Finding 1a returns UNSAT — the published configuration is currently aligned. A heuristic might stop there and declare the configuration safe. Z3 doesn't stop there. The same query, against a one-line variant that represents a common developer change, returns SAT.

The article's claim is not "your config is broken right now." It's "your config is one developer change away from being broken, and the change you'd most naturally make is the one that breaks it." That's a stronger statement than a heuristic can make because it requires reasoning about the configuration under perturbation — which is exactly what an SMT solver gives you.

The remediation

Three changes. None requires architectural rework:

 {
   "Version": "2012-10-17",
   "Statement": [
     {
       "Effect": "Deny",
       "Principal": "*",
       "Action": "execute-api:Invoke",
-      "Resource": "execute-api:/prod/GET/*",
+      "Resource": "execute-api:/*",
       "Condition": {
         "StringNotEquals": {
-          "aws:sourceVpc": "vpc-0b52ca08e7db8531f"
+          "aws:sourceVpce": "vpce-0abc123def456789"
         }
       }
     },
     {
       "Effect": "Allow",
       "Principal": "*",
       "Action": "execute-api:Invoke",
-      "Resource": "execute-api:/prod/GET/*"
+      "Resource": "execute-api:/*"
     }
   ]
 }

Plus the method-level change to authorization-type AWS_IAM.

After remediation:

Finding 1: UNSAT (patterns aligned at execute-api:/*).
Finding 2: UNSAT (aws:sourceVpce scopes to the specific endpoint).
Finding 3: UNSAT (IAM auth gates the request before the resource policy is consulted).

The pattern alignment is now structural — both statements use the same execute-api:/* — not an accident of the author choosing the same literal twice.

The prevention lesson

Three layers, in priority order:

Resource-policy template review. Whoever publishes infrastructure tutorials should include the alignment invariant ("Allow.Resource ⊆ Deny.Resource union with the inverse condition") as a checked property, not an implicit one. Z3 can check this automatically. Humans cannot reliably check it under deadline.

aws:sourceVpce is the scoping condition for private API restrictions, not aws:sourceVpc. Treat any AWS tutorial that uses the latter for "endpoint-specific" restriction as outdated, and update the policy when copy-pasting. The Vpc form admits every endpoint in the VPC — usually not what the author intended.

Authorization-type NONE is a deliberate choice, not a default. If the API serves authenticated traffic, use AWS_IAM. The resource policy then becomes a second layer, and the resource-policy alignment fragility above stops being a single point of failure.

Checklist

Allow and Deny statements in API Gateway resource policies use the same Resource pattern (or the Deny is broader)
VPC-restriction conditions use aws:sourceVpce (specific endpoint), not aws:sourceVpc (entire VPC)
Private REST APIs use --authorization-type AWS_IAM (or another non-NONE type) so the resource policy is a second layer behind authentication
Resource-policy templates run through formal verification at publish time; tutorials include the verification step in the walkthrough
Pre-merge CI runs the equivalent of this iteration's Z3 prover against the post-deploy observation snapshot

The article author's published configuration is currently safe. It works. The EC2 reaches the API. The intended VPC endpoint is the only path. As infrastructure documentation, the tutorial does its job. As a security artefact, it's one well-meant developer change away from an open API. Z3 can tell you that. Pattern matchers can't.

The example shipped with this article can be found at stave/examples/apigw-private-api-scoped-deny/ — two binaries side by side: a CEL foil that runs Stave's CTL.APIGATEWAY.NETWORK.PRIVATE.POLICY.001 control against the writeup, broadened-allow, and remediated configurations and reports COMPLIANT on all three (the existing control fires only when the private API has no VPC restriction at all), and a Z3 SAT prover that runs the four queries described in this article. The Z3 binary lives in a sibling Go module so its libz3 link stays out of Stave's main vendored tree. Stave detects this pattern and 31 other H1-grounded scenarios from local AWS configuration snapshots, with no cloud credentials.

Global State in Go: 5 Kinds We Found, 3 We Eliminated, 2 We Kept

Bala Paranj — Fri, 08 May 2026 10:58:34 +0000

A mutable registry populated by init(), a session field leaking between evaluations, a validation limit set by a setter, an immutable singleton, and a cached detection result — how to tell which globals are dangerous and which are acceptable.

Not all global state is bad. A var ErrNotFound = errors.New("not found") is global state. So is var controlIDPattern = regexp.MustCompile(...). Nobody argues these should be parameters.

The problem is when global state is mutable and shared across execution boundaries — when one function writes it and another reads it without explicit coordination. In a CLI, this means two evaluations in the same process see each other's side effects. In tests, it means parallel tests corrupt each other's state.

We found 5 kinds of global state in a Go security CLI. Three were dangerous. Two were acceptable. Here's how we decided.

Dangerous: Mutable Global Populated by init()

The Problem

// 14 init() functions across 14 files, all writing to this:
var ControlRegistry = NewRegistry()

// access_block_public.go
func init() {
    ControlRegistry.MustRegister(&accessBlockPublic{
        Definition: NewDefinition(
            WithID("ACCESS.001"),
            WithSeverity(policy.SeverityCritical),
        ),
    })
}

// audit_server_logging.go
func init() {
    ControlRegistry.MustRegister(&auditServerLogging{ ... })
}

// ... 12 more files

14 init() functions write to a package-level ControlRegistry during import. The consequences:

No test isolation. Every test that imports compliance gets all 14 controls loaded. Can't test with a subset.
No parallel safety. Two parallel tests share the same registry. If one test modifies the registry (registering a test-only control), the other sees the modification.
No ordering control. Go doesn't guarantee init() execution order across files. Adding a control that depends on another being registered first is fragile.
Hidden side effects. Importing a package changes global state. The import statement import _ "pkg/compliance" has invisible consequences.

The Fix: Factory Closures + On-Demand Catalogs

var ControlRegistry = NewRegistry()

var allControlConstructors []func() Control

func RegisterControl(factory func() Control) {
    allControlConstructors = append(allControlConstructors, factory)
    ControlRegistry.MustRegister(factory())
}

// Test-only: create an isolated catalog from the same factories
func NewTestCatalog() *ControlCatalog {
    cat := NewRegistry()
    for i := range allControlConstructors {
        cat.MustRegister(allControlConstructors[i]())
    }
    return cat
}

// Test-only: create a catalog with specific controls only
func NewCatalogWith(controls ...Control) *ControlCatalog {
    cat := NewRegistry()
    for _, ctl := range controls {
        cat.MustRegister(ctl)
    }
    return cat
}

Each init() now registers a factory closure instead of a concrete instance:

func init() {
    RegisterControl(func() Control {
        return &accessBlockPublic{
            Definition: NewDefinition(
                WithID("ACCESS.001"),
                WithSeverity(policy.SeverityCritical),
            ),
        }
    })
}

Production is unchanged: ControlRegistry is still populated at import time. Existing code that reads ControlRegistry.Lookup("ACCESS.001") works as before.

Tests are now isolated: NewTestCatalog() creates a fresh catalog by calling each factory — new instances, no shared state. NewCatalogWith(myControl) creates a catalog with just one control for focused testing. Two parallel tests get two independent catalogs.

Dangerous: Session State on a Long-Lived Config Object

The Problem

type Runner struct {
    // Configuration (long-lived, set once)
    Controls     []policy.ControlDefinition
    Clock        func() time.Time
    SLAThreshold time.Duration

    // Session state (per-evaluation, mutable) — DANGER
    StaveVersion     string
    InputHashes      *evaluation.InputHashes
    identitiesByTime map[time.Time][]asset.CloudIdentity
}

identitiesByTime is a mutable map set during Evaluate(). If the Runner is reused for a second evaluation, the identity map from run 1 leaks into run 2. The second evaluation sees identities from snapshots it didn't load.

StaveVersion and InputHashes are per-evaluation metadata on a struct that's supposed to be reusable configuration. Setting them before evaluation and reading them during report assembly creates a temporal coupling — the fields must be set in the right order.

The Fix: Separate by Lifetime

// Configuration (reusable, immutable after construction)
type Assessor struct {
    Controls     []policy.ControlDefinition
    Clock        ports.Clock
    SLAThreshold time.Duration
}

// Per-call parameters (passed as argument, not stored)
type AssessmentOptions struct {
    StaveVersion string
    InputHashes  *evaluation.InputHashes
}

// Per-evaluation state (created in Assess, garbage collected after)
type assessmentSession struct {
    assessor  *Assessor
    idIndex   IdentityIndex         // built fresh per evaluation
    collector *AssessmentCollector   // accumulates per evaluation
    auditTime time.Time             // computed per evaluation
    opts      AssessmentOptions
}

identitiesByTime became IdentityIndex — a value type constructed fresh inside Assess() and stored on the session. When Assess() returns, the session is garbage collected. No leaking between evaluations.

The principle: separate by lifetime. Configuration lives for the process. Options live for one call. Session state lives for one evaluation.

Dangerous: Set-Once Global With No Coordination

The Problem

var maxValidationErrors = DefaultMaxValidationErrors

func SetMaxValidationErrors(n int) {
    if n > 0 {
        maxValidationErrors = n
    }
}

A package-level variable set by a Set* function during bootstrap. The intent is "configure once at startup, read during validation." But nothing enforces the "once" part:

If two tests call SetMaxValidationErrors(5) and SetMaxValidationErrors(10), the last one wins for both tests.
If validation runs concurrently with SetMaxValidationErrors, the read is racy.
The function name doesn't communicate that it's a one-time bootstrap operation.

The Fix: Document the Contract

// maxValidationErrors controls how many errors are shown before truncating.
// Set via SetMaxValidationErrors at startup. This is a process-level display
// preference, not domain state — acceptable as a package variable since it's
// set once during bootstrap and read during validation.
var maxValidationErrors = DefaultMaxValidationErrors

// SetMaxValidationErrors overrides the validation error display cap.
// Must be called during process initialization (e.g., bootstrap), not
// concurrently with validation calls.
func SetMaxValidationErrors(n int) {
    if n > 0 {
        maxValidationErrors = n
    }
}

We chose documentation over refactoring here because:

There's only one caller (cmd/bootstrap_limits.go)
The variable is a display preference, not domain logic
Moving it to a parameter would thread it through 5 functions that don't care about it

When this becomes a problem: If a second caller appears, or if tests need different values, refactor to pass the limit through the function call chain or via a ValidationConfig struct.

Acceptable: Immutable Singletons

The Pattern

var SafeResult = ComplianceReport{Exposed: false}

var GlobalScope = &AuditScope{global: true}

var ErrZeroTimestamp = errors.New("record observation: time must not be zero")

var controlIDPattern = regexp.MustCompile(`^CTL\.[A-Z][A-Z0-9]*(\.[A-Z][A-Z0-9]*){1,}\.\d{3}$`)

Why these are fine:

Immutable. No Set* function. No mutation after package initialization. SafeResult is a value type — copying it creates an independent instance.
No side effects. Reading GlobalScope doesn't change state anywhere.
Compile-time constant behavior. ErrZeroTimestamp always returns the same error. controlIDPattern always matches the same strings.

The litmus test: If you can replace the global with a const (conceptually, even if Go doesn't support const for the type), it's safe. SafeResult is conceptually const ComplianceReport{Exposed: false}. ErrZeroTimestamp is conceptually const error("...").

Acceptable: Cached Detection Results

The Pattern

var ttyCache sync.Map

func CanColor(out io.Writer) bool {
    f, ok := out.(*os.File)
    if !ok {
        return false
    }
    key := reflect.ValueOf(f).Pointer()
    if cached, ok := ttyCache.Load(key); ok {
        v, _ := cached.(bool)
        return v
    }
    enabled := detectTTY(f)
    ttyCache.Store(key, enabled)
    return enabled
}

Why this is fine:

Idempotent. detectTTY(f) returns the same result for the same file descriptor. Caching doesn't change behavior — just avoids redundant syscalls.
Thread-safe. sync.Map handles concurrent reads and writes correctly.
No test pollution. Two tests using os.Stdout get the same cached result — which is correct, because os.Stdout has the same TTY status in both tests. The IsTTY *bool override on Runtime allows tests to bypass the cache entirely.

var globalNoColor bool

func SetNoColor(v bool) { globalNoColor = v }

Similar reasoning for globalNoColor: set once during bootstrap, read many times. The --no-color flag is process-level state — it doesn't change during execution. Tests that need different behavior use the Runtime.NoColor field, not the global.

The Classification Framework

Kind	Mutable?	Set When?	Read When?	Verdict
`ControlRegistry` + `init()`	YES	Import time (14 sites)	Runtime (many)	Eliminate — factory pattern
`identitiesByTime` on Runner	YES	Per-evaluation	Same evaluation	Extract — session struct
`maxValidationErrors`	YES	Bootstrap (1 site)	Validation (few)	Document — set-once contract
`SafeResult`, `ErrZeroTimestamp`	NO	Package init	Anywhere	Keep — immutable singleton
`ttyCache`	YES (append-only)	First access	Subsequent access	Keep — idempotent cache

The Three Questions

For each package-level var, ask:

1. Can two callers see different values?
If yes → eliminate. ControlRegistry shows 14 controls to test A and 14 controls to test B, but test A might want only 1.

2. Does mutation in one context leak into another?
If yes → extract. identitiesByTime from evaluation 1 leaked into evaluation 2.

3. Is the value set once and never changed?
If yes → keep (or document). globalNoColor, maxValidationErrors, compiled regexps.

The last question has a trap: set once is only safe if you can guarantee it's called before any reads. In a CLI, bootstrap runs before any command — safe. In a library used by multiple goroutines, set once is a race condition. Know your execution model.

These 5 global state patterns were found in Stave, a Go CLI for offline security evaluation. The ControlRegistry factory pattern enabled parallel test isolation for 14 security controls. The session extraction fixed a state leak between sequential evaluations. The immutable singletons and caches remain — they're the right tool for process-level state that doesn't change.

The dog that didn't bark: finding security holes in what's missing, not what's misconfigured

Bala Paranj — Thu, 07 May 2026 11:30:32 +0000

Every security scanner examines resources that exist. Nobody checks whether the resources your IAM policies reference actually exist. A deleted S3 bucket name referenced in an active policy is a structural hole — the permission is live, the resource is gone, and the name is reclaimable by any attacker. The absence is the evidence.

In Arthur Conan Doyle's Silver Blaze, a prize racehorse is stolen from a guarded stable. Scotland Yard investigates the crime scene, interviews witnesses, examines evidence. They focus on what happened — what they can see, measure, and catalog.

Sherlock Holmes solves the case by noticing what didn't happen.

Is there any point to which you would wish to draw my attention?
To the curious incident of the dog in the night-time.
The dog did nothing in the night-time.
That was the curious incident.

The guard dog should have barked at an intruder entering the stable. It didn't. Therefore the person who took the horse wasn't a stranger. The dog knew them. Every investigator examined the evidence that was present. Holmes noticed the evidence that was absent.

Cloud security scanners examine resources that exist. They check properties, configurations, and permissions on things that are there:

Is this S3 bucket public? Check the bucket.
Is this RDS instance encrypted? Check the instance.
Is this IAM role over-privileged? Check the role.
Is this security group open? Check the security group.

Every check follows the same pattern: find a resource, read its configuration, evaluate a predicate. The resource exists. The scanner examines it. The finding describes what's wrong with it.

This is Scotland Yard examining the crime scene. Thorough, methodical, and looking at everything that's there.

What scanners don't look at:

An IAM policy says: "Allow PutObject to arn:aws:s3:::prod-audit-logs."

Every scanner checks the policy's permissions. Is it too broad? Does it grant admin access? Does it follow least privilege? They examine the policy — the thing that exists.

Nobody checks whether prod-audit-logs exists.

The bucket was deleted six months ago during a migration. The policy wasn't updated. The permission is active. The resource is gone. The ARN in the policy points at nothing.

This is the dog that didn't bark. The resource should exist. It doesn't. The absence is the evidence.

S3 bucket names are globally unique across all AWS accounts. When a bucket is deleted, its name becomes available for registration by anyone. Any AWS account, anywhere in the world, can create a bucket with that exact name.

The IAM policy still says "Allow PutObject to prod-audit-logs." The Lambda function that writes audit logs still runs every hour. It calls PutObject on prod-audit-logs. If nobody owns that bucket, the write fails silently. If an attacker registers the bucket name, the write succeeds — to the attacker's bucket.

The organization's audit logs — potentially containing PHI, financial records, user activity, or compliance evidence — begin flowing to an attacker-controlled destination. The Lambda function doesn't error. The CloudWatch metrics look normal. The data delivery succeeds. It just goes to the wrong place.

The organization is generating compliance evidence and delivering it to an adversary.

Not every missing resource is equally dangerous. The risk depends on what the policy allows and whether the resource name is reclaimable.

Tier 1: Any dangling reference. An IAM policy references a resource ARN that doesn't exist in the current inventory. The permission is active, the resource is absent. This is a structural hole — the policy's intent no longer matches reality. Maybe the resource was deleted intentionally and the policy cleanup was forgotten. Maybe the resource was renamed. Maybe it never existed (typo in the policy). Regardless, the permission points at nothing. Severity: high.

Tier 2: Write permission to a reclaimable name. The policy grants PutObject, SendMessage, Publish, or other write actions to a resource name that an attacker can claim. This isn't a latent risk. The organization's systems are actively trying to send data to this destination. The attacker claims the name and the data starts arriving. Severity: critical. This is the exfiltration tier.

Tier 3: KMS key reference to a deleted key. The policy grants kms:Decrypt or kms:Encrypt on a key that's been scheduled for deletion or already deleted. KMS key ARNs include random IDs and can't be reclaimed by another account — the risk is operational, not exfiltration. Systems configured to encrypt with a deleted key either fail or fall back to unencrypted writes. The policy maintains the illusion that encryption is active. An auditor reads the policy and sees encryption permissions. The key behind those permissions is gone. Severity: high.

The structural limitation isn't that scanners are poorly built. It's that the finding doesn't live on any single resource.

A per-resource scanner iterates through resources: for each S3 bucket, check its configuration. For each IAM role, check its policies. For each EC2 instance, check its security group.

A ghost reference finding lives in the gap between two inventories: the set of ARNs in IAM policies and the set of resources that actually exist. The finding is the difference between these two sets. No single resource carries it. The bucket doesn't exist to be scanned. The policy exists but looks normal — it has valid JSON, well-formed ARNs, and reasonable permissions. The problem is only visible when you compare the policy's ARNs against the resource inventory and notice an ARN that doesn't resolve.

This is cross-inventory reasoning. The scanner must compare two datasets and notice what's in one but not the other. Per-resource scanners don't do this because their architecture processes one resource at a time. The dog that didn't bark is invisible to any investigator who only examines witnesses who showed up.

The detection requires three inputs:

Input 1: Policy ARN extraction. Parse every Allow statement in every IAM policy (user policies, group policies, role policies, managed and inline). Extract every fully-qualified, non-wildcard ARN. Wildcard ARNs (arn:aws:s3:::prod-*) can't be cross-referenced against the inventory — they match a pattern, not a specific resource.

Input 2: Resource inventory. Every resource the extractor collected: S3 buckets, SQS queues, SNS topics, Lambda functions, KMS keys, DynamoDB tables. Each with its ARN.

Input 3: Cross-reference. For every ARN in a policy, check whether a resource with that ARN exists in the inventory. If it doesn't, the policy references a ghost.

The finding output tells the operator what they need to act:

Finding: CTL.IAM.POLICY.GHOSTREF.002 [CRITICAL]

  DEFECT:
    IAM policy "AuditLogWriter" grants s3:PutObject
    to arn:aws:s3:::prod-audit-logs which does not
    exist in the resource inventory. The bucket name
    is globally reclaimable.

  INFECTION:
    The Lambda function "WriteAuditLogs" executes
    hourly with this policy's permissions. It calls
    PutObject on prod-audit-logs. If an attacker
    registers this bucket name, the function's
    writes succeed — to the attacker's bucket. The
    function sees no errors. The data delivery
    appears normal.

  FAILURE:
    Silent data exfiltration. Audit logs containing
    PHI are delivered to an attacker-controlled S3
    bucket. The organization continues generating
    compliance evidence and delivering it to an
    adversary.

  DELTA:
    Remove arn:aws:s3:::prod-audit-logs from the
    AuditLogWriter policy, or recreate the bucket
    and verify ownership.

The operator reads this and understands: the policy is pointing at a bucket that doesn't exist, the bucket name can be claimed by anyone, and an active Lambda function is trying to write to it right now. The fix is immediate: either remove the dangling reference from the policy or recreate the bucket.

The ghost reference alone is dangerous. Combined with missing logging, it's invisible.

If CloudTrail data-write logging is enabled, the PutObject calls to the ghost bucket are logged — even when they fail. A security team reviewing CloudTrail can see "PutObject to prod-audit-logs failed with NoSuchBucket" and investigate. The ghost reference is discoverable through log analysis, even without the cross-inventory detection.

But if data-write logging is also disabled, the PutObject calls generate no log entries. The writes fail silently or succeed to an attacker's bucket with no observable signal. The ghost reference is invisible to the scanner AND invisible in the logs.

When the ghost reference finding co-occurs with missing write logging, the compound risk is total: the exfiltration path is open and there is no forensic trail to detect it. This is the compound chain — two independent findings that together produce a risk neither captures alone.

Ghost references aren't created by malice. They are created by mundane operational workflows:

Team provisions an S3 bucket for audit logs
IAM policy is written granting Lambda write access to the bucket
Lambda function runs for months, writing logs
Team migrates logging to a new architecture — new bucket name, new function
Old bucket is deleted
Old Lambda function is deleted
Old IAM policy is... still there

Step 7 is the failure. Steps 1-6 are normal operations. The migration was successful. The new architecture works. Nobody noticed that the old policy still exists because the old policy isn't attached to anything that's actively used — or is it? Maybe a different Lambda function in a different team's account inherited the old policy through a role that was shared. Maybe a CI/CD pipeline still references the old role. Maybe the policy is attached to a group that 40 developers belong to.

The gap between resource deleted and policy updated grows with organizational complexity. In small teams, one person manages both the resource and the policy. In large organizations, different teams manage infrastructure, IAM, and applications. The resource owner deletes the resource. The IAM team doesn't know the resource was deleted. The policy persists.

Over months and years, the ghost reference count grows. Each one is a structural hole. Most are dormant. The resource type isn't globally reclaimable, or no active system references the ghost. But the write-permission ghosts pointing at reclaimable S3 bucket names are live exfiltration paths waiting for someone to notice.

Holmes didn't just notice the dog didn't bark. He deduced why it didn't bark and that deduction solved the case. The absence wasn't just a curiosity. It was the key evidence that every other investigator missed because they were looking at what was present.

Ghost resource detection works the same way. The absence of a resource behind an active IAM permission isn't a cleanup task. It's evidence of a structural security gap that no amount of per-resource scanning will find. The policy looks correct. The permissions are well-scoped. The JSON is valid. Everything present is fine. What's missing is the problem.

Every scanner on the market examines what's there. The most dangerous findings are in what isn't.

Ghost resource detection — cross-inventory reasoning about IAM policies referencing non-existent resources — is implemented in Stave, an open-source security CLI. Three controls detect dangling ARN references at escalating severity: general ghost references, write-permission exfiltration paths, and orphaned KMS key references. The finding lives in the gap between two inventories. No single resource carries it.

DEV Community: Bala Paranj

Visual Regression Testing for CLIs with VHS

Using VHS

How This Differs from Asciinema

Visual Regression Testing Pattern

Step 1: Create a .tape file per workflow

Step 2: Generate the baseline

Step 3: Compare in CI

Step 4: Review with PR comments

What Visual Tests Catch That Unit Tests Miss

Table alignment

Color and formatting

Progress indicators

Help text layout

VHS .tape Cheat Sheet

Combining Both Tools

Getting Started

Z3 Can Prove Your Cloud is Unsafe. It Can't Tell You Why.

What Z3 outputs

The two translation boundaries

What an orchestration layer provides

1. Encoding explanation — "Did the tool understand my configuration?"

2. Human verdict — "What does the result mean?"

3. Fix guidance — "What do I do about it?"

4. Traceability — "Which property caused this?"

5. Encoding verification — "Can I trust the translation?"

What you get without orchestration vs. with it

Why this matters more for compound detection

The bottom line

Proof, not prediction: where formal verification beats AI in cloud security

What is a proof

Proof vs prediction

The cost structure that nobody mentions

Why this matters for insurance and evidence

Where AI genuinely belongs

The foundation-layer architecture

A 130-millisecond demo

What this is not

The structural shift

Zero-cost abstractions in Go: deleting your way to better code

1. Pass-through packages

2. Thin wrapper functions

3. Anemic files

4. Premature generic frameworks

5. Backward-compatibility aliases

6. Dead methods

The cost model

When to delete

The Real Zero Cost Abstraction

The $0 cloud infrastructure security stack

Inspired by a $0 stack

The infrastructure security pipeline

What scanners check vs. what Stave verifies

What 2,650 controls cover

Nine engines, one fact export

Where this fits in a security program

Setting it up

What you get for $0

Infrastructure security doesn't have to cost anything

Your Go Golden Tests Don't Need to Regenerate Everything

The problem with regenerate everything

Two kinds of golden tests

The in-process pattern: UPDATE_GOLDEN env var

Why an env var instead of a flag

Why writeIfChanged matters

The e2e pattern: wrap what already exists

The full Makefile surface

What I didn't do

The verification that matters

Results

9 Go Performance Patterns That Don't Need a Profiler to Find

1. Pre-Allocate Slices and Maps

The Cost of Growth

The Fix

Where to Apply

2. Index-Based Iteration for Large Structs

The Cost of Range-Value Copy

The Fix

When It Matters

3. Switch Over Map for Hot-Path Dispatch

Step 1: Create a `.tape` file per workflow

VHS `.tape` Cheat Sheet