Proof Portal

Sign in
Projects

jsonparser

ProbeLabs36 findings · 123 requirements
Back to findings
Problem reportDEFECT-260727-T7P7

Set on top-level array-index beyond length returns KeyPathNotFoundError (SYS-REQ-110 contract gap)

FixedFixedMedium

This defect has been fixed and verified.

Resolved 1 known issue:KI-4

Introduced

When and where this issue first entered the codebase — the commit it traces back to.

Inception (latent from the first version)
Origin
Audit Finding

Affected requirements

The requirement(s) this issue violates — click through to the spec.

SYS-REQ-110

Severity, explained

Why this is rated the way it is — and the scoring signals behind the rating (each ⓘ explains the term).

MediumRated severity — the impact if this issue is exploited or hit.
risk area
Data Integrity

Root cause

What actually went wrong underneath — and how it is classified.

parser.go:Set, endOffset==-1 branch: the code path for "path not found at all" only handles (pathIsIndex && dataIsObject) and (pathIsObjectKey && dataIsArray) cross-type coercions; the matching (pathIsIndex && dataIsArray) case is explicitly rejected with KeyPathNotFoundError. SYS-REQ-110 does not carve out this exception, so it is a spec/code divergence that requires either narrowing the spec or extending Set.

Spec gap— this behaviour wasn't specified

Proof it's fixed

The tests, tightened requirements and new obligations that prove this defect is gone — and can't quietly return.

Covered by a known issue.

strengthened requirements
SYS-REQ-110

Blast radius

If you touch this issue, what else may need re-checking — the requirements it affects and the code and tests that hang off them.

Open in graph
Tracing blast radius…

Touch this finding and you re-check 1 requirements · 2 code files · 7 tests.

Requirements (1)
SYS-REQ-110
Code files (2)
  • append.go
  • parser.go
Tests (7)
  • append_test.go
  • fuzz_native_test.go
  • mcdc_supplement_test.go
  • parser_test.go
  • reference_oracle_test.go
  • set_spec_test.go
  • sys_req_110_111_witness_test.go

Per-requirement evidence

For each requirement this finding touches: the implementing code, verifying tests, and proof obligations that discharge it.

SYS-REQ-110
Implementing code (4)
  • append.go
    Append
  • parser.go
    Set
  • parser.go
    createInsertComponent
  • parser.go
    setConfig
Tests & evidence (9)
  • README.md
  • append_test.go
  • docs/proof-gap-root-cause.md
  • fuzz_native_test.go
  • mcdc_supplement_test.go
  • parser_test.go
  • reference_oracle_test.go
  • set_spec_test.go
  • sys_req_110_111_witness_test.go
Proof obligations (3)
boundary

Behavior at limits, thresholds, and edge-of-range values.

  • ✓nominal (required) — sys_req_110_111_witness_test.go:33
  • ✓negative — parser_test.go:2484
element_type_partition
  • ✓nominal (required) — parser_test.go:2485
nested_mutation
  • ✓nominal (required) — sys_req_110_111_witness_test.go:81

Discussions

Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.

Sign in to discuss this with the proof team.Sign in