The KAIST Professor Ryu Seok-young's research team has pioneered a novel automated C-to-Rust code transformation technology, addressing the critical security vulnerabilities inherent in the widely used C language. The core methodology of this research distinguishes itself from large language model (LLM)-based approaches by guaranteeing the "mathematical correctness" of the conversion. This assurance implies that the transformed Rust code is provably semantically equivalent or preserves crucial properties of the original C code, thereby preventing the introduction of new bugs or security flaws during the translation process.

This foundational technology is rooted in programming language theory, leveraging rigorous formal methods to ensure the integrity of the transformation. Specifically, the team has developed and presented individual conversion techniques for complex C constructs at top-tier international conferences:

1. Mutex Conversion: Presented at ICSE in May 2023, this technique addresses the accurate and safe translation of C's mutexes for program synchronization into Rust's concurrency primitives, ensuring data race freedom and correct locking behavior.
2. Output Parameter Conversion: Unveiled at PLDI in June 2024, this method focuses on transforming C functions that return values via output parameters (e.g., pointers passed by reference) into idiomatic and safe Rust patterns, likely leveraging Rust's ownership and borrowing system to guarantee memory safety and prevent use-after-free or double-free errors.
3. Union Conversion: Presented at ASE in October 2024, this technique tackles the challenging task of converting C's union types, which allow different data types to occupy the same memory location, into safe Rust equivalents, potentially utilizing enums with data or discriminated unions to maintain type safety and prevent undefined behavior arising from misinterpreting union members.

The mathematical correctness of their transformation is established by theoretically demonstrating that the transformation rules preserve the program's intended behavior and safety properties. This likely involves:

• Formal Semantics: Defining precise operational or denotational semantics for the C constructs and their corresponding Rust translations.
• Proof of Preservation: Rigorously proving that the transformation function $\mathcal{T}: \text{C Program} \to \text{Rust Program}$ satisfies properties such as semantic equivalence, i.e., for a given C program $P_C$, its transformed Rust counterpart $P_R = \mathcal{T}(P_C)$ exhibits the same observable behavior or satisfies stronger safety guarantees (e.g., memory safety guaranteed by Rust's borrow checker) that were not provably present in $P_C$. This can be expressed as $\forall P_C, \text{semantics}(P_C) \equiv \text{semantics}(\mathcal{T}(P_C))$, where $\equiv$ denotes equivalence under a suitable notion.

The significance of this research is underscored by global efforts, including recommendations from the US White House to cease C language usage and DARPA's initiatives for automated C-to-Rust conversion. The team's work, which has been featured as a cover paper in ACM's CACM, offers a scientifically rigorous and practical solution to enhance software security by facilitating the migration of legacy C codebases to the memory-safe Rust language.