DECOMPILATION UNDER THE LENS: AN INTEGRATED FRAMEWORK WITH SYMBOLIC DIFFERENTIATION TESTING AND LLM-BASED FINE-TUNING

Decompilation, the process of transforming low-level binary code back into high-level source code, stands as a cornerstone technology for software security, vulnerability analysis, and legacy system maintenance. Despite its critical role, modern decompilers face a dilemma: the trade-off between semantic accuracy and code readability. Traditional heuristic-based approaches often sacrifice strict semantic fidelity to generate structured pseudo-code, leading to a prevalent lack of trust among reverse engineers. Moreover, the output, even when semantically correct, remains difficult for humans to comprehend due to obscure naming and redundant logic. Meanwhile, while recent advances in Large Language Models (LLMs) offer a promising avenue to enhance readability, their probabilistic nature introduces the risk of "hallucinations," potentially altering the original program semantics and creating new security vulnerabilities. This dissertation addresses these challenges by proposing a comprehensive ecosystem for high-fidelity binary decompilation, integrating generative artificial intelligence with formal verifications.First, to establish a rigorous standard for decompilation correctness, this research introduces D-Helix, a generic and automated testing framework that operates without the need for source code. D-Helix overcomes the limitations of previous testing methods by employing a novel iterative Recompiler to resolve syntactic errors in decompiled output and utilizing a symbolic differentiation engine, SymDiff, to verify semantic equivalence against the original binary at the function level. Furthermore, it incorporates a Tuner component to automatically isolate the specific heuristic rules within decompilers that cause semantic deviations. Application of D-Helix on widely used decompilers like Ghidra and angr revealed numerous previously unknown bugs, demonstrating the fragility of rule-based decompilation. Building upon this verification capability, the dissertation presents D-LiFT, an enhanced decompiler-LLM pipeline designed to improve code quality while strictly preserving semantics. D-LiFT fundamentally shifts the paradigm of neural decompilation by establishing the principle that readability improvements must not compromise accuracy. Central to this system is D-Score, a multi-dimensional quality metric that combines the symbolic verification of D-Helix with established software engineering readability standards. By utilizing D-Score as a reward signal for Reinforcement Learning, specifically Group Relative Policy Optimization (GRPO), D-LiFT fine-tunes LLMs to internalize binary semantic constraints. Evaluation results demonstrate that D-LiFT significantly enhances the quality of decompiled code for a majority of test cases without introducing new errors, effectively bridging the gap between machine verification and human understanding.