7 ms·

The Scope of Unsafe

78 points by panic 11y ago

rcthompson 11y ago
So, one question might be whether it's possible to encode some of these implicit invariants into the type so that the "evil" function would actually fail to compile.
- Animats 11y ago
  That's quite possible, and most proof of correctness systems can do it, but there's no syntax in Rust for talking about the necessary object invariants. Object invariants are assertions which must be true whenever control is not within the object. The object invariants must be true when control leaves the object by exiting any public function. Nothing outside the object must be able to alter the variables involved in the object invariant. Only one execution thread can be in the object at a time. If you can demonstrate all of those conditions, assuming the invariant is true at entry to the object, you have proved the object invariant. This is a useful and well-understood concept in the proof world, but isn't seen much in programming languages.
  - ralfj 11y ago
    Since Rust supports concurrency, it is worth mentioning that these techniques have been scaled to handle objects that can be accessed from multiple threads at once - while maintaining the modularity of the approach. See, for example, <http://plv.mpi-sws.org/iris/> http://plv.mpi-sws.org/iris/> and <http://software.imdea.org/fcsl/> http://software.imdea.org/fcsl/>.
- gsg 11y ago
  Dependent types allow for this kind of thing. Another possibility that doesn't require such heavy language machinery is something like OCaml's private types, where the scope of unrestricted access is unsafe blocks rather than the body of a module. In this approach there is no type-level correspondence between the value of the length member and the extent of the array: private types only ensure that any potentially invariant-breaking mutation is restricted to a certain scope, not that the code is correct.
- jeffdavis 11y ago
  Has anyone discussed adding ada-style contracts to rust?
losvedir 11y ago
Oh, that's interesting. I follow rust development with interest but have only built a few toy projects in myself and was definitely under the impression that these sorts of issues resided solely in `unsafe { ... }` blocks. But, yeah, with this example it makes sense. I'm relieved to hear that at least it doesn't pollute beyond module boundaries. But now I'm questioning what the difference is between `unsafe {...}` code and within-module code that accesses it, if the latter also has to deal with memory safety issues? Should `unsafe` only be declared at the module level then?
- pcwalton 11y ago
  No, I don't think that it should. Note that the only reason why the semantic invariant that len/cap aren't mutated is relevant to type safety is because the unsafe blocks depend on that to do the right thing. The reason for the phenomenon described in the article is not that it's possible to do unsafe things outside unsafe blocks. It's that, in practice, unsafe blocks often depend on invariants that are only enforced by module-level privacy.
- derefr 11y ago
  The idea with unsafe{} is that, while you might temporarily break an invariant (which Rust assumes for its memory-safety) while inside the unsafe{} block, you will restore that invariant before the end of the block. In other words, when you use unsafe{} code idiomatically, there shouldn't be anything like uninitialized-yet-accessible memory buffers "leaked out of" the unsafe{} code into safe code, even within the same module. The safe code should only see things it's possible to get from talking to safe code. The problem, of course, is that there's no way to enforce only this idiomatic (and rather strict) usage of unsafe{}. Well, that, and there may be some data structures that are fully impossible to implement with their promised complexity guarantees if you have to restore memory-safety invariants after every atomic step. This is justification enough for leaving unsafe{} the way it is, from my perspective; this is the same "leave it to the professionals" kind of code you tend to see in every standard library's data structure implementations, and not at all similar to the kind of code you'll ever need to write yourself (in 99% of cases.) I guess there's a lesson there, though: no, Rust will not magically protect you any more than C will when you wade into the "thorns" of domains like scientific computing or GIS. If you're implementing data structures that "must" reveal dirty or indeterminate state to the world to achieve full efficiency, there's not much you can do to be "fully" memory-safe. You can be safe at the higher level of your module boundary, but there's really no way to achieve the same elegant lexical bound on your invariants that you can with idiomatic unsafe{} code. When you leak things out of an unsafe{} block, you're taking the type system into your own hands, and it's up to you to re-establish the invariant at all dynamic module entry- and exit-points.
