Files
Vlaicu_32341700_2025.pdf
Open access - Adobe PDF
- 1.39 MB
Details
- Supervisors
- Faculty
- Degree label
- Abstract
- This thesis addresses the challenge of proving the logical correctness of Rust code through weakest precondition calculus while staying as close as possible to the source code. Unlike existing solutions that often focus on unsafe code or focus on the Mid-Level Intermediate Representation (MIR) generated by the Rust compiler, we propose Secured Rust (Secrust), an extensible tool designed to provide formal verification of safe Rust methods. Taking advantage of Cargo, the Rust package manager, Secrust is a cargo-based package that generates control flow graphs (CFGs), identifies execution paths, and using weakest-precondition (WP) calculus derives final logical implications for verification. These implications are then checked using Microsoft Research’s Z3 SMT solver. The contributions of this thesis include the design and implementation of Secrust, CFG generation, postcondition substitution mechanisms with WP calculus, and Z3 integration. Secrust’s results demonstrate its ability to verify logical correctness while laying the groundwork for further and broader language features. Secrust is currently implemented to work on a subset of the Rust language, handling loops, conditions and most arithmetical operations.