A KAIST research team led by Professor Sukyoung Ryu has achieved a global milestone with mathematically proven C-to-Rust conversion technology, redefining the path toward safe, verifiable, and future-proof software engineering.
Research: Automatically Translating C to Rust. Image Credit: Tee11 / Shutterstock
As the C programming language, long the foundation of critical global software systems, faces increasing scrutiny over security vulnerabilities, researchers at the Korea Advanced Institute of Science and Technology (KAIST) are leading an effort to establish mathematically verified methods for converting C code into the more secure Rust language. Their innovation offers a new paradigm for enhancing software reliability and cybersecurity, addressing a limitation that even large language model (LLM)-based approaches have yet to overcome.
The significance of this breakthrough was recognized globally when the research was selected as the cover story for the November 2025 issue of Communications of the ACM (CACM), the flagship journal of the Association for Computing Machinery (ACM), the world’s largest computing society.
Global recognition for foundational programming language research
KAIST announced on November 9 that the CACM cover story highlights the work of Professor Sukyoung Ryu and her Programming Language Research Group in the School of Computing. The publication comprehensively presents the team’s advances in C-to-Rust automatic conversion. This technology has been internationally acclaimed for its technical rigor and its visionary approach to future software security research.
From C to Rust: a paradigm shift in secure programming
Developed in the 1970s, the C language remains widely used across the software industry but has well-known structural limitations that contribute to critical bugs and memory safety vulnerabilities. In contrast, Rust, introduced in 2015, enforces strong memory safety and concurrency guarantees, enabling error detection and prevention at compile time. These capabilities have driven its adoption in operating system kernels, web browsers, and high-assurance software systems.
In response to the growing urgency of C-related security issues, the U.S. White House released a 2024 technology report recommending a phase-out of C in favor of safer alternatives. Simultaneously, the Defense Advanced Research Projects Agency (DARPA) identified Rust as the key successor language and initiated programs supporting automatic C-to-Rust translation technologies. Remarkably, Professor Ryu’s group had begun advancing this line of research before these international policy efforts gained traction.
World-first advances in automatic C-to-Rust conversion
Since 2023, Ryu’s team has developed multiple core technologies addressing the automatic conversion of key C features into Rust, each presented at top-tier international conferences:
- Mutex Conversion Technology (program synchronization), presented at the International Conference on Software Engineering (ICSE), May 2023.
- Output Parameter Conversion Technology (for result delivery), presented at Programming Language Design and Implementation (PLDI), June 2024.
- Union Conversion Technology (for heterogeneous data storage), presented at Automated Software Engineering (ASE), October 2024.
Each of these studies represents a world-first achievement, successfully demonstrating high-completeness conversion for complex C constructs.
Mathematical correctness: beyond AI-driven approaches
The CACM paper, authored by Dr. Jaemin Hong (Postdoctoral Research Fellow, KAIST Information and Electronics Research Institute) as first author, establishes a mathematically proven framework for verifying the correctness of C-to-Rust conversion. “Our conversion technology is built on programming language theory, and its greatest strength is the logical proof of correctness,” Dr. Hong explained. “While most research relies on large language models, our method provides mathematical guarantees of conversion accuracy.”
Dr. Hong will join the Department of Computer Science at UNIST as an Assistant Professor in March 2025.
Expanding international influence and future directions
Professor Ryu’s group has published in Communications of the ACM annually since 2023, reinforcing its position as a global leader in programming language and software verification research. The team also has four papers accepted at Automated Software Engineering (ASE) 2025, covering diverse fields in software engineering and automation. These include:
- Verification of quantum computing program correctness.
- WEST technology, automated validation and test generation for WebAssembly programs, which received the Distinguished Paper Award.
- Automated simplification of complex WebAssembly code to accelerate bug detection.
Support and impact
This research was supported by the National Research Foundation of Korea through the Leading Research Center and Mid-Career Researcher Support Programs, the Institute of Information & Communications Technology Planning & Evaluation (IITP), and Samsung Electronics. Together, these initiatives underscore KAIST’s leadership in secure software innovation and its global role in shaping the next generation of programming language research.
Source:
Journal reference:
Quantum-Secured Photonics Breakthrough Powers Next-Generation AI Data Centers