Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution

• URL: http://arxiv.org/abs/2605.12731v1
• Date: Tue, 12 May 2026 20:33:33 GMT
• Title: Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Modern high-assurance software systems development favors memory safe languages such as SPARK (ADA) or Rust. However, developers often encounter non-memory safe code (e.g., C) in legacy systems and libraries which would be prohibitively expensive or risky to re-write. In response, developers have begun turning to machine learning/AI systems and other automated code translators. Automated translation comes with its own risks, however. The original and ported code are not precisely the same, semantically - otherwise there would be no point in performing the translation. To reduce these risks, we have developed cozy, a comparative binary analysis tool that simultaneously analyzes a binary compiled from "unsafe" source code and a binary compiled from a translation of the source code to a memory safe language. 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. Outside of the flagged differences, the binaries are formally verified to be equivalent. Consequently, the review process guarantees equivalence modulo changes approved by the developer. cozy has applications to automated translation, bug correction, code reviews, operation authorization, and automatic translation.

Related papers

• Mostly Automatic Translation of Language Interpreters from C to Safe Rust [9.34230791716657]
  We present Reboot, a technique that translates real-world interpreter programs from C to safe Rust.<n>We have translated six interpreters ranging from 6k to 23k lines of C code to safe Rust, with each translation requiring only 1 to 11 brief user interventions.<n>All translations pass 100% of the provided test suites, and achieve 62%--92% pass rates on separately created validation tests.
  arXiv  Detail & Related papers  (2026-06-25T14:59:08Z)
• Decaf: Improving Neural Decompilation with Automatic Feedback and Search [64.02615739798277]
  High-level syntax, identifiers, and custom data types are generally lost as the compiler translates human-readable code to low-level machine code.<n>Generative AI models are a natural fit for reconstructing high-level syntax, identifiers, and types.<n>We argue that compiler feedback can be used to dramatically improve the semantic correctness of neural decompiler outputs via search.
  arXiv  Detail & Related papers  (2026-05-12T04:21:26Z)
• Deterministic Fully-Static Whole-Binary Translation without Heuristics [4.112095753709181]
  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.
  arXiv  Detail & Related papers  (2026-05-08T19:25:06Z)
• Context-Guided Decompilation: A Step Towards Re-executability [50.71992919223209]
  Binary decompilation plays an important role in software security analysis, reverse engineering and malware understanding.<n>Recent advances in large language models (LLMs) have enabled neural decompilation, but the generated code is typically only semantically plausible.<n>We propose ICL4Decomp, a hybrid decompilation framework that leverages in-context learning (ICL) to guide LLMs toward generating re-executable source code.
  arXiv  Detail & Related papers  (2025-11-03T17:21:39Z)
• 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)
• Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis [8.361424157571468]
  Syzygy is an automated approach to translate C to safe Rust.<n>This is the largest automated and test-validated C to safe Rust code translation achieved so far.
  arXiv  Detail & Related papers  (2024-12-18T18:55:46Z)
• RedCode: Risky Code Execution and Generation Benchmark for Code Agents [50.81206098588923]
  RedCode is a benchmark for risky code execution and generation. RedCode-Exec provides challenging prompts that could lead to risky code execution. RedCode-Gen provides 160 prompts with function signatures and docstrings as input to assess whether code agents will follow instructions.
  arXiv  Detail & Related papers  (2024-11-12T13:30:06Z)
• Context-aware Code Segmentation for C-to-Rust Translation using Large Language Models [1.8416014644193066]
  Large language models (LLMs) show promise for automating this translation by generating more natural and safer code than rule-based methods. We propose an LLM-based translation scheme that improves the success rate of translating large-scale C code into compilable Rust code. In experiments with 20 benchmark C programs, including those exceeding 4 kilo lines of code, we successfully translated all programs into compilable Rust code.
  arXiv  Detail & Related papers  (2024-09-16T17:52:36Z)
• BinGo: Identifying Security Patches in Binary Code with Graph Representation Learning [19.22004583230725]
  We propose BinGo, a new security patch detection system for binary code. BinGo consists of four phases, namely, patch data pre-processing, graph extraction, embedding generation, and graph representation learning. Our experimental results show BinGo can achieve up to 80.77% accuracy in identifying security patches between two neighboring versions of binary code.
  arXiv  Detail & Related papers  (2023-12-13T06:35: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)
• Predicting Vulnerability In Large Codebases With Deep Code Representation [6.357681017646283]
  Software engineers write code for various modules, quite often, various types of errors get introduced. Same or similar issues/bugs, which were fixed in the past (although in different modules), tend to get introduced in production code again. We developed a novel AI-based system which uses the deep representation of Abstract Syntax Tree (AST) created from the source code and also the active feedback loop.
  arXiv  Detail & Related papers  (2020-04-24T13:18:35Z)

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.