3 ms·

I'm confused over lines such as "Profiles have to reject pointer arithmetic, because there’s no static analysis protection against indexing past the end of the

by mimd 2y ago

I'm confused over lines such as "Profiles have to reject pointer arithmetic, because there’s no static analysis protection against indexing past the end of the allocation." Can't frama-c/etc do that? Additionally, section 2.3 is narrower than what is implied by the words "safe" and "out-of-contract" and is more concerned with what C/C++ call "undefined behavior" requirements than contract correctness. Ie. An integer which is defined to wrap overflows and violates the requirement of the function contract, which I can cause in a safe release build rust.

bjornsing 2y ago
How is it supposed to do that (in the general case)? If I write a C++ program that will index out of bounds iif the Riemann hypothesis is true, then frama-c would have to win the millennium prize to do its job. I bet it can’t.
- bluGill 2y ago
  Often when I look into questions like this I discover the general case is impossible, but simple hysterics can get 99.999% of the cases and so I can get almost all the benefit even though some rare cases are missed.
  - zozbot234 2y ago
    My own semi-random guess is that "simple hysterics" is indeed how a vast majority (if perhaps not quite 99.999%) of C/C++ devs approaches the code correctness problem - which is why safety mechanisms like the one proposed by OP may in fact be urgently needed. Simple heuristics are likely to be significantly more worthwhile, if appropriately chosen.
    - bluGill 2y ago
      C++ for sure needs better safety mechanisms. And I don't know the exact number of issues simple heuristics can catch.
steveklabnik 2y ago
You cannot cause undefined behavior with integer overflow using + in Rust. That behavior is considered an error, but is well defined.
- mimd 2y ago
  If it requires the programmer to bear the responsibility for proper usage (eg. must use checked_add not rely on panic), how's that different than the issues with undefined behavior? I'm also concerned with the differing functional behavior between debug and release, and the mistaken impression it could create (eg. code handles overflow in debug fine due to panic but blows up on release as the proper solution is not used). And a resulting propagation of the overflow error to a precondition of an unsafe call that modifies memory.
  - aw1621107 2y ago
    > If it requires the programmer to bear the responsibility for proper usage (eg. must use checked_add not rely on panic), how's that different than the issues with undefined behavior? It comes down to the blast radius for a mistake. A mistake involving UB can potentially result in completely arbitrary behavior. A mistake in the safe subset of a language is still a mistake, but the universe of possible consequences is smaller. How much smaller depends on the language in question. > I'm also concerned with the differing functional behavior between debug and release IIRC this was a compromise. In an ideal world Rust would always panic on overflow, but the performance consequences were considered to be severe enough to potentially hinder adoption. In addition, overflow checking was not considered memory safety-critical as mandatory bounds checks in safe code would prevent overflow errors from causing memory safety issues in safe Rust. I believe at the time it was stated that if the cost of overflow checking ever got low enough checking may be (re)enabled on release builds. I'm not sure whether that's still in the cards. It's not ideal and can lead to problems as you point out when unsafe code is involved (also e.g., CVE-2018-1000810 [0]), but that's the nature of compromises, for better or worse. [0]: https://groups.google.com/g/rustlang-security-announcements/c/CmSuTm-SaU0 https://groups.google.com/g/rustlang-security-announcements/...

by mimd 2y ago

bjornsing 2y ago

How is it supposed to do that (in the general case)? If I write a C++ program that will index out of bounds iif the Riemann hypothesis is true, then frama-c would have to win the millennium prize to do its job. I bet it can’t.

bluGill 2y ago
Often when I look into questions like this I discover the general case is impossible, but simple hysterics can get 99.999% of the cases and so I can get almost all the benefit even though some rare cases are missed.
- zozbot234 2y ago
  My own semi-random guess is that "simple hysterics" is indeed how a vast majority (if perhaps not quite 99.999%) of C/C++ devs approaches the code correctness problem - which is why safety mechanisms like the one proposed by OP may in fact be urgently needed. Simple heuristics are likely to be significantly more worthwhile, if appropriately chosen.
  - bluGill 2y ago
    C++ for sure needs better safety mechanisms. And I don't know the exact number of issues simple heuristics can catch.

steveklabnik 2y ago

You cannot cause undefined behavior with integer overflow using + in Rust. That behavior is considered an error, but is well defined.

mimd 2y ago
If it requires the programmer to bear the responsibility for proper usage (eg. must use checked_add not rely on panic), how's that different than the issues with undefined behavior? I'm also concerned with the differing functional behavior between debug and release, and the mistaken impression it could create (eg. code handles overflow in debug fine due to panic but blows up on release as the proper solution is not used). And a resulting propagation of the overflow error to a precondition of an unsafe call that modifies memory.
- aw1621107 2y ago
  > If it requires the programmer to bear the responsibility for proper usage (eg. must use checked_add not rely on panic), how's that different than the issues with undefined behavior? It comes down to the blast radius for a mistake. A mistake involving UB can potentially result in completely arbitrary behavior. A mistake in the safe subset of a language is still a mistake, but the universe of possible consequences is smaller. How much smaller depends on the language in question. > I'm also concerned with the differing functional behavior between debug and release IIRC this was a compromise. In an ideal world Rust would always panic on overflow, but the performance consequences were considered to be severe enough to potentially hinder adoption. In addition, overflow checking was not considered memory safety-critical as mandatory bounds checks in safe code would prevent overflow errors from causing memory safety issues in safe Rust. I believe at the time it was stated that if the cost of overflow checking ever got low enough checking may be (re)enabled on release builds. I'm not sure whether that's still in the cards. It's not ideal and can lead to problems as you point out when unsafe code is involved (also e.g., CVE-2018-1000810 [0]), but that's the nature of compromises, for better or worse. [0]: https://groups.google.com/g/rustlang-security-announcements/c/CmSuTm-SaU0 https://groups.google.com/g/rustlang-security-announcements/...