Repository navigation
[verification] prove and fix three defects on the JSON number path - #17
Merged
Merged
Conversation
Pins cJSON.cpp, JsonSerializer.cpp, Document.cpp and StringUtils.cpp with the header cone they need, plus upstream cJSON v1.7.19 as the reference the fork is compared against. The stubs are the ones the earlier targets use: memory system, logging, and the two CRT headers Array.h pulls in.
Six well-formed response bodies through JsonValue and Document, under ASan and UBSan; the conversion over a symbolic double under Z3 and Bitwuzla; and 60k libFuzzer mutations of the parser, which finds nothing -- the parser is not where the defects are, and the negative result is part of the evidence. The suite also asserts that ESBMC's own --overflow-check does not see an out-of-range floating-point conversion, so the day it does, the row fails and the harness can stop stating the property itself.
The three defects all grow from one AWS addition to cJSON: parse_number keeps a big integer's literal in valuestring, a field the printer sizes for a double and the wrapper reads as a string's. Records the reachability -- generated deserializers hit the two conversion defects on every int64 field -- and what the fuzz leg establishes, which is that the parser itself is not implicated.
…y body
LiteralToInt64 kept strtoll's answer only when errno was clear, discarding a
saturation strtoll had already performed exactly; it now takes that answer
whenever the whole literal was consumed and falls back to the double only for
the exponent forms, which is what turns 5e9 from 5 into 5000000000.
The writers returned "{}" when the printer failed, which is the body of every
generated SerializePayload: a failed print would have been indistinguishable
from a document the caller left empty, and the service would have accepted it.
They now log at ERROR and return an empty string. The Android arm of
ConvertToInt64 goes too -- both arms called the same function after the change.
Two checks could pass without proving anything: the upstream-parse_number row compared a grep count of an empty sed range, which prints 0 either way, and the patch-applies row compared a literal with itself. The numeric rows matched by substring, so exit status 134 satisfied "0". Case 4 of the fix leg contributed to the clean count with no answer of its own, and five of the twelve defective sites -- GetInt64 and WriteReadable in both files, Document's IsFloatingPointType -- were named in the report but never called. The ESBMC rows were about a transcription of the fix; EQUIVALENCE now carries the shipped helper beside the model and asserts they agree, and mutating the shipped copy breaks it. The delta leg pins the diff's content by hash, since a line count would not notice a bounded write swapped for an unbounded one. Two stubs still described the stream-buffer target.
5e9 is kept as a literal too -- parse_number's bound is int's, not int64's -- so J-3 corrupts a value the SDK could have represented exactly, which is a stronger statement than 1e300 reading as 1 and it was missing from both write-ups. Also says what the ESBMC rows are about now that EQUIVALENCE pins them to the shipped helper, marks the fork-versus-upstream reading as a human judgement rather than a checked property, explains why the writers return an empty string, notes the stale valuestring in SetNumberHelper that the patch leaves alone, and corrects four line citations and three quoted ranges.
…defect
The report claimed the literal-keeping feature was absent at 1.9.99 and so
predated everything; it is present there, under the pre-rename cJSON_strdup at
aws-cpp-sdk-core/source/external/cjson/cJSON.cpp:361-366. J-1 and J-2 do
predate. J-3 does not: until 1.11.659 the guard was `isInteger`, cleared on
e/E as well as '.', so an exponent form kept no literal and AsInt64 answered
5000000000. Commit 87042947e93a replaced the flag with has_decimal_point, which
only '.' sets. Built against each release's own cJSON.cpp -- AsInt64 is
byte-identical across the change -- {"n":5e9} gives 5000000000 at 1.11.659 and 5
at 1.11.660, which tag bisection pins as the first release carrying it.
Also corrects three claims a reviewer would check in one grep: the ESBMC
equivalence row proves model-vs-transcription, not the shipped helper, since
nothing feeds the patch to ESBMC; Aws::InitAPI does install cJSON hooks
(Aws.cpp:165-168), and the allocator model is faithful because they fall through
to malloc, not because they are absent; and the J-2 evidence table listed two of
the four Document sites where the summary listed all four.
J-1's 26th character was asserted from the failing side only, and J-2's four GetInt64 sites -- the ones the whole reachability argument rests on -- were never asserted at all, on either accessor. The post-fix sanitizer sweep skipped the Document path entirely, so half of "the patched tree is clean" was claimed rather than measured. Adds eight witness cases and fifteen checks, 55 to 70. The load-bearing pair is 2^63 and -2^63: the smallest double outside int64's range must saturate and its representable counterpart must not, which is exactly what a guard written `d <= (double)INT64_MAX` gets wrong, since that conversion rounds up to 2^63. Mutating the fix that way produces six diagnostics -- three on the newly swept Document path -- and reads 2^63 back as INT64_MIN, so the rows fail as intended. Also stops the log-guard check matching AWS_LOG's guard when J-1 runs through AWS_LOGSTREAM's, and renames the ESBMC equivalence row to say what it proves.
…t lied stubs/aws/crt/Types.h was copied from the streambuf artifact and kept six declarations nothing here references, plus two comments describing PreallocatedStreamBuf and HashingUtils -- neither of which exists in this tree. They were the only citations in the artifact that did not check out. ByteBuf and get_aws_allocator stay; Array.h needs them. reproduce.sh now cds to its own directory first, so running it from elsewhere fails on the thing that is actually wrong instead of reporting "no network" from a malformed URL. Scratch trees are tracked in one list with a single EXIT trap rather than a RETURN trap that would outlive its function and fire on a stale variable. The fuzz corpus is rebuilt per run, since libFuzzer writes new inputs into it and the "60,000 executions" were drifting from the seeds.
A VERIFICATION FAILED verdict says a violating double exists; it does not hand anyone a test they can run. This adds ESBMC's test-case generation (--branch-coverage --generate-ctest-testcase) over a harness that splits the conversion's input into the three regions its precondition distinguishes, so the solver names a concrete double in each: on our runs 2^63, a representable value, and about -2^64. The generated CMakeLists.txt would rebuild the harness with those values, which only re-runs the model. json_number_replay.cpp links the generated __VERIFIER_nondet_double() against the real JsonSerializer.cpp and Document.cpp, renders the double as a response body and reads it back as a generated deserializer would -- so the witness is executed against the SDK. Two of the three are undefined on the pristine accessors and all three are clean under the patch. The driver checks the rendered text parses back bit-identical first; rendering with %.6g makes that check fire. Seventh leg, 70 to 76 checks. It witnesses J-2, whose precondition is a property of the value; J-1 and J-3 are properties of the literal text and stay with the native witness.
The suite led with sanitizers and reached for ESBMC afterwards, and only for J-2 -- so the tool that should be doing the finding was reduced to seconding a diagnostic. Now each defect is stated as a property over symbolic input, with no harness naming a triggering value: J-1 over the literal's length, J-2 over the double, J-3 over the mantissa and exponent. All three are refuted under both solvers, and J-3's defect is found in ESBMC's own atoll model rather than in anything we wrote. Each then gets a region-splitting harness so the test-case generator has to name a concrete value per region, and a replay driver that links those values against the real JsonSerializer.cpp and Document.cpp under ASan and UBSan. Eight witnesses: one aborts, two are undefined, one reads back wrong, and all eight are clean under the patch -- checked as presence of an answer, since absence of a crash also describes a binary that did nothing. Where ESBMC could not analyse the SDK's own source the reason is recorded rather than worked around: it does not finish on cJSON.cpp, a second C++ TU loses its function bodies with no diagnostic, snprintf does not return the length C11 7.21.6.5p3 requires, and the C++ frontend rejects StringUtils.cpp. The claim is that ESBMC finds these from symbolic input, not that it did so first; the 2^63 boundary it picks was also reached by hand, independently. Legs reordered esbmc -> ctest -> sanitizer, 76 to 106 checks, and the run now pins its own total so a leg returning early cannot read as a shorter suite. Corrects atoll's UB citation to C11 7.22.1p1 -- 7.22.1.2p3 is the Returns clause -- and three line references that pointed at J-2's sites while describing J-3's.
A review of the previous commit found the J-2 replay's pristine rows still bucketed on "no sanitizer diagnostic", which a binary that printed nothing also satisfies -- the asymmetry the patched side had already fixed. Counts the answer beside it; muting the driver's printfs now turns three rows red instead of one. Also drops an overshooting claim -- the sanitizer leg does more than confirm what ESBMC names, since its fifteen bodies are chosen by hand and go further -- and corrects two comments: the else arm is four lines below the literal arm, not two, and ensure() tests INT_MAX twice, before and after adding the buffer's offset. Unsplices a paragraph in the fix section whose StringUtils sentences had ended up attached to the wrong bullet.
Three timed runs of the full suite from a fresh unpack land at 4m37-4m45, not the ~3 min both documents quoted; the figure predates the ESBMC rows the suite has since grown. Nothing else changes.
AWS closed all three in aws/aws-sdk-cpp#3921, merged 2026-09-10 and first tagged in 1.11.891: the fix/ patch's logic with its helpers moved to a new NumericUtils.h, shipped as a bug fix with no advisory. The witness table rebuilt against the 1.11.891 files matches the patched tree on all 30 runs.
lucasccordeiro
added
documentation
lucasccordeiro
force-pushed
the
verify/cjson-esbmc
branch
from
September 27, 2026 15:40
22a813c to
2aba4bb
Compare
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.
The JSON number read path in
JsonValue/Documenthas three defects at 1.11.886, all reachable from a service response: a 26+ character number aborts the process onWriteCompact/WriteReadable(J-1), an out-of-range double hits UB in fourstatic_cast<long long>sites (J-2), and{"n":5e9}reads back as5, a regression since 1.11.660 (J-3).ESBMC finds all three from symbolic input, and its counterexamples are replayed against the pristine SDK under ASan/UBSan.
fix/closes them.Reported to AWS on 2026-09-05 and fixed upstream in aws/aws-sdk-cpp#3921, first shipped in 1.11.891, which matches our patch on all 30 witness runs.
See verification/cjson/;
./reproduce.shruns 107 checks in ~5 min.