[mimd]

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]

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]

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]

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]

C++ for sure needs better safety mechanisms. And I don't know the exact number of issues simple heuristics can catch.

[steveklabnik]

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

[mimd]

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]

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

[mimd]

Thanks for the input and links. I'll need to test out the costs of the mitigations.

BTW, I found one of the rust rfc documents helpful for understanding the borrow checker. Do you know if there is a similar rust RFC document for the upcoming polonius borrowchecker, even if it's just a working copy? I'm having trouble finding anything beyond some blog posts.

[aw1621107]

Unfortunately I'm not super-familiar with developments around Polonius, so chances are what I can point you towards are the same things you found when searching. The most relevant bits appear to be the Polonius book [0] linked from the repo [1], but I don't know how up to date the book is or if there are more up-to-date resources. The RFC book [2] doesn't seem to have anything obviously about Polonius either.

[0]: https://rust-lang.github.io/polonius/

[1]: https://github.com/rust-lang/polonius

[2]: https://rust-lang.github.io/rfcs/

[steveklabnik]

Because defined behavior and undefined behavior operate very differently. One has guaranteed semantics, and the other can do literally anything.