From bda99303ef902f1df7115c4a45556bb822d69b7d Mon Sep 17 00:00:00 2001 From: Josh Terry Date: Mon, 17 Aug 2026 18:41:42 -0700 Subject: [PATCH] Close the six confirmed holes from the adversarial intake verification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The design reviewer attacked the merged implementation with live fixtures and confirmed six defects; each fix carries a regression test: 1. Read intake documents BEFORE any repository probe executes — a changed test demonstrably wrote the configured document during its own probe run and minted T4 for itself. 2. Canonical containment for the out-of-tree boundary: every path component of the document and the repo root is symlink-resolved before the prefix check (a symlinked parent smuggled an in-tree file past the lexical version), the final component opens with O_NOFOLLOW, regularity is judged on the opened fd, and size bounds ride a limited reader on that single open. 3. Supplier-scoped duplicate keys: one supplier's pass no longer suppresses another's counterexample on the same raw probe id (refutation dominance was demonstrably violated). A contradictory duplicate within one supplier fails the run loudly. 4. Required means USABLE: an admitted document with zero accepted rows blocks the gate. 5. Strict decoding rejects duplicate JSON keys at any depth — the stdlib's last-wins parsing smuggled a verified outcome behind a counterexample, and duplicate keys would make future signatures ambiguous. 6. Every stored external field is scrubbed (now including DEL and C1) and bounded — a live ESC reached the text receipt through a rejected row. Also from the same review: binding markers accumulate so in-tree coverage cannot hide an acting external row; a discarded external pass on an LLM claim is now explained on the remainder row; intake records carry the supplier version and the config digest. Two recommendations are consciously declined and documented (open mechanism tokens; invoker-supplied paths in stderr diagnostics). Schema 0.0.13. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_015GeUG1gboWiZSnFyzQghyp --- DESIGN.md | 38 ++++++ cmd/correctful/main.go | 29 +++-- internal/intake/hardening_test.go | 206 +++++++++++++++++++++++++++++ internal/intake/intake.go | 210 ++++++++++++++++++++++-------- internal/intake/intake_test.go | 2 +- internal/receipt/receipt.go | 25 ++-- schema/schema.go | 17 ++- 7 files changed, 451 insertions(+), 76 deletions(-) create mode 100644 internal/intake/hardening_test.go diff --git a/DESIGN.md b/DESIGN.md index 360203a..fe60c27 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -511,6 +511,44 @@ refutation external, and blocked; deleting the required document blocked with "not admitted — REQUIRED" on the intake line. All three gate legs behaved to specification on the first run. +Verified adversarially (schema 0.0.13): the same reviewer then attacked +the MERGED implementation with live fixtures and confirmed six holes, each +now closed with a regression test pinning it: + +1. Repository probes ran before intake documents were read, so a changed + test could write the configured document during its own probe run and + mint T4 for itself — demonstrated live. Intake now reads, hashes, and + binds every document BEFORE any probe executes; the ordering comment in + main names itself load-bearing. +2. The out-of-tree boundary was a lexical prefix check, and a symlinked + parent directory smuggled an in-tree document past it. Containment is + now CANONICAL (every component of both paths resolved), the final + component is opened with O_NOFOLLOW, regularity is judged on the opened + fd, and the size bound rides a limited reader on that single open. +3. Duplicate detection was global with a supplier-less key: one supplier's + pass caused another supplier's counterexample on the same raw probe id + to be rejected as a duplicate — refutation dominance violated. + Duplicates are now per supplier; a contradictory duplicate WITHIN a + supplier fails the run loudly (silently keeping either verdict could + launder the other away). +4. An admitted-but-empty required document satisfied the gate. Required + now means USABLE: zero accepted rows blocks. +5. The stdlib JSON decoder keeps a duplicate key's last value, which + smuggled an "outcome": "verified" behind a counterexample. Strict + decoding now rejects duplicate keys at any depth — also a precondition + for unambiguous future signatures. +6. Rejected-row fields bypassed the control-character scrub (a live ESC + reached the text receipt), and the scrub missed DEL and C1. Every + stored external field is now scrubbed and bounded, rejections included. + +Two reviewer recommendations are consciously NOT taken, stated here so the +divergence is a decision rather than an omission: policy mechanisms stay +an open token vocabulary (a registry would couple policy validation to +intake configuration that differs between local and CI invocations; the +typo cost fails closed as an unsatisfiable floor), and stderr diagnostics +keep the invoker-supplied intake paths (the flag value already appears in +the CI configuration; the RECEIPT never carries them). + ## 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/cmd/correctful/main.go b/cmd/correctful/main.go index d0a741d..533b3c9 100644 --- a/cmd/correctful/main.go +++ b/cmd/correctful/main.go @@ -148,24 +148,29 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL claims, mentions = harvest.AnchorClaims(claims, harvest.BuildDefIndex(root, docs), change.Files) coverage.SuppressedMentions = mentions - evidence := probe.NewDispatcher(concurrency, probe.Default()...). - Dispatch(ctx, root, claims) - - // Admit external evidence AFTER the in-tree probes: supplied rows join - // each claim's evidence list and are weighed by the same rules. - var intakeRecords []schema.IntakeRecord + // Admit external evidence BEFORE any in-tree probe executes. The order + // is load-bearing (verified adversarially): repository probes run the + // change's own test code, and a probe that writes the configured intake + // document during its run must find the document already read, hashed, + // and bound — the reviewed change must not supply its own evidence. + var ( + intakeRecords []schema.IntakeRecord + extra map[string][]schema.Evidence + ) if intakeCfg != nil { subj := intake.Subject{HeadSHA: change.HeadSHA, InputDigest: change.InputDigest} - extra, records, err := intake.Run(intakeCfg, root, subj, claims) + extra, intakeRecords, err = intake.Run(intakeCfg, root, subj, claims) if err != nil { return err } - for i := range claims { - if rows := extra[claims[i].ID]; len(rows) > 0 { - evidence[i] = append(evidence[i], rows...) - } + } + + evidence := probe.NewDispatcher(concurrency, probe.Default()...). + Dispatch(ctx, root, claims) + for i := range claims { + if rows := extra[claims[i].ID]; len(rows) > 0 { + evidence[i] = append(evidence[i], rows...) } - intakeRecords = records } r := receipt.Assemble(change, claims, evidence, coverage) diff --git a/internal/intake/hardening_test.go b/internal/intake/hardening_test.go new file mode 100644 index 0000000..2ca2af0 --- /dev/null +++ b/internal/intake/hardening_test.go @@ -0,0 +1,206 @@ +package intake + +// Regression tests for the adversarial verification findings: each test +// here pins a CONFIRMED hole from the post-implementation review of the +// intake contract. + +import ( + "fmt" + "os" + "path/filepath" + "strings" + "testing" + + "github.com/joshft/correctful/schema" +) + +// TestContradictoryVerdictsFailLoudly: a supplier that reports both a pass +// and a counterexample for the same probe is a supplier bug — silently +// keeping either verdict could launder the other away, so the run errors. +func TestContradictoryVerdictsFailLoudly(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + rows := `{"claim_id": "INV-009", "probe_id": "p", "outcome": "verified"}, + {"claim_id": "INV-009", "probe_id": "p", "outcome": "counterexample"}` + 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) + } + if _, _, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims()); err == nil || + !strings.Contains(err.Error(), "contradictory verdicts") { + t.Errorf("contradiction tolerated: %v", err) + } +} + +// TestCrossSupplierCounterexampleSurvives: refutation dominance across +// suppliers. Supplier A's pass on a raw probe id must NOT suppress supplier +// B's counterexample on the same raw id — the namespaced probes are +// distinct evidence, and the demonstrated global-dedupe hole let a pass +// launder a refutation away. +func TestCrossSupplierCounterexampleSurvives(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + subj := Subject{HeadSHA: "abc", InputDigest: goodDigest} + passDoc := write(t, outside, "a.json", docFor("prover-a", "abc", goodDigest, + `{"claim_id": "INV-009", "probe_id": "shared", "outcome": "verified"}`)) + cxDoc := write(t, outside, "b.json", docFor("prover-b", "abc", goodDigest, + `{"claim_id": "INV-009", "probe_id": "shared", "outcome": "counterexample", "detail": "trace"}`)) + cfgPath := write(t, outside, "cfg.json", fmt.Sprintf(`{ + "intake_version": 1, + "suppliers": [ + {"name": "prover-a", "mechanism": "proof-a", "max_tier": 4, "document": %q}, + {"name": "prover-b", "mechanism": "proof-b", "max_tier": 4, "document": %q} + ] +}`, passDoc, cxDoc)) + cfg, err := LoadConfig(cfgPath, repo) + if err != nil { + t.Fatal(err) + } + extra, records, err := Run(cfg, repo, subj, testClaims()) + if err != nil { + t.Fatal(err) + } + if records[0].Accepted != 1 || records[1].Accepted != 1 { + t.Fatalf("accepted = %d/%d, want both suppliers' rows: %+v", records[0].Accepted, records[1].Accepted, records) + } + rows := extra["INV-009"] + if len(rows) != 2 { + t.Fatalf("evidence rows = %d, want 2 distinct namespaced probes", len(rows)) + } + refuted := false + for _, ev := range rows { + if ev.Refuted() { + refuted = true + } + } + if !refuted { + t.Error("the counterexample was suppressed — refutation dominance violated") + } +} + +// TestDuplicateJSONKeysRejected: the stdlib decoder keeps a duplicate +// key's last value — demonstrated to smuggle "outcome": "verified" behind +// a counterexample — so strict decoding refuses duplicates at any depth. +func TestDuplicateJSONKeysRejected(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + doc := `{ + "intake_version": 1, + "supplier": "dafny-worker", + "subject": {"head_sha": "abc", "input_digest": "` + goodDigest + `"}, + "results": [ + {"claim_id": "INV-009", "probe_id": "p", "outcome": "counterexample", "outcome": "verified"} + ] +}` + docPath := write(t, outside, "doc.json", doc) + cfgPath := write(t, outside, "cfg.json", configFor(docPath, false)) + cfg, err := LoadConfig(cfgPath, repo) + if err != nil { + t.Fatal(err) + } + if _, _, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims()); err == nil || + !strings.Contains(err.Error(), "duplicate key") { + t.Errorf("duplicate key tolerated: %v", err) + } +} + +// TestParentSymlinkCannotSmuggleInTreeFiles: containment is CANONICAL. A +// symlinked parent directory that resolves into the repository tree was +// demonstrated to pass a lexical prefix check; the resolved path is what +// the boundary judges. +func TestParentSymlinkCannotSmuggleInTreeFiles(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + if err := os.MkdirAll(filepath.Join(repo, "evil"), 0o755); err != nil { + t.Fatal(err) + } + write(t, filepath.Join(repo, "evil"), "doc.json", docFor("dafny-worker", "abc", goodDigest, + `{"claim_id": "INV-009", "probe_id": "p", "outcome": "verified"}`)) + linkDir := filepath.Join(outside, "looks-external") + if err := os.Symlink(filepath.Join(repo, "evil"), linkDir); err != nil { + t.Fatal(err) + } + cfgPath := write(t, outside, "cfg.json", configFor(filepath.Join(linkDir, "doc.json"), false)) + cfg, err := LoadConfig(cfgPath, repo) + if err != nil { + t.Fatal(err) + } + if _, _, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims()); err == nil || + !strings.Contains(err.Error(), "inside the repository tree") { + t.Errorf("parent symlink smuggled an in-tree document: %v", err) + } +} + +// TestRequiredNeedsUsableEvidence: an admitted document with zero accepted +// rows — empty, or every row rejected — satisfies nothing. Required means +// usable evidence arrived. +func TestRequiredNeedsUsableEvidence(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + subj := Subject{HeadSHA: "abc", InputDigest: goodDigest} + for name, rows := range map[string]string{ + "empty": "", + "all rejected": `{"claim_id": "INV-404", "probe_id": "p", "outcome": "verified"}`, + } { + docPath := write(t, outside, "doc-"+strings.ReplaceAll(name, " ", "-")+".json", + docFor("dafny-worker", "abc", goodDigest, rows)) + cfgPath := write(t, outside, "cfg-"+strings.ReplaceAll(name, " ", "-")+".json", configFor(docPath, true)) + cfg, err := LoadConfig(cfgPath, repo) + if err != nil { + t.Fatal(err) + } + _, records, err := Run(cfg, repo, subj, testClaims()) + if err != nil { + t.Fatal(err) + } + r := schema.Receipt{Intake: records} + if !r.GateBlocked() { + t.Errorf("%s: required document with nothing usable did not block", name) + } + } +} + +// TestRejectedRowsAreScrubbed: rejection fields render in receipts, so +// control characters (an ESC sequence, demonstrated live; DEL and C1 are +// covered by the same scrub) must not survive into them — and the audit +// record carries the supplier version and the config digest. The ESC +// arrives through JSON's \u001b escape, exactly as a hostile document +// would deliver it. +func TestRejectedRowsAreScrubbed(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + rows := `{"claim_id": "INV-\u001b[31m999", "probe_id": "p1", "outcome": "verified"}` + docPath := write(t, outside, "doc.json", docFor("dafny-worker", "abc", goodDigest, rows)) + cfgPath := write(t, outside, "cfg.json", strings.Replace(configFor(docPath, false), + `"mechanism"`, `"version": "1.2.0", "mechanism"`, 1)) + cfg, err := LoadConfig(cfgPath, repo) + if err != nil { + t.Fatal(err) + } + _, records, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims()) + if err != nil { + t.Fatal(err) + } + rec := records[0] + if len(rec.Rejected) != 1 { + t.Fatalf("rejected = %+v", rec.Rejected) + } + for _, s := range []string{rec.Rejected[0].ClaimID, rec.Rejected[0].ProbeID} { + for _, r := range s { + if r < 0x20 || r == 0x7F || (r >= 0x80 && r <= 0x9F) { + t.Errorf("control character %U survived in %q", r, s) + } + } + } + if !strings.Contains(rec.Rejected[0].ClaimID, "INV-") || !strings.Contains(rec.Rejected[0].ClaimID, "999") { + t.Errorf("scrub destroyed the printable content: %q", rec.Rejected[0].ClaimID) + } + if rec.SupplierVersion != "1.2.0" { + t.Errorf("supplier version = %q, want the profile's declaration", rec.SupplierVersion) + } + if rec.ConfigDigest == "" { + t.Error("config digest absent — the authority file is unpinned") + } +} diff --git a/internal/intake/intake.go b/internal/intake/intake.go index ead1472..e40a232 100644 --- a/internal/intake/intake.go +++ b/internal/intake/intake.go @@ -33,28 +33,34 @@ import ( "bytes" "crypto/sha256" "encoding/json" + "errors" "fmt" + "io" "os" "path/filepath" "regexp" "strings" + "syscall" "github.com/joshft/correctful/schema" ) // Bounds — strict limits so a document cannot balloon a receipt. const ( - maxSuppliers = 16 - maxDocBytes = 4 << 20 - maxRows = 500 - maxDetailLen = 300 - maxProbeIDLen = 200 + maxSuppliers = 16 + maxConfigBytes = 64 << 10 + maxDocBytes = 4 << 20 + maxRows = 500 + maxDetailLen = 300 + maxProbeIDLen = 200 ) // Config is the invoker-owned intake configuration: the authority grants. type Config struct { IntakeVersion int `json:"intake_version"` Suppliers []Profile `json:"suppliers"` + + digest string // SHA-256 over the config's exact bytes — the authority pin } // Profile is one supplier's authority grant. @@ -62,6 +68,10 @@ type Profile struct { // Name identifies the supplier; token shape, and the value every // admitted row's Evidence.Supplier carries. Name string `json:"name"` + // Version identifies the supplier build the invoker vouches for — + // echoed into the receipt's intake record so two receipts are + // comparable across supplier upgrades. Optional. + Version string `json:"version,omitempty"` // Mechanism is the evidence class the invoker vouches this supplier // produces (e.g. "dafny-proof"). Policy floors reference it. Must not // collide with a built-in runner mechanism. @@ -134,12 +144,9 @@ var builtinMechanisms = map[string]bool{ // a broken authority grant must never fail open. repoRoot guards the // out-of-tree rule for the config itself and every document path. func LoadConfig(path, repoRoot string) (*Config, error) { - if err := outsideTree(path, repoRoot); err != nil { - return nil, fmt.Errorf("intake config: %w", err) - } - data, err := os.ReadFile(path) + data, err := readOutsideTree(path, repoRoot, maxConfigBytes) if err != nil { - return nil, fmt.Errorf("reading intake config: %w", err) + return nil, fmt.Errorf("intake config: %w", err) } var c Config if err := strictDecode(data, &c); err != nil { @@ -166,9 +173,12 @@ func LoadConfig(path, repoRoot string) (*Config, error) { return nil, fmt.Errorf("intake config: supplier %q max_tier %d out of range (1–4)", p.Name, p.MaxTier) case p.Document == "": return nil, fmt.Errorf("intake config: supplier %q has no document path", p.Name) + case len(p.Version) > 64: + return nil, fmt.Errorf("intake config: supplier %q version exceeds 64 bytes", p.Name) } seen[p.Name] = true } + c.digest = fmt.Sprintf("%x", sha256.Sum256(data)) return &c, nil } @@ -188,11 +198,19 @@ func Run(c *Config, repoRoot string, subj Subject, claims []schema.Claim) (map[s } extra := map[string][]schema.Evidence{} var records []schema.IntakeRecord - seenProbe := map[string]bool{} // (claim, probe) across ALL documents + // Duplicates are per SUPPLIER, keyed by outcome too: two suppliers may + // legitimately probe the same target (their evidence is distinct — the + // namespaced probe ids differ), so a global key would let one + // supplier's pass suppress another's counterexample, violating + // refutation dominance (found adversarially, live). Within a supplier, + // a contradictory duplicate is a supplier bug and fails LOUDLY — + // silently keeping either verdict could launder the other away. + seenOutcome := map[string]string{} // supplier\x00claim\x00probe -> outcome for _, p := range c.Suppliers { - rec := schema.IntakeRecord{Supplier: p.Name, Mechanism: p.Mechanism, - MaxTier: schema.Tier(p.MaxTier), Required: p.Required} + rec := schema.IntakeRecord{Supplier: p.Name, SupplierVersion: scrub(p.Version), + Mechanism: p.Mechanism, MaxTier: schema.Tier(p.MaxTier), + Required: p.Required, ConfigDigest: c.digest} doc, digest, reason, err := admit(p, repoRoot, subj) if err != nil { return nil, nil, err @@ -204,14 +222,19 @@ func Run(c *Config, repoRoot string, subj Subject, claims []schema.Claim) (map[s } rec.Admitted, rec.DocDigest = true, digest for _, r := range doc.Results { - if reason := rejectRow(r, claimByID, seenProbe); reason != "" { + key := p.Name + "\x00" + r.ClaimID + "\x00" + r.ProbeID + if prev, dup := seenOutcome[key]; dup && prev != r.Outcome { + return nil, nil, fmt.Errorf("intake document for %q: contradictory verdicts for %s / %s (%s vs %s)", + p.Name, r.ClaimID, r.ProbeID, prev, r.Outcome) + } + if reason := rejectRow(r, claimByID, seenOutcome, key); reason != "" { rec.Rejected = append(rec.Rejected, schema.IntakeRejection{ - ClaimID: clip(r.ClaimID, maxProbeIDLen), ProbeID: clip(r.ProbeID, maxProbeIDLen), - Outcome: r.Outcome, Reason: reason, + ClaimID: scrub(clip(r.ClaimID, maxProbeIDLen)), ProbeID: scrub(clip(r.ProbeID, maxProbeIDLen)), + Outcome: scrub(clip(r.Outcome, 32)), Reason: reason, }) continue } - seenProbe[r.ClaimID+"\x00"+r.ProbeID] = true + seenOutcome[key] = r.Outcome ev := evidenceFrom(p, r) extra[r.ClaimID] = append(extra[r.ClaimID], ev) rec.Accepted++ @@ -225,18 +248,12 @@ func Run(c *Config, repoRoot string, subj Subject, claims []schema.Claim) (map[s // missing or mismatched document is (nil, reason) — recorded, not an error; // a malformed one IS an error, same as a malformed config. func admit(p Profile, repoRoot string, subj Subject) (*document, string, string, error) { - if err := outsideTree(p.Document, repoRoot); err != nil { - return nil, "", "", fmt.Errorf("intake document for %q: %w", p.Name, err) - } - data, err := os.ReadFile(p.Document) + data, err := readOutsideTree(p.Document, repoRoot, maxDocBytes) if os.IsNotExist(err) { return nil, "", "no document at the configured path", nil } if err != nil { - return nil, "", "", fmt.Errorf("reading intake document for %q: %w", p.Name, err) - } - if len(data) > maxDocBytes { - return nil, "", "", fmt.Errorf("intake document for %q exceeds %d bytes", p.Name, maxDocBytes) + return nil, "", "", fmt.Errorf("intake document for %q: %w", p.Name, err) } var doc document if err := strictDecode(data, &doc); err != nil { @@ -258,7 +275,7 @@ func admit(p Profile, repoRoot string, subj Subject) (*document, string, string, } // rejectRow returns the reason a row does not become evidence, or "". -func rejectRow(r row, claims map[string]*schema.Claim, seen map[string]bool) string { +func rejectRow(r row, claims map[string]*schema.Claim, seen map[string]string, key string) string { switch { case !validOutcomes[r.Outcome]: return "unknown outcome (want verified, counterexample, inconclusive, not_run, or error)" @@ -266,8 +283,9 @@ func rejectRow(r row, claims map[string]*schema.Claim, seen map[string]bool) str return "probe_id empty or too long" case r.ClaimID == "": return "claim_id empty" - case seen[r.ClaimID+"\x00"+r.ProbeID]: - return "duplicate (claim_id, probe_id) across intake documents" + } + if _, dup := seen[key]; dup { + return "duplicate (claim_id, probe_id) for this supplier" } c, ok := claims[r.ClaimID] if !ok { @@ -311,39 +329,71 @@ func evidenceFrom(p Profile, r row) schema.Evidence { return ev } -// outsideTree rejects symlinks, non-regular files, and any path under the -// repository root: evidence the reviewed change can write is not evidence. -func outsideTree(path, repoRoot string) error { - fi, err := os.Lstat(path) +// readOutsideTree reads one intake file with the boundary checks the +// contract depends on, hardened adversarially: +// +// - CANONICAL containment, not lexical: every path component of both the +// file's directory and the repo root is symlink-resolved before the +// prefix comparison — a symlinked parent directory was demonstrated to +// smuggle an in-tree file past a lexical check. +// - The final component must not be a symlink, enforced at open time +// with O_NOFOLLOW — an Lstat-then-open pair leaves a swap window. +// - The size bound applies through a limited reader on the single opened +// fd, and the fd's own Stat (not the path) decides regularity. +// +// A missing file returns the raw not-exist error so callers can treat +// absence as recordable rather than fatal. +func readOutsideTree(path, repoRoot string, maxBytes int64) ([]byte, error) { + abs, err := filepath.Abs(path) if err != nil { - if os.IsNotExist(err) { - return nil // absence is handled by the caller (recorded, not fatal) - } - return err + return nil, err + } + canonDir, err := filepath.EvalSymlinks(filepath.Dir(abs)) + if err != nil { + return nil, err // includes not-exist for the parent } - if fi.Mode()&os.ModeSymlink != 0 { - return fmt.Errorf("%s is a symlink — intake paths must be regular files", path) + canon := filepath.Join(canonDir, filepath.Base(abs)) + canonRoot, err := filepath.EvalSymlinks(repoRoot) + if err != nil { + return nil, err } - if !fi.Mode().IsRegular() { - return fmt.Errorf("%s is not a regular file", path) + if canon == canonRoot || strings.HasPrefix(canon, canonRoot+string(filepath.Separator)) { + return nil, fmt.Errorf("%s resolves inside the repository tree — the reviewed change must not supply its own evidence", path) } - abs, err := filepath.Abs(path) + f, err := os.OpenFile(canon, os.O_RDONLY|syscall.O_NOFOLLOW, 0) if err != nil { - return err + if errors.Is(err, syscall.ELOOP) { + return nil, fmt.Errorf("%s is a symlink — intake paths must be regular files", path) + } + return nil, err } - root, err := filepath.Abs(repoRoot) + defer f.Close() + st, err := f.Stat() if err != nil { - return err + return nil, err } - if abs == root || strings.HasPrefix(abs, root+string(filepath.Separator)) { - return fmt.Errorf("%s is inside the repository tree — the reviewed change must not supply its own evidence", path) + if !st.Mode().IsRegular() { + return nil, fmt.Errorf("%s is not a regular file", path) } - return nil + data, err := io.ReadAll(io.LimitReader(f, maxBytes+1)) + if err != nil { + return nil, err + } + if int64(len(data)) > maxBytes { + return nil, fmt.Errorf("%s exceeds the %d-byte bound", path, maxBytes) + } + return data, nil } -// strictDecode parses JSON with unknown fields rejected and trailing -// content refused. +// strictDecode parses JSON with unknown fields rejected, trailing content +// refused, and DUPLICATE KEYS refused. The stdlib decoder silently keeps a +// duplicate's last value — demonstrated to smuggle a second "outcome": +// "verified" behind a "counterexample" — and last-wins parsing would also +// make any future signature ambiguous across JSON parsers. func strictDecode(data []byte, v any) error { + if err := rejectDupKeys(json.NewDecoder(bytes.NewReader(data))); err != nil { + return err + } dec := json.NewDecoder(bytes.NewReader(data)) dec.DisallowUnknownFields() if err := dec.Decode(v); err != nil { @@ -355,12 +405,68 @@ func strictDecode(data []byte, v any) error { return nil } -// scrub strips control characters from an external string — supplied text -// reaches terminals and PR comments, and must not carry escapes. Path +// rejectDupKeys walks the token stream and fails on a repeated object key +// at any depth. +func rejectDupKeys(dec *json.Decoder) error { + t, err := dec.Token() + if err != nil { + return err + } + return rejectDupKeysIn(dec, t) +} + +func rejectDupKeysIn(dec *json.Decoder, t json.Token) error { + d, ok := t.(json.Delim) + if !ok { + return nil + } + switch d { + case '{': + seen := map[string]bool{} + 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) + } + seen[k] = true + vt, err := dec.Token() + if err != nil { + return err + } + if err := rejectDupKeysIn(dec, vt); err != nil { + return err + } + } + _, err := dec.Token() // consume '}' + return err + case '[': + for dec.More() { + vt, err := dec.Token() + if err != nil { + return err + } + if err := rejectDupKeysIn(dec, vt); err != nil { + return err + } + } + _, err := dec.Token() // consume ']' + return err + } + return nil +} + +// scrub strips control characters — C0 (except newline and tab), DEL, and +// the C1 range — from an external string: supplied text reaches terminals +// and PR comments, and must not carry escapes. Applied to EVERY stored +// external field, rejected rows included (a rejection renders too). Path // scrubbing happens later at the receipt's sanitization chokepoint. func scrub(s string) string { return strings.Map(func(r rune) rune { - if r < 0x20 && r != '\n' && r != '\t' { + if (r < 0x20 && r != '\n' && r != '\t') || r == 0x7F || (r >= 0x80 && r <= 0x9F) { return -1 } return r diff --git a/internal/intake/intake_test.go b/internal/intake/intake_test.go index 71d8ac3..efbaba2 100644 --- a/internal/intake/intake_test.go +++ b/internal/intake/intake_test.go @@ -264,7 +264,7 @@ func TestRowRejections(t *testing.T) { `{"claim_id": "INV-999", "probe_id": "p1", "outcome": "counterexample", "detail": "boom"}`, `{"claim_id": "INV-777", "probe_id": "p2", "outcome": "verified"}`, `{"claim_id": "INV-009", "probe_id": "p3", "outcome": "verified"}`, - `{"claim_id": "INV-009", "probe_id": "p3", "outcome": "counterexample"}`, + `{"claim_id": "INV-009", "probe_id": "p3", "outcome": "verified"}`, }, ",") docPath := write(t, outside, "doc.json", docFor("dafny-worker", "abc", goodDigest, rows)) cfgPath := write(t, outside, "cfg.json", configFor(docPath, false)) diff --git a/internal/receipt/receipt.go b/internal/receipt/receipt.go index 1d8f321..a560d75 100644 --- a/internal/receipt/receipt.go +++ b/internal/receipt/receipt.go @@ -158,28 +158,30 @@ func anchoringSummary(claims []schema.Claim) *schema.AnchoringSummary { // least one probe and no annotated region was reached; no marker means no // coverage check applied. func bindingNote(res schema.ClaimResult) string { - nameOnly, external := false, "" + covered, nameOnly, external := "", false, "" for _, e := range res.Evidence { switch e.Binding { case schema.BindingCovered: - return " [binding: coverage-proven]" + covered = " [binding: coverage-proven]" case schema.BindingFileCovered: - return " [binding: file-coverage-proven]" + if covered == "" { + covered = " [binding: file-coverage-proven]" + } case schema.BindingNameOnly: nameOnly = true case schema.BindingSupplierAttested: if e.CountsFor(res.Claim) { - external = e.Supplier + external = " [external: " + e.Supplier + " — supplier-attested]" } } } - switch { - case external != "": - return " [external: " + external + " — supplier-attested]" - case nameOnly: + // Markers ACCUMULATE: an in-tree coverage proof must not hide that an + // external row is also acting on the claim (it may be the row setting + // the effective tier), and vice versa. + if covered == "" && external == "" && nameOnly { return " [binding: name-only]" } - return "" + return covered + external } // externalRefutationNote marks a refuted row whose refuting evidence was @@ -224,6 +226,9 @@ func intakeLine(rec schema.IntakeRecord) string { if n := len(rec.Rejected); n > 0 { s += fmt.Sprintf(", %d rejected", n) } + if rec.Required && rec.Accepted == 0 { + s += " — REQUIRED with nothing usable (the gate blocks here)" + } return s } @@ -244,6 +249,8 @@ func llmEdgeNote(res schema.ClaimResult) string { switch e.Binding { case schema.BindingFileNotReached: return " [llm edge rejected: the probe passed but never executed " + res.Claim.Source.File + "]" + case schema.BindingSupplierAttested: + return " [external pass by " + e.Supplier + " not counted: a model-proposed claim verifies only through a coverage-confirmed edge]" case "": return " [llm edge unconfirmed: no coverage profile, so the pass raised nothing]" } diff --git a/schema/schema.go b/schema/schema.go index d51f2a5..57954a3 100644 --- a/schema/schema.go +++ b/schema/schema.go @@ -436,7 +436,12 @@ func (r Receipt) GateBlocked() bool { return true } for _, rec := range r.Intake { - if rec.Required && !rec.Admitted { + // Required means USABLE evidence arrived: an admitted document + // 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) { return true } } @@ -481,6 +486,14 @@ type PolicyMiss struct { type IntakeRecord struct { // Supplier is the profile's name (invoker-owned, never row-claimed). Supplier string `json:"supplier"` + // SupplierVersion echoes the profile's declared supplier build, when + // the invoker stated one — the chain needs it to compare receipts + // across supplier upgrades. + SupplierVersion string `json:"supplier_version,omitempty"` + // ConfigDigest is the SHA-256 (hex) over the intake config's exact + // bytes — the pin for the authority file that granted this supplier + // its mechanism and tier. + ConfigDigest string `json:"config_digest,omitempty"` // Mechanism and MaxTier echo the profile: the authority the invoker // granted, which every admitted row is clamped to. Mechanism string `json:"mechanism"` @@ -512,4 +525,4 @@ type IntakeRejection struct { } // SchemaVersion is the current version of the receipt schema (the payload). -const SchemaVersion = "0.0.12" +const SchemaVersion = "0.0.13"