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.<n>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: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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

• An Empirical Study on the Effectiveness of Large Language Models for Binary Code Understanding [50.17907898478795]
  This work proposes a benchmark to evaluate the effectiveness of Large Language Models (LLMs) in real-world reverse engineering scenarios. Our evaluations reveal that existing LLMs can understand binary code to a certain extent, thereby improving the efficiency of binary code analysis.
  arXiv  Detail & Related papers  (2025-04-30T17:02:06Z)
• StrTune: Data Dependence-based Code Slicing for Binary Similarity Detection with Fine-tuned Representation [5.41477941455399]
  BCSD can address binary tasks such as malicious code snippets identification and binary patch analysis by comparing code patterns. Because binaries are compiled with different compilation configurations, existing approaches still face notable limitations when comparing binary similarity. We propose StrTune, which slices binary code based on data dependence and perform slice-level fine-tuning.
  arXiv  Detail & Related papers  (2024-11-19T12:20:08Z)
• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  We train and evaluate neural networks directly as binary classifiers of strings. We provide results on a variety of languages across the Chomsky hierarchy for three neural architectures. Our contributions will facilitate theoretically sound empirical testing of language recognition claims in future work.
  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)
• Symbol-LLM: Leverage Language Models for Symbolic System in Visual Human Activity Reasoning [58.5857133154749]
  We propose a new symbolic system with broad-coverage symbols and rational rules. We leverage the recent advancement of LLMs as an approximation of the two ideal properties. Our method shows superiority in extensive activity understanding tasks.
  arXiv  Detail & Related papers  (2023-11-29T05:27:14Z)
• CP-BCS: Binary Code Summarization Guided by Control Flow Graph and Pseudo Code [79.87518649544405]
  We present a control flow graph and pseudo code guided binary code summarization framework called CP-BCS. CP-BCS utilizes a bidirectional instruction-level control flow graph and pseudo code that incorporates expert knowledge to learn the comprehensive binary function execution behavior and logic semantics.
  arXiv  Detail & Related papers  (2023-10-24T14:20:39Z)
• 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)
• 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)
• 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)
• Soft-Labeled Contrastive Pre-training for Function-level Code Representation [127.71430696347174]
  We present textbfSCodeR, a textbfSoft-labeled contrastive pre-training framework with two positive sample construction methods. Considering the relevance between codes in a large-scale code corpus, the soft-labeled contrastive pre-training can obtain fine-grained soft-labels. SCodeR achieves new state-of-the-art performance on four code-related tasks over seven datasets.
  arXiv  Detail & Related papers  (2022-10-18T05:17:37Z)
• Pre-Training Representations of Binary Code Using Contrastive Learning [13.570375923483452]
  We propose a COntrastive learning Model for Binary cOde Analysis, or COMBO, that incorporates source code and comment information into binary code during representation learning. COMBO is the first language representation model that incorporates source code, binary code, and comments into contrastive code representation learning.
  arXiv  Detail & Related papers  (2022-10-11T02:39:06Z)
• BinBert: Binary Code Understanding with a Fine-tunable and Execution-aware Transformer [2.8523943706562638]
  In this paper we present BinBert, a novel assembly code model. BinBert is built on a transformer pre-trained on a huge dataset of both assembly instruction sequences and symbolic execution information. Through fine-tuning, BinBert learns how to apply the general knowledge acquired with pre-training to the specific task.
  arXiv  Detail & Related papers  (2022-08-13T17:48:52Z)
• 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.