diff --git a/DESIGN.md b/DESIGN.md
index 82101ef..c988d5c 100644
--- a/DESIGN.md
+++ b/DESIGN.md
@@ -630,6 +630,68 @@ parent receipt digest is its own backlog item; until it ships, signed
receipts are authenticated individual records, and the docs do not use
the word "chain" for them).
+### Verified adversarially (schema 0.0.14 → hardening)
+
+After signing merged, the same reviewer attacked the implementation with
+live fixtures and confirmed NINE holes — every one reproduced, not
+argued. All nine are closed with regression tests; the highest-value one
+was not on the signing path at all:
+
+1. **Case-variant intake key (CRITICAL, live path).** The strict decoder
+ rejected exact-duplicate keys, but `encoding/json` matches struct
+ fields case-INsensitively and lets a later key win — so a row carrying
+ both `"outcome": "counterexample"` and `"Outcome": "verified"` decoded
+ to a pass, laundering a counterexample away and defeating refutation
+ dominance at the external boundary. This hit every intake run, signed
+ or not. The decoder now rejects any two keys in one object that are
+ equal under case folding but not byte-equal — honest producers never
+ emit such a pair, so the cost is zero.
+2. **Head-only gate accepted the wrong diff (HIGH).** One head commit has
+ many possible diffs (different bases, a dirty tree). `verify -gate`
+ now requires `-base`, so a signed receipt for an empty diff at the
+ same head cannot stand in for the real change.
+3. **Evidence could verify a different claim (HIGH).** The consistency
+ check re-derived the summary but never tied an evidence row to the
+ claim it sat under, so a claim could be renamed to `AUTH-999 / All
+ privileged operations reject unauthenticated callers` while keeping
+ evidence from an unrelated test. Validation now requires every
+ evidence row's `claim_id` to match its claim, and the coverage file
+ set to equal the change file set (the measured scope and the stated
+ scope must be the same).
+4. **Negative intake count slipped the required-supplier gate (HIGH).**
+ `GateBlocked` checked `Accepted == 0`; a forged `-1` read as "usable
+ evidence arrived". The gate now blocks on `Accepted < 1`, and
+ validation rejects negative counts before they reach it.
+5. **Renderers injected terminal and Markdown control (MEDIUM).** A
+ crafted `base_ref` carried an ESC clear-screen and a `## Forged gate
+ pass` heading into the text and Markdown output. Both renderers now
+ scrub every string field of control runes (one place, `scrubForDisplay`)
+ and strip Markdown-structural characters from code spans and cells, so
+ a rendering cannot fake authority — and the rendering still states it
+ is not itself signed.
+6. **Cross-parser integer differential (MEDIUM).** An `int` field above
+ 2⁵³ canonicalized and verified but read back as a different value in a
+ double-based parser. Counts are now bounded to the exact-integer range
+ every JSON parser shares.
+7. **Invalid tiers were signable (MEDIUM).** A tier of 99 weighed to
+ "verified" because the check was only `Tier > T0`. Tiers are now
+ validated in `T0..T4` before weighing.
+8. **Audience admitted C1 controls (LOW).** The control-free rule checked
+ ASCII only; it now uses `unicode.IsControl`, so the documented
+ guarantee is true.
+9. **Keygen followed a symlinked parent directory (LOW).** `O_NOFOLLOW`
+ protected the filenames but not the `-out` directory. Keygen now opens
+ the directory with `O_NOFOLLOW` and creates both files relative to
+ that descriptor (`openat`), so neither the directory nor a filename
+ can be redirected by a symlink.
+
+The lesson threading 1, 3, 4, 6, and 7 together: a signature
+authenticates bytes, and byte-authenticity is worthless if the bytes are
+internally incoherent. The consistency validator is therefore the load-
+bearing companion to the signature, and it must re-derive and range-check
+every field a reader or a gate trusts — not just the summary arithmetic
+the first pass covered.
+
## Known limitations (found by dogfooding, stated honestly)
correctful was run on itself and on a real 101-file production change on its
diff --git a/README.md b/README.md
index 01beb5a..eff20c7 100644
--- a/README.md
+++ b/README.md
@@ -233,16 +233,20 @@ correctful sign -receipt receipt.json -key /ci/keys/correctful.key \
# Step 3 — verify, in a protected workflow the change cannot edit.
correctful verify -receipt receipt.signed.json -pub /ci/keys/correctful.pub \
- -head "$GITHUB_SHA" -audience github.com/org/repo -gate
+ -head "$GITHUB_SHA" -base "$MERGE_BASE" -audience github.com/org/repo -gate
```
The rules:
- The main command has no signing flag. A process that runs reviewed test
code must never hold the signing key.
-- `verify` needs the expected head SHA. A signature alone proves that SOME
- receipt is authentic. The subject match ties it to THIS change. Pass
- `-any-subject` only when you check an archived receipt.
+- A merge gate must pin the exact change, not just its head. One head
+ commit has many possible diffs — different bases, or a dirty working
+ tree — so `-gate` requires `-base` as well (CI knows the merge base).
+ For a mid-branch or dirty tree, add `-input-digest` for the strongest
+ pin. A signature alone proves that SOME receipt is authentic; the
+ subject match ties it to THIS change. Pass `-any-subject` to gate on
+ authenticity only (an archived receipt).
- The trusted key comes from your `-pub` file, never from the receipt. The
key inside the receipt is an identity claim, and `verify` requires it to
match your pinned key.
diff --git a/cmd/correctful/subcommands.go b/cmd/correctful/subcommands.go
index 3c9fd5c..7dd4dde 100644
--- a/cmd/correctful/subcommands.go
+++ b/cmd/correctful/subcommands.go
@@ -97,6 +97,15 @@ func cmdVerify(args []string) error {
if *in == "" || *pubPath == "" {
return fmt.Errorf("need -receipt and -pub")
}
+ // A merge gate must pin the exact change, not just its head commit: one
+ // head commit has many possible diffs (different bases, dirty overlays),
+ // and a valid signature over SOME receipt at that head is not a valid
+ // receipt for THIS change. So when -gate is set, require the base SHA
+ // too (CI knows it — the merge base / $GITHUB_BASE_REF). -input-digest
+ // is the strongest additional pin for a mid-branch or dirty tree.
+ if *gate && !*anySubject && *base == "" {
+ return fmt.Errorf("-gate requires -base (the head commit alone does not identify the exact diff); pass the merge base, or -any-subject to gate on authenticity only")
+ }
data, err := readArtifact(*in)
if err != nil {
diff --git a/internal/intake/hardening_test.go b/internal/intake/hardening_test.go
index 2ca2af0..d85aa6b 100644
--- a/internal/intake/hardening_test.go
+++ b/internal/intake/hardening_test.go
@@ -204,3 +204,25 @@ func TestRejectedRowsAreScrubbed(t *testing.T) {
t.Error("config digest absent — the authority file is unpinned")
}
}
+
+// TestCaseVariantOutcomeKeyRejected: the CRITICAL live-path hole. An intake
+// row carrying both "outcome" and "Outcome" passed exact-match duplicate
+// detection, and Go's case-insensitive field matching then read the second
+// one — turning a counterexample into a pass and defeating refutation
+// dominance at the external boundary. The strict decoder now rejects the
+// case-fold collision, so the whole document fails loudly.
+func TestCaseVariantOutcomeKeyRejected(t *testing.T) {
+ repo := t.TempDir()
+ outside := t.TempDir()
+ rows := `{"claim_id": "INV-009", "probe_id": "p", "outcome": "counterexample", "Outcome": "verified"}`
+ docPath := write(t, outside, "doc.json", docFor("dafny-worker", "abc", goodDigest, rows))
+ cfgPath := write(t, outside, "cfg.json", configFor(docPath, false))
+ cfg, err := LoadConfig(cfgPath, repo)
+ if err != nil {
+ t.Fatal(err)
+ }
+ _, _, err = Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims())
+ if err == nil || !strings.Contains(err.Error(), "case-variant key collision") {
+ t.Errorf("case-variant outcome key tolerated: %v", err)
+ }
+}
diff --git a/internal/receipt/markdown.go b/internal/receipt/markdown.go
index 9a6cc78..bea3244 100644
--- a/internal/receipt/markdown.go
+++ b/internal/receipt/markdown.go
@@ -21,6 +21,7 @@ const MarkdownMarker = ""
// (it is the part reviewers already trust), and coverage closes the comment so
// "all verified" can never be read apart from "out of how much".
func WriteMarkdown(w io.Writer, r schema.Receipt) {
+ r = scrubForDisplay(r)
s := r.Summary
fmt.Fprintln(w, MarkdownMarker)
fmt.Fprintf(w, "## correctful receipt\n\n")
@@ -30,13 +31,13 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) {
fmt.Fprintf(w, "Anchoring: %d of %d spec-id claims resolved to definitions · %d ambiguous · %d orphan\n\n",
a.Resolved, a.SpecIDClaims, a.Ambiguous, a.Orphan)
}
- fmt.Fprintf(w, "Change: `%s...%s`%s — %d files\n", r.Change.BaseRef, r.Change.HeadRef,
+ fmt.Fprintf(w, "Change: `%s...%s`%s — %d files\n", mdCell(r.Change.BaseRef), mdCell(r.Change.HeadRef),
mdCell(shaNote(r.Change)), len(r.Change.Files))
if note := exclusionNote(r.Change.Excluded); note != "" {
fmt.Fprintf(w, "%s\n", note)
}
if p := r.Policy; p != nil {
- fmt.Fprintf(w, "policy: `%s` · %s · %d rule(s)%s\n", p.Path, short(p.Digest), p.Rules, exemptNote(p))
+ fmt.Fprintf(w, "policy: `%s` · %s · %d rule(s)%s\n", mdCell(p.Path), short(p.Digest), p.Rules, exemptNote(p))
}
for _, rec := range r.Intake {
fmt.Fprintf(w, "intake: %s\n", mdCell(intakeLine(rec)))
@@ -80,7 +81,7 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) {
for _, res := range r.Remainder {
fmt.Fprintf(w, "| `%s` | %s | `%s:%d` |\n",
mdCell(res.Claim.ID), mdCell(res.Claim.Text+anchorNote(res.Claim)+llmNote(res.Claim)+llmEdgeNote(res)),
- res.Claim.Source.File, res.Claim.Source.Line)
+ mdCell(res.Claim.Source.File), res.Claim.Source.Line)
}
}
fmt.Fprintln(w)
@@ -118,8 +119,14 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) {
fmt.Fprintf(w, "\nschema %s%s · exit gate: %s; the remainder informs, never fails\n", r.SchemaVersion, toolNote(r), gateLegs(r))
}
-// mdCell makes text safe inside a markdown table cell.
+// mdCell makes text safe inside a markdown table cell OR a code span: a
+// pipe is escaped so it cannot start a new cell, a backtick is removed so a
+// value rendered inside `...` cannot break out and inject markup, and any
+// residual newline collapses to a space. Control runes are already gone
+// (scrubForDisplay runs first), so this handles only the structural
+// characters that survive as printable text.
func mdCell(s string) string {
+ s = strings.ReplaceAll(s, "`", "")
s = strings.ReplaceAll(s, "|", `\|`)
return strings.ReplaceAll(s, "\n", " ")
}
diff --git a/internal/receipt/receipt.go b/internal/receipt/receipt.go
index c8bcba6..6a3d83e 100644
--- a/internal/receipt/receipt.go
+++ b/internal/receipt/receipt.go
@@ -454,6 +454,7 @@ func WriteJSON(w io.Writer, r schema.Receipt) error {
// its own section because it is the part a reader most needs to see and the part
// every other tool hides.
func WriteText(w io.Writer, r schema.Receipt) {
+ r = scrubForDisplay(r)
s := r.Summary
fmt.Fprintf(w, "correctful receipt (schema %s%s)\n", r.SchemaVersion, toolNote(r))
fmt.Fprintf(w, "change: %s...%s%s", r.Change.BaseRef, r.Change.HeadRef, shaNote(r.Change))
diff --git a/internal/receipt/scrub.go b/internal/receipt/scrub.go
new file mode 100644
index 0000000..1699b7d
--- /dev/null
+++ b/internal/receipt/scrub.go
@@ -0,0 +1,190 @@
+package receipt
+
+import (
+ "strings"
+ "unicode"
+
+ "github.com/joshft/correctful/schema"
+)
+
+// clean strips every control rune from a display string: ESC (terminal
+// escape injection), CR/LF (breaking out of a markdown code span or table
+// cell to inject a heading), and the DEL/C1 range. A receipt rendered to a
+// terminal or a PR comment is UNTRUSTED — render does not verify, and even
+// a verified receipt carries attacker-authored claim text — so no field may
+// carry an active control sequence into the reader's terminal or a
+// structural break into the Markdown. Legitimate fields are single-line
+// printable text, so dropping controls is lossless for honest receipts.
+func clean(s string) string {
+ return strings.Map(func(r rune) rune {
+ if unicode.IsControl(r) {
+ return -1
+ }
+ return r
+ }, s)
+}
+
+// scrubForDisplay returns a copy of the receipt with every string field
+// control-stripped. Both renderers call it first, so the control-injection
+// defense lives in ONE place and cannot be bypassed by a print site that
+// forgets to wrap a field. Digests and base64 are cleaned too even though
+// they are already constrained shapes — a hostile receipt is not obligated
+// to honor them, and cleaning costs nothing.
+func scrubForDisplay(r schema.Receipt) schema.Receipt {
+ r.Change = scrubChange(r.Change)
+ r.Results = scrubResults(r.Results)
+ r.Remainder = scrubResults(r.Remainder)
+ r.Coverage = scrubCoverage(r.Coverage)
+ if r.Policy != nil {
+ p := *r.Policy
+ p.Path = clean(p.Path)
+ p.Digest = clean(p.Digest)
+ misses := make([]schema.PolicyMiss, len(p.Misses))
+ for i, m := range p.Misses {
+ misses[i] = schema.PolicyMiss{File: clean(m.File), Rule: clean(m.Rule), Detail: clean(m.Detail)}
+ }
+ p.Misses = misses
+ r.Policy = &p
+ }
+ if len(r.Intake) > 0 {
+ intake := make([]schema.IntakeRecord, len(r.Intake))
+ for i, rec := range r.Intake {
+ rec.Supplier = clean(rec.Supplier)
+ rec.SupplierVersion = clean(rec.SupplierVersion)
+ rec.ConfigDigest = clean(rec.ConfigDigest)
+ rec.Mechanism = clean(rec.Mechanism)
+ rec.Reason = clean(rec.Reason)
+ rec.DocDigest = clean(rec.DocDigest)
+ rej := make([]schema.IntakeRejection, len(rec.Rejected))
+ for j, x := range rec.Rejected {
+ rej[j] = schema.IntakeRejection{
+ ClaimID: clean(x.ClaimID), ProbeID: clean(x.ProbeID),
+ Outcome: clean(x.Outcome), Reason: clean(x.Reason),
+ }
+ }
+ rec.Rejected = rej
+ intake[i] = rec
+ }
+ r.Intake = intake
+ }
+ if r.Signature != nil {
+ b := *r.Signature
+ b.Alg = clean(b.Alg)
+ b.PublicKey = clean(b.PublicKey)
+ b.Audience = clean(b.Audience)
+ b.Sig = clean(b.Sig)
+ r.Signature = &b
+ }
+ r.ToolVersion = clean(r.ToolVersion)
+ r.SchemaVersion = clean(r.SchemaVersion)
+ return r
+}
+
+func scrubChange(c schema.ChangeRef) schema.ChangeRef {
+ c.Repo = clean(c.Repo)
+ c.BaseRef = clean(c.BaseRef)
+ c.HeadRef = clean(c.HeadRef)
+ c.BaseSHA = clean(c.BaseSHA)
+ c.HeadSHA = clean(c.HeadSHA)
+ c.InputDigest = clean(c.InputDigest)
+ c.Files = cleanSlice(c.Files)
+ if len(c.Excluded) > 0 {
+ ex := make([]schema.Exclusion, len(c.Excluded))
+ for i, e := range c.Excluded {
+ ex[i] = schema.Exclusion{Reason: clean(e.Reason), Count: e.Count, Dirs: cleanSlice(e.Dirs)}
+ }
+ c.Excluded = ex
+ }
+ return c
+}
+
+func scrubResults(rs []schema.ClaimResult) []schema.ClaimResult {
+ if len(rs) == 0 {
+ return rs
+ }
+ out := make([]schema.ClaimResult, len(rs))
+ for i, res := range rs {
+ res.Claim = scrubClaim(res.Claim)
+ res.Evidence = scrubEvidence(res.Evidence)
+ out[i] = res
+ }
+ return out
+}
+
+func scrubClaim(c schema.Claim) schema.Claim {
+ c.ID = clean(c.ID)
+ c.Text = clean(c.Text)
+ c.Source = scrubSource(c.Source)
+ c.ProbeIDs = cleanSlice(c.ProbeIDs)
+ if c.Anchor != nil {
+ a := *c.Anchor
+ a.Title = clean(a.Title)
+ a.Sites = scrubSources(a.Sites)
+ c.Anchor = &a
+ }
+ c.RefSites = scrubSources(c.RefSites)
+ return c
+}
+
+func scrubSource(s schema.Source) schema.Source {
+ s.File = clean(s.File)
+ s.Ref = clean(s.Ref)
+ return s
+}
+
+func scrubSources(ss []schema.Source) []schema.Source {
+ if len(ss) == 0 {
+ return ss
+ }
+ out := make([]schema.Source, len(ss))
+ for i, s := range ss {
+ out[i] = scrubSource(s)
+ }
+ return out
+}
+
+func scrubEvidence(es []schema.Evidence) []schema.Evidence {
+ if len(es) == 0 {
+ return es
+ }
+ out := make([]schema.Evidence, len(es))
+ for i, e := range es {
+ e.ClaimID = clean(e.ClaimID)
+ e.ProbeID = clean(e.ProbeID)
+ e.Detail = clean(e.Detail)
+ e.Duration = clean(e.Duration)
+ e.Binding = clean(e.Binding)
+ e.Mechanism = clean(e.Mechanism)
+ e.Scope = clean(e.Scope)
+ e.Environment = clean(e.Environment)
+ e.Supplier = clean(e.Supplier)
+ out[i] = e
+ }
+ return out
+}
+
+func scrubCoverage(c schema.Coverage) schema.Coverage {
+ if len(c.Files) == 0 {
+ return c
+ }
+ files := make([]schema.FileCoverage, len(c.Files))
+ for i, fc := range c.Files {
+ fc.File = clean(fc.File)
+ fc.ReadBy = cleanSlice(fc.ReadBy)
+ fc.SkipReason = clean(fc.SkipReason)
+ files[i] = fc
+ }
+ c.Files = files
+ return c
+}
+
+func cleanSlice(in []string) []string {
+ if len(in) == 0 {
+ return in
+ }
+ out := make([]string, len(in))
+ for i, s := range in {
+ out[i] = clean(s)
+ }
+ return out
+}
diff --git a/internal/receipt/scrub_test.go b/internal/receipt/scrub_test.go
new file mode 100644
index 0000000..496c76a
--- /dev/null
+++ b/internal/receipt/scrub_test.go
@@ -0,0 +1,88 @@
+package receipt
+
+import (
+ "strings"
+ "testing"
+ "unicode"
+
+ "github.com/joshft/correctful/internal/gitdiff"
+ "github.com/joshft/correctful/schema"
+)
+
+// hostileReceipt seeds every renderer-visible string with a terminal escape
+// and a Markdown-structural break: an ESC + clear-screen, newlines, a
+// heading, a code-span-breaking backtick, and a table-breaking pipe.
+func hostileReceipt() schema.Receipt {
+ bad := "\x1b[2J\n\n## Forged gate pass\n`backtick`|pipe"
+ claims := []schema.Claim{{
+ ID: "A1" + bad, Shape: schema.ShapeAssertion, Text: "text" + bad,
+ Source: schema.Source{File: "f.go" + bad, Line: 1, Ref: "r" + bad},
+ ProbeIDs: []string{"p" + bad},
+ }, {
+ ID: "A2" + bad, Shape: schema.ShapeAssertion, Text: "unverified" + bad,
+ Source: schema.Source{File: "g.go" + bad},
+ }}
+ evidence := [][]schema.Evidence{
+ {{ClaimID: claims[0].ID, ProbeID: "px" + bad, Tier: schema.T1Assertion, Ran: true, Passed: true, Detail: "d" + bad, Mechanism: "m" + bad}},
+ {{ClaimID: claims[1].ID, Ran: false}},
+ }
+ cov := schema.Coverage{
+ Files: []schema.FileCoverage{{File: "f.go" + bad, ReadBy: []string{"h" + bad}, Claims: 1}, {File: "g.go" + bad, ReadBy: []string{"h"}}},
+ Claimed: 1, Scanned: 1,
+ }
+ r := Assemble(gitdiff.Change{
+ Repo: "repo" + bad, BaseRef: "base" + bad, HeadRef: "head" + bad,
+ Files: []string{"f.go" + bad, "g.go" + bad},
+ }, claims, evidence, cov)
+ r.ToolVersion = "v" + bad
+ r.Policy = &schema.PolicyResult{
+ Path: "correctful.json" + bad, Digest: strings.Repeat("a", 64), Rules: 1,
+ Misses: []schema.PolicyMiss{{File: "f.go" + bad, Rule: "rule" + bad, Detail: "detail" + bad}},
+ }
+ r.Intake = []schema.IntakeRecord{{
+ Supplier: "s" + bad, Mechanism: "proof" + bad, MaxTier: schema.T4Mechanical, Admitted: true, Accepted: 1,
+ Rejected: []schema.IntakeRejection{{ClaimID: "c" + bad, ProbeID: "p" + bad, Outcome: "error" + bad, Reason: "why" + bad}},
+ }}
+ r.Signature = &schema.SignatureBlock{Alg: "ed25519", PublicKey: "k" + bad, Audience: "aud" + bad, Sig: "sig" + bad}
+ return r
+}
+
+// TestRenderersStripControlRunes: neither renderer may emit a control rune,
+// no matter what a hostile receipt carries. A rendering reaches a terminal
+// or a PR comment, and render does not verify its input.
+func TestRenderersStripControlRunes(t *testing.T) {
+ for _, tc := range []struct {
+ name string
+ render func() string
+ }{
+ {"text", func() string { var b strings.Builder; WriteText(&b, hostileReceipt()); return b.String() }},
+ {"markdown", func() string { var b strings.Builder; WriteMarkdown(&b, hostileReceipt()); return b.String() }},
+ } {
+ out := tc.render()
+ for i, r := range out {
+ // The renderers emit newlines for their own structure; those
+ // are the only control runes allowed, and only because they
+ // come from the renderer, never from a field (fields have
+ // their newlines stripped).
+ if r == '\n' {
+ continue
+ }
+ if unicode.IsControl(r) {
+ t.Fatalf("%s: control rune %#U at offset %d", tc.name, r, i)
+ }
+ }
+ }
+}
+
+// TestMarkdownRejectsInjectedHeading: the forged "## Forged gate pass"
+// heading must never appear at the start of a line — that is how a pasted
+// receipt would fake an authoritative section.
+func TestMarkdownRejectsInjectedHeading(t *testing.T) {
+ var b strings.Builder
+ WriteMarkdown(&b, hostileReceipt())
+ for _, line := range strings.Split(b.String(), "\n") {
+ if strings.HasPrefix(strings.TrimSpace(line), "## Forged") {
+ t.Fatalf("injected heading reached a line start: %q", line)
+ }
+ }
+}
diff --git a/internal/receipt/validate.go b/internal/receipt/validate.go
index b7c7934..4a07186 100644
--- a/internal/receipt/validate.go
+++ b/internal/receipt/validate.go
@@ -4,12 +4,24 @@ import (
"fmt"
"reflect"
"regexp"
+ "sort"
"github.com/joshft/correctful/schema"
)
var hexDigestRe = regexp.MustCompile(`^[0-9a-f]{64}$`)
+// maxSafeInt is 2^53 − 1, the largest integer an IEEE-754 double represents
+// exactly. Receipt counts are bounded to it so a JavaScript (or any
+// double-based) consumer reads the same integer this tool signed — a value
+// above it is a cross-parser differential, demonstrated with policy.rules =
+// 9007199254740993 reading back as ...992.
+const maxSafeInt = 1<<53 - 1
+
+// inRange reports whether n is a sane non-negative count within the
+// exact-integer range every conforming JSON parser shares.
+func inRange(n int) bool { return n >= 0 && n <= maxSafeInt }
+
// ValidateConsistency recomputes every locally derivable field of a receipt
// and rejects any mismatch. The signer runs it before signing and the
// verifier after signature checking, because a signature authenticates
@@ -33,6 +45,20 @@ func ValidateConsistency(r schema.Receipt) error {
claims := make([]schema.Claim, 0, len(r.Results))
var remainder []schema.ClaimResult
for i, res := range r.Results {
+ // Validate the evidence BEFORE weighing it: weigh treats any Tier
+ // > T0 as verifying strength, so an out-of-range tier (99) would
+ // otherwise weigh to a "verified" result at tier 99 that matches
+ // its own inflated stated tier and passes. And a row must carry
+ // the id of the claim it sits under — evidence for TestX must not
+ // be presented as proof of a renamed AUTH-999 claim.
+ for j, e := range res.Evidence {
+ if e.Tier < schema.T0Unverified || e.Tier > schema.T4Mechanical {
+ return fmt.Errorf("result %d (%s) evidence %d: tier %d is outside T0..T4", i, res.Claim.ID, j, e.Tier)
+ }
+ if e.ClaimID != res.Claim.ID {
+ return fmt.Errorf("result %d (%s) evidence %d: claim_id %q does not match its claim", i, res.Claim.ID, j, e.ClaimID)
+ }
+ }
status, tier := weigh(res.Claim, res.Evidence)
if res.Status != status || res.EffectiveTier != tier {
return fmt.Errorf("result %d (%s): stated %s/%s, evidence weighs to %s/%s", i, res.Claim.ID, res.Status, res.EffectiveTier, status, tier)
@@ -71,7 +97,7 @@ func ValidateConsistency(r schema.Receipt) error {
return fmt.Errorf("anchoring summary does not match the claims it summarizes")
}
- if err := validateCoverage(r.Coverage); err != nil {
+ if err := validateCoverage(r.Coverage, r.Change.Files); err != nil {
return err
}
@@ -79,6 +105,9 @@ func ValidateConsistency(r schema.Receipt) error {
if !hexDigestRe.MatchString(p.Digest) {
return fmt.Errorf("policy digest %q is not a sha256 hex digest", p.Digest)
}
+ if !inRange(p.Rules) || !inRange(p.ExemptTestFiles) {
+ return fmt.Errorf("policy counts out of range")
+ }
for _, m := range p.Misses {
if m.File == "" || m.Rule == "" {
return fmt.Errorf("policy miss with empty file or rule")
@@ -90,18 +119,41 @@ func ValidateConsistency(r schema.Receipt) error {
if rec.MaxTier < schema.T1Assertion || rec.MaxTier > schema.T4Mechanical {
return fmt.Errorf("intake %q states max tier %d outside 1..4", rec.Supplier, rec.MaxTier)
}
+ // The accepted count must be a sane non-negative integer. A
+ // negative value slipped the required-supplier gate: GateBlocked
+ // now blocks on Accepted <= 0, but the value must also never reach
+ // that check malformed.
+ if !inRange(rec.Accepted) {
+ return fmt.Errorf("intake %q states an out-of-range accepted count %d", rec.Supplier, rec.Accepted)
+ }
if !rec.Admitted && rec.Accepted != 0 {
return fmt.Errorf("intake %q accepted %d rows from a document it did not admit", rec.Supplier, rec.Accepted)
}
}
+
+ if !inRange(r.Coverage.SuppressedMentions) {
+ return fmt.Errorf("coverage suppressed-mentions count out of range")
+ }
+ if a := r.Summary.Anchoring; a != nil {
+ if !inRange(a.SpecIDClaims) || !inRange(a.Resolved) || !inRange(a.Ambiguous) || !inRange(a.Orphan) {
+ return fmt.Errorf("anchoring counts out of range")
+ }
+ }
return nil
}
// validateCoverage re-derives the coverage arithmetic from its own file
-// rows. SuppressedMentions is set outside the tally and is not derivable.
-func validateCoverage(c schema.Coverage) error {
+// rows AND ties the coverage rows to the change's file set: the harvest
+// produces exactly one row per changed file, so a receipt that claims N
+// changed files while its coverage accounts for a different set is
+// internally inconsistent — the scope a reader trusts and the scope the
+// harvest measured must be the same. SuppressedMentions is set outside the
+// tally and is not derivable here (its range is checked by the caller).
+func validateCoverage(c schema.Coverage, changeFiles []string) error {
var claimed, scanned, unread, unreadPolicy int
+ covFiles := make([]string, 0, len(c.Files))
for _, fc := range c.Files {
+ covFiles = append(covFiles, fc.File)
switch {
case fc.Claims > 0:
claimed++
@@ -118,5 +170,11 @@ func validateCoverage(c schema.Coverage) error {
return fmt.Errorf("coverage arithmetic (%d/%d/%d/%d) does not match its file rows (%d/%d/%d/%d)",
c.Claimed, c.Scanned, c.Unread, c.UnreadPolicy, claimed, scanned, unread, unreadPolicy)
}
+ change := append([]string(nil), changeFiles...)
+ sort.Strings(change)
+ sort.Strings(covFiles)
+ if !reflect.DeepEqual(change, covFiles) {
+ return fmt.Errorf("coverage accounts for %d files but the change lists %d — the measured scope and the stated scope differ", len(covFiles), len(change))
+ }
return nil
}
diff --git a/internal/receipt/validate_test.go b/internal/receipt/validate_test.go
index f2eb0c9..0adb50f 100644
--- a/internal/receipt/validate_test.go
+++ b/internal/receipt/validate_test.go
@@ -24,7 +24,10 @@ func consistentReceipt(t *testing.T) schema.Receipt {
Unread: 2,
UnreadPolicy: 1,
}
- r := Assemble(gitdiff.Change{Repo: "repo", BaseRef: "main", HeadRef: "wip"}, claims, evidence, cov)
+ r := Assemble(gitdiff.Change{
+ Repo: "repo", BaseRef: "main", HeadRef: "wip",
+ Files: []string{"x.go", "y.go", "z.bin", ".ci/tool.cfg"},
+ }, claims, evidence, cov)
r.ToolVersion = "test"
return r
}
@@ -62,6 +65,19 @@ func TestValidateConsistencyRejectsTampering(t *testing.T) {
{"intake accepted without admission", func(r *schema.Receipt) {
r.Intake = []schema.IntakeRecord{{Supplier: "s", MaxTier: schema.T3Property, Accepted: 2}}
}, "did not admit"},
+ {"evidence for a renamed claim", func(r *schema.Receipt) { r.Results[0].Claim.ID = "AUTH-999" }, "does not match its claim"},
+ {"out-of-range evidence tier", func(r *schema.Receipt) {
+ r.Results[0].Evidence[0].Tier = 99
+ r.Results[0].EffectiveTier = 99
+ r.Summary.TierCounts = map[string]int{"T?-invalid": 1, "T1-assertion": 1}
+ }, "outside T0..T4"},
+ {"coverage scope differs from change", func(r *schema.Receipt) { r.Change.Files = append(r.Change.Files, "phantom.go") }, "measured scope"},
+ {"negative intake accepted", func(r *schema.Receipt) {
+ r.Intake = []schema.IntakeRecord{{Supplier: "s", MaxTier: schema.T3Property, Required: true, Admitted: true, Accepted: -1}}
+ }, "out-of-range accepted"},
+ {"unsafe integer count", func(r *schema.Receipt) {
+ r.Policy = &schema.PolicyResult{Path: "correctful.json", Digest: strings.Repeat("a", 64), Rules: 1<<53 + 1}
+ }, "policy counts out of range"},
}
for _, c := range cases {
r := consistentReceipt(t)
@@ -87,7 +103,7 @@ func TestCanonicalGoldenVector(t *testing.T) {
if err != nil {
t.Fatal(err)
}
- const want = "f52a70f30f50c45bb5d51401e2d5866d34287600d8a5024aaf42a53976b43297"
+ const want = "eb91a86f71c3aaee3f50dcf7380eee0d6e0aa48975310951a76280d6642f41d3"
if got := hex.EncodeToString(sha256sum(b)); got != want {
t.Fatalf("canonical encoding drifted:\n got sha256 %s\nwant sha256 %s\nfirst 200 bytes:\n%s", got, want, b[:200])
}
diff --git a/internal/signing/keys.go b/internal/signing/keys.go
index f5c3364..dd20281 100644
--- a/internal/signing/keys.go
+++ b/internal/signing/keys.go
@@ -17,10 +17,12 @@ import (
const maxKeyFileBytes = 16 << 10
// Keygen mints an Ed25519 keypair into dir as correctful.key (PKCS#8 PEM,
-// 0600) and correctful.pub (PKIX PEM, 0644). Both files are created
-// exclusively — an existing file or a pre-planted symlink at either path
-// fails the whole operation, and a failed public write removes the private
-// file so no partial pair survives.
+// 0600) and correctful.pub (PKIX PEM, 0644). The directory is opened once,
+// with O_NOFOLLOW, and both files are created RELATIVE to that descriptor
+// (openat) — so neither a symlinked output directory nor a pre-planted
+// symlink at either filename can redirect a write outside where the
+// operator pointed. Both files are created exclusively; a failed public
+// write removes the private file so no partial pair survives.
func Keygen(dir string) (privPath, pubPath string, err error) {
pub, priv, err := ed25519.GenerateKey(rand.Reader)
if err != nil {
@@ -37,11 +39,20 @@ func Keygen(dir string) (privPath, pubPath string, err error) {
privPath = filepath.Join(dir, "correctful.key")
pubPath = filepath.Join(dir, "correctful.pub")
- if err := writeExclusive(privPath, pemBytes("PRIVATE KEY", privDER), 0o600); err != nil {
+ // O_NOFOLLOW here rejects a SYMLINKED output directory; O_DIRECTORY
+ // rejects a non-directory.
+ dirFile, err := os.OpenFile(dir, os.O_RDONLY|syscall.O_NOFOLLOW|syscall.O_DIRECTORY, 0)
+ if err != nil {
+ return "", "", fmt.Errorf("opening output directory %s: %w", dir, err)
+ }
+ defer dirFile.Close()
+ dirFD := int(dirFile.Fd())
+
+ if err := writeExclusiveAt(dirFD, "correctful.key", privPath, pemBytes("PRIVATE KEY", privDER), 0o600); err != nil {
return "", "", err
}
- if err := writeExclusive(pubPath, pemBytes("PUBLIC KEY", pubDER), 0o644); err != nil {
- os.Remove(privPath)
+ if err := writeExclusiveAt(dirFD, "correctful.pub", pubPath, pemBytes("PUBLIC KEY", pubDER), 0o644); err != nil {
+ syscall.Unlinkat(dirFD, "correctful.key")
return "", "", err
}
return privPath, pubPath, nil
@@ -51,19 +62,23 @@ func pemBytes(blockType string, der []byte) []byte {
return pem.EncodeToMemory(&pem.Block{Type: blockType, Bytes: der})
}
-func writeExclusive(path string, data []byte, mode os.FileMode) error {
- fh, err := os.OpenFile(path, os.O_WRONLY|os.O_CREATE|os.O_EXCL|syscall.O_NOFOLLOW, mode)
+// writeExclusiveAt creates name inside the directory named by dirFD (openat),
+// exclusively and without following a final-component symlink. label is the
+// full path used only for error messages.
+func writeExclusiveAt(dirFD int, name, label string, data []byte, mode uint32) error {
+ fd, err := syscall.Openat(dirFD, name, syscall.O_WRONLY|syscall.O_CREAT|syscall.O_EXCL|syscall.O_NOFOLLOW, mode)
if err != nil {
- return fmt.Errorf("creating %s: %w", path, err)
+ return fmt.Errorf("creating %s: %w", label, err)
}
+ fh := os.NewFile(uintptr(fd), label)
_, werr := fh.Write(data)
cerr := fh.Close()
if werr != nil {
- os.Remove(path)
+ syscall.Unlinkat(dirFD, name)
return werr
}
if cerr != nil {
- os.Remove(path)
+ syscall.Unlinkat(dirFD, name)
return cerr
}
return nil
diff --git a/internal/signing/keys_test.go b/internal/signing/keys_test.go
index 77e00b1..331d393 100644
--- a/internal/signing/keys_test.go
+++ b/internal/signing/keys_test.go
@@ -148,3 +148,25 @@ func TestLoadKeyRejections(t *testing.T) {
t.Fatalf("private key accepted as public: %v", err)
}
}
+
+// TestKeygenRefusesSymlinkedParentDir: O_NOFOLLOW on the final filename is
+// not enough — a symlinked OUTPUT DIRECTORY would redirect both writes.
+// Keygen opens the directory with O_NOFOLLOW and creates the files relative
+// to that descriptor, so a symlinked -out dir is refused.
+func TestKeygenRefusesSymlinkedParentDir(t *testing.T) {
+ base := t.TempDir()
+ real := filepath.Join(base, "real")
+ if err := os.Mkdir(real, 0o755); err != nil {
+ t.Fatal(err)
+ }
+ link := filepath.Join(base, "link")
+ if err := os.Symlink(real, link); err != nil {
+ t.Fatal(err)
+ }
+ if _, _, err := Keygen(link); err == nil {
+ t.Fatalf("Keygen wrote into a symlinked output directory")
+ }
+ if _, err := os.Lstat(filepath.Join(real, "correctful.key")); !os.IsNotExist(err) {
+ t.Errorf("a key was created through the symlinked directory: %v", err)
+ }
+}
diff --git a/internal/signing/signing.go b/internal/signing/signing.go
index 662f5dc..de837f3 100644
--- a/internal/signing/signing.go
+++ b/internal/signing/signing.go
@@ -23,6 +23,8 @@ import (
"encoding/base64"
"fmt"
"strings"
+ "unicode"
+ "unicode/utf8"
"github.com/joshft/correctful/internal/receipt"
"github.com/joshft/correctful/internal/strictjson"
@@ -180,14 +182,19 @@ func preimage(audience string, payload []byte) []byte {
return out
}
-// checkAudience keeps the preimage unambiguous: a NUL or control byte in
-// the audience could shift the boundary between audience and payload.
+// checkAudience keeps the preimage unambiguous and the "control-free"
+// documentation true: any control rune — ASCII C0, DEL, or the C1 range
+// (0x80–0x9F), which the ASCII-only check used to admit — is refused, so a
+// receipt cannot carry an audience with an invisible or line-breaking rune.
func checkAudience(a string) error {
if len(a) > 200 {
return fmt.Errorf("audience exceeds 200 bytes")
}
+ if !utf8.ValidString(a) {
+ return fmt.Errorf("audience is not valid UTF-8")
+ }
for _, c := range a {
- if c < 0x20 || c == 0x7f {
+ if unicode.IsControl(c) {
return fmt.Errorf("audience contains a control character")
}
}
@@ -215,7 +222,18 @@ func decodeB64(s string, wantLen int, what string) ([]byte, error) {
return raw, nil
}
+// shortKey abbreviates a key for an error message. The value can come from
+// a hostile receipt (Sign's already-signed refusal, Verify's wrong-key
+// error both quote the embedded public_key), so control runes are stripped
+// before it reaches a terminal — an error string must not carry an escape
+// sequence.
func shortKey(b64 string) string {
+ b64 = strings.Map(func(r rune) rune {
+ if unicode.IsControl(r) {
+ return -1
+ }
+ return r
+ }, b64)
if len(b64) > 12 {
return b64[:12] + "…"
}
diff --git a/internal/signing/signing_test.go b/internal/signing/signing_test.go
index 9d1326f..8f94379 100644
--- a/internal/signing/signing_test.go
+++ b/internal/signing/signing_test.go
@@ -313,6 +313,20 @@ func TestRFC8032Vector(t *testing.T) {
}
}
+// TestSignRejectsC1Audience: the "control-free" audience rule must cover
+// the C1 range (0x80–0x9F), not only ASCII — an ASCII-only check admitted
+// U+0085 (next line), making the documented guarantee false.
+func TestSignRejectsC1Audience(t *testing.T) {
+ _, priv := testKey(t)
+ c1 := "github.com/org/\u0085repo" // U+0085, a C1 control
+ if _, err := Sign(fixtureReceipt(t), priv, c1); err == nil {
+ t.Fatalf("C1 control in audience accepted")
+ }
+ if _, err := Sign(fixtureReceipt(t), priv, "github.com/org/repo"); err != nil {
+ t.Fatalf("plain ASCII audience rejected: %v", err)
+ }
+}
+
func b64(raw []byte) string {
return base64.StdEncoding.EncodeToString(raw)
}
diff --git a/internal/strictjson/strictjson.go b/internal/strictjson/strictjson.go
index 75efd4e..b16433a 100644
--- a/internal/strictjson/strictjson.go
+++ b/internal/strictjson/strictjson.go
@@ -17,14 +17,15 @@ import (
"errors"
"fmt"
"io"
+ "strings"
"unicode/utf8"
)
// Decode parses data into v under the strict contract. The stdlib decoder
// alone keeps a duplicate key's last value, matches struct fields
-// case-insensitively (accepted: canonical producers emit exact names, and
-// the signature layer separately requires byte-identical re-encoding), and
-// — the trailing-content gap — Decoder.More reports false at a stray
+// case-insensitively (so a case-variant sibling key silently overrides — see
+// rejectDupKeysIn, which rejects the collision), and — the trailing-content
+// gap — Decoder.More reports false at a stray
// closing delimiter, so "{...}]" passes a More-based check. Decode demands
// io.EOF from the token stream instead.
func Decode(data []byte, v any) error {
@@ -62,17 +63,31 @@ func rejectDupKeysIn(dec *json.Decoder, t json.Token) error {
}
switch d {
case '{':
- seen := map[string]bool{}
+ var seen []string
for dec.More() {
kt, err := dec.Token()
if err != nil {
return err
}
k, _ := kt.(string)
- if seen[k] {
- return fmt.Errorf("duplicate key %q", k)
+ // Exact duplicates are the obvious smuggle. Case-fold
+ // collisions are the subtle one: encoding/json matches a JSON
+ // key to a struct field case-INsensitively and lets a later
+ // key win, so {"outcome":"counterexample","Outcome":"verified"}
+ // decodes to "verified" while our exact-match check saw two
+ // distinct keys. Demonstrated live to turn an intake
+ // counterexample into a pass. Honest producers never emit two
+ // keys equal under case folding, so rejecting the collision
+ // costs nothing and closes the differential at the source.
+ for _, prev := range seen {
+ if prev == k {
+ return fmt.Errorf("duplicate key %q", k)
+ }
+ if strings.EqualFold(prev, k) {
+ return fmt.Errorf("case-variant key collision: %q and %q decode to one field", prev, k)
+ }
}
- seen[k] = true
+ seen = append(seen, k)
vt, err := dec.Token()
if err != nil {
return err
diff --git a/internal/strictjson/strictjson_test.go b/internal/strictjson/strictjson_test.go
index 913592a..7de6511 100644
--- a/internal/strictjson/strictjson_test.go
+++ b/internal/strictjson/strictjson_test.go
@@ -32,6 +32,7 @@ func TestStrictRejections(t *testing.T) {
}{
{"duplicate key", `{"a":"x","a":"y"}`, "duplicate key"},
{"duplicate key nested", `{"a":"x","b":[{"c":1,"c":2}]}`, "duplicate key"},
+ {"case-variant key collision", `{"a":"x","A":"y"}`, "case-variant key collision"},
{"unknown field", `{"a":"x","zz":1}`, "unknown field"},
{"trailing value", `{"a":"x"} true`, "trailing content"},
{"stray closing delimiter", `{"a":"x"}]`, "trailing content"},
diff --git a/schema/schema.go b/schema/schema.go
index fadeeb7..a24f5db 100644
--- a/schema/schema.go
+++ b/schema/schema.go
@@ -445,8 +445,10 @@ func (r Receipt) GateBlocked() bool {
// whose every row was rejected — or an empty one — satisfies
// nothing (demonstrated adversarially; the manifest protocol is
// the full fix and stays deferred, but zero accepted rows must
- // not read as a delivered requirement).
- if rec.Required && (!rec.Admitted || rec.Accepted == 0) {
+ // not read as a delivered requirement). The bound is Accepted < 1
+ // (not == 0), so a hand-forged negative count — which slipped the
+ // == 0 form — cannot read as delivered either.
+ if rec.Required && (!rec.Admitted || rec.Accepted < 1) {
return true
}
}