From: Ralf Jung Date: Sat, 2 Jan 2016 18:06:36 +0000 (+0100) Subject: tune the new blog post; use longer dashes X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/4d9c13e4b5c8fd488ab78ae72db7f095669fcb67 tune the new blog post; use longer dashes --- diff --git a/personal/_drafts/the-scope-of-unsafe.md b/personal/_drafts/the-scope-of-unsafe.md index 36c972d..641b4bb 100644 --- a/personal/_drafts/the-scope-of-unsafe.md +++ b/personal/_drafts/the-scope-of-unsafe.md @@ -7,14 +7,17 @@ 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). +The "scope" in the title refers to the extent of the code that has to be manually checked for correctness, once `unsafe` is used. +What I am saying is that the scope of `unsafe` is larger than the `unsafe` block itself. + +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 we have to check (seemingly) safe code, 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 this is actually the case. Consider the type `Vec`, which is roughly defined as follows: {% highlight rust %} @@ -47,10 +50,10 @@ So, this example clearly shows that to evaluate the safety of types like `Vec`, ## The reason why -So, why is it the case that a safe function can break `Vec`? +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. +The intuitive answer 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. @@ -59,10 +62,15 @@ 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. +That's why I think it's worth dedicating an entire blog post to this point. +But we are not done yet, we can actually use this observation to learn more about types and type systems. ## The semantic perspective There is another way to phrase the intuition of types having additional invariants: + +> *There is more to types like `Vec` than their definition gives away*. + Imagine we define another type in our Rust program: {% highlight rust %} pub struct MyType { @@ -87,9 +95,9 @@ 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`: +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. 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`. +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`. 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*. @@ -103,21 +111,24 @@ In order to do so, I will first have to figure out what exactly the semantics of 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`. + +While proving soundness of `Vec`, it would then turn out 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 `*f = 42u32` to a `f: &mut f32`. +The difference between `Vec` and `MyType` is no less significant than the difference between `f32` and `u32`. +It's just that the compiler has been specifically taught about `f32`, while 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? +Or, to put it slightly differently: If the scope of `unsafe` grows beyond the syntactc `unsafe` blocks, then how far does it reach? +Does it sprawl through all our code, silently infecting everything we write -- 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*. +As you probably imagined, of course there *is* a limit. Rust would not be a useful language otherwise. +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. +Due to the privacy rules enforced 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 @@ -127,19 +138,20 @@ This nicely brings us to another important point, which I can only glimpse at he > *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`*. +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 would actually be *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. +This should not be entirely surprising if you read the aforementioned [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*. +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. +We rely on the fact that the type system lets us build abstraction boundaries that cannot be violated by safe code. +We may call this *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. +However, few languages embrace using unsafe primitives and encapsulating them behind a layer of 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. diff --git a/personal/_posts/2015-10-12-formalizing-rust.md b/personal/_posts/2015-10-12-formalizing-rust.md index 672f900..9f5dc7a 100644 --- a/personal/_posts/2015-10-12-formalizing-rust.md +++ b/personal/_posts/2015-10-12-formalizing-rust.md @@ -4,7 +4,7 @@ categories: research rust reddit: /rust/comments/3ofkz6/formalizing_rust/ --- -My current research project - and the main topic of my PhD thesis - is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system. +My current research project -- and the main topic of my PhD thesis -- is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system. Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety. Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](http://www.oreilly.com/programming/free/files/why-rust.pdf) a lot on why we need such a language, so I won't lose any more words on this. Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out [Rust-101](https://www.ralfj.de/projects/rust-101/main.html), a hands-on Rust tutorial I wrote. @@ -13,7 +13,7 @@ I am going to assume some basic familiarity with Rust in the following. Why do we want to do research on Rust? First of all, I'm (becoming) a programming languages researcher, and Rust is an interesting new language to study. It's going to be fun! Honestly, that's enough of a reason for me. But there are other reasons: It shouldn't be a surprise that [bugs](https://github.com/rust-lang/rust/issues/24292) have [been](https://github.com/rust-lang/rust/issues/25860) [found](https://github.com/rust-lang/rust/issues/24880) in Rust. -There are lots of things that can be done about such bugs - my take on this is that we should try to *prove*, in a mathematical rigorous way, that no such bugs exist in Rust. +There are lots of things that can be done about such bugs -- my take on this is that we should try to *prove*, in a mathematical rigorous way, that no such bugs exist in Rust. This goes hand-in-hand with other approaches like testing, fuzzing and [static analysis](https://homes.cs.washington.edu/~emina/pubs/crust.ase15.pdf). However, we (at my [research group](http://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do. @@ -25,7 +25,7 @@ Let me just get this out of the way at the beginning: The formal model is not go Some of the missing pieces will hopefully be added later, some maybe not, and some just don't matter for what I am attempting to do. Our focus is on the type system, on ownership and borrowing and the ideas these concepts found on. Many features of Rust are pretty much orthogonal to this, so I won't attempt to model them accurately. -This starts with the language itself: The syntax, the concrete set of primitive operations (except for those that concern pointers), the structure of code with modules and crates - none of this really matters. +This starts with the language itself: The syntax, the concrete set of primitive operations (except for those that concern pointers), the structure of code with modules and crates -- none of this really matters. I have some idea what to do with traits, unwinding and a few other pieces, but trying to get all of that right in the beginning would just be a distraction. In terms of what we are interested in, these features do not significantly change the game. @@ -52,14 +52,14 @@ However, such a proof only gets us so far: The moment your program uses [`unsafe It is the whole purpose of `unsafe` to permit writing dangerous code that the compiler cannot check, and hence it cannot be covered by any proof relying solely on such compiler checks. In the following, we will consider programs containing `unsafe` as not being well-typed. (We could also consider them well-typed in a more liberal type system that above result does not, and cannot, apply to. This is closer to what the Rust compiler does, but it's not helpful in our context.) -Note that this issue is viral: `Vec`, `RefCell`, `Rc` - all these and many more standard library data structures use `unsafe`, any if your program uses any of them, you're out of luck. +Note that this issue is viral: `Vec`, `RefCell`, `Rc` -- all these and many more standard library data structures use `unsafe`, any if your program uses any of them, you're out of luck. ## Semantics to the rescue Intuitively, why do we even think that a program that uses `Vec`, but contains no `unsafe` block *itself*, should be safe? It's not just the compiler checks making sure that, e.g., we don't call `push` on a shared borrow. -We also rely on `Vec` *behaving well* - or, I should rather say, *behaving well-typed*. -Yes, `Vec` uses `unsafe` - but it should not be possible to *observe* this in a well-typed safe program, calling only the interface provided by `Vec`. +We also rely on `Vec` *behaving well* -- or, I should rather say, *behaving well-typed*. +Yes, `Vec` uses `unsafe` -- but it should not be possible to *observe* this in a well-typed safe program, calling only the interface provided by `Vec`. There are some rules that Rust enforces, some invariants that safe, well-typed code automatically upholds, that people writing unsafe code have to maintain themselves. `Vec` performs checks and bookkeeping to get its tracking of the size and capacity of the container right. `RefCell` counts the number of outstanding borrows, to make sure at run-time that no two mutable borrows to the same cell exist. @@ -73,7 +73,7 @@ The core idea is that we can define the inhabitants of a type solely in terms of For example, to check that a function is semantically well-typed, you check what it does on every well-typed input, and make sure the output makes sense. It doesn't matter *how* the function performs these operations. This is in contrast to the *syntactic* notion of well-typedness of a function, which involves looking at the *code* of the function and checking it against a bunch of rules. -Only recently, research has been able to scale up such semantic methods to languages that combine state (i.e., mutable variables, a heap) with higher-order functions - languages like Rust, where I can take a closure (a `Fn{,Mut,Once}`) and store it in memory, for later use. +Only recently, research has been able to scale up such semantic methods to languages that combine state (i.e., mutable variables, a heap) with higher-order functions -- languages like Rust, where I can take a closure (a `Fn{,Mut,Once}`) and store it in memory, for later use. Lucky enough, my advisor [Derek Dreyer](http://www.mpi-sws.org/~dreyer/) is one of the world experts in this field, which permits me to intensively study Rust (which I would have done anyways) and call it research! ## What we are doing @@ -88,7 +88,7 @@ In this case, we have to go back to step one and change the semantics of our typ By combining this manual proof with the first result covering all syntactically well-typed Rust programs, we finally obtain the desired proof that safe programs using only the unsafe bits that were proven correct, are memory safe. No matter what the safe client does with the exposed API of the unsafe data structures, we then know in a mathematical rigorous way that everything will be all right. Isn't this a beautiful theorem? I certainly think so, even with the [caveats](#scope) described above. -We've only recently started this though, there is still a long way to go - lots of fun to be had. +We've only recently started this though, there is still a long way to go -- lots of fun to be had. I will track my progress, in very high-level terms, in [this Rust issue](https://github.com/rust-lang/rust/issues/9883). Once we got a proper semantic model, we also hope to be able to translate some of these insights back into the vocabulary of Rust programmers, and tell them what it is they have to be checking when writing unsafe Rust code.