A Static analysis for Rust in Infer
A.M. Seijs (TU Delft - Electrical Engineering, Mathematics and Computer Science)
M.A. Costea – Mentor (TU Delft - Programming Languages)
S.S. Chakraborty – Mentor (TU Delft - Programming Languages)
S. Dumančić – Graduation committee member (TU Delft - Algorithmics)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Rust is a systems programming language that guarantees both performance and Memory Safety through its memory model. With unsafe rust it is possible to opt-out of some security guarantees made by the compiler. However, this comes at the risk of re-introducing memory bugs. While various tools already exist for detecting memory errors in (unsafe) Rust, they are either dynamic or focus on proving the absence of bugs. In this thesis we lay the foundations for a static analysis for Rust that focuses on proving the presence of bugs (Under Approximation) instead of their absence (Over Approximation). We show how we can use a formal framework called incorrectness separation logic (ISL) to show the presence of memory errors in Rust. We add Rust support to Infer, a static analysis tool by Meta that uses ISL to prove the presence of bugs. This is done by translating Rust to a Verification Intermediate Language. Finally, we show that our extension to can be used to detect memory bugs in Rust such as null pointer dereferences, dangling pointer dereferences and use after frees.
Dataset: https://doi.org/10.4121/f0b3b808-51c3-4637-b6ff-3654506da71c