From ff29c5d2813b80d704e4c3fb6423bfd4257c9154 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 2 Jan 2016 17:42:05 +0100 Subject: [PATCH] unsafe post: finish first draft --- ralf/_drafts/the-scope-of-unsafe.md | 118 ++++++++++++++++++++++++++-- 1 file changed, 110 insertions(+), 8 deletions(-) diff --git a/ralf/_drafts/the-scope-of-unsafe.md b/ralf/_drafts/the-scope-of-unsafe.md index f6af9a0..36c972d 100644 --- a/ralf/_drafts/the-scope-of-unsafe.md +++ b/ralf/_drafts/the-scope-of-unsafe.md @@ -8,14 +8,15 @@ I'd like to talk about an important aspect of dealing with unsafe code, that sti > *When checking unsafe code, it is not enough to just check the contents of every `unsafe` block.* It turns out that the underlying reason for this observation is also a nice illustration for the concept of *semantic* types that comes up in my [work on formalizing Rust]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}) (or rather, its type system). +Finally, this discussion will once again lead us to realize that we rely on our type systems to provide much more than just type safety. ## An Example -Before we dive into the deeper reasons for why this is the case, let me start by convincing your that the above statement is actually true. +Before we dive into the deeper reasons for why we have to check (seemingly) safe code, let me start by convincing your that the above statement is actually true. -Consider the type `Vec`, which is roughly defined as follows: +Consider the type `Vec`, which is roughly defined as follows: {% highlight rust %} pub struct Vec { ptr: *mut T, @@ -30,17 +31,118 @@ Roughly speaking, `ptr` points to the heap-allocated block of memory holding the It is very easy to add a function to `Vec` that contains no `unsafe` code, and still breaks the safety of the data structure: {% highlight rust %} -fn evil(&mut self) { - self.cap += 2; +impl Vec { + fn evil(&mut self) { + self.len += 2; + } } {% endhighlight %} Why is this bad? -The next time `push` is called, the vector will think that it has space for two more element than it actually does, which will eventually (after sufficiently many calls to `push`) result in using unallocated memory. -Oops. +We can now "access" two more elements of the vector that have never been added! +This means we will read from uninitialized memory, or worse, from unallocated memory. +Oops! So, this example clearly shows that to evaluate the safety of types like `Vec`, we have to look at *every single function* provided by that data structure, even if it does not contain any `unsafe` code. -## A Reason +## The reason why + +So, why is it the case that a safe function can break `Vec`? +How can we even say that it is the safe function which is at fault, rather than some piece of `unsafe` code elsewhere in `Vec`? + +The intuitive answer most people will give is that `Vec` has *additional invariants* on its fields. +For example, `cap` must be greater than or equal to `len`. +More precisely speaking, `ptr` points to an array of type `T` and size `cap`, of which the first `len` elements have already been initialized. +The function `evil` above violates this invariant, while all the functions actually provided by `Vec` (including the ones that are implemented unsafely) preserve the invariant. +That's why `evil` is the bad guy. (The name kind of gave it away, didn't it?) + +This may seem obvious in hindsight, but I think it is actually fairly subtle. +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. + +## The semantic perspective + +There is another way to phrase the intuition of types having additional invariants: +Imagine we define another type in our Rust program: +{% highlight rust %} +pub struct MyType { + ptr: *mut T, + cap: usize, + len: usize, +} +{% endhighlight %} +We will define only one function for this type: +{% highlight rust %} +impl MyType { + fn evil(&mut self) { + self.len += 2; + } +} +{% endhighlight %} +This type *looks* exactly like `Vec`, doesn't it? +The two types are *syntactically* equal, and the same goes for the two `evil` functions. +Still, `MyType::evil` is a perfeclty benign function (despite its name). +How can this be? + +Remember that in a [previous blog post]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}), I argued that types have a *semantic* aspect. +For example, a function is semantically well-typed if it *behaves* properly on all valid arguments, independently of how, *syntactically*, the function body has been written down. + +Semantically speaking, `Vec` is very different from `MyType`: +If I have a `Vec`, I actually know that `ptr` is valid, that `len <= cap`, and so on. +I know nothing like that about an arbitrary instance of `MyType`: All I know here is that `cap` and `len` are valid elements of `usize`. +In other words, the additional invariants that we associate with `Vec` actually make this an *entirely different type*. +In order to formally describe what it means to be a `Vec`, we can't just say "well, that's a `struct` with these three fields". +That would be *wrong*. +But still, that's actually all the Rust compiler knows, and it is all that it actually checks: +When type checking `Vec::evil`, the compiler *thinks* that `Vec` is like `MyType`, and under that assumption, it deems `evil` a good function. +(Clearly, the compiler did not watch enough movies with serious villains.) + +In other words, we have to look beyond the mere syntactic appearance of a type, and into its deeper, semantic meaning. +As part of my work on formalizing Rust, I will eventually want to prove the soundness of types like `Vec` or `RefCell` and their associated operations. +In order to do so, I will first have to figure out what exactly the semantics of these types are. (This will be fairly easy for `Vec`, but really hard for `RefCell`. Can you guess why?) +Then I will have to check *every* function operating on these types and prove that they are actually well-typed. +Even if the Rust compiler says "yup, that function over there is fine, I checked every single statement of it", that's not enough because the Rust compiler has no idea about which types these functions are *actually* about. +All it sees is the syntactic surface. +It would then turn out, for example, that `Vec::evil` is actually not a semantically well-typed function. It may leave an invalid `Vec` in `self`. +This is just as bad as a function assigning `*b = 42` to a `b: &mut bool`. +The only difference is that the compiler will catch the second example since it knows all about the semantics of `bool`. It doesn't know enough about the semantics of `Vec`. + +## The actual scope of unsafe + +At this point, you may be slightly worried about the safety of the Rust ecosystem. +I just spent two sections arguing that the Rust compiler actually dosn't know what it is doing when it comes to checking functions that work on `Vec`. +How does it come that people carelessly use `Vec` in their programs without causing havoc all the time? +Or, to put it slightly different: If the "scope" of `unsafe` (i.e., the code that is potentially "infected" and has to be checked manually) grows beyond the syntactc `unsafe` blocks, then how far does it reach? +Does it sprawl through all our code, or is there some limit to its effect? + +As you probably imagined, of course there *is* a limit: The scope of `unsafe` ends at the next *abstraction boundary*. +This means that everything outside of the `std::vec` module does not have to worry about `Vec`. +Due to the privacy rules enforces by the compiler, code outside of that module cannot access the private fields of `Vec`, and hence it cannot tell the difference between the syntactic appearance of `Vec` and its actual, semantic meaning. +Of course, this also means that *everything* inside `std::vec` is potentially dangerous and needs to be proven to respect the semantics of `Vec`. + +## Abstraction Safety + +This nicely brings us to another important point, which I can only glimpse at here: + +> *The purpose of type systems goes far beyond type safety: They (also) serve to establish safe abstractions.* + +If the type system of Rust lacked a mechanism to establish abstraction (i.e., if there were no private fields), type safety would not be affected. +However, it would be very dangerous to write a type like `Vec` that has a semantic meaning beyond its syntactic appearance: +Since users of `Vec` can accidentally perform invalid operations, there is actually *no bound to the scope of `unsafe`*. +To formally establish safety, one would have to literally go over the entire program and prove that it doesn't misuse `Vec`. +The safety promise of Rust would be pretty much useless. + +This should not be entirely surprising if you read my previous [post about formalizing Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}), where I already argued that a proof of (syntactic) type safety does not help to justify safety of most Rust programs out there. +I am now making a similar point, coming from a different angle. + +The fact that Rust programers *can* use `Vec` and many other types without much care is a property of the type system that is independent of type safety. +We may call it *abstraction safety*. +Many type systems have this property, just think of `private` fields in Java or C++, or opaque signatures in ML. +However, few languages embrace using unsafe primitives and encapsulating them behind an abstraction as much as Rust does. +In some sense, Rust relies way more on abstraction safety than most languages - though in practice, programmers of all languages rely on abstraction safety a lot, if it is available. +(Most scripting languages, I am looking at you.) + +Abstraction safety is a very deep point that deserves its own blog post, I only skimmed the surface. +Watch this space, a link to such a post will eventually appear. (And I hope I don't have to write it myself.) + -So, why is this the case? -- 2.30.2