📝 SummarXiv

Abstract

Although Rust primarily intends to be a safe programming language that excludes undefined behaviour, it provides its users with the escape hatch of unsafe Rust, allowing them to circumvent some of its strong compile-time checks. This additional freedom has some advantages, including potentially more efficient code, which is one of the main reasons why unsafe code is used extensively throughout Rust's standard library. However, because unsafe code also re-opens the door to undefined behaviour, Amazon has convened a community to verify the safety of the standard library, and in particular the unsafe code contained therein. Given that this effort is done in public and open-sourced, we have access to a wealth of information on how people are verifying the standard library, as well as what is currently possible and what still appears to be beyond the state of the art for verified software. In this paper, we discuss the lessons learned thus far from this verification effort, from both our work on it, as well as that of the broader community. In particular, we start by reviewing what has been accomplished thus far, as well as the main tools used (specifically, their advantages and their limitations). We then focus on some of the remaining fundamental obstacles to verifying the standard library, and propose potential solutions to overcome them. We hope that these observations can guide future verification of not only the standard library, but also unsafe Rust code in general.