UC Santa Barbara

Infrastructure software is written in low-level programming languages like C toallow precise control of resources. However, C lacks safety features to ensure memory and thread safety. These safety issues result in serious security vulnerabilities or unreliable behavior. Rust is a programming language that provides the same fine-grained control with automatically-checked safety measures. Rust is being adopted by some large C and C++ code bases such as Linux, Firefox, and Chromium. However, proving a program's safety to the Rust compiler requires non-local reasoning about ownership and lifetimes of objects in the program so translating C programs to safe Rust programs is nontrivial.

This thesis presents the challenges in translating C programs to safe Rustprograms, along with a categorization of different classes of unsafety. To kick-start automated translation from C to safe Rust, I present a novel method to infer object lifetimes and ownership using the compiler as an oracle. I then develop an evaluation methodology to measure the potential impact of this method independent of other causes of unsafety in the program. With this methodology, I show that the efficacy of this method (along with any potential method to discover existing safe uses of objects in the program) is limited by the precision of the type system when propagating unsafety information. Then, I investigate the impact of more sensitive data flow analyses to curb the spread of unsafety, and show that they can be encoded by transforming the program without changing the type system. Overall, the findings of this thesis are that (1) the causes of unsafety are intertwinend, (2) using the compiler errors to derive lifetime information is effective for discovering existing safe uses of objects, (3) imprecision of the type system leads to excessive spread of unsafety (as lack of provable safety according to the compiler), and (4) this can be mitigated by transforming the program to make the results of a more precise analysis available to the type checker.