
The Scope of Unsafe - panic
https://www.ralfj.de/blog/2016/01/09/the-scope-of-unsafe.html
======
losvedir
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?

~~~
fmstephe
"I'm relieved to hear that at least it doesn't pollute beyond module
boundaries."

This isn't true, it is easy to come up with an example where lack of safety
spreads past module boundaries.

    
    
        impl Vec<T> {
            pub fn evil(&mut self, len: i32, cap: i32) {
                self.len = len;
                self.cap = cap;
            }
        }
    

If we want to know our program is broken now, we need to look across all of
the source code to see if evil is called in breaking ways.

The point was that Rust provides abstraction facilities which allow us to
contain these invariants. If we are careful.

~~~
Manishearth
`len` and `cap` are private fields and can't be accessed outside the module
boundary, even by an impl.

~~~
phaylon
I've been wondering if it would make sense to encapsulate internal fields that
are part of the unsafe machinery in a type forcing you to use unsafe blocks,
even inside the type impl. [edit: Removed note about UnsafeCell since it's not
really like the thing described above]

I haven't really played with it though, most of my unsafe use is FFI.

~~~
Manishearth
You can, but IMO it's not so necessary. The module boundary thing doesn't
cause many issues in practice is straightforward to reason about if you're
aware of it.

(And if you weren't aware of it you would probably not use `UnsafeField`
either, since the compiler can't force you to do that)

~~~
phaylon
I'm more thinking about the documentation effect of such a wrapper type. Both
in the data structure and in the parts of the code that are foced to use
unsafe.

~~~
ralfj
I suggested something kind-of-similar at <[https://internals.rust-
lang.org/t/pre-rfc-unsafe-types/3073>](https://internals.rust-lang.org/t/pre-
rfc-unsafe-types/3073>)

------
rcthompson
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
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
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/>).

------
rdtsc
>

    
    
        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
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
Runtime checks don't constitute "compile-time enforcement".

~~~
rdtsc
Yeah I think it would be compile-time addition of runtime-enforcement checks.

------
nanofortnight
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.

~~~
ralfj
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
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.

