3 ms·

I'm not really sure what the problem is here: having to formally verify a module doesn't seem fundamentally different to formally verify a single function. I me

by dbaupp 11y ago

I'm not really sure what the problem is here: having to formally verify a module doesn't seem fundamentally different to formally verify a single function. I mean, sure, it's some more code, but there's still well-defined containment. And, being "allowed" to reason about a whole module (well, usually one just cares about a whole type, but these often match, especially for unsafe code) seems far more useful: one can build far more interesting abstractions. If one was forced to reason about a single function at a time, Vec couldn't exist in a useful way, as every function would have to assume the incoming Vec value could be arbitrarily invalid. In any case, there are many many modules with no `unsafe` code, e.g. std::option has none [1], iron::response has none [2], image::jpeg has none [3] (just some random examples). These are automatically safe, if you assume that that the code they call is safe, which seems to me like the only assumption that can make sense: if the safe modules call unsafe ones that aren't safe... well, the problem is in the unsafe ones, not the safe ones. What I'm trying to say is this paragraph doesn't seem to change anything fundamental about the objections to safe vs. unsafe you sometimes write about; it is not introducing anything new, and so the refutations you often receive still apply. [1]: https://github.com/rust-lang/rust/blob/dfaddb732ced1da9d310990df095ca36f43fbc3d/src/libcore/option.rs https://github.com/rust-lang/rust/blob/dfaddb732ced1da9d3109... [2]: https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e07b2dc3f9749ee/src/response.rs https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e... [3]: https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c02b827190671ea9302716e86028/src/jpeg https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c...

shadowmint 11y ago
Well, given the most common refute of my concerns is 'you just have to make sure your unsafe blocks are verified to be correct', and the point of this article, is explicitly that this isnt the case... Now its that you have to just make sure all your code is correct, not just the unsafe blocks. /me shrugs I think thats lame, and breaks the promises rust is trying to make about writing safe secure software. If safe code may not be safe, whats the point of it at all. You, are of course welcome to your own oppinion.
- kibwen 11y ago
  > Now its that you have to just make sure all your code is > correct, not just the unsafe blocks. You appear to be misunderstanding the article, which likely explains all the downvotes. Rust keeps you from doing memory-unsafe operations unless you use an `unsafe` block somewhere. Once you do, then it is your duty to ensure that those `unsafe` blocks don't cause memory unsafety, regardless of what the rest of your program does. Following from that, if the correctness of your `unsafe` block relies on invariants in your data, then it is your duty to keep your data private so that those invariants cannot be broken by consumers (or alternatively, provide safe accessor functions that allow consumers to fiddle with things while performing runtime checks to ensure invariants are upheld).
- ralfj 11y ago
  No, it doesn't break the promises in any way. If all your code does potentially dangerous memory manipulation, then there's very little hope that there will ever be an automatic checker for the safety of your program. The promise of Rust rests on the assumption that most code is not like that. There are a few fundamental data structures that do crazy stuff, and okay, we have to use `unsafe` there - and if we want to have any formal guarantees, we have to do a formal proof. If are happy with less, we just manually audit that data structure extra carefully. We also put every such data structure in its own module, which carefully limits the amount of code that is exposed to this unsafety. However, most of the code will just use those data structures, and that's where Rust gives you a safety guarantee. Combing `Vec` and `HashMap` and all the other types from the standard library in any way you want, hammer them from multiple threads, send stuff across channels, whatever - you can do all of that safely, and if your code crashes, you don't have to look at all this code because you did not write `unsafe`, only the standard library did - and you are in a separate module. > Now its that you have to just make sure all your code is correct, not just the unsafe blocks. This is not correct. As I wrote in the post, you have to check all code within a module that contains `unsafe`. Most of the modules people write do not contain `unsafe`, and hence are not checked. I'd be curious to learn why you think this is the case.
  - shadowmint 11y ago
    The point I'm making is that, and this surprised me, the onus on soneone writing a module with unsafe code, to ensure it does not violate memory safety is much higher than I realized. It is not 'all rust' you must verify; just all rust that touches unsafe code. You might argue this is nothing new, and indeed if you read this comment thread you'll see the suggestion that the difference between verifying an entire module and verifying only the unsafe blocks in it is insignificant. My point is that there is at least an order of magnitude more safe code than unsafe code in an unsafe module, and I suspect it is not scrutinized nearly as much as the unsafe code. There are a lot of crates that use unsafe code in one form or another; and it troubles me (although no one else cares) that they are probably more dangerous than I realized. 'Just verify the unsafe blocks' is something I've literally heard people say.

by dbaupp 11y ago

shadowmint 11y ago

Well, given the most common refute of my concerns is 'you just have to make sure your unsafe blocks are verified to be correct', and the point of this article, is explicitly that this isnt the case... Now its that you have to just make sure all your code is correct, not just the unsafe blocks. /me shrugs I think thats lame, and breaks the promises rust is trying to make about writing safe secure software. If safe code may not be safe, whats the point of it at all. You, are of course welcome to your own oppinion.

kibwen 11y ago
> Now its that you have to just make sure all your code is > correct, not just the unsafe blocks. You appear to be misunderstanding the article, which likely explains all the downvotes. Rust keeps you from doing memory-unsafe operations unless you use an `unsafe` block somewhere. Once you do, then it is your duty to ensure that those `unsafe` blocks don't cause memory unsafety, regardless of what the rest of your program does. Following from that, if the correctness of your `unsafe` block relies on invariants in your data, then it is your duty to keep your data private so that those invariants cannot be broken by consumers (or alternatively, provide safe accessor functions that allow consumers to fiddle with things while performing runtime checks to ensure invariants are upheld).
ralfj 11y ago
No, it doesn't break the promises in any way. If all your code does potentially dangerous memory manipulation, then there's very little hope that there will ever be an automatic checker for the safety of your program. The promise of Rust rests on the assumption that most code is not like that. There are a few fundamental data structures that do crazy stuff, and okay, we have to use `unsafe` there - and if we want to have any formal guarantees, we have to do a formal proof. If are happy with less, we just manually audit that data structure extra carefully. We also put every such data structure in its own module, which carefully limits the amount of code that is exposed to this unsafety. However, most of the code will just use those data structures, and that's where Rust gives you a safety guarantee. Combing `Vec` and `HashMap` and all the other types from the standard library in any way you want, hammer them from multiple threads, send stuff across channels, whatever - you can do all of that safely, and if your code crashes, you don't have to look at all this code because you did not write `unsafe`, only the standard library did - and you are in a separate module. > Now its that you have to just make sure all your code is correct, not just the unsafe blocks. This is not correct. As I wrote in the post, you have to check all code within a module that contains `unsafe`. Most of the modules people write do not contain `unsafe`, and hence are not checked. I'd be curious to learn why you think this is the case.
- shadowmint 11y ago
  The point I'm making is that, and this surprised me, the onus on soneone writing a module with unsafe code, to ensure it does not violate memory safety is much higher than I realized. It is not 'all rust' you must verify; just all rust that touches unsafe code. You might argue this is nothing new, and indeed if you read this comment thread you'll see the suggestion that the difference between verifying an entire module and verifying only the unsafe blocks in it is insignificant. My point is that there is at least an order of magnitude more safe code than unsafe code in an unsafe module, and I suspect it is not scrutinized nearly as much as the unsafe code. There are a lot of crates that use unsafe code in one form or another; and it troubles me (although no one else cares) that they are probably more dangerous than I realized. 'Just verify the unsafe blocks' is something I've literally heard people say.