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.
* 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.
> 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.
* 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%...
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...
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.
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/