5 ms·

However, if the unsafe code is written correctly, it is in fact well encapsulated. We can prove this now, it's no longer just conjecture.

foldr 9y ago
If the unsafe code is written "correctly" then of course, by definition, there isn't anything to worry about. The same is true of unsafe code in C or assembly. I took a look at the paper that you're obliquely referring to [1], and I think you are exaggerating the significance of its results for practical Rust programming. In fact, the paper underlines how difficult it is to use 'unsafe' correctly. As soon as you use any unsafe code, the language can no longer guarantee that any of your code is safe. Thus, to guarantee safety, you must either never use unsafe code except in libraries which have already been proven safe, or develop proofs for your own unsafe code. There are many instances where it is almost mandatory to use unsafe code in Rust (e.g. writing a mutable iterator for a custom data structure), so this is not a theoretical problem. As far as provable safety is concerned, the situation seems pretty similar to the situation in C++ (for which there is already a vast literature on techniques for formal verification of safety). That is not to deny that Rust code is likely to be safer than C++ code in practice. However, that has nothing to do with having unsafe operations block-scoped and tagged with the 'unsafe' keyword. I'm not a fan of this syntax because it can easily give newcomers to the language the mistaken impression that the danger is somehow contained within the relevant block. [1] http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202.pdf?ip=88.98.193.174&id=3158154&acc=OA&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2EC1E31BC46E58D5B8&__acm__=1523184964_df705dd5d3b548febf25f0e2b505a5c8 http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202....
- flurrything 9y ago
  That link is broken, but if it's the paper I think it is, the key result is that you can extend safe Rust with safe components that do use `unsafe` as long as you are able to prove these components to be sound. The same is not true of neither C nor assembly, and there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound. With safe Rust + the standard library there are almost no data-structures that you can't write.
  - foldr 9y ago
    >The same is not true of neither C nor assembly I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. > there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound Only if 'most' means 'all'! The paper itself notes that "...the problem cannot easily be contained by blessing a fixed set of standard libraries as primitive and just verifying the soundness of those; for although it is considered a badge of honor for Rust programmers to avoid the use of unsafe code entirely, many nevertheless find it necessary to employ a sprinkling of unsafe code in their developments." Non-broken link: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
    - Jweb_Guru 9y ago
      > I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? What isn't possible is encapsulating many of the safe APIs that Rust supports using C's type system. You can restrict all of the C code in a program to a subset that is safe, but it isn't a subset that anyone actually uses; by contrast, it is absolutely feasible to write programs that use safe Rust outside a handful of unsafe functions in the standard library. The primary reason is that Rust's type system is capable of encapsulating many more safe guarantees than C's is. As someone who works on the RustBelt team, you are misunderstanding the paper. What the paper is arguing is that we need to be able to prove modularity for arbitrary unsafe code, not just treat the standard library as type system primitives, because we want Rust's set of "primitives" to be easily extensible. > The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. It is fundamentally different. C++ does not have lifetimes or compile time verification of ownership; its references cannot be safely encapsulated behind an API, and it does not have "modes" like share and own. These are all critical for Rust's safety proofs. This is not for lack of trying; many people have attempted to define safe subsets of C or C++, or add these features to C, such as Cyclone. In all cases, new concepts and types needed to be added to the language and most existing code was no longer usable.
- Jweb_Guru 9y ago
  The situation isn't remotely similar to C++. After you prove an algorithm correct in C++, you can still generally not guarantee that it is used correctly by the program--the needed preconditions and postconditions are not expressible in its type system, and code that passes the C++ type checker can easily violate invariants elsewhere. In Rust, after you prove code in an unsafe module correct with respect to its type, you can use the module from any safe block and still preserve memory safety and data race freedom. The important thing that is different about code proved in Rustbelt is that the guarantees can be made local. Once you prove a semantic type for a particular piece of unsafe code, you do not have to know anything about that unsafe code when you prove some other piece of unsafe code correct, as long as they are independent of each other (including unsafe code that is invoked parametrically). This means that the proof effort does not scale with the size of your overall code, or quadratically with the number of unsafe modules, but linearly with the number of unsafe modules. That's absolutely not true in C++; it works entirely because of Rust's precise accounting of ownership. Finally: even in Rust that uses a lot (relatively speaking) of unsafe code, only a small percentage of the overall code is unsafe. Typical codebases have many hundreds of lines of safe code per line of unsafe code. This means the proof effort is quite reasonable. Automated proofs about C and C++ programs are not trivial and all known techniques do not scale to real code that is more than a few hundred lines, and proof assistant based techniques generally must either prove things about the entire program, or use restricted subsets and annotate them with information very much like what is in Rust's type system. The sel4 microkernel is one of the largest formally verified C programs, and it took 20 man-years of effort and hundreds of thousands of lines to prove, while the actual C code clocks in at under 10,000 lines. While the sel4 proof effort cared about more than memory safety, a significant amount of it was devoted to that. By contrast, I have personally written 10,000+ line Rust codebases with 4 lines of unsafe in them (and even those could be avoided if I were willing to sacrifice a bit of performance); I used only a few standard library functions, and third party crates like Rayon that have undergone a fair amount of verification effort themselves. Memory safety in Rust actually scales to realistic codebase sizes. The existing result isn't everything; there is still a lot of work to do to make sure it's accurately capturing all of Rust's semantics. But most of the "hard parts" have been done--we are pretty confident that the encapsulation I'm describing actually works. That is far better than the situation in C++.