rdtsc 11y ago
> pub fn evil(&mut self) { self.len += 2; } Does it makes sense to think if it takes a mutable instance of the "unsafe" structure, then whatever it does to it could be "usafe". So it seems to fix it by hand, one could wrap all the calls which touch instances of this Vec with safe validation code -- basically guard code that runs at runtime to prevent corruptions from spreading. Can it be easily done during compile time?
- majewsky 11y ago
  That's called "Design By Contract". You formally specify pre/post-conditions of functions and invariants of classes (such as "cap >= len" in this case), and have the compiler enforce that automatically, e.g. by inserting runtime checks.
  - catnaroek 11y ago
    Runtime checks don't constitute "compile-time enforcement".
    - rdtsc 11y ago
      Yeah I think it would be compile-time addition of runtime-enforcement checks.
- dbaupp 11y ago
  &mut vs. & isn't fundamentally about mutability: having unique access (as in &mut) does imply that mutation will be "safe" (as in, act of mutating won't cause problems, although it may violate invariants in whatever is being mutated), but types with internal mutability allow safe mutation even when shared (as in &), examples are Cell, RefCell, Mutex and the atomics. Fields wrapped in these types can have invariants that can be violated, e.g. struct Foo { must_be_even: Cell<i32> } impl Foo { fn evil(&self) { self.must_be_even.set(1); // whoops } // ... unsafe code that relies on evenness assumption ... } > So it seems to fix it by hand, one could wrap all the calls which touch instances of this Vec with safe validation code -- basically guard code that runs at runtime to prevent corruptions from spreading Yes, but unfortunately one can't always detect the corruption easily/cheaply, e.g. there's no guarantee of a detectable runtime difference between push_good and push_bad without having to introduce overhead as there's no way to look at an arbitrary memory location and tell if it has been initialised or not: /// Push the value x onto the end of the vector fn push_good(&mut self, x: T) { // need space for one more element self.reserve(1); unsafe { // move x into the space we just reserved ptr::write(self.ptr.offset(self.len), x); } // register that there's a new element self.len += 1; } // just like `evil` fn push_bad(&mut self, x: T) { self.reserve(1); // don't bother writing `x`, too slow! self.len += 1; } Also, there are various opt-in modes that will try to detect problems in this vein automatically (opt-in because they have non-trivial overhead). For example, debug_assertions mode built into rustc (enables integer overflow checking, and any `debug_assert!`s in libraries), and sanitisers/checkers designed for C/C++ such as valgrind (works with Rust), TSan and ASan (don't yet work).
nanofortnight 11y ago
I don't think this is very surprising; if you do something unsafe hapharzardly within an unsafe block you can put the program in a state a safe program would not be able to reach, so further computation is in an unsafe state. In fact isn't this why we have unsafe in the first place; so that such code can be more easily verified? I disagree with the notion the author suggests that the problem isn't in the unsafe code.
- Manishearth 11y ago
  The thing is that it's not always possible to scope unsafety to unsafe blocks. The example of vec in the post above isn't about haphazard unsafe code, it's about code within Vec's module boundary being able to mess up invariants without needing to use unsafe. This could be fixed with things like "unsafe fields" and "unsafe types", but IMO that's not really necessary.
- ralfj 11y ago
  To reach a conclusion here, we will have to agree on what it means to be the "cause of the problem". It is true that if a program crashes, then there has to be some unsafe code in that program. This statement is however not very helpful, because pretty much all programs use libstd which contains unsafe code. So, I'd define the "cause" of a bug to be the piece of code that you fix to get rid of the bug. If `evil` was in libstd, the fix would be to remove `evil` (or somehow make it take a default value, grow the `Vec` to be large enough and fill the two new slots with that default value). In that sense, the problem here clearly was in the safe code `evil`, since it's that code which had to be changed to get rid of the problem.
  - Gankro 11y ago
    The guarantee I prefer is "If there's a segfault and you didn't write `unsafe`, it's not your fault". This is not necessarily referring to a single change, but rather the application as a whole. Dependencies like libstd are ignored here . As soon as there's any `unsafe` in your code, you've unlocked hard mode and everything is probably your fault.
shadowmint 11y ago
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. ... Of course, this also means that everything inside std::vec is potentially dangerous and needs to be proven to respect the semantics of Vec. So wait, in a nutshell, a module is 'safe' if and only if you formally prove that every public interface into the module and every way that public interface can be invoked... is error free. How is that any improvement on any other language? If the burden of 'safety' is formal proof of the entire module, then you're (surely) no better off than using C++ and doing exactly the same thing. I mean, obviously the borrow checker can help to some extent, but what you're basically saying is that it's not enough; you can't trust the borrow checker for safety; you must formally verify a module in order to know it's safe, if it contains any unsafe code. In other words, if your rust program has any module in any dependency that has unsafe code (ie. every rust program), it is potentially unsafe, regardless of the borrow checker (because some code path may invoke a 'safe' function that has not be formally verified to be safe, and results in undefined behaviour despite being safe). That's quite a troubling conclusion.
- Jweb_Guru 11y ago
  > How is that any improvement on any other language? Rust provides more facilities for exposing efficient, safe interfaces to unsafe code than do many other languages. The existence of safe and unsafe are not particularly interesting by themselves.
  - shadowmint 11y ago
    Perhaps... but if you have to formally verify the entire module, those facilities aren't doing much good are they?
    - Jweb_Guru 11y ago
      You don't have to formally verify the entire module. The module "just" has to be correct :P. Additionally, very often, unsafe code is used in ways that cannot contaminate the entire module (that's the ideal, in fact), and the module that the unsafe code is used in is made deliberately small.
catnaroek 11y ago
How exactly is this notion of “semantic types” formalized? Is it something like NuPRL, where the base language's type system isn't sufficiently precise to rule out all misbehaviors, and on top of that a more precise type system is added, whose typing rules might be defined in terms of the base language's evaluation/execution rules?
btrask 11y ago
Perhaps a quick fix would be to allow variables themselves to be tagged as unsafe, so they could only be changed from unsafe blocks.
- btrask 11y ago
  I tried suggesting this directly on GitHub. Here was the response: > There's an old idea of unsafe fields that would come up for datatypes. It can be emulated with a Unsafe<T> wrapper that has unsafe methods to get references to its interior, or to read/write. It's not widely used, or used at all afaik, since the gains aren't that great. People writing unsafe code generally know the issues, and that privacy is the #1 way the abstraction boundary is maintained. https://github.com/rust-lang/rust/issues/9883#issuecomment-170716254 https://github.com/rust-lang/rust/issues/9883#issuecomment-1... Privacy may be the best way to limit unsafety, but C and C++ already have privacy.

78 points by panic 11y ago

So, one question might be whether it's possible to encode some of these implicit invariants into the type so that the "evil" function would actually fail to compile.

Animats 11y ago
That's quite possible, and most proof of correctness systems can do it, but there's no syntax in Rust for talking about the necessary object invariants. Object invariants are assertions which must be true whenever control is not within the object. The object invariants must be true when control leaves the object by exiting any public function. Nothing outside the object must be able to alter the variables involved in the object invariant. Only one execution thread can be in the object at a time. If you can demonstrate all of those conditions, assuming the invariant is true at entry to the object, you have proved the object invariant. This is a useful and well-understood concept in the proof world, but isn't seen much in programming languages.
- ralfj 11y ago
  Since Rust supports concurrency, it is worth mentioning that these techniques have been scaled to handle objects that can be accessed from multiple threads at once - while maintaining the modularity of the approach. See, for example, <http://plv.mpi-sws.org/iris/> http://plv.mpi-sws.org/iris/> and <http://software.imdea.org/fcsl/> http://software.imdea.org/fcsl/>.
gsg 11y ago
Dependent types allow for this kind of thing. Another possibility that doesn't require such heavy language machinery is something like OCaml's private types, where the scope of unrestricted access is unsafe blocks rather than the body of a module. In this approach there is no type-level correspondence between the value of the length member and the extent of the array: private types only ensure that any potentially invariant-breaking mutation is restricted to a certain scope, not that the code is correct.
jeffdavis 11y ago
Has anyone discussed adding ada-style contracts to rust?

losvedir 11y ago

Oh, that's interesting. I follow rust development with interest but have only built a few toy projects in myself and was definitely under the impression that these sorts of issues resided solely in `unsafe { ... }` blocks. But, yeah, with this example it makes sense. I'm relieved to hear that at least it doesn't pollute beyond module boundaries. But now I'm questioning what the difference is between `unsafe {...}` code and within-module code that accesses it, if the latter also has to deal with memory safety issues? Should `unsafe` only be declared at the module level then?

pcwalton 11y ago
No, I don't think that it should. Note that the only reason why the semantic invariant that len/cap aren't mutated is relevant to type safety is because the unsafe blocks depend on that to do the right thing. The reason for the phenomenon described in the article is not that it's possible to do unsafe things outside unsafe blocks. It's that, in practice, unsafe blocks often depend on invariants that are only enforced by module-level privacy.
derefr 11y ago
The idea with unsafe{} is that, while you might temporarily break an invariant (which Rust assumes for its memory-safety) while inside the unsafe{} block, you will restore that invariant before the end of the block. In other words, when you use unsafe{} code idiomatically, there shouldn't be anything like uninitialized-yet-accessible memory buffers "leaked out of" the unsafe{} code into safe code, even within the same module. The safe code should only see things it's possible to get from talking to safe code. The problem, of course, is that there's no way to enforce only this idiomatic (and rather strict) usage of unsafe{}. Well, that, and there may be some data structures that are fully impossible to implement with their promised complexity guarantees if you have to restore memory-safety invariants after every atomic step. This is justification enough for leaving unsafe{} the way it is, from my perspective; this is the same "leave it to the professionals" kind of code you tend to see in every standard library's data structure implementations, and not at all similar to the kind of code you'll ever need to write yourself (in 99% of cases.) I guess there's a lesson there, though: no, Rust will not magically protect you any more than C will when you wade into the "thorns" of domains like scientific computing or GIS. If you're implementing data structures that "must" reveal dirty or indeterminate state to the world to achieve full efficiency, there's not much you can do to be "fully" memory-safe. You can be safe at the higher level of your module boundary, but there's really no way to achieve the same elegant lexical bound on your invariants that you can with idiomatic unsafe{} code. When you leak things out of an unsafe{} block, you're taking the type system into your own hands, and it's up to you to re-establish the invariant at all dynamic module entry- and exit-points.

rdtsc 11y ago

> pub fn evil(&mut self) { self.len += 2; } Does it makes sense to think if it takes a mutable instance of the "unsafe" structure, then whatever it does to it could be "usafe". So it seems to fix it by hand, one could wrap all the calls which touch instances of this Vec with safe validation code -- basically guard code that runs at runtime to prevent corruptions from spreading. Can it be easily done during compile time?

majewsky 11y ago
That's called "Design By Contract". You formally specify pre/post-conditions of functions and invariants of classes (such as "cap >= len" in this case), and have the compiler enforce that automatically, e.g. by inserting runtime checks.
- catnaroek 11y ago
  Runtime checks don't constitute "compile-time enforcement".
  - rdtsc 11y ago
    Yeah I think it would be compile-time addition of runtime-enforcement checks.
dbaupp 11y ago
&mut vs. & isn't fundamentally about mutability: having unique access (as in &mut) does imply that mutation will be "safe" (as in, act of mutating won't cause problems, although it may violate invariants in whatever is being mutated), but types with internal mutability allow safe mutation even when shared (as in &), examples are Cell, RefCell, Mutex and the atomics. Fields wrapped in these types can have invariants that can be violated, e.g. struct Foo { must_be_even: Cell<i32> } impl Foo { fn evil(&self) { self.must_be_even.set(1); // whoops } // ... unsafe code that relies on evenness assumption ... } > So it seems to fix it by hand, one could wrap all the calls which touch instances of this Vec with safe validation code -- basically guard code that runs at runtime to prevent corruptions from spreading Yes, but unfortunately one can't always detect the corruption easily/cheaply, e.g. there's no guarantee of a detectable runtime difference between push_good and push_bad without having to introduce overhead as there's no way to look at an arbitrary memory location and tell if it has been initialised or not: /// Push the value x onto the end of the vector fn push_good(&mut self, x: T) { // need space for one more element self.reserve(1); unsafe { // move x into the space we just reserved ptr::write(self.ptr.offset(self.len), x); } // register that there's a new element self.len += 1; } // just like `evil` fn push_bad(&mut self, x: T) { self.reserve(1); // don't bother writing `x`, too slow! self.len += 1; } Also, there are various opt-in modes that will try to detect problems in this vein automatically (opt-in because they have non-trivial overhead). For example, debug_assertions mode built into rustc (enables integer overflow checking, and any `debug_assert!`s in libraries), and sanitisers/checkers designed for C/C++ such as valgrind (works with Rust), TSan and ASan (don't yet work).

nanofortnight 11y ago

I don't think this is very surprising; if you do something unsafe hapharzardly within an unsafe block you can put the program in a state a safe program would not be able to reach, so further computation is in an unsafe state. In fact isn't this why we have unsafe in the first place; so that such code can be more easily verified? I disagree with the notion the author suggests that the problem isn't in the unsafe code.

Manishearth 11y ago
The thing is that it's not always possible to scope unsafety to unsafe blocks. The example of vec in the post above isn't about haphazard unsafe code, it's about code within Vec's module boundary being able to mess up invariants without needing to use unsafe. This could be fixed with things like "unsafe fields" and "unsafe types", but IMO that's not really necessary.
ralfj 11y ago
To reach a conclusion here, we will have to agree on what it means to be the "cause of the problem". It is true that if a program crashes, then there has to be some unsafe code in that program. This statement is however not very helpful, because pretty much all programs use libstd which contains unsafe code. So, I'd define the "cause" of a bug to be the piece of code that you fix to get rid of the bug. If `evil` was in libstd, the fix would be to remove `evil` (or somehow make it take a default value, grow the `Vec` to be large enough and fill the two new slots with that default value). In that sense, the problem here clearly was in the safe code `evil`, since it's that code which had to be changed to get rid of the problem.
- Gankro 11y ago
  The guarantee I prefer is "If there's a segfault and you didn't write `unsafe`, it's not your fault". This is not necessarily referring to a single change, but rather the application as a whole. Dependencies like libstd are ignored here . As soon as there's any `unsafe` in your code, you've unlocked hard mode and everything is probably your fault.

shadowmint 11y ago

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. ... Of course, this also means that everything inside std::vec is potentially dangerous and needs to be proven to respect the semantics of Vec. So wait, in a nutshell, a module is 'safe' if and only if you formally prove that every public interface into the module and every way that public interface can be invoked... is error free. How is that any improvement on any other language? If the burden of 'safety' is formal proof of the entire module, then you're (surely) no better off than using C++ and doing exactly the same thing. I mean, obviously the borrow checker can help to some extent, but what you're basically saying is that it's not enough; you can't trust the borrow checker for safety; you must formally verify a module in order to know it's safe, if it contains any unsafe code. In other words, if your rust program has any module in any dependency that has unsafe code (ie. every rust program), it is potentially unsafe, regardless of the borrow checker (because some code path may invoke a 'safe' function that has not be formally verified to be safe, and results in undefined behaviour despite being safe). That's quite a troubling conclusion.

Jweb_Guru 11y ago
> How is that any improvement on any other language? Rust provides more facilities for exposing efficient, safe interfaces to unsafe code than do many other languages. The existence of safe and unsafe are not particularly interesting by themselves.
- shadowmint 11y ago
  Perhaps... but if you have to formally verify the entire module, those facilities aren't doing much good are they?
  - Jweb_Guru 11y ago
    You don't have to formally verify the entire module. The module "just" has to be correct :P. Additionally, very often, unsafe code is used in ways that cannot contaminate the entire module (that's the ideal, in fact), and the module that the unsafe code is used in is made deliberately small.

catnaroek 11y ago

How exactly is this notion of “semantic types” formalized? Is it something like NuPRL, where the base language's type system isn't sufficiently precise to rule out all misbehaviors, and on top of that a more precise type system is added, whose typing rules might be defined in terms of the base language's evaluation/execution rules?

btrask 11y ago

Perhaps a quick fix would be to allow variables themselves to be tagged as unsafe, so they could only be changed from unsafe blocks.

btrask 11y ago
I tried suggesting this directly on GitHub. Here was the response: > There's an old idea of unsafe fields that would come up for datatypes. It can be emulated with a Unsafe<T> wrapper that has unsafe methods to get references to its interior, or to read/write. It's not widely used, or used at all afaik, since the gains aren't that great. People writing unsafe code generally know the issues, and that privacy is the #1 way the abstraction boundary is maintained. https://github.com/rust-lang/rust/issues/9883#issuecomment-170716254 https://github.com/rust-lang/rust/issues/9883#issuecomment-1... Privacy may be the best way to limit unsafety, but C and C++ already have privacy.