personal/_posts/2016-01-09-the-scope-of-unsafe.md

   1 ---
   2 title: The Scope of Unsafe
   3 categories: research rust
   4 reddit: /rust/comments/4065l2/the_scope_of_unsafe/
   5 license: CC BY-SA 4.0
   6 license-url: https://creativecommons.org/licenses/by-sa/4.0/
   7 ---
   8
   9 I'd like to talk about an important aspect of dealing with unsafe code, that still regularly seems to catch people on the wrong foot:
  10
  11 > *When checking unsafe code, it is not enough to just check the contents of every `unsafe` block.*
  12
  13 The "scope" in the title refers to the extent of the code that has to be manually checked for correctness, once `unsafe` is used.
  14 What I am saying is that the scope of `unsafe` is larger than the `unsafe` block itself.
  15
  16 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]({% post_url 2015-10-12-formalizing-rust %}) (or rather, its type system).
  17 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.
  18
  19 **Update (Jan 11th):** Clarified the role of privacy; argued why `evil` is the problem.
  20
  21 <!-- MORE -->
  22
  23 ## An Example
  24
  25 Before we dive into the deeper reasons for *why* we have to check (seemingly) safe code, let me start by convincing your that this is actually the case.
  26
  27 Consider the type `Vec`, which is roughly defined as follows:
  28 {% highlight rust %}
  29 pub struct Vec<T> {
  30     ptr: *mut T,
  31     cap: usize,
  32     len: usize,
  33 }
  34 {% endhighlight %}
  35 (I know this definition is not entirely right. If you want to know how the actual `Vec` works, check out the [corresponding section of the Rustonomicon](https://doc.rust-lang.org/nightly/nomicon/vec.html).)
  36
  37 Roughly speaking, `ptr` points to the heap-allocated block of memory holding the contents of the vector, `cap` holds the size of that memory block (counted in number of `T`), and `len` stores how many elements are actually stored in the vector right now.
  38 `cap` and `len` can be different if the memory block contains some extra (uninitialized) space beyond the end of the vector, which speeds up pushing an element to the end of the vector (at the cost of some extra memory usage).
  39
  40 It is very easy to add a function to `Vec` that contains no `unsafe` code, and still breaks the safety of the data structure:
  41 {% highlight rust %}
  42 impl Vec<T> {
  43     pub fn evil(&mut self) {
  44         self.len += 2;
  45     }
  46 }
  47 {% endhighlight %}
  48
  49 Why is this bad?
  50 We can now "access" two more elements of the vector that have never been added!
  51 This means we will read from uninitialized memory, or worse, from unallocated memory.
  52 Oops!
  53
  54 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.
  55
  56 ## The Reason Why
  57
  58 Why is it the case that a safe function can break `Vec`?
  59 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`?
  60
  61 The intuitive answer is that `Vec` has *additional invariants* on its fields.
  62 For example, `cap` must be greater than or equal to `len`.
  63 More precisely speaking, `ptr` points to an array of type `T` and size `cap`, of which the first `len` elements have already been initialized.
  64 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.
  65 That's why `evil` is the bad guy. (The name kind of gave it away, didn't it?)
  66
  67 Some will disagree here and say: "Wait, but there is some `unsafe` code in `Vec`, and without that `unsafe` code `evil` would be all right, so isn't the problem actually that `unsafe` code?"
  68 This observation is correct, however I don't think this position is useful in practice.
  69 `Vec` with `evil` clearly is a faulty data structure, and to fix the bug, we would remove `evil`.
  70 We would never even think about changing the `unsafe` code such that `evil` would be okay, that would defeat the entire purpose of `Vec`.
  71 In that sense, it is `evil` which is the problem, and not the `unsafe` code.
  72
  73 This may seem obvious in hindsight (and it is also [discussed in the Rustonomicon](https://doc.rust-lang.org/nightly/nomicon/working-with-unsafe.html)), but I think it is actually fairly subtle.
  74 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.)
  75 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.
  76 That's why I think it's worth dedicating an entire blog post to this point.
  77 But we are not done yet, we can actually use this observation to learn more about types and type systems.
  78
  79 ## The Semantic Perspective
  80
  81 There is another way to phrase the intuition of types having additional invariants:
  82
  83 > *There is more to types like `Vec` than their syntactic definition gives away*.
  84
  85 Imagine we define another type in our Rust program:
  86 {% highlight rust %}
  87 pub struct MyType<T> {
  88     ptr: *mut T,
  89     cap: usize,
  90     len: usize,
  91 }
  92 {% endhighlight %}
  93 We will define only one function for this type:
  94 {% highlight rust %}
  95 impl MyType<T> {
  96     pub fn evil(&mut self) {
  97         self.len += 2;
  98     }
  99 }
 100 {% endhighlight %}
 101 This type *looks* exactly like `Vec`, doesn't it?
 102 The two types are *syntactically* equal, and the same goes for the two `evil` functions.
 103 Still, `MyType::evil` is a perfectly benign function (despite its name).
 104 How can this be?
 105
 106 Remember that in a [previous blog post]({% post_url 2015-10-12-formalizing-rust %}), I argued that types have a *semantic* aspect.
 107 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.
 108
 109 The reason for `MyType::evil` being fine, while `Vec::evil` is bad, is that semantically speaking, `Vec` is very different from `MyType` -- even though they look so similar.
 110 If I have a `Vec`, I actually know that `ptr` is valid, that `len <= cap`, and so on.
 111 I know nothing like that about an arbitrary instance of `MyType`: All I have here is that `cap` and `len` are valid elements of `usize`.
 112 In other words, the additional invariants that we associate with `Vec` actually make this an *entirely different type*.
 113 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".
 114 That would be *wrong*.
 115 But still, that's actually all the Rust compiler knows, and it is all that it actually checks:
 116 When type checking `Vec::evil`, the compiler *thinks* that `Vec` is like `MyType`, and under that assumption, it deems `evil` a good function in both cases.
 117 (Clearly, the compiler did not watch enough movies with serious villains.)
 118
 119 In other words, we have to look beyond the mere syntactic appearance of a type, and into its deeper, semantic meaning.
 120 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.
 121 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?)
 122 Then I will have to check *every* function operating on these types and prove that they are actually well-typed.
 123
 124 The compiler, however, cannot guess or check the actual semantics of `Vec`, the additional invariants we came up with; and this can make seemingly safe code like `Vec::evil` become unsafe.
 125 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.
 126 All it sees is the syntactic surface.
 127
 128 While proving soundness of `Vec`, it would then turn out that `Vec::evil` is actually not a semantically well-typed function.
 129 It will invalidate `self`, such that is is no longer an instance of the *actual* (semantic) type `Vec`.
 130 This is just as bad as a function assigning `*f = 42u32` to a `f: &mut f32`.
 131 The difference between `Vec` and `MyType` is no less significant than the difference between `f32` and `u32`.
 132 It's just that the compiler has been specifically taught about `f32`, while it doesn't know enough about the semantics of `Vec`.
 133
 134 ## The Actual Scope of Unsafe
 135
 136 At this point, you may be slightly worried about the safety of the Rust ecosystem.
 137 I just spent two sections arguing that the Rust compiler actually doesn't know what it is doing when it comes to checking functions that work on `Vec`.
 138 How does it come that people carelessly use `Vec` in their programs without causing havoc all the time?
 139 Or, to put it slightly differently: If the scope of `unsafe` grows beyond the syntactic `unsafe` blocks, then just how far does it reach?
 140 Does it sprawl through all our code, silently infecting everything we write -- or is there some limit to its effect?
 141
 142 As you probably imagined, of course there *is* a limit. Rust would not be a useful language otherwise.
 143 *If* all your additional invariants are about *private* fields of your data structure, then the scope of `unsafe` ends at the next *abstraction boundary*.
 144 This means that everything outside of the `std::vec` module does not have to worry about `Vec`.
 145 Due to the privacy rules enforced by the compiler, code outside of that module cannot access the private fields of `Vec`.
 146 That code does not have a chance to violate the additional invariants of `Vec` -- it cannot tell the difference between the syntactic appearance of `Vec` and its actual, semantic meaning.
 147 Of course, this also means that *everything* inside `std::vec` is potentially dangerous and needs to be proven to respect the semantics of `Vec`.
 148
 149 ## Abstraction Safety
 150
 151 This nicely brings us to another important point, which I can only glimpse at here:
 152
 153 > *The purpose of type systems goes far beyond type safety: They (also) serve to establish safe abstractions.*
 154
 155 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.
 156 However, it would be very dangerous to write a type like `Vec` that has a semantic meaning beyond its syntactic appearance.
 157 All code could perform invalid operations like `Vec::evil`, operations that rely on the assumption that `Vec` is just like `MyType`.
 158 There would actually be *no bound to the scope of `unsafe`*.
 159 To formally establish safety, one would have to literally go over the entire program and prove that it doesn't misuse `Vec`.
 160 The safety promise of Rust would be pretty much useless.
 161
 162 This should not be entirely surprising if you read the aforementioned [post about formalizing Rust's type system]({% 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.
 163 I am now making a similar point, coming from a different angle.
 164
 165 The fact that Rust programmers *can* use `Vec` and many other types without much care is a property of the type system that is independent of type safety.
 166 We rely on the fact that the type system lets us build abstraction boundaries that cannot be violated by safe code.
 167 We may call this *abstraction safety*.
 168 Many type systems have this property, just think of `private` fields in Java or C++, or opaque signatures in ML.
 169 However, few languages embrace using unsafe primitives and encapsulating them behind a layer of abstraction as much as Rust does.
 170 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.
 171 (Most scripting languages, I am looking at you.)
 172
 173 Abstraction safety is a very deep point that deserves its own blog post, I only skimmed the surface here.
 174 Watch this space, a link to such a post will eventually appear. (And I hope I don't have to write it myself.)
 175
 176