fix(Delete): guard against negative prevTok on leading-comma input (OSS-Fuzz 4649128545288192)#283
Open
fix(Delete): guard against negative prevTok on leading-comma input (OSS-Fuzz 4649128545288192)#283
Conversation
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Deletepanicked withruntime error: index out of range [-1]on malformed inputs that begin with a stray comma (e.g.,{"test":1{},,""{"test":0}).go test -fuzzwrappers around the existing OSS-Fuzz targets infuzz.go, with panic-recover crash recording, so local fuzzing can find many distinct crashes per run instead of stopping at the first.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
Deleteremoves the last sibling of an object, it reassignskeyOffsetto the offset of the preceding sibling-separator comma returned byfindTokenStart. On malformed input with a garbage leading comma at offset 0,findTokenStartreturns 0 →keyOffset = 0→prevTok = lastToken(data[:0]) = -1→ the subsequentdata[prevTok]reads index-1and panics.Fix
Guard the
data[prevTok]dereference. WhenprevTok < 0there is no content before the key, sonewOffset = 0is the natural answer.Test plan
go test ./...— full suite passesdeleteTestscovering the OSS-Fuzz repro and the variant the local fuzzer producedDeleteafter the patch finds zero crashes🤖 Generated with Claude Code