{"id":"5777b45c-cefd-423a-8fe5-03d2b6f7e56b","arxiv_id":"2505.12690","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A new black-box tool uses active automata learning with timing variations and pairwise differential analysis to expose 55 QUIC handshake faults, five CVEs, and an RFC ambiguity.","lead":"QUICtester learns finite-state behavior models of QUIC server implementations and compares them to flag specification violations. It found 55 real faults across 19 servers, including a DoS and an authentication bypass, earning five CVEs and two bug bounties.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Output symbols are pruned before differential comparison, so output-only noncompliance may escape the automated analyzer and undercut the central 'automated noncompliance' claim.","rationale":"The reader's weakest assumption, completeness of the hand-built symbol dictionary, is real and explicitly acknowledged in Section 7, but it does not threaten the existence of the 55 findings. My concern is different and, to my reading, not addressed: the automated comparison stage discards output information, which is precisely where protocol noncompliance often manifests. The paper deserves credit for shipping code, PoCs, CVEs, and manual root-cause case studies; those independently support the empirical findings. However, the central methodological claim that pairwise differential analysis of learned models automatically identifies noncompliance is weakened if the pruned comparison cannot see output-only deviations. A conditional acceptance asking the authors to clarify or fix this issue is appropriate, alongside the acknowledged symbol-completeness limitation. My agreement with the reader is partial: both concerns are about completeness of the learned abstraction, but the reader pointed to input symbolization while I point to the output-alphabet pruning inside the analyzer itself.","tokens_in":33718,"tokens_out":11434,"duration_ms":129878,"concrete_test":"Take the optimized learned models used for the S-11 (PQUIC PSK) and S-15 (Quant Basic) findings and rerun the Differential Analyzer twice: once exactly as described in Section 3.3 (outputs pruned) and once with output labels retained in the LTS_Diff input, i.e., on the original Mealy machines. If the S-11/S-15 deviations appear only in the output-retained comparison, the published pipeline could not have detected these faults automatically and the 'automated' claim fails for this class. If they appear in both comparisons, the pruning does not hide the reported faults and the concern is refuted. Add a minimal synthetic control pair that differs only in one output label on an otherwise identical source/input/target transition to confirm the pruning behavior directly.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim is that pairwise differential analysis of learned models identifies non-compliance instances automatically and property-agnostically. In Section 3.3 (C6), however, the authors state: 'We prune all the output symbols from the optimized learned models and use the Labeled Transition System Differential (LTS_Diff) algorithm.' LTS_Diff then compares only state and input-transition structure. A QUIC server's noncompliance can consist solely of emitting the wrong response while remaining in the same abstract state, e.g., S-11 (PQUIC 'Does not send HANDSHAKE_DONE after the handshake is confirmed') and S-15 (Quant 'Incorrect handling of an initialPing message') are output-behavior faults. Under output pruning, two models that agree on all inputs and state changes but differ in an output label are indistinguishable; the automated analyzer will not flag them. The 55 faults in Table 2 are presented as QUICtester findings, but the paper does not show which were discovered by the pruned differential analyzer versus by manual model/source inspection. Without that separation, the 'automated noncompliance checking' contribution and the property-agnostic, no-formal-model claim are overstated. This is an internal-consistency concern, not a disagreement with the security community.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents QUICtester, a black-box framework that uses active automata learning (LearnLib TTT algorithm with Wp-method conformance testing) to infer finite state machine models of 19 QUIC server implementations under five handshake security configurations. The learning alphabet is a manual symbolization of 30 QUIC messages and parameters, parameterized by short and long timeouts, and the framework includes a custom test harness, a model optimizer, a crash logger, and a differential analyzer based on LTS_Diff. The authors report 55 confirmed faults across the implementations, including 44 specification violations, 8 memory-corruption bugs, and 3 logical flaws, with 5 CVEs and two bug bounties awarded. They also identify a QUIC specification ambiguity around initial packets without a CRYPTO frame and propose an RFC amendment.","tokens_in":33998,"tokens_out":6516,"duration_ms":67325,"significance":"If the claims hold, this is a significant contribution: it is the first open-source black-box noncompliance checker for the ratified QUIC protocol, and it provides concrete external validation through developer-confirmed fixes, CVE assignments, bug bounties, and reproducible PoCs. The time-parameterized learning idea is genuinely novel and is essential to finding M-4, which is a compelling case study. The curated reference models and public repository are useful assets for future testing. The paper is also unusually candid about its limitations, including the unfaithful-oracle problem and possible symbolization gaps. The main weakness is that some central claims go beyond what the automated pipeline as described can actually deliver.","major_comments":[{"comment":"The automated differential analysis cannot detect output-only noncompliance. Section 3.3 states: \"We prune all the output symbols from the optimized learned models and use the Labeled Transition System Differential (LTS_Diff) algorithm.\" Several faults in Table 2 are output-only by nature: S-11 (PQUIC does not send HANDSHAKE_DONE after the handshake is confirmed), S-15 (Quant incorrect handling of an initialPing message), and S-6 (MsQuic does not issue its initial_source_connection_id at the correct connection state). Two models that agree on all inputs and state transitions but differ only in emitted symbols are indistinguishable after output pruning, so these faults cannot be flagged by the automated analyzer. The paper needs to state, per fault or per category, which findings were produced by the differential analyzer, which by the crash logger, and which by manual model or source inspection, and either extend the comparison to output symbols or revise the abstract and contribution claims from \"automated noncompliance checking\" to \"automated deviation discovery followed by manual confirmation.\"","section":"3.3 (C6)"},{"comment":"The \"no false positives\" claim conflates automated deviation detection with manual validation. Section 4 says deviating behaviors were validated manually and that crashes, trace data, and crashing seeds were examined as a separate source; Section 7 adds that all 186 models were manually validated. Therefore the zero-false-positive statement is a property of the combined human-in-the-loop pipeline, not of the Differential Analyzer alone. Please report the raw number of candidate deviations produced by LTS_Diff and how many were discarded as benign implementation variation, such as the differing initialPing behaviors in Section 5.4. This would let the reader assess how much of the 55-fault result is automated and how much is due to the authors' subsequent manual analysis.","section":"4 and 7"}],"minor_comments":[{"comment":"The abstract contains a duplicated word: \"analyze analyze 186 learned models.\"","section":"Abstract"},{"comment":"The first paragraph of Section 2 contains the typo \"addbefore\" in \"active automata learning addbefore delving.\"","section":"Section 2"},{"comment":"The heading \"S-18 Client Authentication Bypass in Quiche\" uses S-18, but Table 2 lists the Quiche client-authentication bypass as S-12; renumber or cross-reference consistently.","section":"Section 5.1"},{"comment":"In the M-4 case study, the text refers to \"Figure 8 in the Appendix,\" but Figure 8 appears in the main body; the cross-reference should be updated.","section":"Section 5.2"},{"comment":"The text refers to \"M-18\" in connection with QUT status detection, but Table 2 has M-8 as the Quinn panic; the numbering is inconsistent.","section":"Appendix A.1"},{"comment":"The output-symbol descriptions for <ConnectionActive> and <ConnectionClosed> appear swapped relative to the prose in Section A.1: the table says <ConnectionActive> indicates the QUT has closed the connection while <ConnectionClosed> indicates the connection is still active, which is the reverse of the surrounding text.","section":"Appendix Table 8"}],"recommendation":"major_revision","confidential_remarks":"The empirical security results are strong and independently valuable, and the authors are candid about their limitations. The revision burden is mainly about aligning the paper's claims with what the automated pipeline actually does: the output-symbol pruning and the manual validation steps need to be reflected in the wording of the contributions and in a per-finding attribution of discovery method. I do not see a basis for rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this paper is legitimate and the main results hold up. The team built the first active-automata-learning plus differential-analysis framework for the ratified QUIC handshake, covering all five security configurations, and ran it across 19 open-source implementations. The headline findings - a client-auth bypass in Cloudflare's Quiche, DoS via retained Initial keys in Kwik and XQUIC, the Picoquic race - are confirmed by five CVEs and two bug bounties. The genuinely new idea is time-parameterized learning: parameterizing input symbols with short/long/mixed waits exposed a Picoquic segfault that a single-timeout learner would not have reached. That alone is a real contribution, and the curated reference model library is a useful artifact.\n\nThe undercarriage is honest. LearnLib TTT with Wp-method conformance testing, LTS_Diff, standard pipeline. Code and PoCs are open-sourced. They even report a failed LLM-based symbolization attempt (69% miss rate) instead of hiding it. The load-bearing assumptions - hand-built symbol dictionary completeness and the 'all implementations could share a bug' oracle caveat - are stated in plain words in Section 7. The empirical findings are anchored to RFC text and developer fixes, not to the tool's own output, so there is no circularity problem.\n\nWhere the paper overreaches: the 'automated, property-agnostic' differential analyzer. Section 3.3 prunes all output symbols before running LTS_Diff, so the comparison sees states and input transitions only. Output-only faults - PQUIC not sending HANDSHAKE_DONE (S-11), Quant's initialPing handling (S-15) - cannot be flagged by that automated step, since two models can share every transition and differ only in what they emit. The paper never attributes the 55 faults across the differential analyzer, the crash logger, and manual model/source inspection; and ~10 minutes of human validation per model (1860 minutes total) is disclosed, which further softens the 'automated' framing. That is a revision issue, not a rejection issue: add a per-fault attribution table and either keep outputs in the comparison or say plainly that output-behavior faults required human eyes.\n\nMinor: fault numbering is inconsistent (S-18 vs S-12 for the Quiche bypass; a stray 'M-18' in Appendix A.1), and 'no false positives' needs the same caveat, since spec-ambiguity deviations had to be classified by hand.\n\nWho this is for: protocol state fuzzing / noncompliance-checking researchers and QUIC implementers. It deserves a serious referee. I would accept pending a clear response on the automated-versus-manual split.","headline":"Real findings and a genuinely new timing-aware learning idea, but the 'fully automated' differential analysis is weaker than claimed because outputs are pruned before comparison - worth a revision, not a rejection.","tokens_in":34543,"tokens_out":7484,"would_cite":true,"duration_ms":73638,"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":"By learning each QUIC server as a state machine, a black-box checker found 55 faults, 5 CVEs, and a DoS flaw across 19 implementations—with no formal model.","keywords":["QUIC","protocol noncompliance","active automata learning","differential analysis","state machine inference","denial-of-service","RFC 9000","black-box testing"],"falsifier":"Plant a deliberately non-conforming behavior in a QUIC server that triggers only on a message type or parameter combination outside the 30-symbol dictionary (for example, an exotic transport parameter value), run the full learning and pairwise differential pipeline with that server added to the original 19, and check whether the planted deviation produces any flagged edge; if it does not, the dictionary is shown to be the coverage ceiling. A complementary check: introduce the same bug into all 19 implementations and observe that the differential analyzer reports nothing, because its oracle is purely comparative.","tokens_in":33474,"feed_emoji":"🐛","tokens_out":12272,"duration_ms":106306,"temperature":0.7,"pith_summary":"The paper claims that QUICtester, an open-source black-box testing tool, can automatically surface non-compliant and vulnerable behaviors in QUIC server implementations without a formal reference model to check against. The tool learns each server's behavior as a finite state machine by actively probing it with valid and invalid QUIC messages at different timing intervals, then compares the learned machines across many implementations so that deviations stand out. Tested on 19 open-source QUIC servers across all five handshake security configurations, it reports 55 confirmed implementation faults: 44 specification violations, eight memory-corruption bugs, and three logical flaws, many of which enable denial-of-service attacks. If correct, this reduces protocol noncompliance checking for QUIC to an automated pipeline, and the paper's curated set of conforming reference models lets developers check new implementations against a known-good behavior baseline.","feed_headline":"Black-box probing finds 55 bugs in QUIC servers","feed_subtitle":"Learned state machines from 19 implementations catch spec violations, crashes, and a DoS flaw—no formal model needed.","key_machinery":"The working core is active automata learning paired with differential comparison of the learned state machines. A Learner implementing the TTT algorithm with Wp-method conformance testing generates input sequences from a manually curated dictionary of 30 symbols, which encode QUIC packet types, frames, cipher suites, configuration toggles, and two timing intervals; a Test Harness translates each symbol into real QUIC packets and back, maintaining encryption keys across all five handshake configurations. Each server's observable behavior is thereby abstracted into a finite state machine whose transitions are labeled by input and output symbols. An Optimizer drops self-loops and merges timing variants that lead to the same next state, removing up to 90 percent of edges in the best case, and then a Differential Analyzer using the LTS_Diff algorithm compares models pair by pair: the same server under short versus long timing, and every model against every other implementation's models, yielding the deviating input sequences for manual confirmation. A Crash Logger watches the server's process after each learning step so that crashes triggered by specific inputs are recorded even when hidden from the learned model.","core_discovery":"The paper's central claim is that noncompliance in QUIC implementations can be detected without a formal reference model, by treating the ecosystem of many independent implementations as the oracle. QUICtester learns a finite state machine for each server through active automata learning, then runs pairwise differential analysis on the learned models: any state or transition present in one model but absent in another is flagged as a deviation, and each deviation is then validated by hand to confirm it is a genuine fault. The method's distinctive addition is time-parameterized learning: inputs carry a short or long wait interval, chosen automatically per implementation before learning, so timing-dependent behavior such as retransmission handling and key discard appears as distinct states. Applied to 19 open-source QUIC servers under all five security configurations, the pipeline produced 186 learned models and 55 confirmed faults: 44 specification violations, eight memory-corruption bugs, and three logical flaws, including a client-authentication bypass in Quiche, a crash in Picoquic reachable only through short-timing inputs, and a specification ambiguity over connectionless first packets that lets servers be forced into creating connection contexts. The findings led to five CVE assignments and two bug bounties, and the authors curate 11 conforming reference models so that future targets can be checked against a known-good baseline.","pith_inferences":["The dictionary sets the discovery ceiling, which makes the completeness claim testable: re-run learning with the symbol set augmented by fuzz-discovered or newly observed message variants; if new deviations appear, the published dictionary was incomplete, and if none do, its coverage is empirically supported.","The purely comparative oracle has a common-mode blind spot the authors concede: a noncompliance shared by every tested implementation is invisible, so the method's assurance is relative to the diversity of the test set rather than absolute.","The recipe is protocol-generic: any protocol family with several independent implementations and timing-sensitive states (idle timeouts, retransmission queues, key lifetimes) could be tested with the same two-interval learning plus pairwise differencing, once a harness and symbol dictionary are built.","The two-interval timing choice could itself be optimized: the runtime cost of mixed timing (76.5 hours per model on average) suggests adaptively selecting intervals that maximize new-state discovery could scale the method to larger test suites."],"forward_implications":["Developers can run QUICtester against a new target using the 11 curated reference FSMs, and the Differential Analyzer will extract non-conforming transitions automatically, without repeating the full 19-server differential campaign.","Timing-varied learning is necessary for completeness: the Picoquic crash is present in the short-timeout learned model and absent from the long-timeout model, so a checker that ignores event timing would miss it.","The RFC 9000 ambiguity over first packets without a CRYPTO frame is exploitable in practice: 10 of the 19 servers create a connection context for a bare initial PING, memory use grows from roughly 500 MB to 3 GB under 50,000 such clients, and the Kwik server crashes; the proposed amendment requires a CRYPTO frame in the first packet.","Vendor responses corroborate the findings: five CVEs were assigned (Kwik, LSQUIC, PQUIC, and Quinn), two bug bounties were paid, and the reported faults were fixed or acknowledged by the respective maintainers."],"supporting_citations":[{"why":"The ratified QUIC transport specification under test; supplies the handshake semantics and the connection-management passage whose ambiguity yields the DoS finding.","marker":"[40]"},{"why":"The TLS-in-QUIC specification; its key-discard rule (Section 4.9) is the standard violated by the encryption-key-retention faults (S-2, S-5, S-10, S-19).","marker":"[62]"},{"why":"The QUIC implementation the Test Harness extends to build and parse packets for all five security configurations, including client authentication.","marker":"[1]"},{"why":"The Java library providing the active automata learning framework in which the Learner is implemented.","marker":"[39]"},{"why":"The TTT algorithm used for hypothesis construction during model learning.","marker":"[38]"},{"why":"The Wp-method used for conformance testing of learned hypotheses.","marker":"[16]"},{"why":"The LTS_Diff algorithm used by the Differential Analyzer to extract deviating transitions between learned models.","marker":"[64]"},{"why":"The TLS library whose mis-set certificate-verification flag is the root cause of the Quiche client-authentication bypass.","marker":"[2]"}],"fun_headline_variants":["QUICtester: 55 bugs found in 19 QUIC servers via differential learning","No formal model needed: QUICtester finds 55 bugs via differential testing","Differential automata learning reveals 55 QUIC implementation flaws","QUICtester: 55 server bugs found without a formal spec model","QUICtester: 19 implementations as cross-check oracles expose 55 bugs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The tool's reach is capped by its hand-built dictionary of 30 message symbols and by the bet that among the 19 tested servers, at least one behaves per the specification for every behavior that matters; a deviation that no symbolized message can reach, or one shared by every implementation, would go undetected.","fun_headline_variants_meta":{"raw":{"variants":["QUICtester: 55 bugs found in 19 QUIC servers via differential learning","No formal model needed: QUICtester finds 55 bugs via differential testing","Differential automata learning reveals 55 QUIC implementation flaws","QUICtester: 55 server bugs found without a formal spec model","QUICtester: 19 implementations as cross-check oracles expose 55 bugs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001025,"raw_usage":{"total_tokens":4367,"prompt_tokens":1037,"completion_tokens":3330,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":653,"completion_tokens_details":{"reasoning_tokens":3226}},"tokens_in":653,"tokens_out":3330,"duration_ms":20297,"temperature":1.0,"reasoning_tokens":3226,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T20:28:43.348739+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Plant a deliberately non-conforming behavior in a QUIC server that triggers only on a message type or parameter combination outside the 30-symbol dictionary (for example, an exotic transport parameter value), run the full learning and pairwise differential pipeline with that server added to the original 19, and check whether the planted deviation produces any flagged edge; if it does not, the dictionary is shown to be the coverage ceiling. A complementary check: introduce the same bug into all 19 implementations and observe that the differential analyzer reports nothing, because its oracle is purely comparative.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The ratified QUIC transport specification under test; supplies the handshake semantics and the connection-management passage whose ambiguity yields the DoS finding."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The TLS-in-QUIC specification; its key-discard rule (Section 4.9) is the standard violated by the encryption-key-retention faults (S-2, S-5, S-10, S-19)."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The QUIC implementation the Test Harness extends to build and parse packets for all five security configurations, including client authentication."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The Java library providing the active automata learning framework in which the Learner is implemented."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The TTT algorithm used for hypothesis construction during model learning."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The Wp-method used for conformance testing of learned hypotheses."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The LTS_Diff algorithm used by the Differential Analyzer to extract deviating transitions between learned models."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The TLS library whose mis-set certificate-verification flag is the root cause of the Quiche client-authentication bypass."}],"review_version":1}