arXiv subjects

Hengyuan Liu

Publications and source records attributed to Hengyuan Liu.

4 recordsLinked to original sources

arXiv2026

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

Manual formal analysis of cryptographic schemes is labor-intensive and requires substantial expertise. While model-checking tools (e.g., Scyther and Tamarin) and computational-security tools (e.g., CryptoVerif and EasyCrypt) improve the automation of security proofs, they still rely on experts to abstract schemes and write tool-specific formal descriptions. Large language models (LLMs) are a promising alternative, but their effectiveness in this domain remains unexplored due to the absence of standardized evaluation methodologies. To fill this gap, we introduce CrypFormBench (C.F.B for short), a comprehensive benchmark jointly covering symbolic and computational security to evaluate five core LLM capabilities: interpretation, generation, completion, transformation, and correction. It comprises 700 instances spanning 677 schemes, 7 mainstream formal verifier languages, and 160 security properties. The evaluation of 9 state-of-the-art LLMs reveals that most of them perform well on interpretation and completion, given their code-awareness advantages, but struggle with generation, transformation, and correction. Overall, their performance remains limited, with Claude-3.5 achieving the highest score at 48.7 out of 100. We further provide practical guidance, e.g., few-shot prompting, Pass@K sampling, and lightweight fine-tuning, to mitigate the executability bottleneck and improve tool-usable outputs. Taken together, our benchmark and analyses offer a grounded view of current progress and concrete directions toward reliable LLM-assisted formal cryptographic analysis.

cs.CR↗

arXiv2025

Exploring the Potential and Limitations of Large Language Models for Novice Program Fault Localization

Novice programmers often face challenges in fault localization due to their limited experience and understanding of programming syntax and logic. Traditional methods like Spectrum-Based Fault Localization (SBFL) and Mutation-Based Fault Localization (MBFL) help identify faults but often lack the ability to understand code context, making them less effective for beginners. In recent years, Large Language Models (LLMs) have shown promise in overcoming these limitations by utilizing their ability to understand program syntax and semantics. LLM-based fault localization provides more accurate and context-aware results than traditional techniques. This study evaluates six closed-source and seven open-source LLMs using the Codeflaws, Condefects, and BugT datasets, with BugT being a newly constructed dataset specifically designed to mitigate data leakage concerns. Advanced models with reasoning capabilities, such as OpenAI o3 and DeepSeekR1, achieve superior accuracy with minimal reliance on prompt engineering. In contrast, models without reasoning capabilities, like GPT-4, require carefully designed prompts to maintain performance. While LLMs perform well in simple fault localization, their accuracy decreases as problem difficulty increases, though top models maintain robust performance in the BugT dataset. Over-reasoning is another challenge, where some models generate excessive explanations that hinder fault localization clarity. Additionally, the computational cost of deploying LLMs remains a significant barrier for real-time debugging. LLM's explanations demonstrate significant value for novice programmer assistance, with one-year experience participants consistently rating them highly. Our findings demonstrate the potential of LLMs to improve debugging efficiency while stressing the need for further refinement in their reasoning and computational efficiency for practical adoption.

cs.SE↗

arXiv2025

MBFL-DKMR: Improving Mutation-based Fault Localization through Denoising-based Kill Matrix Refinement

Software debugging is a critical and time-consuming aspect of software development, with fault localization being a fundamental step that significantly impacts debugging efficiency. Mutation-Based Fault Localization (MBFL) has gained prominence due to its robust theoretical foundations and fine-grained analysis capabilities. However, recent studies have identified a critical challenge: noise phenomena, specifically the false kill relationships between mutants and tests, which significantly degrade localization effectiveness. While several approaches have been proposed to rectify the final localization results, they do not directly address the underlying noise. In this paper, we propose a novel approach to refine the kill matrix, a core data structure capturing mutant-test relationships in MBFL, by treating it as a signal that contains both meaningful fault-related patterns and high-frequency noise. Inspired by signal processing theory, we introduce DKMR (Denoising-based Kill Matrix Refinement), which employs two key stages: (1) signal enhancement through hybrid matrix construction to improve the signal-to-noise ratio for better denoising, and (2) signal denoising via frequency domain filtering to suppress noise while preserving fault-related patterns. Building on this foundation, we develop MBFL-DKMR, a fault localization framework that utilizes the refined matrix with fuzzy values for suspiciousness calculation. Our evaluation on Defects4J v2.0.0 demonstrates that MBFL-DKMR effectively mitigates the noise and outperforms the state-of-the-art MBFL techniques. Specifically, MBFL-DKMR achieves 129 faults localized at Top-1 compared to 85 for BLMu and 103 for Delta4Ms, with negligible additional computational overhead (0.11 seconds, 0.001\% of total time). This work highlights the potential of signal processing techniques to enhance the effectiveness of MBFL by refining the kill matrix.

cs.SE↗

arXiv2025

FLIMs: Fault Localization Interference Mutants, Definition, Recognition and Mitigation

Mutation-based Fault Localization (MBFL) has been widely explored for automated software debugging, leveraging artificial mutants to identify faulty code entities. However, MBFL faces significant challenges due to interference mutants generated from non-faulty code entities but can be killed by failing tests. These mutants mimic the test sensitivity behaviors of real faulty code entities and weaken the effectiveness of fault localization. To address this challenge, we introduce the concept of Fault Localization Interference Mutants (FLIMs) and conduct a theoretical analysis based on the Reachability, Infection, Propagation, and Revealability (RIPR) model, identifying four distinct interference causes. Building on this, we propose a novel approach to semantically recognize and mitigate FLIMs using LLM-based semantic analysis, enhanced by fine-tuning techniques and confidence estimation strategies to address LLM output instability. The recognized FLIMs are then mitigated by refining the suspiciousness scores calculated from MBFL techniques. We integrate FLIM recognition and mitigation into the MBFL workflow, developing MBFL-FLIM, a fault localization framework that enhances MBFL's effectiveness by reducing misleading interference while preserving real fault-revealing information. Our empirical experiments on the Defects4J benchmark with 395 program versions using eight LLMs demonstrate MBFL-FLIM's superiority over traditional SBFL and MBFL methods, advanced dynamic feature-based approaches, and recent LLM-based fault localization techniques. Specifically, MBFL-FLIM achieves an average improvement of 44 faults in the Top-1 metric, representing a significant enhancement over baseline methods. Further evaluation confirms MBFL-FLIM's robust performance in multi-fault scenarios, with ablation experiments validating the contributions of the fine-tuning and confidence estimation components.

cs.SE↗