foldr 9y ago

If the unsafe code is written "correctly" then of course, by definition, there isn't anything to worry about. The same is true of unsafe code in C or assembly. I took a look at the paper that you're obliquely referring to [1], and I think you are exaggerating the significance of its results for practical Rust programming. In fact, the paper underlines how difficult it is to use 'unsafe' correctly. As soon as you use any unsafe code, the language can no longer guarantee that any of your code is safe. Thus, to guarantee safety, you must either never use unsafe code except in libraries which have already been proven safe, or develop proofs for your own unsafe code. There are many instances where it is almost mandatory to use unsafe code in Rust (e.g. writing a mutable iterator for a custom data structure), so this is not a theoretical problem. As far as provable safety is concerned, the situation seems pretty similar to the situation in C++ (for which there is already a vast literature on techniques for formal verification of safety). That is not to deny that Rust code is likely to be safer than C++ code in practice. However, that has nothing to do with having unsafe operations block-scoped and tagged with the 'unsafe' keyword. I'm not a fan of this syntax because it can easily give newcomers to the language the mistaken impression that the danger is somehow contained within the relevant block. [1] http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202.pdf?ip=88.98.193.174&id=3158154&acc=OA&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2EC1E31BC46E58D5B8&__acm__=1523184964_df705dd5d3b548febf25f0e2b505a5c8 http://delivery.acm.org/10.1145/3160000/3158154/popl18-p202....

flurrything 9y ago
That link is broken, but if it's the paper I think it is, the key result is that you can extend safe Rust with safe components that do use `unsafe` as long as you are able to prove these components to be sound. The same is not true of neither C nor assembly, and there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound. With safe Rust + the standard library there are almost no data-structures that you can't write.
- foldr 9y ago
  >The same is not true of neither C nor assembly I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. > there are already soundness proofs of most unsafe components in the standard library available, which means that safe Rust + the standard library is sound Only if 'most' means 'all'! The paper itself notes that "...the problem cannot easily be contained by blessing a fixed set of standard libraries as primitive and just verifying the soundness of those; for although it is considered a badge of honor for Rust programmers to avoid the use of unsafe code entirely, many nevertheless find it necessary to employ a sprinkling of unsafe code in their developments." Non-broken link: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
  - Jweb_Guru 9y ago
    > I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? What isn't possible is encapsulating many of the safe APIs that Rust supports using C's type system. You can restrict all of the C code in a program to a subset that is safe, but it isn't a subset that anyone actually uses; by contrast, it is absolutely feasible to write programs that use safe Rust outside a handful of unsafe functions in the standard library. The primary reason is that Rust's type system is capable of encapsulating many more safe guarantees than C's is. As someone who works on the RustBelt team, you are misunderstanding the paper. What the paper is arguing is that we need to be able to prove modularity for arbitrary unsafe code, not just treat the standard library as type system primitives, because we want Rust's set of "primitives" to be easily extensible. > The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. It is fundamentally different. C++ does not have lifetimes or compile time verification of ownership; its references cannot be safely encapsulated behind an API, and it does not have "modes" like share and own. These are all critical for Rust's safety proofs. This is not for lack of trying; many people have attempted to define safe subsets of C or C++, or add these features to C, such as Cyclone. In all cases, new concepts and types needed to be added to the language and most existing code was no longer usable.
Jweb_Guru 9y ago
The situation isn't remotely similar to C++. After you prove an algorithm correct in C++, you can still generally not guarantee that it is used correctly by the program--the needed preconditions and postconditions are not expressible in its type system, and code that passes the C++ type checker can easily violate invariants elsewhere. In Rust, after you prove code in an unsafe module correct with respect to its type, you can use the module from any safe block and still preserve memory safety and data race freedom. The important thing that is different about code proved in Rustbelt is that the guarantees can be made local. Once you prove a semantic type for a particular piece of unsafe code, you do not have to know anything about that unsafe code when you prove some other piece of unsafe code correct, as long as they are independent of each other (including unsafe code that is invoked parametrically). This means that the proof effort does not scale with the size of your overall code, or quadratically with the number of unsafe modules, but linearly with the number of unsafe modules. That's absolutely not true in C++; it works entirely because of Rust's precise accounting of ownership. Finally: even in Rust that uses a lot (relatively speaking) of unsafe code, only a small percentage of the overall code is unsafe. Typical codebases have many hundreds of lines of safe code per line of unsafe code. This means the proof effort is quite reasonable. Automated proofs about C and C++ programs are not trivial and all known techniques do not scale to real code that is more than a few hundred lines, and proof assistant based techniques generally must either prove things about the entire program, or use restricted subsets and annotate them with information very much like what is in Rust's type system. The sel4 microkernel is one of the largest formally verified C programs, and it took 20 man-years of effort and hundreds of thousands of lines to prove, while the actual C code clocks in at under 10,000 lines. While the sel4 proof effort cared about more than memory safety, a significant amount of it was devoted to that. By contrast, I have personally written 10,000+ line Rust codebases with 4 lines of unsafe in them (and even those could be avoided if I were willing to sacrifice a bit of performance); I used only a few standard library functions, and third party crates like Rayon that have undergone a fair amount of verification effort themselves. Memory safety in Rust actually scales to realistic codebase sizes. The existing result isn't everything; there is still a lot of work to do to make sure it's accurately capturing all of Rust's semantics. But most of the "hard parts" have been done--we are pretty confident that the encapsulation I'm describing actually works. That is far better than the situation in C++.