The Rust language is at the forefront of the Safe Coding methodology, with both governments and corporations advocating for a transition to Rust in order to guarantee the safety and reliability of criti-cal software infrastructure. Despite its promise, however, using Rust is not a silver bullet: safety guar-antees can be compromised, e.g., through the use of unsafe code, while properties related to correct-ness or security are out of scope for what Rust can establish.

To address these issues, the formal verification community has been investigating the development of static analysis and verification tools. While initial results are promising, significant scientific chal-lenges remain when reasoning about larger, real-world Rust systems, notably those using a mixture of unsafe code, interior mutability (a.k.a. dynamic borrow-checking), or concurrency and asynchronous tasks, for which existing tools and techniques propose no definitive answer.

This Dagstuhl Seminar will therefore focus on the theory and practice of Rust formal analysis and verification, bringing together tool developers and practitioners. Specifically, we will address three intertwined problems: first, theoretical foundations of the Rust language, specifically aspects that are crucial for analysis and verification; second, techniques for the analysis and verification of Rust pro-grams; and third, engineering practices and tool ecosystems that implement those techniques.

This three-day seminar will start with quick presentations from tool developers to provide an overview of existing, state-of-the-art Rust verifiers and analyzers. Small working groups will then focus on spe-cific topics, including clarifying the finer points of Rust semantics, discussing a common specification language for Rust, or surveying common engineering challenges when interacting with the Rust compiler. This work will be complemented by the creation of “VerifyThis”-like challenges for deduc-tive verification tools and “AnalyzeThat”-like challenges for static analysis tools, which will permit the comparison of existing tools and identify current shortcomings, fostering future collaborations between participants. An additional outcome will be identifying a list of blockers and/or challenges in Rust semantics that deserve the attention of this research community.

Creative Commons BY 4.0

Aymeric Fromherz, Peter Müller, Bryan Parno, and Jonathan Protzenko