6 ms·

Totally not expert on formal verification. If Rust’s base libraries get formally verified, and one does not use unsafe code, does that means all Rust programs t

by fsloth 2y ago

Totally not expert on formal verification. If Rust’s base libraries get formally verified, and one does not use unsafe code, does that means all Rust programs that use the formally verified libs get de-facto formally verified quality regarding their memoryhandling?

hu3 2y ago
I'm no Rust expert but it seems to have a lot of unsafe in core code. And understandably so: https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+language%3ARust&type=code&p=5&l=Rust https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l... I don't think coq, as being presented here, can verify all unsafe calls.
- steveklabnik 2y ago
  Most of the interest in formalizing Rust is specifically about formalizing the model that unsafe code is supposed to uphold.
Galanwe 2y ago
Rust safety has very little to do with bugs. Rust has its own definition of what "safe" means, which is arguably a subset of memory safety. You can have perfectly safe Rust code with data races, deadlocks, memory exhaustion, etc. Not even talking about logical errors.
- dist1ll 2y ago
  > You can have perfectly safe Rust code with data races No, you can't. Data races are explicitly one type of race condition that Rust protects you from. Anything else would indicate an unsound library or compiler bug. For reference, you can take a look at the non-exhaustive list of undefined behaviors[0]. None of those behaviours should be possible to trigger from safe Rust. [0] https://doc.rust-lang.org/reference/behavior-considered-undefined.html https://doc.rust-lang.org/reference/behavior-considered-unde...
  - hu3 2y ago
    As per https://doc.rust-lang.org/nomicon/races.html https://doc.rust-lang.org/nomicon/races.html > However Rust does not prevent general race conditions. > This is mathematically impossible in situations where you do not control the scheduler, which is true for the normal OS environment. > For this reason, it is considered "safe" for Rust to get deadlocked or do something nonsensical with incorrect synchronization: this is known as a general race condition or resource race. Obviously such a program isn't very good, but Rust of course cannot prevent all logic errors.
    - couchand 2y ago
      On the one hand, we like to encourage learning here. On the other, we prefer not to copy-paste a bunch of possibly-irrelevant content. Well, forgive me for pasting in a StackOverflow answer that may be relevant here: https://stackoverflow.com/questions/11276259/are-data-races-and-race-condition-actually-the-same-thing-in-context-of-conc#18049303 https://stackoverflow.com/questions/11276259/are-data-races-... > Are "data races" and "race condition" actually the same thing in context of concurrent programming > No, they are not the same thing. They are not a subset of one another. They are also neither the necessary, nor the sufficient condition for one another. The really curious thing here is that the Nomicon page also describes this distinction in great detail.
      - hu3 2y ago
        [flagged]
        couchand 2y ago
        I apologize if my comment came off as snark. Your comment was nothing but pasted text which ommitted relevant detail, so it was not clear what the intent was. In context, to me, it did not seem to be illuminating. It actually seemed to be introducing confusion where there previously was none. Data races are not possible in safe Rust. Race conditions are. The distinction is made clear in the Nomicon article, but commenters here are really muddying the waters...
