todo: Add some words around the following useful links
Blog posts about unsafe
Ralf Jung The scope of unsafe
This post makes the point that unsafe code often depends on invariants holding and that adding safe code that breaks the invariants can make code incorrect.
There used to be claims on the interwebs that “if a Rust program crashes, the bug must be in some unsafe block”. (And there probably still are.) Even academic researchers working on Rust got this wrong, arguing that in order to detect bugs in data structures like Vec it suffices to check functions involving unsafe code.
- Niko Matsakis
- Unsafe abstractions
This post makes the point that you need to look at which data structure fields are accessible to understand whether your unsafe code is safe because even unsafe code could break your code’s invariants. For that reason, the unsafe boundary is closer to the module boundary (assuming the fields are not public).
- Alex Ozdemir
An early automated empirical analysis of thousands of Rust crates looking at how ‘unsafe’ is used in Rust code. See astrauskas:oopsla:2020, qin:pldi:2020 and evans:icse:2020 for more recent analyses that dig into this from various perspectives.
A “public escape” occurs when a safety condition escapes through a safe public interface so that that interface cannot uphold the “Abstraction Safety Contract” (ASC).
Proposes a backwards analysis to calculate the safety condition (precondition?) of a public, safe function and check that the condition always holds.
Notes related to Rust unsafe code
Papers related to Rust unsafe code
- Fidelius Charm: Isolating unsafe Rust code [almohri:codaspy:2018]
- How do programmers use unsafe Rust? [astrauskas:oopsla:2020]
- Verifying Rust programs with SMACK [baranowski:atva:2018]
- Verifying safe clients of unsafe code and trait implementations in Rust [beckmann:msc:2020]
- You can't spell trust without Rust [beingessner:msc:2015]
- Is Rust used safely by software developers? [evans:icse:2020]
- Safe systems programming in Rust: The promise and the challenge [jung:cacm:2021]
- RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
- Stacked borrows: An aliasing model for Rust [jung:popl:2020]
- The case for writing a kernel in Rust [levy:apsys:2017]
- Securing unsafe Rust programs with XRust [liu:icse:2020]
- Exploiting mixed binaries [papaevripides:acmtps:2021]
- Understanding memory and thread safety practices and issues in real-world Rust programs [qin:pldi:2020]
- Crust: A bounded verifier for Rust [toman:ase:2015]
- Memory-safety challenge considered solved? An in-depth study with all Rust CVEs [xu:arxiv:2021]
- GhostCell: Separating permissions from data in Rust [yanovski:unknown:2021]