------
btrask
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
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-1...](https://github.com/rust-
lang/rust/issues/9883#issuecomment-170716254)

Privacy may be the best way to limit unsafety, but C and C++ already have
privacy.

------
catnaroek
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?

------
shadowmint

        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.

~~~
dbaupp
I'm not really sure what the problem is here: having to formally verify a
module doesn't seem fundamentally different to formally verify a single
function. I mean, sure, it's some more code, but there's still well-defined
containment. And, being "allowed" to reason about a whole module (well,
usually one just cares about a whole type, but these often match, especially
for unsafe code) seems far more useful: one can build far more interesting
abstractions. If one was forced to reason about a single function at a time,
Vec couldn't exist in a useful way, as every function would have to assume the
incoming Vec value could be arbitrarily invalid.

In any case, there are many many modules with no `unsafe` code, e.g.
std::option has none [1], iron::response has none [2], image::jpeg has none
[3] (just some random examples). These are automatically safe, if you assume
that that the code they call is safe, which seems to me like the only
assumption that can make sense: if the safe modules call unsafe ones that
aren't safe... well, the problem is in the unsafe ones, not the safe ones.

What I'm trying to say is this paragraph doesn't seem to change anything
fundamental about the objections to safe vs. unsafe you sometimes write about;
it is not introducing anything new, and so the refutations you often receive
still apply.

[1]: [https://github.com/rust-
lang/rust/blob/dfaddb732ced1da9d3109...](https://github.com/rust-
lang/rust/blob/dfaddb732ced1da9d310990df095ca36f43fbc3d/src/libcore/option.rs)

[2]:
[https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e...](https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e07b2dc3f9749ee/src/response.rs)

[3]:
[https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c...](https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c02b827190671ea9302716e86028/src/jpeg)

~~~
shadowmint
Well, given the most common refute of my concerns is 'you just have to make
sure your unsafe blocks are verified to be correct', and the _point_ of this
article, is _explicitly_ that this isnt the case...

Now its that you have to just make sure all your code is correct, not just the
unsafe blocks.

/me shrugs

I think thats lame, and breaks the promises rust is trying to make about
writing safe secure software.

If safe code may not be safe, whats the point of it at all.

You, are of course welcome to your own oppinion.

~~~
ralfj
No, it doesn't break the promises in any way. If _all your code_ does
potentially dangerous memory manipulation, then there's very little hope that
there will ever be an automatic checker for the safety of your program.

The promise of Rust rests on the assumption that _most code is not like that_.
There are a few fundamental data structures that do crazy stuff, and okay, we
have to use `unsafe` there - and if we want to have any formal guarantees, we
have to do a formal proof. If are happy with less, we just manually audit that
data structure extra carefully. We also put every such data structure in its
own module, which carefully limits the amount of code that is exposed to this
unsafety.

However, most of the code will just _use_ those data structures, and that's
where Rust gives you a safety guarantee. Combing `Vec` and `HashMap` and all
the other types from the standard library in any way you want, hammer them
from multiple threads, send stuff across channels, whatever - you can do all
of that safely, and if your code crashes, you don't have to look at all this
code because you did not write `unsafe`, only the standard library did - and
you are in a separate module.

> Now its that you have to just make sure all your code is correct, not just
> the unsafe blocks.

This is not correct. As I wrote in the post, you have to check _all code
within a module that contains `unsafe`_. Most of the modules people write do
not contain `unsafe`, and hence are not checked.

I'd be curious to learn why you think this is the case.

~~~
shadowmint
The point I'm making is that, and this surprised me, the onus on soneone
writing a module with unsafe code, to ensure it does not violate memory safety
is _much higher_ than I realized.

It is not 'all rust' you must verify; just all rust that touches unsafe code.

You might argue this is nothing new, and indeed if you read this comment
thread you'll see the suggestion that the difference between verifying an
entire module and verifying only the unsafe blocks in it is insignificant.

My point is that there is at least an order of magnitude more safe code than
unsafe code in an unsafe module, and I suspect it is not scrutinized nearly as
much as the unsafe code.

There are _a lot_ of crates that use unsafe code in one form or another; and
it troubles me (although no one else cares) that they are probably more
dangerous than I realized.

'Just verify the unsafe blocks' is something I've literally heard people say.

~~~
dbaupp
A lot of people care: e.g. the Rustonomicon[1] spends a lot of time caring
about unsafe code (that is one of the main reasons for it to exist), and the
massive RustBelt project[2], which Ralf (author of the blog post) is part of,
is because people care. Even the lowest level developers (working on OSes)
care about being very careful about how they use `unsafe`, e.g. [3]. One thing
that some of us are hopeful will come out of RustBelt are more advanced
`unsafe` checkers (i.e. some sort of proof assistant, possibly with lints
built into the compiler).

In any case, talking about "order of magnitude" misses the point somewhat:
there might be a large amount more code, but a lot of it is trivial to verify,
e.g. the declaration of a struct doesn't need any verification, nor do
comments, and if T, the type with invariants, has no internal mutability
(which is fairly typical for unsafe code outside std, IME), then any safe
function that takes &T is automatically safe.

[1]: [http://doc.rust-lang.org/doc/stable/nomicon/](http://doc.rust-
lang.org/doc/stable/nomicon/) [2]: [http://plv.mpi-
sws.org/rustbelt/](http://plv.mpi-sws.org/rustbelt/) [3]: [http://os.phil-
opp.com/printing-to-screen.html](http://os.phil-opp.com/printing-to-
screen.html)

~~~
shadowmint
linked_list.rs once you strip the comments, struct defs, and whatnot out has
415 lines, of which 64 reside in unsafe blocks, 6x as much code to check.

That's one trivial module. The piston modules and other c bindings have much
worse ratios.

When the amount of code that you have to verify manually jumps by 6x (or
worse), that's surprising. I was surprised and troubled by that.

