{"id":"5ff3949e-cab5-4bca-be4f-11ab3875288f","arxiv_id":"2509.06509","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"LeaSyn synthesizes leakage contracts for RISC-V processor designs that are proved sound and more precise than prior contracts.","lead":"A new tool, LeaSyn, automatically writes leakage contracts, formal descriptions of what a processor leaks through timing side channels, by testing and formally verifying the chip's design. It produced sound and highly precise contracts for six open-source RISC-V processors, more precise than contracts from earlier methods.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Soundness guarantee depends on the user-supplied template being complete for the target's leaks; the tool's behavior when no sound contract exists in the template is unspecified.","rationale":"The reader's weakest_assumption—that soundness depends on the user-provided template being expressive enough to represent every leak—is the same load-bearing concern I identify. The paper is honest about this dependency in Section 7 and even shows in RQ3 that insufficient templates make sound synthesis impossible. I do not see an internal inconsistency in the formal model: Proposition 6 is conditional on Phase 3 passing, and Phase 3, if it succeeds, does establish soundness via LeaVe's unbounded verification. The main gap is operational: the paper does not describe how LeaSyn behaves when the ILP becomes infeasible because no contract in T can distinguish a discovered counterexample. Since the technique's raison d'être is to remove the need for a human who already knows the processor's leaks, this unspecified failure mode is the least secure part of the argument. The precision-formula typo in Section 6.1 (FP/(TP+FP) vs. TP/(TP+FP)) is real but minor and does not affect the central methodology. The evaluation is substantial: six open cores, reproducible artifacts, soundness checks via unbounded verification, and comparisons with prior contracts. The manual invariants reused from [50] weaken the 'automatic' claim but are disclosed. Overall, the reader's CONDITIONAL verdict is appropriate; my concern reinforces the need for the condition rather than changing it.","tokens_in":30256,"tokens_out":9233,"duration_ms":117112,"concrete_test":"Run LeaSyn on Ibex-small using the I-only template (only instruction-encoding atoms, no register, memory, branch, or value atoms), with the same bounds as Table 1. Because RQ3 states that no sound contract exists in this template, the synthesis loop should eventually produce a bounded counterexample whose SD_t and XOR_t are empty, making the Eq. 1 ILP infeasible. Check whether the tool (a) terminates with an explicit 'no sound contract exists in this template' diagnostic, (b) silently returns an unsound contract, or (c) hangs/loops. This distinguishes a contained, well-communicated limitation from a failure of the automatic-synthesis claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that LeaSyn automatically synthesizes a sound and precise contract from RTL. The weakest load-bearing condition is template completeness. LeaSyn can only return a subset of the user-provided template T, so if the target processor has a leak that cannot be expressed by any combination of atoms in T, no sound contract exists in the search space. The paper explicitly acknowledges this in Section 7: \"Our approach critically relies on user-provided contract atoms that are able to capture the leakage of the target processor soundly and precisely.\" RQ3 demonstrates it concretely: for the isolated I, R, and M templates, LeaSyn cannot synthesize a sound contract for Ibex-small because no sound contract exists in those templates. What the paper does not specify is what the tool does when it reaches an attacker-distinguishable counterexample that no subset of T can distinguish. In that case, SD_t and XOR_t for the counterexample are empty, and the ILP constraint in Eq. 1 becomes 0 >= 1, i.e., infeasible. Section 4.3 only states that each iteration rules out at least one candidate and that the loop \"eventually\" terminates, but if no sound contract exists, the loop cannot terminate with a contract; the infeasibility handling and user-facing diagnostic are absent. This matters for the \"automatic\" claim: a user who does not already know the leaks cannot tell whether LeaSyn failed because of a weak template, a too-small bound, or a tool bug. Relatedly, the unbounded verification phase in the evaluation reuses relational invariants manually constructed in prior work (Section 6.1), so the automatic soundness proof is not demonstrated from scratch on the six cores. These are limitations rather than internal inconsistencies, but they are precisely where the headline guarantee is least secure.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents LeaSyn, a tool and methodology for synthesizing leakage contracts for RISC-V processors directly from RTL. The user provides a contract template consisting of atoms; LeaSyn simulates generated test cases to characterize attacker-visible and contract-distinguishable behavior, uses an ILP to pick the most precise subset of atoms, alternates synthesis with bounded model checking to discover missed leaks, and finally invokes the LeaVe verifier for an unbounded soundness check. The authors evaluate on six open-source RISC-V cores and report contracts that are more precise than those from prior tools (LeaVe, Mohr et al., ConjunCT, VeloCT, RTL2MμPATH). The formal development includes propositions connecting the ILP constraints to distinguishability, the bounded verification to a bounded soundness guarantee, and the final Phase 3 to soundness of the synthesized contract.","tokens_in":30634,"tokens_out":4277,"duration_ms":50259,"significance":"If the results hold, this is a useful step toward automating a labor-intensive hardware-security task: deriving sound and precise ISA-level leakage contracts. The paper's strengths are its explicit formal model, the combination of empirical characterization with bounded and unbounded verification, the open-source implementation, and a broad evaluation over multiple core families with comparisons to several prior approaches. The central insight—using strongly-distinguishing atoms and xor-distinguishing pairs to characterize template distinguishability—is clean and well suited to the ILP formulation. The significance is somewhat qualified by the dependence on user-provided templates and on manually supplied invariants for the final unbounded verification, both acknowledged in the paper but relevant to the \"automatic\" claim.","major_comments":[{"comment":"The definition of precision as \"FP/(TP+FP)\" contradicts every reported value. With that formula, a perfect contract would have precision 0 and the Ibex-cache result 0.579 would be better than 0.999. Table 1, Table 2, Table 3, and Figure 2(b) are all consistent with the standard definition precision = TP/(TP+FP). This is a load-bearing error for the RQ1/RQ4 conclusions and must be corrected in the formula and in any accompanying prose.","section":"§6.1 (Evaluating precision)"},{"comment":"The unbounded soundness guarantee is not obtained by LeaSyn alone: Phase 3 relies on the LeaVe verifier with user-supplied relational invariants, and the evaluation explicitly re-uses manually constructed invariants from Wang et al. [50]. The paper presents LeaSyn as \"automatically synthesizing\" sound contracts, but for a new core a user may need to hand-craft these invariants. The manuscript should state this dependency in the main contributions and clarify which parts of the pipeline are automatic and which require expert input.","section":"§4.4, §5, §6.1"},{"comment":"The soundness of any output contract is conditional on the user-provided template being expressive enough to capture all leaks of the target. Section 7 acknowledges this, and RQ3 shows templates I, R, M alone admit no sound contract. However, the paper does not specify what LeaSyn does when the ILP in Eq. (1) becomes infeasible or when Phase 2b keeps producing counterexamples that no subset of T can distinguish. Since the termination argument in §4.3 only says each iteration rules out at least one contract, the behavior in the no-sound-contract case should be described explicitly, including the diagnostic returned to the user.","section":"§4.3 and §7"},{"comment":"The theorem states that the synthesized contract \"distinguishes as few attacker-distinguishable test cases as possible,\" but the ILP objective in §4.2 minimizes false positives among attacker-indistinguishable test cases, and the surrounding text in §1 and §4.2 uses \"attacker-indistinguishable.\" As written, Proposition 6 is either a typo or a different, unproved claim. Please correct the wording so the formal guarantee matches the synthesis objective.","section":"Proposition 6"}],"minor_comments":[{"comment":"The retirement predicate is denoted φ in §3.1 and ψ in §4.3 and Appendix C; please unify the notation.","section":"§4.3"},{"comment":"The precision metric should be defined with enough context to distinguish TP and FP (e.g., TP = contract- and attacker-distinguishable, FP = contract-distinguishable but attacker-indistinguishable). The current sentence is also unclear about whether the validation set is balanced or whether TP+FP is always nonzero.","section":"§6.1"},{"comment":"In the example, Ctr2 is written both as { (div, \"Reg[RS2]\") } and then later as { (div, \"Reg[RS2]=0?\") } in the same section; this is confusing even though the template has changed. Consider renaming the contracts across template revisions.","section":"§2.4"},{"comment":"The table labels \"same-programs\" and \"different-programs\" are used inconsistently with a hyphen and as separate words; please make them consistent.","section":"§6.2 (RQ4)"},{"comment":"In the proof of Proposition 2, Lemmas 1–3 are stated after Lemma 1 references them; reordering or forward-referencing would improve readability.","section":"§A.2"}],"recommendation":"major_revision","confidential_remarks":"The precision-formula error and the manual-invariant dependence both need to be addressed before the paper can be accepted. The template-completeness issue is a known limitation rather than a fatal flaw, provided the paper states it as a first-class caveat and documents the infeasible-template behavior."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The short version: this is a solid paper and a genuine advance over the prior state of the art. Mohr et al. synthesized precise but unsound contracts; ConjunCT/VeloCT gave sound but very imprecise ones. LeaSyn closes the gap with a clean loop: empirical test generation, ILP-based synthesis that handles shared leakage functions via XOR-distinguishing pairs, bounded refinement with counterexamples, and a final unbounded check via LeaVe. The formal model is coherent, the proofs in the appendix line up, and the evaluation is serious: six RISC-V cores, multiple templates, and a comparison that shows their contracts are substantially more precise than previous sound ones. Credit is due for shipping an open-source tool and for reporting reproducible benchmarks.\n\nNow the soft spots, in proportion. First, there is a plain typo in Section 6.1: the precision definition says FP/(TP+FP), but the reported numbers are clearly TP/(TP+FP). That should be fixed before publication; it is embarrassing but not substantive. Second, the \"automatic\" claim is real but qualified. The unbounded verification step reuses manually constructed relational invariants from the earlier LeaVe paper, and the paper says so. If the criterion is \"push-button from RTL to a proof,\" this is not quite that. Third, the dependence on the user-provided template is real and is acknowledged in Section 7, but the failure mode when no sound contract exists in the template is left unspecified. RQ3 shows that isolated templates can make synthesis impossible, yet the paper does not say what the tool does when the ILP becomes infeasible or when the loop cannot terminate. That is a usability gap, not an inconsistency in the method. The precision guarantee is explicitly relative to the test cases explored, which is honest, but it means the headline \"precise\" should be read with that caveat.\n\nThe stress-test note about template completeness is on target, but it is already a stated limitation rather than a hidden one. The missing piece is a clear diagnostic for users who pick a bad template. That deserves a fix, not a rejection.\n\nWho is this for? Anyone working on hardware leakage contracts, side-channel verification, or secure RISC-V designs. It is worth a serious referee and, after minor revisions, a place in a top venue. I would bring it to a reading group and would cite it in work on contract synthesis.","headline":"A real step forward in leakage-contract synthesis, with a couple of addressable warts: a precision-formula typo and an honest but under-specified dependence on template completeness.","tokens_in":31136,"tokens_out":2537,"would_cite":true,"duration_ms":31649,"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":"LeaSyn automatically synthesizes leakage contracts that are both sound and precise for RISC-V processors, directly from register-transfer-level designs.","keywords":["side channels","leakage contracts","RISC-V","register-transfer level","contract synthesis","timing leaks","hardware verification"],"falsifier":"Take a processor with a known timing leak that is absent from the supplied template, for example a cache whose timing depends on whether two consecutive accesses hit the same line when the template only exposes addresses. Running LeaSyn should fail to produce a sound contract, or should return a contract with low precision, as the Ibex-cache experiment already shows. More directly, one could take a synthesized contract and search by black-box differential testing on random program pairs for a pair of executions with identical contract traces but different retirement times; finding one would fa","tokens_in":30184,"feed_emoji":"🔒","tokens_out":5364,"duration_ms":55817,"temperature":0.7,"pith_summary":"LeaSyn aims to close the gap between two existing kinds of leakage-contract synthesis for RISC-V processors: one that produces precise contracts but cannot guarantee soundness, and one that produces sound but very imprecise contracts. Starting from an RTL design and a user-supplied contract template, LeaSyn alternates between an ILP-based synthesis step that picks the most precise contract consistent with empirical tests and a bounded verification step that hunts for leaks the tests missed, then finishes with an unbounded verification that proves the final contract sound. The paper reports that this pipeline synthesized sound contracts for six open-source RISC-V cores in under 48 hours each, with precision above 0.99 for all but one core where the template cannot capture the cache's actual leakage. If the method works as claimed, it removes a major manual step in hardware side-channel assurance: programmers get a processor-specific, machine-checked description of what timing information the CPU exposes.","feed_headline":"Automatic tool writes sound, precise leakage contracts for RISC-V CPUs","feed_subtitle":"LeaSyn derives them from RTL designs and proves them sound on six open-source cores.","key_machinery":"The load-bearing object is the contract template: a finite set of contract atoms, each an applicability predicate over architectural states and a leakage function that maps a state to an observation. Any subset of atoms is a candidate contract. The paper introduces two notions that make template-based synthesis tractable: strongly-distinguishing atoms and xor-distinguishing pairs, which together fully characterize when any contract distinguishes a test case (Proposition 1). This characterization feeds an ILP whose objective minimizes false positives while forcing all empirically attacker-distinguishable tests to be contract-distinguishable. A stuttering product circuit built from two copies","core_discovery":"The central claim is that LeaSyn is the first tool to automatically synthesize leakage contracts that are both sound and precise from register-transfer-level processor designs. Soundness means any two executions an attacker can tell apart by observing instruction retirement must produce different contract traces; precision means the contract over-approximates actual leakage as little as possible. The paper formalizes contracts as subsets of a user-provided template of atoms, each an applicability predicate paired with a leakage function. LeaSyn first characterizes leakage empirically on generated test cases, solves an integer-linear program to pick a minimal atom set that distinguishes all a","pith_inferences":["Because the guarantee in Proposition 6 is relative to the test cases explored during synthesis, the claimed precision is an empirical property of those tests, not a mathematical optimum over all possible programs; different test sets could yield different optimal contracts.","The single-line-cache case suggests the main practical bottleneck is template expressiveness: richer atoms encoding something like 'same address as the immediately preceding access' could probably restore high precision for cores with small caches.","The same synthesis loop could in principle be applied to other attacker models and instruction sets, since the formal model is not RISC-V-specific; the RISC-V formal interface is only the implementation substrate.","If templates were extended with atoms that expose sequences of instructions or speculation-related events, the method might generalize to speculative-leak contracts, though the paper explicitly leaves that to future work."],"forward_implications":["A user who can write or reuse a template no longer needs to reverse-engineer timing leaks manually; the tool returns a machine-checked contract from RTL.","Software-level constant-time reasoning can be tied to a specific processor: programs can be checked against the synthesized contract instead of against a generic, overly conservative policy.","The alternating loop is guaranteed to terminate because each bounded counterexample rules out at least one candidate contract, so the search is finite.","The precision measurements indicate that contracts synthesized by LeaSyn distinguish far fewer attacker-indistinguishable executions than contracts from prior sound synthesis approaches, so fewer secure programs would be rejected as leaky.","The bounded-verification step with a dynamic instruction bound can serve as a fast pre-filter before expensive unbounded verification, reducing total synthesis time."],"supporting_citations":[{"why":"Defines contract satisfaction and microarchitectural satisfaction, and supplies the LeaVe unbounded verifier and relational invariants used in Phase 3.","marker":"[50]"},{"why":"Prior precise-but-unsound contract synthesis; contributes the ILP formulation and modifier functions that LeaSyn extends with xor-distinguishing pairs and soundness checks.","marker":"[38]"},{"why":"ConjunCT: sound but very imprecise contract synthesis; serves as a baseline for precision comparison.","marker":"[21]"},{"why":"VeloCT: follow-up safe-instruction synthesis; used as another baseline.","marker":"[22]"},{"why":"RTL2MmuPATH: synthesizes microarchitectural path leakage descriptors; used as a baseline and template model for comparison.","marker":"[33]"},{"why":"Introduces leakage contracts and the sequential leakage-clause model that LeaSyn's atoms are built on.","marker":"[30]"},{"why":"RISC-V Formal Interface, used to instantiate contract templates across different cores.","marker":"[6]"},{"why":"Self-composition, the basis for the bounded model checking encoding over pairs of executions.","marker":"[15]"}],"fun_headline_variants":["First tool auto-synthesizes sound, precise RISC-V leakage contracts","LeaSyn: automatic synthesis of sound and precise leakage contracts for RISC-V","Auto-generating verified leakage contracts for RISC-V processors","LeaSyn: first to synthesize sound RISC-V leakage contracts automatically","RISC-V leakage contracts: LeaSyn automates sound and precise"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"LeaSyn's soundness guarantee holds only if the user-supplied contract template already contains an atom capable of expressing every leak the processor actually has; if some leak has no matching atom, no contract in the search space is sound.","fun_headline_variants_meta":{"raw":{"variants":["First tool auto-synthesizes sound, precise RISC-V leakage contracts","LeaSyn: automatic synthesis of sound and precise leakage contracts for RISC-V","Auto-generating verified leakage contracts for RISC-V processors","LeaSyn: first to synthesize sound RISC-V leakage contracts automatically","RISC-V leakage contracts: LeaSyn automates sound and precise"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001434,"raw_usage":{"total_tokens":5614,"prompt_tokens":733,"completion_tokens":4881,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":477,"completion_tokens_details":{"reasoning_tokens":4787}},"tokens_in":477,"tokens_out":4881,"duration_ms":42803,"temperature":1.0,"reasoning_tokens":4787,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T23:28:37.831357+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a processor with a known timing leak that is absent from the supplied template, for example a cache whose timing depends on whether two consecutive accesses hit the same line when the template only exposes addresses. Running LeaSyn should fail to produce a sound contract, or should return a contract with low precision, as the Ibex-cache experiment already shows. More directly, one could take a synthesized contract and search by black-box differential testing on random program pairs for a pair of executions with identical contract traces but different retirement times; finding one would fa","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines contract satisfaction and microarchitectural satisfaction, and supplies the LeaVe unbounded verifier and relational invariants used in Phase 3."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Prior precise-but-unsound contract synthesis; contributes the ILP formulation and modifier functions that LeaSyn extends with xor-distinguishing pairs and soundness checks."},{"cited_title":"Fletcher","cited_arxiv_id":null,"evidence_quote":"ConjunCT: sound but very imprecise contract synthesis; serves as a baseline for precision comparison."},{"cited_title":"Fletcher","cited_arxiv_id":null,"evidence_quote":"VeloCT: follow-up safe-instruction synthesis; used as another baseline."},{"cited_title":"Mulligan, Gustavo Petri, Christopher W","cited_arxiv_id":null,"evidence_quote":"RTL2MmuPATH: synthesizes microarchitectural path leakage descriptors; used as a baseline and template model for comparison."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces leakage contracts and the sequential leakage-clause model that LeaSyn's atoms are built on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"RISC-V Formal Interface, used to instantiate contract templates across different cores."},{"cited_title":"D’Argenio, and Tamara Rezk","cited_arxiv_id":null,"evidence_quote":"Self-composition, the basis for the bounded model checking encoding over pairs of executions."}],"review_version":1}