Close nine adversarial-verification holes in signing and intake

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

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.

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 {

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)
+	}
+}

internal/receipt/markdown.go

@@ -21,6 +21,7 @@ const MarkdownMarker = "<!-- correctful-receipt -->"
 // (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, "<sub>%s</sub>\n", note)
 	}
 	if p := r.Policy; p != nil {
-		fmt.Fprintf(w, "<sub>policy: `%s` · %s · %d rule(s)%s</sub>\n", p.Path, short(p.Digest), p.Rules, exemptNote(p))
+		fmt.Fprintf(w, "<sub>policy: `%s` · %s · %d rule(s)%s</sub>\n", mdCell(p.Path), short(p.Digest), p.Rules, exemptNote(p))
 	}
 	for _, rec := range r.Intake {
 		fmt.Fprintf(w, "<sub>intake: %s</sub>\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, "\n<sub>schema %s%s · exit gate: %s; the remainder informs, never fails</sub>\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", " ")
 }

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

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
+}