Divide, Conquer and Verify: Improving Symbolic Execution Performance

• URL: http://arxiv.org/abs/2310.03598v2
• Date: Tue, 7 Nov 2023 09:51:41 GMT
• Title: Divide, Conquer and Verify: Improving Symbolic Execution Performance
• Authors: Christopher Scherb, Luc Bryan Heitz, Hermann Grieder, Olivier Mattmann,
• Abstract summary: Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. We present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects.
• Score: 0.14999444543328289
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Compared to other testing methods such as fuzzing, Symbolic Execution has the advantage of providing formal guarantees about the program. However, despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. This is primarily caused by the \emph{path explosion problem} as well as by the computational complexity of SMT solving. In this paper, we present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects. This way, the overall problem size is kept small, reducing the impact of computational complexity on large problems.

Related papers

• To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning [55.52872152909785]
  Chain-of-thought (CoT) via prompting is the de facto method for eliciting reasoning capabilities from large language models (LLMs) We show that CoT gives strong performance benefits primarily on tasks involving math or logic, with much smaller gains on other types of tasks.
  arXiv  Detail & Related papers  (2024-09-18T17:55:00Z)
• Scaling Symbolic Execution to Large Software Systems [0.0]
  Symbolic execution is a popular static analysis technique used both in program verification and in bug detection software. We focus on an error finding framework called the Clang Static Analyzer, and the infrastructure built around it named CodeChecker.
  arXiv  Detail & Related papers  (2024-08-04T02:54:58Z)
• 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)
• Parsimonious Optimal Dynamic Partial Order Reduction [1.5029560229270196]
  We present Parsimonious-OPtimal DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption.
  arXiv  Detail & Related papers  (2024-05-18T00:07:26Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  Large language models (LLMs) of code are typically trained on the surface textual form of programs. We propose NExT, a method to teach LLMs to inspect the execution traces of programs and reason about their run-time behavior.
  arXiv  Detail & Related papers  (2024-04-23T01:46:32Z)
• Holographic Global Convolutional Networks for Long-Range Prediction Tasks in Malware Detection [50.7263393517558]
  We introduce Holographic Global Convolutional Networks (HGConv) that utilize the properties of Holographic Reduced Representations (HRR) Unlike other global convolutional methods, our method does not require any intricate kernel computation or crafted kernel design. The proposed method has achieved new SOTA results on Microsoft Malware Classification Challenge, Drebin, and EMBER malware benchmarks.
  arXiv  Detail & Related papers  (2024-03-23T15:49:13Z)
• 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)
• NAPG: Non-Autoregressive Program Generation for Hybrid Tabular-Textual Question Answering [52.10214317661547]
  Current numerical reasoning methods autoregressively decode program sequences. The accuracy of program generation drops sharply as the decoding steps unfold due to error propagation. In this paper, we propose a non-autoregressive program generation framework.
  arXiv  Detail & Related papers  (2022-11-07T11:25:21Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jl is an extendable symbolic system which uses dynamic multiple dispatch to change behavior depending on the domain needs. We show that by formalizing a generic API on actions independent of implementation, we can retroactively add optimized data structures to our system. We demonstrate the ability to swap between classical term-rewriting simplifiers and e-graph-based term-rewriting simplifiers.
  arXiv  Detail & Related papers  (2021-05-09T14:22:43Z)
• Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results [6.961253535504978]
  Symbolic execution is a powerful technique for bug finding and program testing. We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution tools.
  arXiv  Detail & Related papers  (2020-01-22T08:48:55Z)

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.