Modular Formal Verification of Rust Programs with Unsafe Blocks

TL;DR

This paper presents a modular symbolic execution approach to verify the safety of unsafe Rust code blocks, aiming to ensure soundness despite the programmer’s manual memory safety guarantees.

Contribution

It introduces a novel modular symbolic execution method specifically designed for verifying unsafe Rust code, addressing a critical gap in ensuring memory safety.

Findings

Developed a symbolic execution algorithm for unsafe Rust code

Achieved progress in verifying soundness of unsafe blocks

Potential to improve safety guarantees in Rust programs

Abstract

Rust is a modern systems programming language whose type system guarantees memory safety. For the sake of expressivity and performance it allows programmers to relax typing rules temporarily, using unsafe code blocks. However, in unsafe blocks, the burden of making sure that the code does not end up having undefined behaviour is on the programmer. Even most expert programmers make mistakes and a memory safety bug in an unsafe block renders all the type system guarantees void. To address this problem we are trying to verify soundness of Rust unsafe code applying our Modular Symbolic Execution algorithm. This text outlines our approach and the progress that has been made so far.