From 85773ae906d4e1ed1e57a5b6676e9628d092cee2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20Przytu=C5=82a?= Date: Thu, 19 Dec 2024 09:42:43 +0100 Subject: [PATCH 1/2] Safe code guarantees --- content/lessons/15_unsafe/index.md | 31 ++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/content/lessons/15_unsafe/index.md b/content/lessons/15_unsafe/index.md index 311165f..0f040fb 100644 --- a/content/lessons/15_unsafe/index.md +++ b/content/lessons/15_unsafe/index.md @@ -37,6 +37,37 @@ In the following code sample, we show all superpowers of `unsafe` code: Safe code may **_never_** cause Undefined Behaviour. +This is a valid _sound_ code, with a safe encapsulation over `unsafe` interior. + +```rust +fn index(idx: usize, arr: &[u8]) -> Option { + if idx < arr.len() { + unsafe { + Some(*arr.get_unchecked(idx)) + } + } else { + None + } +} +``` + +_(Un)soundness_ means that there exists a _possibility_ to trigger UB. +The following code is _unsound_ (why? what has changed?): + +```rust +fn index(idx: usize, arr: &[u8]) -> Option { + if idx <= arr.len() { + unsafe { + Some(*arr.get_unchecked(idx)) + } + } else { + None + } +} +``` + +But we only changed safe code! This shows that `unsafe` is unfortunately not perfectly scoped and isolated. We need to be extra careful when writing `unsafe` code. + ## Reading - [The Book, Chapter 19.1](https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html) From 8437981b87acc4fa8173f6a8f49bc91c5203ae7c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20Przytu=C5=82a?= Date: Thu, 19 Dec 2024 09:42:59 +0100 Subject: [PATCH 2/2] RUDRA --- content/lessons/15_unsafe/index.md | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/content/lessons/15_unsafe/index.md b/content/lessons/15_unsafe/index.md index 0f040fb..d766312 100644 --- a/content/lessons/15_unsafe/index.md +++ b/content/lessons/15_unsafe/index.md @@ -35,7 +35,9 @@ In the following code sample, we show all superpowers of `unsafe` code: ## Safe code guarantees -Safe code may **_never_** cause Undefined Behaviour. +The single fundamental property of Safe Rust, _the soundness property_: + +**No matter what, Safe Rust can't cause Undefined Behavior.** This is a valid _sound_ code, with a safe encapsulation over `unsafe` interior. @@ -75,3 +77,15 @@ But we only changed safe code! This shows that `unsafe` is unfortunately not per - [The Rustonomicon](https://doc.rust-lang.org/nomicon/), especially chapter 1 _(Meet Safe and Unsafe)_ - [How unpleasant is Unsafe Rust?](https://www.reddit.com/r/rust/comments/16i8lo2/how_unpleasant_is_unsafe_rust/) + +- [RUDRA: Finding Memory Safety Bugs in Rust at the Ecosystem Scale](https://taesoo.kim/pubs/2021/bae:rudra.pdf) - automatic static analyzer to find 3 most frequent subtle bugs in `unsafe` code: + + 1. panic (unwind) safety bug (analogous to exception-handling guarantees in C++), + 2. higher-order safety invariant (assuming certain properties of the type that the generic is instantiated with that are not guaranteed by the type system, e.g., _purity_), + 3. propagating Send/Sync in Generic Types (implementing Send/Sync unconditionally for T, even if T contains non-Send/non-Sync types inside). + + **RUDRA found 264 previously unknown memory-safety bugs in 145 packages on crates.io!!!** + + Is Rust really a safe language...? + + Only transitively. _Safe Rust_ is sound iff `unsafe` code called by it is sound too.