[klodolph]

> This comment suggests you don't have much domain knowledge about how `unsafe` in Rust works, so I'm surprised you speak with such confidence.

I hate being tone police, but jeez, we're having a discussion about Rust here and talking about my personal competency is inappropriate and unwelcome.

The problem I'm talking about happens when you write libraries that contain "unsafe" blocks. You want to prove (or at least assure yourself) that no unsafe behavior is observable by clients of the library. However, the way to do this is not entirely clear, although there is research being done in this area. One known trap is that it is not sufficient to demonstrate that Rust code without "unsafe" blocks cannot observe unsafe behavior in your library.

See: https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf

These concerns are not hypothetical, there have been soundness problems in the Rust standard library before and I expect it to happen again.

[tatterdemalion]

Proving the correctness of unsafe code is totally different from what you talked about, which was composing different abstractions with unsafe internals together.

Users of safe Rust do not need to worry about whether the composition of two safe interfaces that use unsafe internally is safe unless one of those interfaces is incorrect. Your comment would suggest that users need to think about the untyped invariants of each library they use, but this is not correct, libraries are not allowed to rely on untyped invariants for the correctness of their safe APIs.

[klodolph]

The problem with talking about this subject is that "safe" and "unsafe" are overloaded terms in Rust, so I can understand why you think I was talking about something different.

Let R be arbitrary Rust code with no "unsafe" blocks. Let X and Y be libraries with "unsafe" blocks. You can prove that R + X is safe, and prove that R + Y is safe, but you haven't yet proven R + X + Y is safe. This is the hard part, because without an understanding of what property of X and Y individually makes R + X + Y + Z + ... safe, we don't have a good definition for what makes an interface "safe".

And this is what I mean when I say that this is not only a pedagogical problem.

[stouset]

You have restated your position, but it is still incorrect in the context of this discussion. Even your original statement of "R be[ing] arbitrary Rust code with no 'unsafe' blocks" is problematic: any Rust code is, very unavoidably, built upon a foundation of unsafe code. It has to be, because it's running on an "unsafe" processor. And yet, any safe Rust code in the core library (barring a safeness bug) is obviously safely composable with any other safe Rust code precisely because it obeys safety guarantees when transitioning from unsafe to safe. The fact that you can mistakenly conceive of Rust code that somehow avoids any internal unsafety simply reinforces how obvious this simple fact is.

But using your original problem statement, if R is safe and X and Y use unsafe code but do not expose any unsafe interfaces, then either R + X + Y is safe or one of [X, Y] has a safety bug and is inaccurately marking an unsafe interface as safe.

This is a generally unsolvable problem, and every other language has this problem as well; the difference being that in most other languages you're typically forced to write the unsafe code in C (where one has much greater variety of footguns available at their disposal). If I write a Ruby FFI wrapper for buggy C code whose interfaces bleed "unsafe" (from the perspective of the Ruby VM) behavior, then I am liable to experience crashes and memory corruption bugs. The only difference here is that Rust allows you to break the seal on the warranty without switching to a different language.

[klodolph]

> ...is obviously safely composable with any other safe Rust code precisely because it obeys safety guarantees when transitioning from unsafe to safe.

And what are those safety guarantees? This is the part where I see a lot of handwaving.

> ...either R + X + Y is safe or one of [X, Y] has a safety bug and is inaccurately marking an unsafe interface as safe.

Correct, but the problem is that we don't have a way to identify which library is incorrect without a definition for what a "safe interface" is. If R + X were unsafe or R + Y were unsafe we would have an easy answer to that question.

> This is a generally unsolvable problem...

The fact that the problem is unsolvable in general did not stop people from inventing the Rust language in the first place. The point of Rust is to solve this problem for a larger and more useful class of programs. Likewise, the research into defining what a "safe interface" is in Rust is important and useful research, e.g., RustBelt.

On a minor note, these kind of negative interactions with individual Rust community members have given me a bad impression of the Rust community as a whole.

[dbaupp]

> And what are those safety guarantees? This is the part where I see a lot of handwaving.

I think this is the contention: correct me if I'm wrong, but you're saying, that, in practice, the safety guarantees of Rust are currently too nebulous to be able to be enforced reliably, whereas most other people in this thread are, I think, visualising the "platonic Rust"/post-RustBelt Rust where the currently vague conditions for safety have been tweaked as needed and proved correct, treating the current situation more like a "just" bug (and the success of RustBelt so far hints that this isn't vapourware/imagination, there's significant concrete progress towards it).

