Modular Formal Verification of Safety Properties of Rust Programs with Unsafe Blocks

Rust is a modern systems programming language whose type system guarantees the absence of undefined behaviour. To enhance expressivity and performance, it allows programmers to temporarily relax typing rules using the syntactic construct called 'unsafe blocks'. However, in unsafe blocks, it is the programmer's responsibility to ensure that the code does not exhibit undefined behaviour. Even most expert programmers make mistakes and a memory safety bug in an unsafe block renders all the type system guarantees void. This research aims to address this problem by verifying the soundness of unsafe code in Rust programs. To do so, we are trying to design a provably sound Modular Symbolic Execution algorithm for Rust programs such that if the algorithm verifies a program, it is guaranteed that no execution of the program performs illegal memory accesses, data races, or any other kind of undefined behaviour.