raphlinus 2y ago
I think that to some extent represents the dream, with caveats. A few pieces need to fall into place. 1. You need to formalize the semantics of unsafe Rust. Ralf Jung's pioneering RustBelt[1] work was a huge step in that direction, but it is not yet complete. One element that's emerging as tricky is "pointer provenance." 2. Part of that is making a formal model of the borrow checker. Stacked borrows[2] was a good attempt, but has some flaws. Tree borrows[3] may correct those flaws, but it's possible something even more refined may emerge. 3. Another part of that is a formal memory model, which is mostly about the behavior of atomics and synchronization (thus, is critically important for standard library components such as Arc). It is widely understood that Rust's memory model should be similar to the C++ one (and that they should interoperate), but there are some remaining flaws in that, such as the "out of thin air" problem and also some missing functionality like seqlocks (part of why the Linux kernel still has its own). 4. You need a proof that the safety guarantees compose well; in particular if you have sound code written in unsafe Rust, composed with other code written in safe Rust, the safety guarantees still hold. There are good results so far but it needs to be proved over the entire system. 5. You do need to close all the remaining soundness bugs in Rust[1], for such a proof to hold for all code. Progress on this is slow, as many of these problems are theoretical, or are only really relevant for adversarial code[5]. When all this is done, you still only have a partial guarantee. Huge amounts of the surface area to interface with the system are based on unsafe code. If you're doing only pure computation, that's one thing, but if you're building, say, a graphical UI, there's a massive amount of stuff that can still go wrong. Even so, there is a practical path forward, and that leads to a much better situation than the usual state of things today, which is of course systems riddled with vulnerabilities. [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/ https://plv.mpi-sws.org/rustbelt/stacked-borrows/ [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html https://www.ralfj.de/blog/2023/06/02/tree-borrows.html [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3AI-unsound https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao... [5]: https://github.com/Speykious/cve-rs https://github.com/Speykious/cve-rs
- clarus 2y ago
  Thanks for the explanations and all the links!

by fsloth 2y ago

hu3 2y ago

I'm no Rust expert but it seems to have a lot of unsafe in core code. And understandably so: https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+language%3ARust&type=code&p=5&l=Rust https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l... I don't think coq, as being presented here, can verify all unsafe calls.

steveklabnik 2y ago
Most of the interest in formalizing Rust is specifically about formalizing the model that unsafe code is supposed to uphold.

Galanwe 2y ago

Rust safety has very little to do with bugs. Rust has its own definition of what "safe" means, which is arguably a subset of memory safety. You can have perfectly safe Rust code with data races, deadlocks, memory exhaustion, etc. Not even talking about logical errors.

dist1ll 2y ago
> You can have perfectly safe Rust code with data races No, you can't. Data races are explicitly one type of race condition that Rust protects you from. Anything else would indicate an unsound library or compiler bug. For reference, you can take a look at the non-exhaustive list of undefined behaviors[0]. None of those behaviours should be possible to trigger from safe Rust. [0] https://doc.rust-lang.org/reference/behavior-considered-undefined.html https://doc.rust-lang.org/reference/behavior-considered-unde...
- hu3 2y ago
  As per https://doc.rust-lang.org/nomicon/races.html https://doc.rust-lang.org/nomicon/races.html > However Rust does not prevent general race conditions. > This is mathematically impossible in situations where you do not control the scheduler, which is true for the normal OS environment. > For this reason, it is considered "safe" for Rust to get deadlocked or do something nonsensical with incorrect synchronization: this is known as a general race condition or resource race. Obviously such a program isn't very good, but Rust of course cannot prevent all logic errors.
  - couchand 2y ago
    On the one hand, we like to encourage learning here. On the other, we prefer not to copy-paste a bunch of possibly-irrelevant content. Well, forgive me for pasting in a StackOverflow answer that may be relevant here: https://stackoverflow.com/questions/11276259/are-data-races-and-race-condition-actually-the-same-thing-in-context-of-conc#18049303 https://stackoverflow.com/questions/11276259/are-data-races-... > Are "data races" and "race condition" actually the same thing in context of concurrent programming > No, they are not the same thing. They are not a subset of one another. They are also neither the necessary, nor the sufficient condition for one another. The really curious thing here is that the Nomicon page also describes this distinction in great detail.
    - hu3 2y ago
      [flagged]
      - couchand 2y ago
        I apologize if my comment came off as snark. Your comment was nothing but pasted text which ommitted relevant detail, so it was not clear what the intent was. In context, to me, it did not seem to be illuminating. It actually seemed to be introducing confusion where there previously was none. Data races are not possible in safe Rust. Race conditions are. The distinction is made clear in the Nomicon article, but commenters here are really muddying the waters...

raphlinus 2y ago

I think that to some extent represents the dream, with caveats. A few pieces need to fall into place. 1. You need to formalize the semantics of unsafe Rust. Ralf Jung's pioneering RustBelt[1] work was a huge step in that direction, but it is not yet complete. One element that's emerging as tricky is "pointer provenance." 2. Part of that is making a formal model of the borrow checker. Stacked borrows[2] was a good attempt, but has some flaws. Tree borrows[3] may correct those flaws, but it's possible something even more refined may emerge. 3. Another part of that is a formal memory model, which is mostly about the behavior of atomics and synchronization (thus, is critically important for standard library components such as Arc). It is widely understood that Rust's memory model should be similar to the C++ one (and that they should interoperate), but there are some remaining flaws in that, such as the "out of thin air" problem and also some missing functionality like seqlocks (part of why the Linux kernel still has its own). 4. You need a proof that the safety guarantees compose well; in particular if you have sound code written in unsafe Rust, composed with other code written in safe Rust, the safety guarantees still hold. There are good results so far but it needs to be proved over the entire system. 5. You do need to close all the remaining soundness bugs in Rust[1], for such a proof to hold for all code. Progress on this is slow, as many of these problems are theoretical, or are only really relevant for adversarial code[5]. When all this is done, you still only have a partial guarantee. Huge amounts of the surface area to interface with the system are based on unsafe code. If you're doing only pure computation, that's one thing, but if you're building, say, a graphical UI, there's a massive amount of stuff that can still go wrong. Even so, there is a practical path forward, and that leads to a much better situation than the usual state of things today, which is of course systems riddled with vulnerabilities. [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/ https://plv.mpi-sws.org/rustbelt/stacked-borrows/ [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html https://www.ralfj.de/blog/2023/06/02/tree-borrows.html [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3AI-unsound https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao... [5]: https://github.com/Speykious/cve-rs https://github.com/Speykious/cve-rs

clarus 2y ago
Thanks for the explanations and all the links!