Deterministic Fully-Static Whole-Binary Translation without Heuristics

• URL: http://arxiv.org/abs/2605.08419v2
• Date: Wed, 13 May 2026 21:22:17 GMT
• Title: Deterministic Fully-Static Whole-Binary Translation without Heuristics
• Abstract summary: Elevator translates entire x86-64 executables to AArch64 debug information, source code, or assumptions about code layout.<n>We evaluate Elevator on a diverse corpus of real-world binaries, including the entire SPECint 2006 suite.
• Score: 4.112095753709181
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present Elevator, the first binary translator that statically translates entire x86-64 executables to AArch64 without debug information, source code, or assumptions about code layout. Unlike existing systems, which rely on heuristics or runtime fallbacks to handle code-versus-data decoding errors, Elevator considers all possible interpretations of every byte and produces a separate translation for each feasible one ahead of time. Any byte may be interpreted as data, an opcode, or an opcode argument; we generate separate control flow paths for all interpretations, pruning only those leading to abnormal termination. Translations are built by composing code "tiles" automatically derived from a high-level description of the source ISA, yielding a nimble translation framework. The approach is deterministic and produces complete, self-contained binaries with no runtime component in the trusted code base. The principal cost is substantial code size expansion. The key benefit is that the output is the actual code that will run, enabling testing, validation, certification, and cryptographic signing prior to deployment, reducing risk compared to emulators or JIT compilers. We evaluate Elevator on a diverse corpus of real-world binaries, including the entire SPECint 2006 suite, demonstrating that static full-program binary translation can be both reliable and practical. Elevator achieves performance on par with or better than QEMU's user-mode JIT emulation.

Related papers

• No Bit Left Behind: Using Brute-Force Lifting to Achieve Fully Static Binary Recompilation [1.5034998782245808]
  This article presents a fully static, whole-program binary lifting system requiring no runtime translation support on the target.<n>We have implemented this approach as a prototype binary runtimer from x86-64 binaries to LLVM IR, requiring no code/data runtimes.
  arXiv  Detail & Related papers  (2026-09-14T23:00:09Z)
• SEDCoT: Enhancing LLM-Based COBOL Code Translation via Symbolic Execution and Delta Debugging [49.898541267264115]
  Maintenance is increasingly challenging due to outdated technologies, sparse documentation, and developer retirement.<n>Traditional rule-based transcompilers yield outputs that are difficult to read and maintain.<n>We propose SEDCoT, a novel-to-C translation framework.
  arXiv  Detail & Related papers  (2026-07-05T03:07:10Z)
• Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution [0.0]
  cozy is a comparative binary analysis tool that analyzes a binary compiled from "unsafe" source code and a binary compiled from a translation of the source code to a memory safe language.<n> cozy walks the developer through differences in the behavior of the two binaries, presenting each difference and asking the user to assess whether the difference is intentional (good) or erroneous.<n> cozy has applications to automated translation, bug correction, code reviews, operation authorization, and automatic translation.
  arXiv  Detail & Related papers  (2026-05-12T20:33:33Z)
• PCodeTrans: Translate Decompiled Pseudocode to Compilable and Executable Equivalent [8.576619291429969]
  PCodeTrans bridges the gap between decompilation, recompilation, and rigorous function-level dynamic validation.<n>It achieves 100% function-level compilability on unstripped binaries alongside 99.55% and 99.89% test-validated behavioral consistency.
  arXiv  Detail & Related papers  (2026-03-16T05:54:24Z)
• Verifiable Provenance of Software Artifacts with Zero-Knowledge Compilation [5.939983212292006]
  We propose a novel approach to verifiable provenance based on compiling software with zero-knowledge virtual machines (zkVMs)<n>By executing a compiler within a zkVM, our system produces both the compiled output and a cryptographic proof attesting that the compilation was performed on the claimed source code with the claimed compiler.<n>Our results show that zk-compilation is applicable to real-world software and provides strong security guarantees.
  arXiv  Detail & Related papers  (2026-02-12T12:36:36Z)
• SALT4Decompile: Inferring Source-level Abstract Logic Tree for LLM-Based Binary Decompilation [17.58664677898224]
  saltm is a novel binary decompilation method that abstracts stable logical features between binary and source code.<n>saltm is highly effective in recovering the logic of the source code, significantly outperforming state-of-the-art methods.
  arXiv  Detail & Related papers  (2025-09-18T05:57:15Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• Function-to-Style Guidance of LLMs for Code Translation [59.487054943812836]
  We propose F2STrans, a function-to-style guiding paradigm designed to improve the performance of large language models in code translation.<n>Our approach comprises two key stages: (1) Functional learning, which optimize translation correctness using high-quality source-target code pairs.<n>We introduce a novel code translation benchmark that includes up-to-date source code, extensive test cases, and manually annotated ground-truth translations.
  arXiv  Detail & Related papers  (2025-07-15T08:25:02Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)
• ExeCoder: Empowering Large Language Models with Executability Representation for Code Translation [57.604506522287814]
  Existing large language models (LLMs) only learn the contextual semantics of code during pre-training.<n>We propose ExeCoder to utilize executability representations such as functional semantics, syntax structures, and variable dependencies.<n>We show that ExeCoder achieves state-of-the-art performance in code translation, surpassing existing open-source code LLMs by over 10.88% to 38.78% and over 27.44% to 42.97% on two metrics.
  arXiv  Detail & Related papers  (2025-01-30T16:18:52Z)
• AlphaTrans: A Neuro-Symbolic Compositional Approach for Repository-Level Code Translation and Validation [5.269923665485903]
  We propose AlphaTrans, a neuro-symbolic approach to automate repository-level code translation.<n>We leveraged AlphaTrans to translate ten real-world open-source projects consisting of 836, 8575, 2719> classes, methods, and tests.
  arXiv  Detail & Related papers  (2024-10-31T16:46:52Z)
• Program Translation via Code Distillation [20.668229308907495]
  Traditional machine translation relies on parallel corpora for supervised translation. Recent unsupervised neural machine translation techniques have overcome data limitations. We propose a novel model called Code Distillation (CoDist)
  arXiv  Detail & Related papers  (2023-10-17T04:59:15Z)
• 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)

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.