Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Should we have a language concept of erroneous behavior? #512

Open
CAD97 opened this issue May 22, 2024 · 7 comments
Open

Should we have a language concept of erroneous behavior? #512

CAD97 opened this issue May 22, 2024 · 7 comments

Comments

@CAD97
Copy link

CAD97 commented May 22, 2024

Defining "erroneous behavior" as an operation that has a defined result (does not cause UB) but is still considered incorrect for a program to perform, endorsing sanitizing environments (such as Miri, Valgrind, or CHERI) diagnosing the presence of erroneous behavior and halting program execution.

I would expect the cases of erroneous behavior to be fairly limited, but it seems like it could be beneficial for those cases where an operation is defined not because we're endorsing doing it but because making it undefined instead would be worse. Potential cases include:

  • Modifying a let bound value without mut and lacking any internal/shared mutability.1
  • Writing through a shared reference to bytes next to but not covered by UnsafeCell.2
  • Relying on exposed provenance instead of using a strict provenance compatible API.3
  • Retagging bytes as a type that they aren't a valid instance of (e.g. reference to uninit).4
  • Cases of transmute by function call ABI that control flow integrity doesn't like allowing.5
  • Diagnosable library UB that isn't immediately elevated to language level UB.6
  • Runtime conditions like Arc reference count exceeding its maximum and aborting.7

(Please don't discuss whether these examples should be allowed or not here; use the issue for each case for that. This issue should focus on whether this is a class of behavior we want to officially recognize as defined but erroneous.)

If UB is an Abstract Machine error, you could think of erroneous behavior as an AM warning. Sanitizers could always choose to diagnose even without any "permission" from the spec, but this would still be a "false positive," and people tend to write code that relies on doing a thing when you tell them that doing the thing is allowed, even if it's discouraged to do so.

Footnotes

  1. Miri could in theory diagnose this similarly to how the immutability of static places is enforced. However, the optimization potential is questionable, and delayed initialization of let bindings makes it less straightforward, since the place is actually just mutable until it isn't.

  2. Stacked Borrows prohibits this for structs/tuples/arrays, but Tree Borrows tags the full reference range uniformly based on any use of UnsafeCell.

  3. Miri already warns when this occurs. IIUC CHERI deterministically segfaults the process when trying to read/write through a spoofed pointer. This could also apply to other fun code crimes like abusing non-pointer-layout carriers of provenance in a way that breaks on CHERI.

  4. Making reference retagging depend on the contents of the retagged memory appears to have no optimization benefits and would still require the concept of shallow validity to exist. However, it could be beneficial to assign blame to the creator of an unsafe reference than only diagnosing the symptom once a read occurs.

  5. I don't know many details here, but IIRC CFI checks want to catch pointer type mismatch and Rust would prefer pointer ABI to only care about the unsized tail kind.

  6. This would imply that cfg(ub_checks) is a kind of lightly sanitizing environment.

  7. Okay, this one is definitely a stretch and is just the runtime behavior of the code as written, but it provides a framework for interpreting the choice between causing an abort or saturating and leaking like the linux kernel would prefer.

@RalfJung
Copy link
Member

I definitely think we should have this tool in our toolbox (though for most of the items you listed I am far from convinced that we want to use this tool there).

@saethlin
Copy link
Member

it could be beneficial for those cases where an operation is defined not because we're endorsing doing it but because making it undefined instead would be worse.

I think the space of things that are well-defined but not endorsed is a bit bigger than what we're intending to use this term for. So I'd like to see a better exploration of what would motivate us to call something erroneous behavior.

@steveklabnik
Copy link
Member

A historic example of a similar thing appearing in the surface language is integer overflow, from RFC 560.

There are various operations which can sometimes produce error conditions (detailed below). Typically these error conditions correspond to under/overflow but not exclusively. It is the programmers responsibility to avoid these error conditions: any failure to do so can be considered a bug, and hence can be flagged by a static/dynamic analysis tools as an error. This is largely a semantic distinction, though.

https://rust-lang.github.io/rfcs/0560-integer-overflow.html

I vaguely remember older versions of this text using the term "program error" to describe this sort of behavior.

@steveklabnik
Copy link
Member

C++ is also doing work here, see

@CAD97
Copy link
Author

CAD97 commented Jul 9, 2024

Seeing EB get used for C++ is what initially got me thinking about its potential use for Rust, in fact. Although I'm far from fully aware what the extent of its implications are for C++. The talk around wanting sanitizers to be able to catch mutation of let bindings not declared as mut (but UB being imo fairly clearly not the tool for that) is what prompted me to bring it up here.

If this is a tool we want to have available, it's a good idea to understand what the tool does and when we do want to use it. So I'll properly ask: is the following an accurate description of what EB would mean in the context of Rust?

Erroneous Behavior is an operational fault recognized at the level of the Abstract Machine, but unlike Undefined Behavior, the result of executing a program which exhibits EB is defined. Executing EB results in either

  • termination of execution as if by program abort, non-unwinding panic, or other crash (such as those controlled by instrumented and/or sanitizing environments), or
  • valid program behavior as specified by the specific origin of EB. (How this behavior is selected and what the options are is defined case-by-case by each origin, and may include nondeterminism, but not immediate UB.)

If that description is accurate, I'd consider it reasonable to close this issue with an answer of yes. Or to keep it open and transition it into a kind of tracking issue, depending.

If that description isn't accurate, we should come up with one that is such that we can utilize EB if/when it is/becomes appropriate.

@RalfJung
Copy link
Member

RalfJung commented Jul 9, 2024

That reflects what I had in mind as well. Another potential usecase for this are ABI mismatches -- some of the ones that are currently well-defined are things that the CFI folks would like to reject as exploit mitigation; we could use EB as a way to carve out what calls they may reject without having to make those calls UB.

But if we close this issue I feel like we should document this somewhere.

@ojeda
Copy link

ojeda commented Aug 6, 2024

A historic example of a similar thing appearing in the surface language is integer overflow, from RFC 560.

I vaguely remember older versions of this text using the term "program error" to describe this sort of behavior.

Indeed, similar wording has been at e.g. https://doc.rust-lang.org/stable/reference/behavior-not-considered-unsafe.html since 2017 (even if not normative), so I considered Rust, in practice, already has EB. In fact, seeing the advantages of it in Rust is why I started supporting introducing and splitting EB from UB for C and C++ in WG14 a few years ago.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants