CHRusty - Translating C to Safer Rust
28/04/2022
Speaker
Abstract
Rust is rapidly gaining popularity for implementing safety-critical systems aiming to replace legacy code written in C and C++. One of the unique features of Rust is the ability to combine so-called safe and unsafe programming modes. Fragments of a program written in the former enjoy memory- and thread-safety, thanks to safe Rust's expressive ownership type system which rejects bug prone coding patterns. Fragments implemented in the latter mode can manipulate raw pointers and perform explicit memory management, allowing one to exercise C-style programming patterns that otherwise would be outlawed by the type system of safe Rust, thus, giving up on most of its static safety guarantees.
In this work, we address the challenge of translating unsafe Rust code to safe one. The conceptual novelty of our approach with regards to the state of the art is in phrasing the core of the translation as a type inference problem for raw pointers. Specifically, we deduce a safe Rust type for a raw pointer by collecting constraints arising from its usages and solving them via Constraint Handling Rules. Our constraint-based formulation enables uniform inference of various statically enforced disciplines for manipulating memory locations in safe Rust, including their ownership, borrowing, as well as representation of structured data, such as arrays and strings. We implemented our type inference algorithm for raw pointers and a type-driven translation from unsafe to safe Rust in a tool called CHRusty. Our evaluation on a series of standard benchmarks demonstrates that CHRusty outperforms existing state-of-the-art approaches both in terms of quantity (it soundly translates more unsafe Rust functions into safe ones) and quality (it produces more idiomatic safe Rust code).
Bio
Andreea is a Research Fellow in the department of computer science at School of Computing, NUS, where she previously obtained her PhD from. Her research interests span across the areas of Programming Languages and Software Engineering, including but not limited to software verification, program synthesis and automated program repair.