A Separation Logic for Stacked Borrows
Daniël Louwrink

Abstract:
Rust is a systems programming language that uses a strong static type system to prevent memory safety issues (such “use-after-free” bugs and buffer overflows) that are common in programs written in languages such as C and C++. The RustBelt project (Jung et al. 2018a) has developed a machine- checked proof of the safety guarantees provided by the Rust language, formally showing that the Rust type system indeed prevents the issues that it claims to prevent. However, RustBelt uses an operational semantics that is incompatible with certain desirable compiler optimizations inspired by the guarantees that the Rust type system provides. Recently, Jung et al. have introduced Stacked Borrows (Jung et al. 2020), a new operational semantics for Rust that allows such compiler optimizations to be performed. However, this new operational semantics has not yet been integrated into the RustBelt safety proof, meaning it has not been formally shown that the safety guarantees of the Rust type system still hold for the new Stacked Borrows semantics.
  This thesis takes the first step toward updating the RustBelt safety proof to account for the new Stacked Borrows semantics. Specifically, we develop a new program logic, which we call Stacked Borrows Separation Logic (SBSL), for reasoning about the behavior of programs executed according to the Stacked Borrows semantics. Building on RustBelt, we have developed a machine-checked proof of the soundness of SBSL using the Coq proof assistant. The key conceptual contribution in SBSL is the notion of ghost stacks, which enables SBSL to abstract away irrelevant implementation details and allows for better reasoning about concurrency compared to a naive approach.