Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics

• URL: http://arxiv.org/abs/2404.04132v2
• Date: Mon, 20 Jan 2025 11:56:45 GMT
• Title: Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
• Authors: Sören Tempel, Tobias Brandt, Christoph Lüth, Christian Dietrich, Rolf Drechsler,
• Abstract summary: We present a prototype for the RISC-V ISA and conduct a case study to demonstrate that it can be easily extended to additional instructions. We perform an experimental comparison with prior work which resulted in the discovery of five previously unknown bugs in the ISA implementation of the popular IR-based symbolic executor angr.
• Score: 2.3589687550723335
• License:
• Abstract: Symbolic execution is an SMT-based software verification and testing technique. Symbolic execution requires tracking performed computations during software simulation to reason about branches in the software under test. The prevailing approach on symbolic execution of binary code tracks computations by transforming the code to be tested to an architecture-independent IR and then symbolically executes this IR. However, the resulting IR must be semantically equivalent to the binary code, making this process complex and error-prone. The semantics of the binary code are specified by the targeted ISA, commonly given in natural language and requiring a manual implementation of the transformation to an IR. In recent years, the use of formal languages to describe ISA semantics in a machine-readable way has gained increased popularity. We investigate the utilization of such formal semantics for symbolic execution of binary code, achieving an accurate representation of instruction semantics. We present a prototype for the RISC-V ISA and conduct a case study to demonstrate that it can be easily extended to additional instructions. Furthermore, we perform an experimental comparison with prior work which resulted in the discovery of five previously unknown bugs in the ISA implementation of the popular IR-based symbolic executor angr.

Related papers

• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  Formal language theory pertains specifically to recognizers. It is common to instead use proxy tasks that are similar in only an informal sense. We correct this mismatch by training and evaluating neural networks directly as binary classifiers of strings.
  arXiv  Detail & Related papers  (2024-11-11T16:33:25Z)
• Unsupervised Binary Code Translation with Application to Code Similarity Detection and Vulnerability Discovery [2.022692275087205]
  Cross-architecture binary code analysis has become an emerging problem. Deep learning-based binary analysis has shown promising success. For some low-resource ISAs, an adequate amount of data is hard to find.
  arXiv  Detail & Related papers  (2024-04-29T18:09:28Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• Code Representation Pre-training with Complements from Program Executions [29.148208436656216]
  We propose FuzzPretrain to explore the dynamic information of programs revealed by their test cases and embed it into the feature representations of code as complements. FuzzyPretrain yielded more than 6%/9% mAP improvements on code search over its counterparts trained with only source code or AST.
  arXiv  Detail & Related papers  (2023-09-04T01:57:22Z)
• ProgSG: Cross-Modality Representation Learning for Programs in Electronic Design Automation [38.023395256208055]
  High-level synthesis (HLS) allows a developer to compile a high-level description in the form of software code in C and C++. HLS tools still require microarchitecture decisions, expressed in terms of pragmas. We propose ProgSG allowing the source code sequence modality and the graph modalities to interact with each other in a deep and fine-grained way.
  arXiv  Detail & Related papers  (2023-05-18T09:44:18Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• A Natural Language Processing Approach for Instruction Set Architecture Identification [6.495883501989546]
  We introduce character-level features of encoded binaries to identify fine-grained bit patterns inherent to each ISA. Our approach results in an 8% higher accuracy than the state-of-the-art features based on byte-histograms and byte pattern signatures.
  arXiv  Detail & Related papers  (2022-04-13T19:45:06Z)
• Semantic-aware Binary Code Representation with BERT [27.908093567605484]
  A wide range of binary analysis applications, such as bug discovery, malware analysis and code clone detection, require recovery of contextual meanings on a binary code. Recently, binary analysis techniques based on machine learning have been proposed to automatically reconstruct the code representation of a binary. In this paper, we propose DeepSemantic utilizing BERT in producing the semantic-aware code representation of a binary code.
  arXiv  Detail & Related papers  (2021-06-10T03:31:29Z)
• How could Neural Networks understand Programs? [67.4217527949013]
  It is difficult to build a model to better understand programs, by either directly applying off-the-shelf NLP pre-training techniques to the source code, or adding features to the model by theshelf. We propose a novel program semantics learning paradigm, that the model should learn from information composed of (1) the representations which align well with the fundamental operations in operational semantics, and (2) the information of environment transition.
  arXiv  Detail & Related papers  (2021-05-10T12:21:42Z)
• 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)
• 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)

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.