{"id":"a431bdd6-98fa-44f6-bd95-668b2751b4d2","arxiv_id":"2509.03711","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"Griller detects vulnerabilities by fuzzing functions in isolation and then filtering out crashes that are unreachable in the full program context.","lead":"This paper presents Griller, a tool that tests individual functions of a program for bugs and then checks whether the bug-triggering inputs can actually be reached from the program's real entry point. It found 28 of 48 known vulnerabilities in five open-source projects and six previously unknown bugs in programs like the Pacman package manager.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Complete-backtracking precision may be unsound because global variable values are not carried through constraint stitching across separately executed drivers.","rationale":"The reader's weakest assumption focused on path consistency between concrete fuzzing and KLEE's pre-constrained symbolic execution, which is a real concern acknowledged in A.10.4. I agree that constraint extraction soundness is load-bearing, but I see an even more direct threat to the 100% precision claim: the stitching procedure itself may omit a class of program state (global variables) that can determine whether a crash is reachable from main. The paper's own A.6 statement indicates this is a deliberate design choice rather than an accidental omission, which makes it a concrete, checkable correctness risk. The proposed toy test isolates this single mechanism: if Griller's complete-backtracking filter accepts a crash that depends on a global fixed to a safe value by main, then the central validation claim fails. This does not invalidate the entire paper, but it means the paradigm's key guarantee should be conditioned on explicit handling of global state, or demonstrated on such cases. The reader's conditional verdict already captures the need for additional validation, so I do not propose changing the verdict; the condition should be sharpened to include global-state stitching.","tokens_in":27701,"tokens_out":7123,"duration_ms":86447,"concrete_test":"Construct a minimal C program: global int G; void target(int *p) { if (G == 0) { volatile char *q = 0; *q = 1; } } void caller(int x) { if (x > 0) G = 5; target(&x); } int main() { G = 1; caller(read_stdin_int()); }. Run Griller end-to-end with target selected. If Griller reports the target crash as completely backtracked and valid, the global state was not stitched and the 100% precision claim is false for global-dependent crashes. If it reports the crash as infeasible or as a partial-backtracking false positive, inspect the Program Database to confirm an equality constraint on G was propagated across both call edges.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is that when Griller's backtracking reaches main, reported crashes are both reachable and triggerable, with 100% precision (§5.1). This requires each stitched call edge to carry all program state that can influence the target's crash constraint. However, §4.5 defines edge constraints as a path condition plus symbolic argument values at the callsite, and A.6 explicitly says global variable values are not extracted because they are 'shared across the program and automatically included in the symbolic state.' That reasoning fails because Griller executes each driver separately: the target function's KLEE run, the caller's KLEE run, and the grand-caller's KLEE run are independent symbolic executions. A global variable read by the target function is symbolic in the target's run, while in the caller's run the same global may be initialized differently or set to a concrete value before the call. If that global's value is not printed and stitched at the callsite, the stitched constraint can leave the target's global-dependent condition as a free variable, so the solver may report satisfiability even when the real call chain fixes the global to a non-crashing value. The paper's 100% precision for complete backtracking is therefore unsupported for crashes whose constraints depend on globals, unless an undocumented global-stitching step exists.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces Reactive Bottom-Up Testing (Reactive BOUT), an approach that tests individual functions in isolation and then validates discovered crashes against the surrounding program context. The proposed system, Griller, operates in three stages: (1) selecting target functions and generating type-aware harnesses; (2) fuzzing the harnesses and, for each crash, using pre-constrained KLEE execution to extract a crashing constraint; (3) backtracking along the program call graph and stitching the crash constraint with symbolic argument values and path conditions at each call edge, reporting only crashes whose stitched constraints are satisfiable up to main. The evaluation uses 48 confirmed CVEs across five projects, reporting 28 detected vulnerabilities with 6 false positives, and six previously unknown vulnerabilities in mblaze, pacman, and pspg, four of which were patched. The paper claims 100% precision for the 15 vulnerabilities whose backtracking reached main.","tokens_in":28041,"tokens_out":6225,"duration_ms":67266,"significance":"If the central precision claim holds, the reactive strategy is a meaningful improvement over proactive BOUT and whole-program fuzzing, because it decouples deep function analysis from the expensive reachability problem and filters only the bug-triggering states. The paper is honest about limitations: it reports false positives separately for partial backtracking, states that global values are not extracted (A.6), and acknowledges path divergence in KLEE (A.10.4) and concrete input generation difficulties (§5.4). The 28/48 detection result and the six zero-day disclosures (four patched) are concrete, falsifiable outputs. However, no machine-checked proof or released artifact is provided, and the load-bearing validation step—constraint stitching—has a gap concerning global variables that directly affects the claimed 100% precision for complete backtracking. The empirical comparison to AFGen is weakened by reliance on published numbers on a refined dataset. Overall, the contribution is potentially significant but requires a fix and a more guarded evaluation before the precision claim can be accepted.","major_comments":[{"comment":"The claim in §5.1 that complete backtracking achieves 100% precision is not supported for crashes involving global variables. Edge constraints are defined as path condition plus symbolic argument values at the callsite (§4.5). A.6 explicitly says global variable values are not extracted because they are 'shared across the program and automatically included in the symbolic state.' This reasoning is incorrect under Griller's own execution model: the target driver and each caller driver are separately generated and separately executed, so the global variable in the target run is a different symbolic variable (or concrete value) from the global in the caller run. No equality constraint is generated at stitching. Consequently, a stitched constraint can leave a global-dependent crash condition as an unconstrained symbolic variable, and the solver may report satisfiable even though the actual c","section":"A.6 / §4.5 / §5.1"},{"comment":"The comparison to AFGen is not direct. Griller is not run against baselines; it relies on published AFGen results. The dataset is refined post hoc using criteria (active maintenance, verification, reproducibility) that remove targets from AFGen's original list. Target functions are manually supplied from vulnerability reports, so the target identification component is not tested end-to-end; RQ2's ranking result does not demonstrate the full pipeline. This weakens the claims of being 'comparable with AFGen' and 'outperforming AFL++ and Beacon.' Please either run the baselines on the same versions and inputs, or present the comparison only as a reference point and clearly label the dataset differences and manual target selection.","section":"§5.1 / A.8"},{"comment":"The false-positive filter assumes identical execution paths in native fuzzing and pre-constrained KLEE. The paper itself lists floating-point operations and pointer-arithmetic based control flow as causes of KLEE path divergence (A.10.4). If divergence occurs, path constraints are not the path of the crashing input, and stitching can return incorrect satisfiability. The paper does not quantify divergence for the 15 complete-backtracking cases. Please provide a per-case check (e.g., compare path constraints with the observed path, or count cases where seed patching was required) and discuss the impact on the 100% precision claim.","section":"Challenge 2 / A.10.4"}],"minor_comments":[{"comment":"The sentence beginning 'For each of the 20' is incomplete; it should refer to the 20 undetected CVEs and state the failure analysis criteria.","section":"§5.1"},{"comment":"The column header 'Ver / Prog' is ambiguous. Please clarify the version/program layout, e.g., with separate columns or an explicit explanation.","section":"Table 3"},{"comment":"Multiple code listings contain stray 'ὁB' characters that appear to be rendering artifacts. These should be removed or replaced with the intended markers.","section":"Listing 1"},{"comment":"The loop indentation in Algorithm 1 obscures that the score is summed inside the loop. Please restructure the pseudocode to make the loop body explicit.","section":"Algorithm 1"},{"comment":"The paper does not state an artifact availability policy. Please include a link or explicitly state that the code will not be released.","section":"General"},{"comment":"Typos: 'Leapord' should be 'LEOPARD', 'Constriant' should be 'Constraint', and 'experimetn' should be 'experiment'.","section":"A.3.3 / A.10.4"}],"recommendation":"major_revision","confidential_remarks":"The paper is within the scope of the journal and the central paradigm is worth considering, but the global-variable stitching gap is a real correctness issue for the headline precision claim. I believe it is fixable by extending the TypePrinter and adding global-equality constraints, so I recommend major revision rather than rejection. The authors should also be encouraged to strengthen the AFGen comparison or soften the comparative wording. The zero-day results are solid evidence of utility even if the 100% precision claim needs qualification."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The reactive framing is the real contribution here: instead of proactively generating feasible states like AFGen, Griller fuzzes the target function unconstrained and then filters infeasible crashing states by stitching symbolic constraints across call edges. That is a genuinely different way to think about bottom-up testing, and the 28/48 known-vulnerability detection plus six zero-days (four patched) show the approach works in practice. The harness generation, symbolic size/null tracking, and staged backtracking are substantial engineering, and the paper is honest about partial backtracking and KLEE path divergence.\n\nThe main soft spot is the precision claim. The paper says that when backtracking reaches main, all reported crashes are true positives (100% precision). That holds only if the stitched constraints carry everything that can affect the crash. They don't. Section A.6 says global variable values need not be extracted because they are \"shared across the program and automatically included in the symbolic state.\" That is wrong for Griller's design: each driver is a separate KLEE run, and the harness generates globals from stdin, so a global-dependent crash constraint in the target's run is stitched into the caller's run without constraining that global to the actual value the caller would see. At the main level the driver still makes globals symbolic, so the solver can pick a global value that no real execution produces. The stress-test note is correct: the 100% precision result is unsupported for crashes that depend on globals. This is a load-bearing flaw in the central claim, though not in the overall approach — many crashes depend on arguments, and the partial backtracking results are still useful.\n\nThe evaluation also has the weaknesses the reader flagged: AFGen, AFL++, and Beacon numbers are taken from a different paper rather than reproduced, the dataset was refined post hoc, and Griller was given the vulnerable functions from CVE reports. That makes the comparison to AFGen apples-to-oranges. The paper is transparent about this, but it means the \"comparable to state-of-the-art\" claim is weaker than it looks.\n\nWho is this for? Security researchers and tool builders in fuzzing and symbolic execution. It is a systems paper with a novel framing and useful empirical findings, and it deserves a serious referee. The global stitching issue and the indirect baseline comparison both need to be addressed before publication, but the core idea is sound and worth engaging with.\n\nRecommendation: send to peer review, major revision expected.","headline":"A credible reactive twist on bottom-up fuzzing with a real precision gap around global variables; worth refereeing, but the headline 100% precision claim needs fixing.","tokens_in":28520,"tokens_out":2811,"would_cite":true,"duration_ms":32562,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper introduces Reactive Bottom-Up Testing: fuzz a function in isolation, capture each crash as a symbolic constraint, then stitch that constraint backward through the call graph so only reachable, triggerable vulnerabilities are repor","keywords":["reactive bottom-up testing","constraint stitching","function-level fuzzing","symbolic execution","crash reachability","false positive filtering","call graph backtracking","vulnerability detection"],"falsifier":"For any crashing input, log the sequence of taken branches or a coverage-trace hash under both the fuzzing harness and the pre-constrained symbolic run. If the two traces differ, the path-consistency premise is violated; if Griller still reports such a crash as feasible from main, the false-positive filter is unreliable for that case.","tokens_in":27614,"feed_emoji":"🐛","tokens_out":9712,"duration_ms":99142,"temperature":0.7,"pith_summary":"Most fuzzing starts at the program's entry point, so vulnerabilities hidden deep in the call graph are hard to reach. The paper argues that testing a function in isolation finds bugs fast but is not enough: a crash in isolation may be unreachable from the real program's inputs. Its answer, Reactive Bottom-Up Testing, fuzzes a target function with an automatically generated harness, turns each crashing input into a symbolic constraint, and then walks backward up the call graph, stitching that constraint with each caller's path condition and argument values to see whether the crash is feasible from main. The prototype Griller reproduced 28 of 48 known vulnerabilities, found 6 previously unknown ones, and every completed backtrack to main was a confirmed true positive. The point is to spend reachability analysis only on states that are already known to trigger bugs, not on all feasible states up front.","feed_headline":"Fuzz functions alone, then stitch crashes back to main","feed_subtitle":"Three-stage bottom-up tester verifies each crash is reachable, cutting false positives and finding deep bugs.","key_machinery":"The load-bearing mechanism is constraint stitching. A crash in a target function is first represented as a crash constraint: the path conditions that led to it conjoined with a root-cause assertion such as 'this pointer is NULL' or 'this buffer is too small.' For every call edge above the target function, Griller records an edge constraint pair: the path condition needed to reach the callsite and the symbolic values of the arguments passed at that callsite. Stitching substitutes the callee's crash constraint into the caller's argument values and conjoins the caller's path condition; if the result is unsatisfiable, the crash is infeasible from that callsite and is dropped. The same stitched c","core_discovery":"Griller's central claim is that the way to make bottom-up testing practical is to be reactive: do not spend effort enumerating feasible program states before testing a function; instead, test the function with an automatically generated, context-aware harness, collect crashing inputs, and only then ask whether any crash is feasible in the whole program. Feasibility is decided by symbolic constraint stitching. Each crashing input is replayed under pre-constrained symbolic execution to produce a crash constraint: the path constraints that led to the crash conjoined with a root-cause assertion. Starting at the target function's caller, Griller conjoins that constraint with the path condition fo","pith_inferences":["Editorial: The stitching machinery only needs a crash constraint, not a particular crash type; injecting root-cause assertions for other observable properties such as assertion failures, leaks, or races would let the same reactive paradigm verify those properties too.","Editorial: The 100% precision figure depends on concrete and symbolic executions taking the same path; adding a runtime branch-trace comparison that fails loudly on divergence would convert a silent accuracy risk into an explicit diagnostic.","Editorial: With per-call-edge symbolic state persisted in the program database, incremental testing after a code change could re-analyze only the affected edges, which would make the approach more practical in continuous integration.","Editorial: The current implementation is source-based; a binary-level port would need equivalent type inference and instrumentation, but the conceptual claim about reactive feasibility checking does not depend on source access."],"forward_implications":["A bottom-up tester no longer needs to generate feasible program states up front: fuzzing the target in isolation finds crashes quickly, and reachability is decided only for the small set of crash-triggering inputs.","Every crash whose constraint stitches successfully all the way to main is reported with a validated path to the entry point, so a developer sees both the bug and a concrete route to it.","The staged design stores symbolic state per call edge, so multiple crashes and multiple target functions can reuse the same backtracking information instead of re-exploring the program from scratch.","In the evaluation, complete backtracking to main achieved 100% precision, and Griller triggered 6 crashes that no baseline fuzzer triggered, making the approach complementary to top-down and directed fuzzing."],"supporting_citations":[{"why":"defines Bottom-Up Testing, the paradigm this work extends with a reactive feasibility check","marker":"[21]"},{"why":"supplies the benchmark dataset of 48 known vulnerabilities and the published detection counts that Griller is compared against","marker":"[32]"},{"why":"provides the coverage-guided fuzzing engine used to find crashes in the generated harnesses","marker":"[13]"},{"why":"supplies the symbolic execution engine used for pre-constrained execution and crash-constraint extraction","marker":"[7]"},{"why":"provides the SMT solver that decides satisfiability of stitched constraints and extracts unsat cores","marker":"[11]"},{"why":"supplies the type-inference technique used to distinguish array pointers from scalar pointers in harness generation","marker":"[47]"},{"why":"supplies the correlation analysis that links pointer arguments to their size parameters for context-aware harnesses","marker":"[50]"}],"fun_headline_variants":["Bottom-up fuzzing, stitched to reality","Fuzz first, verify reachability later","Test functions, then prove crashes reachable","Griller: bottom-up testing that cuts false positives","Reactive bottom-up testing finds deep bugs"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The load-bearing premise is that the crashing input forces the same execution path under native fuzzing and under pre-constrained symbolic execution; if the paths diverge, the stitched feasibility check can return a wrong satisfiability answer.","fun_headline_variants_meta":{"raw":{"variants":["Bottom-up fuzzing, stitched to reality","Fuzz first, verify reachability later","Test functions, then prove crashes reachable","Griller: bottom-up testing that cuts false positives","Reactive bottom-up testing finds deep bugs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000178,"raw_usage":{"total_tokens":1158,"prompt_tokens":797,"completion_tokens":361,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":541,"completion_tokens_details":{"reasoning_tokens":291}},"tokens_in":541,"tokens_out":361,"duration_ms":3830,"temperature":1.0,"reasoning_tokens":291,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T10:43:41.463132+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"For any crashing input, log the sequence of taken branches or a coverage-trace hash under both the fuzzing harness and the pre-constrained symbolic run. If the two traces differ, the path-consistency premise is violated; if Griller still reports such a crash as feasible from main, the false-positive filter is unreliable for that case.","supporting_citations":[{"cited_title":"ISO/IEC/IEEE 24765:2010 - Systems and soft- ware engineering – V ocabulary","cited_arxiv_id":null,"evidence_quote":"defines Bottom-Up Testing, the paradigm this work extends with a reactive feasibility check"},{"cited_title":"Afgen: Whole-function fuzzing for ap- plications and libraries","cited_arxiv_id":null,"evidence_quote":"supplies the benchmark dataset of 48 known vulnerabilities and the published detection counts that Griller is compared against"},{"cited_title":"AFL++: Combining incremental steps of fuzzing research","cited_arxiv_id":null,"evidence_quote":"provides the coverage-guided fuzzing engine used to find crashes in the generated harnesses"},{"cited_title":"Ccured: Type- safe retrofitting of legacy software","cited_arxiv_id":null,"evidence_quote":"supplies the type-inference technique used to distinguish array pointers from scalar pointers in harness generation"},{"cited_title":"Locksmith: Practical static race detection for c","cited_arxiv_id":null,"evidence_quote":"supplies the correlation analysis that links pointer arguments to their size parameters for context-aware harnesses"}],"review_version":1}