Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Can LLMs Recover Program Semantics? A Systematic Evaluation with Symbolic Execution

Rong Feng, Suman Saha

TL;DR

This work tackles the persistent challenge of software obfuscation by proposing a hybrid approach that combines symbolic execution artifacts with fine-tuned large language models. By constructing a diverse dataset obfuscated with four techniques and generating semantic ground truth via KLEE, the authors evaluate three LLMs under baseline and artifact-enhanced training. Results show that GPT-4.1-mini excels in deobfuscation, with KLEE artifacts consistently boosting syntax correctness and semantic fidelity across models, while readablity benefits vary by model. Collectively, the findings suggest that integrating formal symbolic evidence with LLM-based synthesis strengthens automated testing, static analysis, and program understanding in the presence of obfuscation.

Abstract

Obfuscation poses a persistent challenge for software engineering tasks such as program comprehension, maintenance, testing, and vulnerability detection. While compiler optimizations and third-party code often introduce transformations that obscure program intent, existing analysis tools and large language models (LLMs) struggle to recover the original semantics. In this work, we investigate whether LLMs, when fine-tuned with symbolic execution artifacts, can effectively deobfuscate programs and restore analyzability. We construct a benchmark by applying four widely studied transformations-control-flow flattening, opaque predicates, arithmetic encoding, and branch encoding-across diverse C programs from TUM Obfuscation Benchmarks, the LLVM test suite, and algorithmic repositories. We then compare three state-of-the-art LLMs under two training configurations: baseline fine-tuning on obfuscated/original code pairs, and enhanced fine-tuning with additional KLEE artifacts such as SMT constraints, path statistics, and test cases. Our evaluation examines syntactic correctness (compilation success), semantic fidelity (behavioral equivalence under symbolic execution), and code quality (readability and structure). Results show that GPT-4.1-mini achieves the strongest deobfuscation overall, and that incorporating KLEE artifacts consistently improves semantic preservation and compilation success across models. These findings highlight deobfuscation as a broader software engineering concern, demonstrating that combining LLMs with symbolic execution can strengthen automated testing, static analysis, and program comprehension in the presence of obfuscation.

Can LLMs Recover Program Semantics? A Systematic Evaluation with Symbolic Execution

TL;DR

This work tackles the persistent challenge of software obfuscation by proposing a hybrid approach that combines symbolic execution artifacts with fine-tuned large language models. By constructing a diverse dataset obfuscated with four techniques and generating semantic ground truth via KLEE, the authors evaluate three LLMs under baseline and artifact-enhanced training. Results show that GPT-4.1-mini excels in deobfuscation, with KLEE artifacts consistently boosting syntax correctness and semantic fidelity across models, while readablity benefits vary by model. Collectively, the findings suggest that integrating formal symbolic evidence with LLM-based synthesis strengthens automated testing, static analysis, and program understanding in the presence of obfuscation.

Abstract

Obfuscation poses a persistent challenge for software engineering tasks such as program comprehension, maintenance, testing, and vulnerability detection. While compiler optimizations and third-party code often introduce transformations that obscure program intent, existing analysis tools and large language models (LLMs) struggle to recover the original semantics. In this work, we investigate whether LLMs, when fine-tuned with symbolic execution artifacts, can effectively deobfuscate programs and restore analyzability. We construct a benchmark by applying four widely studied transformations-control-flow flattening, opaque predicates, arithmetic encoding, and branch encoding-across diverse C programs from TUM Obfuscation Benchmarks, the LLVM test suite, and algorithmic repositories. We then compare three state-of-the-art LLMs under two training configurations: baseline fine-tuning on obfuscated/original code pairs, and enhanced fine-tuning with additional KLEE artifacts such as SMT constraints, path statistics, and test cases. Our evaluation examines syntactic correctness (compilation success), semantic fidelity (behavioral equivalence under symbolic execution), and code quality (readability and structure). Results show that GPT-4.1-mini achieves the strongest deobfuscation overall, and that incorporating KLEE artifacts consistently improves semantic preservation and compilation success across models. These findings highlight deobfuscation as a broader software engineering concern, demonstrating that combining LLMs with symbolic execution can strengthen automated testing, static analysis, and program comprehension in the presence of obfuscation.

Paper Structure

This paper contains 38 sections, 7 figures, 8 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Code Obfuscation
  4. Symbolic Execution
  5. Large Language Models in Program Analysis
  6. Why Deobfuscation Is Hard
  7. Approach
  8. Dataset
  9. Obfuscation Transformations
  10. Control-Flow Flattening (CFF)
  11. Opaque Predicates (OP)
  12. Arithmetic Encoding (AE)
  13. Branch Encoding (BE)
  14. KLEE Artifacts
  15. Model Configuration
  16. ...and 23 more sections

Figures (7)

  • Figure 1: Overview of our approach. Source programs are obfuscated with four transformations, while KLEE generates semantic artifacts from the original code. These inputs guide LLM fine-tuning, producing deobfuscated programs that are evaluated for syntax, semantics, and quality.
  • Figure 2: Visualization on Compilation Success (Fine-tuned Model)
  • Figure 3: Visualization on Semantic Score (Fine-tuned Model)
  • Figure 4: Visualization on Quality Score (Fine-tuned Model)
  • Figure 5: Visualization on Compilation Success (Base Model)
  • ...and 2 more figures