Modular Formal Verification of Rust Programs with Unsafe Blocks

2022/12/26 by Nima Rahimi Foroushaani, Bart Jacobs, Foroushaani, Nima Rahimi +1 · 1 voice · 1 citation
Computer Science · #Software Testing and Debugging Techniques #Parallel Computing and Optimization Techniques #Formal Methods in Verification

paper · pdf · doi:10.48550/arxiv.2212.12976

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.

Cited by

• Soteria: Efficient Symbolic Execution as a Functional Library

Discussions

• Modular Formal Verification of Rust Programs with Unsafe Blocks [lobsters, 5 points, 0 comments]

Related

• Surveying the Rust Verification Landscape
• A Trace-based Approach for Code Safety Analysis
• Lessons Learned So Far From a Community Effort to Verify the Rust Standard Library (work-in-progress)
• Is rust used safely by software developers?
• A Mixed-Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling