Unsoundness in Pin
internals.rust-lang.org
internals.rust-lang.org
Since (to a first approximation) every individual who has the expertise and contextual knowledge to really evaluate this issue is a poster on internals.rust-lang.org, its pretty surprising to find this thread on the front page of Hacker News. I imagine some Hacker News users who upvoted this link did so out of technical interest, but I suspect a large portion of the attention comes from some combination of these misconceptions:
- The misconception that this could have a practical impact on users (the code being discussed on the thread is all obviously pathological & contrived).
- The misconception that Rust's type system and standard library never contain soundness issues and that this is an exceptional event (in fact we have a number of longstanding soundness issues).
We have a policy of fixing all soundness issues, so this issue will be fixed. In the meantime, while we decide the best solution, it will have no practical impact on Rust users. And none of the solutions we are considering would involve significant breakage to users, or invalidate any real code.
At a high level: the soundness issue occurs because the Pin API was designed based on certain reasoning about the behavior of pointers. This reasoning would be sound but for the fact that we have allowed certain exceptions in relationship to pointers to what are called the "orphan rules" (which usually enable local reasoning like this). These exceptions allow users to introduce code which, while contrived, allows them to violate the guarantees of the Pin API. Such is life.
Famous last words?
I mean I'm not an expert in Rust and even less in Pin, but I've seen my share of theoretical bugs thought of not possibly having any impact in the real world because of too theoretical. In other areas, when you debug a triple segfault and you understand the crazy conditions that lead to it, or when you render a piece of C++ code conforming instead of technically UB and it then starts to crash when in its UB form it worked perfectly, you start to consider that everything is possible :)
The idea that someone could think an issue is theoretical and then discover it is practically significant is obvious and no insight at all - it reduces to "people are sometimes wrong." I am declaring based on my significant relevant expertise that this issue is not practically important. Your comment contributes nothing but baseless contradiction.
There is nothing wrong about having bugs, of course, but the reaction to the bug in this thread shows that mathematical correctness is not as universally valued as I thought it would be. I agree with the sentiment that this is a bigger issue that shouldn't be discussed in a technical thread about a specific bug. However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases. Almost all of the popular languages don't care about this, for instance.)
[0] https://youtu.be/t0mhvd3-60Y?t=130 [1] https://plv.mpi-sws.org/rustbelt/
It's a balance. We cannot drop everything, nor stop all development, in order to get proofs. However, we are actively working toward formalizing the language itself, because we do see value in it.
The GitHub label for these bugs is A-Unsound, which has the description "A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness".
Please note that threads on internals are able to be posted to by anyone; things expressed there may not represent the way that the team feels about things.
However, an important thing to note is that Rust strives to be safe only against unintentional bugs, and not against intentional malicious code (against which you are supposed to use OS/CPU-level sandboxing), so unsoundness issues that are very unlikely to be accidentally triggered aren't necessarily a very high priority.
This is a reasonable policy, since current Rust does not have a certified provably correct compiler and Rust programs in current practice don't come with formal proofs, so full provable soundness in type system doesn't really translate to any useful properties, since programs can intentionally fail to do what they are supposed to do in other ways (just do something safe but malicious or incorrect or exploit bugs in rustc or LLVM).
For instance, this issue is very unlikely to be triggered by non-malicious code, so emergency action to fix it is not being taken, and instead it will probably be fixed only once there is clear consensus on the best fix.
It's only a problem if you try to restrict I/O APIs and use the Rust type system as a security boundary, which is something that I don't think anyone does and that should not be done since the surface area is too vast to secure without formal proofs of the whole Rust stack, which are too time-consuming to produce with current technologies.
> A capsule is a Rust struct and associated functions. Capsules interact with each other directly, accessing exposed fields and calling functions in other capsules. Trusted platform configuration code initializes them, giving them access to any other capsules or kernel resources they need. Capsules can protect internal state by not exporting certain functions or fields.
> ...
> Rust’s language protection offers strong safety guarantees. Unless a capsule is able to subvert the Rust type system, it can only access resources explicitly granted to it, and only in ways permitted by the interfaces those resources expose. However, because capsules are cooperatively scheduled in the same single-threaded event loop as the kernel, they must be trusted for system liveness. If a capsule panics, or does not yield back to the event handler, the system can only recover by restarting.
I take it from the present discussion that that might not be as good of an idea as they think.
Worth noting that they also have process isolation on top, but it doesn’t seem to be motivated by any potential insecurity of the type system.
I suspect it is not so simple as "Rust's safety ensures malicious rust code can't access data".
Lots of example code https://github.com/tock/tock/tree/master/capsules
Rust does not offer any protection against malicious code and it does not claim to. It offers protection against malicious input to non-malicious code, but no protection against malicious code itself.
That kind of contradict some of the reactions, e.g., in this thread about adding an `Ordering::Unordered` to the language: https://internals.rust-lang.org/t/unordered-as-a-solution-to...
Where it is essentially argued that "all development should be stopped until we have formal proofs".
I guess it depends on which parts of the language things touch. `Ordering::Unordered` touches fundamentals parts of the memory model, and well, `Pin` touches the fundamental kinds of values that Rust has: owned, shared, mut shared, and with pin, also pinned.
When people complain that things are stabilized too quickly, I don't think they complain about async / await taking years. The `Pin` API was unstable for like less than half a year in its final form before being stabilized, that's quite a short time for people to try to find holes in it, given how fundamental it is.
Empirically it's pretty clear that the language is being developed. If that were the decision of the team, it would pretty much have to go through an RFC, and so we'd be able to point to that.
* Infinite loops
* `undefined`
* Abuse of unsafe IO behavior, including monads built on or reducible to IO
Rust's unsoundness bugs are all over [0], and come from so many different angles that they feel indistinct from any other low-level C-like language.
I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt.
[0] https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%...
There are several people working on formalizing aspects of Rust, and though it will take a long time to get there such efforts have already found and fixed bugs in Rust and its standard library. It's fair to take SPJ's critique on the chin for now; Rust deliberately chose the path of eventual soundness in order to produce a usable language in less time, and as long as we keep working towards that goal there's nothing to be ashamed about.
To clarify, we do have a work-in-progress formalization of pinning as part of RustBelt [0] (I worked on it over the summer). We did not discover this issue because RustBelt does not currently model traits, and the problem here is very much about the interaction between traits and pinning. Ralf touches on this in the linked discussion:
> Actually trying to prove things about Pin could have helped, but one of our team actually did that over the summer and he did not find this issue. The problem is that our formalization does not actually model traits. So while we do have a formal version of the contract that Deref/DerefMut need to satisfy, we cannot even state things like "for any Pin<T> where T: Deref, this impl satisfies the contract".
[0] - https://gitlab.mpi-sws.org/iris/lambda-rust/tree/gpirlea/pin...
> Good question. We even had a sketch of a formal model for pinning, but that model was always about the three separate pointer types (PinBox<T>/PinMut<T>/Pin<T>). The switch to the generic Pin was done without formal modelling.
> Actually trying to prove things about Pin could have helped, but one of our team actually did that over the summer and he did not find this issue. The problem is that our formalization does not actually model traits. So while we do have a formal version of the contract that Deref/DerefMut need to satisfy, we cannot even state things like "for any Pin<T> where T: Deref, this impl satisfies the contract"
That does sound scary, but I think the point is that this is a known blind spot in the formal model. It also has a known solution; the trait ought to be unsafe, so that the implementor takes responsibility for upholding the contract. The issue with Pin is it’s using an existing, safe trait, on the informal assumption that it couldn’t be unsoundly aliased by users. (Of course that turns out to be false.)
So you can look at that and say “an unsound feature got into the stdlib without passing formal verification”, and that’s true, speaking to a lack of concern for formalization.
On the other hand, you could look at it and say “the unsoundness of this feature is well isolated by formal methods and leakage at this interface is not the end of the world”, which is also true, and speaks to the utility of the formal work that has been done.
It seems clear to me that the answer for Rust is “balance”. Formal verification is important not not to have, and things that can’t be verified shouldn’t be allowed. But formal verification takes up time when everything could be working 100% in production, and the alternative is likely even less sound formally, so it’s better to build an API now with some known risks than to wait for something known to be risk-free.
Whatever your personal philosophy is, it seems clear that toeing that line has been instrumental to Rust’s success.
* Hack without fear (which can be interpreted as soundness) * Practical programming language (a language you can use to get stuff done)
A full operational semantics of Rust with soundness proofs is probably at least a decade away, blocking the language on that would mean that one can't get anything done until that happens. And that is at tension with Rust being a practical language.
So if you had a spectrum of languages, and you were to classify them along these two axes, Rust would be at the very safe and very practical end of the spectrum. But safety isn't an absolute, it's a spectrum. Rust won't protect you form, e.g., race conditions, dead locks, memory leaks, or somebody breaking into your house and hitting your computer with a baseball bat, etc. You need to have a threat model, and then deduce from it how much safety is enough. Rust aims to only give you memory and thread safety, so there is definitely room for much safer languages than Rust down the road, that protect you from these other things. The art is increasing safety, without sacrificing practicality, performance, etc.
Note that it was known that Pin/Generators had soundness problems when you turned on noalias optimization flags [1]. They have however decided to stabilize it without fixing those problems as they could be fixed afterwards as well. I'm not entirely sure yet about the impact of this one, will have to read the thread I guess.
[1]: https://github.com/rust-lang/rust/issues/62149#issuecomment-...
The cases where I personally wanted Pin were cases that I think will be solved in the future as async improves, but there are probably other more fringe cases which wont.
Otherwise it is impossible to become productive with that part of the language.
If the goal was for users to just use high-level web frameworks, and when there is something that the framework cannot do (which is currently a lot), the expectation is that users should just shrug their shoulders and tell their bosses "Sorry boss, Rust can't do that", then sure, there is no need to understand pinning. But such users do not need to use Rust either, an pretty much any other programming language like Go or Python would have been a much better fit for them.
I don't see any use case in which understanding pinning is not necessary.
If they use async code as just a more office synchronous/threaded code, with purely linear control flow, then no knowledge of Pin is required. The users just sprinkle awaits and are good with it.
If users also explore the areas of which are more unique to async code (e.g. real concurrency, select!, custom combinators, cancellation mechanisms, etc) than they will indeed run fairly early into Pin.
I guess the majority of users who anticipated async/await fall into the first category. Most projects and requests around async code seem to be "just" webservers which handle some APIs. That will likely be the domain where one can live fairly well without Pin - at least if you do not implement the underlying webserver.
At best, when using futures, I randomly wrap things in `Pin<Box<..>>`, hoping that the compiler might stop complaining.
I can imagine an easier-to-understand world in which there is a reference type from which one cannot move during the lifetime of the reference, and in which one only ever gets this type of reference to immovable closures and such. I don’t know if the details would work out, but it would at least seem less weird to me.
I have no answer, it's just the only interesting part of that discussion imo. Everything else is just details of an issue that's too weird to really fully understand for me, and not novel or interesting enough to invest into understanding, anyway.
for<'a, T: ?Sized> &'a T !: DerefMut
https://internals.rust-lang.org/t/unsoundness-in-pin/11311/3...
You’re not wrong to find it illegible; apart from the syntax, that phrase invokes the concepts of lifetimes, mutability, borrowing, and traits, none of which have straightforward semantic analogues in other common languages.
But FWIW they’re primitive concepts in Rust. A typical Rust user wouldn’t read or write code that looks like that very much, but they would know what it means, if that makes any sense.
Edit: Seeing sibling comments about whether this snippet actually parses, I guess I should amend this to say that a typical Rust user has an idea of what it’s supposed to mean :)
It's both a good and bad thing that rust has these sort of deep areas where 95% of users won't ever have to go - Pin being another example. I think it's much more good than bad though.
Here's an analogy: Rust already differs from most languages in that the behavior that you get "by default" when defining a new type is very limited. For example, if I define a type `struct Foo`, then by default this type can't be copied around: `let x = Foo; let y = x;` is a simple operation that in most languages would involve copying memory, but in Rust involves a move instead. You can think of a move as a copy where the original value is no longer accessible (whether or not any bytes in memory actually get copied as a result of a move is an implementation detail, and is (hopefully) often optimized away). In order to make our type copyable, we would add an implementation of the `Copy` trait.
The observation is that moving is a more fundamental operation than copying, therefore, it is easier for types to opt in to copying than to opt out.
When Rust was released in 2015 this was a relatively radical concept for a language targeting a mainstream audience (we're essentially describing Rust's entire concept of ownership here, after all). But it turns out that it's possible that Rust may not have been radical enough! Consider: what if you want a type that not only can't be copied, but can't be moved as well?
Before Rust 1.0 it wasn't clear that such a concept of "unmoveability" would be generally useful. There were certainly cases, such as self-referential structs, that could have benefited from such a concept, however making moveability opt-in rather than opt-out would have required all types that do want to be moveable to explicitly announce that fact (via something like `#[derive(Move)]`), which is an annotation burden on all other code that must be considered.
It wasn't until the async/await work that another, more critical need for unmoveability was found: if the generators interally produced by `async` are capable of moving, then that means that generators are incapable of containing references, which means that async/await would become drastically less useful; there would be an entire fundamental part of the language that simply couldn't be used with it. Thus `Pin` was born in order to denote things that cannot be moved (and whose design is itself a very, very long discussion).
For this reason I'm somewhat amused by one of the comments in the OP asking something like "if `Pin` had remained unstable for an additional year, would this particular instance of unsoundness have been caught?" Because, conversely, we could ask whether Rust itself could have remained unstable for another five years and found a design that would have obviated `Pin` entirely by making moveability opt-in. However, of course, such things are easy to ask in hindsight, and stability is a prerequisite for having a broad base of adoption. Finding a balance between immediate stability and eventual perfection is the holy grail of industrial language design.
(Regarding the bug in the OP itself, I think it's unfortunate but I'm not especially worried by it at this juncture. The fact that Ralf Jung's team is looking into it gives me confidence that formal methods will eventually be applied here to more thoroughly explore the soundness of `Pin` in general (Ralf being one of the people who shaped `Pin` originally), and in the meantime I wouldn't be opposed to a band-aid fix, given that working extensively with `Pin` in the way shown in the OP is rare for normal users.)
When talking about Pin, I think it is important to go back to a more fundamental level.
There are types that are not movable without extra processing, like a `struct` that has fields that reference other fields. When moving, those references become invalid.
Rust chose by allowing types to become unmovable so the `struct` can't go into an invalid state.
While C++ doesn't have the same safety guarantees, they did need to solve this problem. C++ chose to solve this with move constructors. I know move constructors will have their own challenges in Rust but I hope we do get them one day.
Hm, I ran into quite a lot of cases where I wanted Pin or something similar when porting a C program to Rust, and if I recall correctly also the creator of vulkano also ran into plenty of cases when writing it, so I am a bit surprised people did not realize this. My case was a program which in its C version was based around an epoll event loop, so maybe that is a bit similar to the async/generators issue.
I'd like to ask, why is moving generally useful? Why would I want to move x to y and invalidate x?
Does that make sense?
#[derive(!Move)]Isn't `Pin` even crazier, in that the same type can be moveable (when used outside of Pin) or not moveable (when used inside Pin)? A simple derive wouldn't be enough to capture that.
The hypothetical opt-in moveability proposal is difficult to compare directly to `Pin` because they take such different approaches to the problem, but they would both address the problem (at least, as far as I have considered it).
1 & 2 both involve unsafe code that, while possibly reasonable in a complex application, is obviously wrong in the simple case. Of course turning a reference into a mutable reference will cause trouble. Was Pin SUPPOSED to be resilient to unsafe code? In any case, seems like a bug in DerefMut and Clone, not Pin.
The others are a bit more esoteric and do seem potentially concerning, but I'm not sure.
But still, I'm left with my earlier question: just how resilient is Pin supposed to be?
Regardless, for a user to be able to trigger undefined behavior without using the `unsafe` keyword indicates a bug here that must be fixed at the level of the language or standard library.
Remember, unsafe does not mean "I can do whatever I want," it means "I am promising to uphold some guarantee on my own." That is, let's assume we have a function:
/// Makes a new Foo.
///
/// # Safety
///
/// x must never be greater than 5
unsafe fn new(x: i32) -> Foo {
let x = 6;
unsafe {
new(x);
}
In my understanding of the unsafe examples above, the unsafe code was upholding the invariants that it was required to uphold, and so would be more like having written `let x = 2;` in the above example, if that caused an issue, clearly there's a bug.
Also, I believ 1&2 both require unsafe code to implement the trait that allows the unsoundness.
For what &T can I safely implement DerefMut? Is it the fault of Pin that a type has DerefMut implemented that the unsafe block of that implementation doesn't uphold safety?
> For what &T can I safely implement DerefMut? Is it the fault of Pin that a type has DerefMut implemented that the unsafe block of that implementation doesn't uphold safety?
It is the fault of Pin's safety guidelines, which suggest a contract that is not actually enough to uphold safety. That's why this is considered an unsoundness in Pin, and not a problem with the code written with unsafe. That is:
> that the unsafe block of that implementation doesn't uphold safety?
is not correct, the unsafe block does everything it's supposed to to uphold safety.
See the playground link containing a demonstration of the issue: https://play.rust-lang.org/?version=stable&mode=debug&editio...
The 'unsafe' keyword in the internals post is referring to the stdlib implementation of Pin. The stdlib's use of unsafe is supposed to uphold safety guarantees for all functions that aren't exposed as unsafe, and the stdlib failed the guarantee here, thus allowing a soundness bug without the user using 'unsafe' anywhere.