Testing and Verifying Rust's Next Mile

While the Rust language provides memory safety by default, functional correctness and safety of programs using unsafe code remain unchecked. This thesis aims to improve the quality of Rust code and assist adoption of Rust by developing automatic testing and verification techniques for analyzing properties unchecked by the compiler.

For testing unsafe library APIs, we develop Rust semantic-aware synthesizers that generate well-typed Rust API calls to efficiently search through the state space guided by types. We develop SyRust, a synthesizer equipped with awareness of the Rust type semantics. Semantic awareness allows SyRust to generate well-typed API tests for polymorphic Rust library APIs and find memory safety bugs in them. To overcome the scalability limitations of SyRust on large API sets found in popular libraries, we develop Crabtree, a heuristic-guided API test synthesis algorithm that leverages code coverage and coverage over Rust types to guide the synthesis of tests. Results indicate Crabtree yields higher code coverage and faster coverage gain over SyRust.

We also develop automatic tools for lightweight Rust verification and testing of less-explored properties such as developer-annotated assertions, trait invariants, and translation equivalence. We develop propproof and TraitInv, which leverage existing Property-Based Testing harnesses and documented trait invariants respectively to automatically synthesize model-checking harnesses. We deploy these tools on popular open-source libraries and demonstrate their effectiveness in catching bugs. To assist developers migrating from other languages into Rust, we develop VERT, a general translator from multiple languages into Rust with verified equivalence. Our tool provides enhanced assurance of correct translation by checking that the candidate translation has the same input-output behavior as an oracle program generated from the original.