PIs: Meng Wang and Cristina David, University of Bristol

  • Rust is a modern programming language which features a combination of memory safety and low-level control.
  • There is a lot of interest from both academia and industry in migrating legacy codebases from C to Rust. However, C code is often translated to unsafe Rust, which simply replicates the unsafe use of C pointers.
  • We developed a translation tool from C to Rust, that aims to enhance memory safety through a scalable and precise ownership analysis that is able to handle complex inductively-defined data structures and nested pointers.

Rust is a modern programming language featuring an exciting combination of memory safety and low-level control. In particular, Rust takes inspiration from ownership and substructural types and restricts certain memory accesses to their owners.

This means that although multiple pointers to the resource can co-exist (through a mechanism known as borrowing), certain operations can only be performed by the owner. The Rust compiler is able to statically verify the ownership constraints and consequently guarantee memory and thread safety. This distinctive advantage of provable safety makes Rust a very popular language, and the prospect of migrating legacy codebases in C to Rust is very appealing.

In response to this demand, automated tools translating C code to Rust emerge from both industry and academia. However, all existing techniques are either syntax-oriented, thus relying on the use of Rust unsafe regions, or based on trial-and-error, thus making changes to the code until it is accepted by the Rust compiler.

In this project, we take a more principled approach by developing a novel ownership analysis of pointers that is efficient (scaling to large programs), sophisticated (handling nested pointers and inductively-defined data structures), and precise (being field and flow sensitive). Based on this ownership analysis, we then design an automated translation system from C to Rust. By encoding the ownership models in the generated Rust code, the translation is able to refactor unsafe C pointers to safe Rust ones. We implemented our technique in an open-source tool named CROWN.  A web version of it is available at https://crownbristol.github.io/.

PUBLICATIONS. Zhang, C. David, Y. Yu, M. Wang, “Ownership Guided C to Rust Translation”, Proceedings of the International Conference on Computer Aided Verification” (CAV), 2023.

RELATED GRANTS. Royal Society University Research Fellowships Renewals 2022, “Program synthesis for modern, memory safe, programming languages”, 27/06/2023 – 26/06/2026, £363,322.

IMPACT. The evaluation of the tool is still at an early stage,  but there are already interest from industry, including Github and Amazon.