That is to say, most people are talking about the potential of Rust's safety, whereas you're talking about the reality, right now. I think both positions are reasonable to think about, but it obviously leads to confusion when the positions aren't distinguished in a discussion. (I also think that most people would agree with you about Rust right now: there isn't a definite set of safety rules, so it can be hard to work out whether "edge-cases" are correct or not.)

[steveklabnik]

I think this is a good point, thank you. Will be remembering to tease this out in the future!

[steveklabnik]

> And what are those safety guarantees?

It is still that we are still working this out; this is what we're cooprating with academia on, formalizing the exact semantics. Such things take time.

[dbaupp]

> One known trap is that it is not sufficient to demonstrate that Rust code without "unsafe" blocks cannot observe unsafe behavior in your library.

I'm curious: what does this mean/could you point me to the part of the paper that describes it? (Unfortunately, I don't have time to read all 34 pages at the moment.)

[klodolph]

p. 66:3, the two paragraphs starting with "However, there is cause for concern..."

[dbaupp]

Thanks!

I'm not convinced that the statement in the paper translates into what you said: the key piece of that paragraph is "or seems to be". The Leakpocalypse problem was one piece of code (crossbeam's scoped threads API) was relying on an invariant that doesn't actually hold ("destructors will always run"). It was, fundamentally, a bug in the `unsafe` code in crossbeam, meaning it was incorrect for crossbeam to call its API safe: the fact that it took multiple libraries to trigger in that case means nothing, it just happens to be the circumstances under which the problem was noticed.

Of course, to be fair, no-one had thought about this destructor property before, just implicitly relied on it, and so it does demonstrate the necessity for better understanding of/tools for unsafe code, which is what projects like RustBelt are pushing towards.

To summarise, I still don't see how these two sentences are different:

> no unsafe behavior is observable by clients of the library

> [clients] without "unsafe" blocks cannot observe unsafe behavior in [the] library

Indeed, I don't think it makes sense to even attempt to prove that clients with unsafe code can't observe unsafe behaviour (which seems to be the only way for the second sentence to differ from the first). The typical framing is that the safe code can be arbitrarily bad and there'll still be no undefined behaviour, but arbitrary `unsafe` can do anything, including writing directly to another library's data structures, which of course can easily cause UB (e.g. replace a Vec's data pointer with a null one).

[klodolph]

> To summarise, I still don't see how these two sentences are different: ...

To "observe unsafe behavior" means I can write a program that does something safe, e.g., a data race or invalid memory access. It's possible to write library X and Y in such a way that I can observe unsafe behavior using both X and Y in my program, without putting "unsafe" blocks in my program. This is possible even if I can't do the same thing with either X or Y alone.

This is surprising, because it means that the naive definition of "safe interface" is not actually safe enough!

[dbaupp]

I'm still not understanding: other than the hardware/global state thing in another comment in this thread[1], what's a program that demonstrates this "composing safe interfaces is unsafe" property? The example in the paper is not one, it was a bug for crossbeam to mark its API safe.

[1]: I'm ignoring this case, because it's somewhat completely impossible to solve: there's no way Rust (or any language) can control this situation. And, there's a strong argument in my mind that this sort of scenario should have an `unsafe` constructor or something, to act as an assertion from the programmer that they're guaranteeing unique access to the resource.

[AstralStorm]

There is a way. You have to meticulously prove operations down to machine code to not have externally observable side effects.

You can weaken the condition by excluding, say, timing effects or cacheline effects. (Say hello to Spectre)

This means you get to prove bounded access and data race freedom on any piece of memory safe code touches. Likewise prove bounded access for all unsafe code and correct cpu flag and state handling.

It it's not as bad as it seems - you can use the machine code prover designed for seL4 as a good starting point.

[Rusky]

The definition of what you're allowed to do with `unsafe`, however nebulous its specifics may be at the moment, is that such a situation is a bug in one or both of those libraries, not their composition.

To put it another way, if you can't observe unsafety with X or Y alone, but you can with both together, then at least one of them has given you a new capability that you did not have before. Either that new capability is not truly safe, and thus the bug is providing that capability, or it exposes the other library relying on something not truly safe, and thus the bug is relying on that property.

The important point here is that, by definition, at least one of X or Y will have to change when such a situation is discovered, in order to preserve the property that composing safe interfaces is safe.