Secure multi-party computation (MPC) enables privacy-preserving computations using secret data, with applications ranging from health care and finance to machine learning and blockchains. MPC compilers translate high-level function descriptions to the low-level representations required for the actual execution, making them critical for both usability and scalability of MPC. However, these compilers may contain logic bugs that cause them to quietly produce wrong outputs, the consequences of which could be catastrophic given the sensitive applications of this technology. Testing MPC compilers in order to find these severe bugs is, therefore, paramount. With only a single testing tool currently available (which is not publicly available in its entirety and has several serious limitations), this issue is far from resolved. In this paper, we present BabelFuzz, a cost-effective framework for testing MPC compilers. By introducing an expressive intermediate representation (IR) for its seed-program generation, BabelFuzz is able to support multiple compilers that use different input languages, while keeping the development effort of adding new targets low. Even better, this approach allows us to translate our IR to mainstream languages, which provides a powerful differential-testing oracle for highly efficient bug detection. BabelFuzz not only found 27 new logic bugs across four MPC compilers, but it is also able to rediscover every fixed bug the previous state of the art in testing MPC compilers found.
Given the critical nature of Ethereum, exploiting 1-day vulnerabilities that are patched but not yet widely deployed is essential. Meanwhile, Automatic Patch-based Exploit Generation (APEG) is a promising technique for this, as it helps developers understand root causes, verify fixes in downstream forks, and detect incomplete patches. However, existing exploit generation tools can not work well for vulnerabilities on Ethereum due to three key unique challenges: (1) navigating complex and cross-language exploit paths hidden within patches, (2) synthesizing complicated and stateful environment configurations, and (3) handling non-deterministic inconsistencies between blockchain nodes that lead to false alarms. To address these challenges, we introduce ChainDelta , a novel fuzzing agent framework driven by Large Language Models to automatically generate exploits based on Ethereum security patches. ChainDelta consists of three core modules: a directed fuzzer utilizes call graph analysis to guide testing towards vulnerable code based on the patch information; an agent-based environment fuzzer acts as an expert to automatically set up the necessary blockchain states to trigger vulnerabilities; and finally, a state-aware sanitizer performs differential analysis while monitoring the blockchain transient state to distinguish true inconsistencies from benign non-determinism. We evaluate ChainDelta on a diverse benchmark with real-world patches, covering a wide range of types such as data racing and denial-of-service. ChainDelta successfully generated exploits with a 64% success rate and only a 15.8% false positive rate. An ablation study confirms the contribution of each module to the overall performance. To demonstrate its practical impacts, we conducted a real-world auditing campaign on top of ChainDelta , leading to the discovery of four previously undisclosed vulnerabilities with bug bounties.
A type checker must reject ill-typed programs in addition to accepting well-typed programs. Negative type checker tests, programs expected to be rejected, validate that a type checker enforces the language’s typing rules as intended. We focus on negative type checker tests for P4, a domain-specific language for programmable network devices, whose type system encodes design principles and hardware constraints of the network dataplane. Failing to reject an ill-typed P4 program risks violating these principles and constraints, leading to unexpected errors. A comprehensive negative test suite covering subtle and diverse ill-typed conditions is thus important. However, constructing comprehensive negative tests is challenging: the negative input space lacks systematic characterization, and existing P4 program generators do not target subtle type errors. This paper addresses the problem in three steps. (i) We mechanize the P4 type system using the SpecTec framework. Unlike the informal official P4 specification, the mechanized type system is formal and machine-readable. Mechanization enables a systematic analysis of the type system. (ii) Across the mechanized type system, we identify dangling premises, which are premises in the typing rules that, when violated, cause type errors. Based on them, we propose dangling coverage, a novel metric for quantifying negative test coverage. (iii) Finally, we implement a coverage-guided fuzzer that mutates well-typed P4 programs into ill-typed programs that increase dangling coverage. Our method identifies 939 dangling premises that characterize distinct ill-typed conditions in the P4 type system. The fuzzer generates a negative test suite achieving 33.02%p higher dangling coverage than the existing P4C reference compiler’s test suite. The generated tests also reveal 29 previously unknown bugs in the compiler frontend, demonstrating the effectiveness of both the coverage metric and the fuzzer. The tests generated by our fuzzer are now integrated into the P4C test suite.
Smart contracts are self-executing agreements with code-defined terms enabling trustless blockchain transactions. Their immutability and control over significant financial assets make them attractive attack targets, with vulnerabilities potentially causing catastrophic financial losses. Large Language Models (LLMs) have revolutionized numerous domains with remarkable capabilities in code understanding and problem-solving. Despite these advancements, recent research reveals that LLMs still face significant limitations in accurately detecting complex vulnerabilities in smart contracts. This disparity between the capabilities of LLMs and the stringent requirements of security analysis underscores the necessity for tailored methodologies to enhance LLM-based vulnerability detection strategies. In this paper, we propose Synapse, the first smart contract vulnerability detection framework leveraging thought-augmented LLM and fine-grained analysis under focal context. Specifically, Synapse emulates security researchers' vulnerability discovery workflow, including vulnerability pattern learning, thought instantiation, reasoning, and verification. We employ a Buffer of Vulnerability Reasoning Thoughts (BoVRT) approach for LLMs to learn and apply vulnerability-specific reasoning to concrete contracts, improving detection accuracy. We also leverage specialized reasoning and code models to optimize different stages of the vulnerability detection process. To evaluate Synapse, we collected real-world on-chain contract incidents from security company alerts not covered by existing datasets. Synapse identified 117 previously undiscovered vulnerabilities in on-chain smart contracts, including one critical vulnerability that safeguarded assets totaling $30 million from potential losses.
Recent large language models (LLMs) have shown strong performance on software engineering tasks, yet most existing benchmarks evaluate code reasoning at the function level, where all relevant information is localized. This setting fails to reflect real-world development, which requires reasoning across multiple files and complex dependency structures. We introduce RepoReasoner, a benchmark for evaluating repository-level code reasoning. It assesses two complementary abilities: Output Prediction, which measures fine-grained, stateful execution reasoning across files, and Call Chain Prediction, which evaluates high-level architectural dependency understanding under noisy context. Our benchmark is constructed through a multi-stage pipeline that leverages dynamic tracing of pytest executions to obtain ground-truth call chains, along with LLM-based I/O rewriting to reduce memorization effects. We evaluate seven state-of-the-art LLMs. Even under oracle context, the best-performing model achieves only 69.1
Model checking using temporal logic is a key aspect of formal verification of modern complex software systems. These systems are often the result of distributed development processes, involving multiple teams and iterative design cycles. This complexity is mirrored in the corresponding formal specifications, which often consist of a large number of temporal logic properties that need to be verified against a system model. Many of these properties overlap semantically, yet traditional verification treats them as independent, resulting in redundant checks that waste computational resources and inflate engineering effort. We address this by introducing and operationalizing a formal theory of property refinement for temporal logic into a concrete methodology that automatically identifies redundant properties from a verification suite. This is achieved by first partitioning specifications into equivalence classes based on shared atomic propositions, followed by an analysis of intra-class refinement relations to construct the minimal sufficient subset. Our extensive empirical evaluation confirms the practical viability of our approach, demonstrating it can reduce the number of required verification tasks by up to 75% and accelerate model checking by up to three orders of magnitude, with a one-time associated overhead cost of 0.035% for the refinement analysis. The results of the evaluation confirm that the benefits of this approach are threefold: it reduces the computational requirements for formal verification; it allows engineers to focus on the core requirements of the system, hereby reducing engineering effort; finally, the one-time negligible investment in refinement yields compounding returns, making it particularly advantageous for agile and long-term development lifecycles. This work thus establishes property refinement analysis as a key technique for scaling requirement engineering and software verification to modern complex software systems.
Constructing large-scale datasets for the GitHub issue resolution task is crucial for both training and evaluating the software engineering capabilities of Large Language Models (LLMs). However, the existing GitHub issue resolution data construction pipeline is challenging and labor-intensive. We identify three key limitations in existing pipelines: (1) test patches collected often omit binary file changes; (2) the manual construction of evaluation environments is labor-intensive; and (3) the fail2pass validation phase requires manual inspection of test logs and writing custom parsing code to extract test status from logs. In this paper, we propose SWE-Factory, a fully automated issue resolution data construction pipeline, to resolve these limitations. First, our pipeline automatically recovers missing binary test files and ensures the correctness of test patches. Second, we introduce SWE-Builder, an LLM-based agentic system that automates evaluation environment construction. Third, we introduce a standardized, exit-code-based log parsing method to automatically extract test status, enabling a fully automated fail2pass validation. Experiments on 671 real-world GitHub issues across four programming languages show that our method can effectively construct valid evaluation environments for GitHub issues at a reasonable cost. For example, with GPT-4.1 mini, our SWE-Builder constructs 337 valid task instances out of 671 issues, at $0.047 per instance. Our ablation study further shows the effectiveness of different components of SWE-Builder. We also demonstrate through manual inspection that our exit-code-based fail2pass validation method is highly accurate, achieving an F1 score of 0.99. Additionally, we conduct an exploratory experiment to investigate whether we can use SWE-Factory to enhance models’ software engineering ability. After training five models on 2,809 Python task instances collected by our method, all models show improved software engineering ability. For example, the resolve rate of a trained Qwen2.5-Coder-14B-Instruct on SWE-bench Verified increases from 5.8% to 21.0%. We hope our method can accelerate the construction of large-scale, high-quality GitHub issue resolution datasets for both training and evaluation.
