Skip to content

fix(Delete): guard against negative prevTok on leading-comma input (OSS-Fuzz 4649128545288192)#283

Open
buger wants to merge 7 commits intomasterfrom
fix-oss-fuzz-delete-leading-comma
Open

fix(Delete): guard against negative prevTok on leading-comma input (OSS-Fuzz 4649128545288192)#283
buger wants to merge 7 commits intomasterfrom
fix-oss-fuzz-delete-leading-comma

Conversation

@buger
Copy link
Copy Markdown
Owner

@buger buger commented May 1, 2026

Summary

  • Fixes OSS-Fuzz testcase 4649128545288192Delete panicked with runtime error: index out of range [-1] on malformed inputs that begin with a stray comma (e.g. ,{"test":1{}, ,""{"test":0}).
  • Adds native go test -fuzz wrappers around the existing OSS-Fuzz targets in fuzz.go, with panic-recover crash recording, so local fuzzing can find many distinct crashes per run instead of stopping at the first.
  • Adds run_fuzz_campaign.sh, an iterating multi-pass campaign runner that stops once a full pass produces no new unique crash signatures.

Root cause

When Delete removes the last sibling of an object, it reassigns keyOffset to the offset of the preceding sibling-separator comma returned by findTokenStart. On malformed input with a garbage leading comma at offset 0, findTokenStart returns 0 → keyOffset = 0prevTok = lastToken(data[:0]) = -1 → the subsequent data[prevTok] reads index -1 and panics.

Fix

Guard the data[prevTok] dereference. When prevTok < 0 there is no content before the key, so newOffset = 0 is the natural answer.

-if remainedTok > -1 && remainedValue[remainedTok] == '}' && data[prevTok] == ',' {
+if prevTok > -1 && remainedTok > -1 && remainedValue[remainedTok] == '}' && data[prevTok] == ',' {
     newOffset = prevTok
-} else {
+} else if prevTok > -1 {
     newOffset = prevTok + 1
+} else {
+    newOffset = 0
 }

Test plan

  • go test ./... — full suite passes
  • Two new regression cases added to deleteTests covering the OSS-Fuzz repro and the variant the local fuzzer produced
  • 2-minute / 76 M-exec re-fuzz of Delete after the patch finds zero crashes
  • Full multi-target fuzz campaign across all 14 OSS-Fuzz targets (~2.85 B execs) saturated with only this single bug surfacing

🤖 Generated with Claude Code

buger and others added 7 commits May 1, 2026 20:24
OSS-Fuzz testcase 4649128545288192 found that Delete panicked with
"index out of range [-1]" on inputs like `,{"test":1{}` and `,""{"test":0}`.

Root cause: when the deleted entry is the last sibling of an object,
Delete reassigns keyOffset to the offset of the preceding sibling-separator
comma found by findTokenStart. On malformed input with a leading garbage
comma at offset 0, findTokenStart returns 0, keyOffset becomes 0, and the
downstream cleanup computes prevTok = lastToken(data[:0]) = -1, then panics
on data[prevTok].

Fix: guard the data[prevTok] dereference. When prevTok < 0 there is no
content before the key, so newOffset = 0 — the natural answer.

Also adds:
- Native go test -fuzz wrappers around the existing OSS-Fuzz targets in
  fuzz.go, with panic-recover crash recording so a single run can find
  many distinct crashes instead of stopping at the first.
- run_fuzz_campaign.sh: iterating multi-pass campaign runner that loops
  until a full pass finds no new unique crashes.
- Two regression cases in deleteTests covering the OSS-Fuzz repro and the
  variant the local fuzzer produced.

Verified: full test suite passes; 76M-exec re-fuzz of Delete after the
patch finds zero crashes.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- 7 pure-function lemmas added directly on production code, all
  PROVED on Z3: tokenEnd_in_range, tokenStart_in_range,
  nextToken_in_range, lastToken_in_range,
  isUTF16EncodedRune_low_excluded, isUTF16EncodedRune_high_excluded,
  deleteCleanupFixed_prevTok_nonneg.

- Delete-bug demo (Option β, snippet extraction):
  parser_delete_snippet_proof.go encodes the pre-fix /
  post-fix dereference obligations of the OSS-Fuzz panic block
  (testcase 4649128545288192). Z3 returns COUNTEREXAMPLE
  prevTok = -1, remainedTok = 0 on the buggy variant — the exact
  shape of the OSS-Fuzz repro on `,{"test":1{}` — and PROVED on
  the post-fix variant. Snippet is gated behind reqproof_proof
  build tag.

- verify-properties (SYS-REQ): 16 checks, 0 violated, 4 pre-existing
  orphan_no_requirement skips.

- audit: 0 errors, 6 warnings (mostly authored_delta_expected and
  untraced new fuzz wrappers — expected on a feature branch).

- Coverage: 18 / 18 (100%) of branches reached by lemma translation
  are covered.

- Authoring-time refactors of tokenEnd, nextToken, lastToken,
  tokenStart in parser.go and h2I in escape.go: switch -> if-chain
  and character-literals -> ASCII-int. Behavior byte-identical;
  full test suite passes.

- Documented at docs/reqproof-application.md: lemma inventory,
  the Delete-bug COUNTEREXAMPLE in detail, eight translator-gap
  follow-ups including conditional early-return scoping bug,
  E_SWITCH_NOT_SUPPORTED, character literals, type-conversion
  function-call, slice-expr, free package consts, multi-lemma
  per host, Phase AA auto-OOB.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Re-sweep after reqproof translator fixes shipped on
feat/translator-gap-fixes (HEAD 02a8cb94): char literals (Fix #3),
type conversions (Fix #4), package-level const references (Fix #6),
multi-lemma per host (Fix #7).

Coverage went from 18/18 (100%) to 25/25 (100%). Lemma corpus 11 -> 23
(9 -> 21 PROVED via cached path; 22 PROVED + 1 expected COUNTEREXAMPLE
via fresh-translation --coverage path).

- 4 new lemmas via Fix #3 (char literals): h2I_decimal_digit,
  h2I_uppercase_hex, h2I_lowercase_hex, h2I_nondigit_is_badhex.
  All exercise '0'..'9' / 'A'..'F' / 'a'..'f' on h2I.
- Fix #4 (type conversions) is on the same h2I host — its body uses
  int(c-48) etc., which previously made the host untranslatable.
  Without Fix #4 the four char-literal lemmas above would translation-
  error on the host.
- 3 new lemmas via Fix #6 (package consts): h2I_nondigit_is_badhex
  (uses const badHex), isUTF16EncodedRune_const_high_bound (uses const
  highSurrogateOffset), isUTF16EncodedRune_const_bmp_bound (uses const
  basicMultilingualPlaneReservedOffset).
- 6 additional :lemma directives on existing hosts via Fix #7
  (multi-lemma per host): tokenEnd_nonneg, tokenEnd_empty_zero,
  tokenStart_nonneg, tokenStart_empty_zero, nextToken_signed_disjoint,
  lastToken_signed_disjoint. Pre-fix the scanner dropped any second
  :lemma on a host silently.

Tried-and-rejected (still blocked by other deferred translator gaps):
- combineUTF16Surrogates: Fix #6 resolves the package-const refs in
  the body, but `<<` shift op is unsupported (separate gap, not
  one of #1/#2/#5).
- findTokenStart: still blocked by #1 (early-return / __early_val
  scoping bug in switch + return body shape).
- unescapeToUTF8: still blocked by #2 (switch).

No new production bugs surfaced. The single COUNTEREXAMPLE
(deleteCleanupBuggy_prevTok_nonneg_falsifiable) is the existing
documented OSS-Fuzz Delete demo from a6c5ed3 — counterexample
prevTok=-1, remainedTok=0 matches the documented falsifying witness.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- Lemma corpus: 23 (22 PROVED + 1 CE) -> 30 (29 PROVED + 1 CE)
- 7 new PROVED lemmas (5 path-condition + 2 variadic-callee)
- verify-safety: 11 scanned, 62 skipped, 0 findings
- Real bugs found: 0 new (OSS-Fuzz Delete pre-fix witness still
  surfaces via the dedicated snippet COUNTEREXAMPLE lemma; Delete
  itself remains untranslatable due to E_EARLY_RETURN_NO_ELSE)
- One translator follow-up identified: package-scoped tuple-sort
  preamble poisoning when a multi-return helper sits passively in
  the package (workaround: collapse to single return)
- Documented at docs/reqproof-item3-application.md

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…helpers

Move all reqproof:lemma directives from
parser_delete_snippet_proof.go and parser_item3_lemmas_proof.go onto
the production functions they characterize (tokenEnd, tokenStart,
nextToken, lastToken, h2I) in parser.go and escape.go.

Inline the Delete-cleanup obligation helpers and the variadic
keysCount stand-in at the bottom of parser.go behind a
"// --- reqproof verification helpers ---" delimiter, since those
patterns abstract control-flow shapes that the translator does not
yet support directly on Delete.

Lemma corpus preserved: 30 total = 29 PROVED + 1 CE.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Dogfood the Proof obligation-class catalog v1.0.0 against the
jsonparser corpus — first external-project test of catalog v0.3.0.
Added parser/deserializer/accepts_user_data workload tags to the
7 STK-REQs, resolved 33 baseline-obligation findings (24 accepted +
9 suppressed-with-rationale) and 27 decomposition findings via
suppression entries pointing at the SYS-REQ leaves that bear each
obligation. Each suppression cites JSON-specific semantics or
specific SYS-REQs; no bulk-suppression. Coverage flows OWASP-ASVS-v4,
CWE, MISRA-C, NIST-800-53 and IEC-62304 framework references through
the spec corpus. Refreshed trace reviews on 17 directly-changed +
98 cascade-affected requirements. Case study at
PROOF_CATALOG_DOGFOOD_CASE_STUDY.md.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
After this dogfood surfaced three structural findings (loosened
denial_of_service_resistant trigger, leaf-detection in
obligation_decomposition_complete, three-bucket coverage reporting),
they were fixed in ReqProof v0.3.0 before ship. Update the case study
coverage excerpt to use the new accepted/suppressed/missing buckets
with decided/active coverage percentages, and document the three
findings the dogfood produced.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant