Towards Scalable and Verifiable Automated Translation from C to Safe Rust

Abstract

Memory-safety bugs are one of the oldest and most common sources of security vulnerabilities, and their modern-day prevalence is a consequence of the widespread use of non-memory-safe languages such as C and C++. Transitioning away from C and C++ to memory-safe languages, namely Rust, to eliminate memory-safety bugs is growing in popularity as a potential solution, but manual migration of the vast C/C++ codebases in deployment to Rust is hardly practical. This thesis proposes an approach to verifiable automated translation from C to safe Rust that scales to real-world software. By introducing new tools and techniques for reasoning about Rust types, correctness, rewriting, verification, and testing tailored to C-to-Rust translation, this work will show that automated translation from C to Rust that both "does the right thing" is comparable in quality to code written by an experienced Rust developer is possible.