Symbolic Execution in Practice: A Survey of Applications in Vulnerability, Malware, Firmware, and Protocol Analysis

• URL: http://arxiv.org/abs/2508.06643v1
• Date: Fri, 08 Aug 2025 18:43:45 GMT
• Title: Symbolic Execution in Practice: A Survey of Applications in Vulnerability, Malware, Firmware, and Protocol Analysis
• Authors: Joshua Bailey, Charles Nicholas,
• Abstract summary: Symbolic execution is a powerful program analysis technique that allows for the systematic exploration of all program paths.<n>This paper introduces a systematic taxonomy of strategies to enable symbolic execution on complex software systems.<n>We survey applications of symbolic executions in several domains such as vulnerability analysis, malware analysis, firmware re-hosting, and network protocol analysis.
• Score: 3.1844358655583846
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic execution is a powerful program analysis technique that allows for the systematic exploration of all program paths. Path explosion, where the number of states to track becomes unwieldy, is one of the biggest challenges hindering symbolic execution's practical application. To combat this, researchers have employed various strategies to enable symbolic execution on complex software systems. This paper introduces a systematic taxonomy of these strategies, categorizing them into two primary approaches: Scope Reduction, which aims to reduce the scope of symbolic execution to manageable portions of code, and Guidance Heuristics, which steer the symbolic execution engine toward promising paths. Using this taxonomy as a lens, we survey applications of symbolic executions in several domains such as vulnerability analysis, malware analysis, firmware re-hosting, and network protocol analysis. Finally, we identify promising directions for future research, including the application of symbolic execution to real-time operating systems and modern, type-safe languages.

Related papers

• Zorya: Automated Concolic Execution of Single-Threaded Go Binaries [1.0696270564342327]
  We build upon Zorya, a concolic execution framework that translates Go binaries to Ghidra's P-Code intermediate representation.<n>We add the detection of bugs in concretely not taken paths and a multi-layer filtering mechanism to concentrate symbolic reasoning on panic-relevant paths.
  arXiv  Detail & Related papers  (2025-12-11T16:43:51Z)
• Can Large Language Models Solve Path Constraints in Symbolic Execution? [32.45630887872447]
  We focus on investigating the possibility of adopting large language models (LLM) for path constraint solving.<n>We build new evaluation pipelines and benchmarks for two tasks: test case generation and path classification.<n>Our experiment results show that state-of-the-art LLMs are able to solve path constraints in both generation and classification tasks.
  arXiv  Detail & Related papers  (2025-11-23T04:54:48Z)
• ThinkGeo: Evaluating Tool-Augmented Agents for Remote Sensing Tasks [54.52092001110694]
  ThinkGeo is a benchmark designed to evaluate tool-augmented agents on remote sensing tasks via structured tool use and multi-step planning.<n>Inspired by tool-interaction paradigms, ThinkGeo includes human-curated queries spanning a wide range of real-world applications.<n>Our analysis reveals notable disparities in tool accuracy and planning consistency across models.
  arXiv  Detail & Related papers  (2025-05-29T17:59:38Z)
• Exposing Go's Hidden Bugs: A Novel Concolic Framework [2.676686591720132]
  We present Zorya, a novel methodology to evaluate Go programs comprehensively.<n>By systematically exploring execution paths to uncover vulnerabilities beyond conventional testing, symbolic execution offers distinct advantages.<n>Our solution employs Ghidra's P-Code as an intermediate representation (IR)
  arXiv  Detail & Related papers  (2025-05-26T16:26:20Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages.<n>This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• DOCE: Finding the Sweet Spot for Execution-Based Code Generation [69.5305729627198]
  We propose a comprehensive framework that includes candidate generation, $n$-best reranking, minimum Bayes risk (MBR) decoding, and self-ging as the core components. Our findings highlight the importance of execution-based methods and the difference gap between execution-based and execution-free methods.
  arXiv  Detail & Related papers  (2024-08-25T07:10:36Z)
• Path-optimal symbolic execution of heap-manipulating programs [5.639904484784126]
  This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally accomplishes path optimality against heap-manipulating programs. We formalize the POSE algorithm for a tiny, but representative object-oriented programming language, and implement the formalization into a prototype symbolic executor to experiment the algorithm against a benchmark of sample programs that take data structures as inputs.
  arXiv  Detail & Related papers  (2024-07-23T20:35:33Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. We present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel.
  arXiv  Detail & Related papers  (2024-02-19T08:26:52Z)
• Code Prompting: a Neural Symbolic Method for Complex Reasoning in Large Language Models [74.95486528482327]
  We explore code prompting, a neural symbolic prompting method with both zero-shot and few-shot versions which triggers code as intermediate steps. We conduct experiments on 7 widely-used benchmarks involving symbolic reasoning and arithmetic reasoning.
  arXiv  Detail & Related papers  (2023-05-29T15:14:09Z)
• Symbolic Visual Reinforcement Learning: A Scalable Framework with Object-Level Abstraction and Differentiable Expression Search [63.3745291252038]
  We propose DiffSES, a novel symbolic learning approach that discovers discrete symbolic policies. By using object-level abstractions instead of raw pixel-level inputs, DiffSES is able to leverage the simplicity and scalability advantages of symbolic expressions. Our experiments demonstrate that DiffSES is able to generate symbolic policies that are simpler and more scalable than state-of-the-art symbolic RL methods.
  arXiv  Detail & Related papers  (2022-12-30T17:50:54Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  We introduce a technique for representing partially written programs in a program synthesis engine. We learn an approximate execution model implemented as a modular neural network. We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
  arXiv  Detail & Related papers  (2020-12-23T20:40:18Z)
• Symbolic Techniques for Deep Learning: Challenges and Opportunities [4.416697289927759]
  We look at some of the most popular deep learning frameworks being used today, including Keras, PyTorch, and MXNet. We focus this paper on symbolic techniques because they influence not only how neural networks are built but also the way in which they are executed.
  arXiv  Detail & Related papers  (2020-10-01T23:02:45Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.