Language vision regarding safety guarantees

A starting point would be anything that is more than a single auditable implementation. If it has generics or is otherwise pluggable or configurable it becomes too difficult to account for all possible combinations.

And even if it is a singular implementation I'd look at how precise the API is worded. If it's loose prose then it may as well be a "well, if we end up in a corrupted state anything can happen and you can't rely on anything" thing. If you find explicit wording such as HashMap's relation to bad Ord impls then it likely is what Ralf has called "super-safe", i.e. making additional hard promises beyond basic safety, similar to unsafe impl Trait making promises unsafe code can rely on.

This sounds like safety guarantees to me, but up to the interpretation of the reader, instead of using unambiguous terminology from the language (like documenting those guarantees under the # Safety section of the documentation).

Do you suggest the language convention, instead of being "unsafe code may rely on the logic contract of its dependencies", to be more something like "unsafe code may rely on explicit hard promises beyond basic safety from its dependencies"? Which is to be compared to the more straightforward "unsafe code may rely on safety guarantees of its dependencies".

Maybe there's a good reason for the language to be vague (like avoiding responsibilities), but it would be good to know it, because that's part of the design decision process.

The best way is to have an unsafe Trait with a safety section outlining what implementors have to uphold, which callers can the rely on. But without inherent impls we can't do that for inherent methods.

Putting a # Safety section on safe structs making extra promises doesn't seem to be an established convention, perhaps it should be.

There's also the contracts experiment which could specify postconditions, but that's not used anywhere yet.

So without any of these it's a social process. You can study the docs and the impl, ask the maintainers of a crate for more precise promises and how confident they feel about it if needed, perhaps contribute fuzzing, check what changed on major updates, etc. And then judge whether the API's correctness contract is something you're willing to rely on and willing to elevate to UB if it doesn't hold.

As a counterexample, Instant has a correctness promise to be monotonic. But underlying platforms have been observed to deviate from their own API contract, so you couldn't rely on it for soundness unless you're willing to accept UB on broken systems, which might be acceptable to some users but not to others who would like to keep using their broken systems.

2 Likes

That's indeed the summary of the situation.

Small detail regarding that point. I think a good property would be for contacts experiment to simply be a formal version of the existing informal safety documentation (including guarantees) rather than a completely new different thing. So either those post conditions must be the logic contract (like illustrated in top post) or we don't have this nice property.

I disagree. As I stated before in this thread, if we assume contract experiment is stabilized, then: all above conditions are not met (no unsafe Trait, no # Safety on safe struct, no contract post-conditions), then you MUST check the assumption at runtime, even if the upstream implementation indeed conforms to the contract.

Unfortunately, yes. It's a social problem; there's not a technical solution to the social blame game. As a community we can try to lay out guidelines that we suggest for how to communicate expectations, but this is fundamentally a fuzzy thing. If a logic error causes a soundness error, the responsibility is split between the source of the error and the consumer that made it soundness critical. What exactly that split is depends on a whole number of fuzzy factors that aren't possible to neatly put in a binary solution.

This is by design in my understanding of the problem space. Reasonable people can disagree. What's fine to trust for delegating soundness critical guarantees is a question without a single answer, and it's imho a good thing that the ecosystem can support projects operating at different levels.

It's best to avoid the implications of tying monetary blame to any OSS provided & used without warranty, but I do admit in the same breath that time is also a valuable currency.

One part of the problem which is clear imo — in the case of a disagreement, or a mismatch in urgency of fixes, it falls onto the party with the unsafe code to fix their unsoundness. My personal cutoff is roughly that I'd be willing to maintain an as-is fork to fix the guarantee I am choosing to rely on if upstream ever breaks it and we can't restore it upstream.

If I'm fully honest with myself, I don't always apply this uniformly, and a guesstimated likelihood of needing to follow through on the forking does also factor in to my decision. But I also have different levels for different projects that I offer different trust levels for.

And it only becomes your problem if they bring it to your issue tracker, at which point it is also largely a social problem. And as a social problem, it doesn't strictly need a strict technical answer. If it was a guarantee you advertise, and you're still supporting the library, you either fix the issue when you have the bandwidth or enable the people with the problem to fix it.

Contracts may be the formal technical way of describing it, but in a world of social contracts, I find much more shared ground by labeling the idea of offered trust. There's the default trust level that a published crate has, which should be smaller than a lot of developers do in practice. And there's a default for established crates, roughly that any intentionally documented property holds.

Projects can also offer their own trustworthiness, by documenting stronger guarantees, or by disclaimers such as stating a project is a proof of concept, still in alpha state, or not intended for production. If a party doesn't believe they should be trusted with upholding correctness for downstream client soundness proofs then I would be ill advised in trusting them anyway.

In reality, mio took ownership of the bug willingly, so that's the answer. They intended it to be the case, it wasn't, that caused a vulnerability.

In the case where mio's maintainers are unreachable, mio would be labeled as unmaintained in RustSec, and tokio would be expected to take over a fork as the largest project relying on mio.

In the case where mio says that was not a property we intended to guarantee for client consumption, the security advisory gets placed on clients that relied on the non-guarantee.

This can be shortcut by the dependency explicitly documenting what is and isn't intended to be given to clients for use in soundness proofs, but in practice it social backpressure has been sufficient so far to rely on for locating and deploying fixes.

Aside: part of the issue with the blame game is the scope. Suits see "security advisory" and think it must be bad. But in practice Rust is more granular with its security advisories; it's not uncommon to see some advisory that's roughly "if you deliberately misuse an API, it can cause UB when it said it couldn't," and that doesn't actually turn into a vulnerability if no client enables the API to be misused that way.

As a disclaimer, I am speaking for myself, not for any group. I would say the current situation is less really deliberate and more a natural conclusion from the other deliberate choices in 2015–2018 guidance in ecosystem direction. To be fair to early Rust, it was still busy proving that unsafe encapsulation was a measurable benefit at all, even with all of the leaky contracts from dependency to client.

… then when you're discussing with the crate maintainers the discussion would be about adding the post conditions instead of just stricter prose in documentation.

4 Likes

Otherwise, will breaking the prose be a breaking change? If the crate maintainer agree, then it should be in post conditions; If not, the downstream user should check it at runtime.

Otherwise, will breaking the prose be a breaking change

Yes, always has been.

I disagree with this. The technical solution is the unsafe mental model (a robust keyword for functions with safety guarantees, which require an unsafe block to return and unwind). That's obviously overkill and too late. So the next best thing is just regular documentation without any type system support (documenting guarantees in the # Safety section). The blaming is clear. Either the safety guarantee holds and it's the client which is incorrect, or the safety guarantee does not hold and it's the dependency which is incorrect. Of course we can still argue about the meaning of the documentation since it's informal English prose, but that's out of scope (contracts experiment is a solution but not realistic at ecosystem scale) and not the blaming issue we're discussing.

I agree with the first part, but I don't understand how you argue the second. When is it fuzzy? Those safety guarantees are in the exact same language as safety requirements. Do you mean safety requirements are also fundamentally fuzzy?

The whole point of safety guarantees is to prevent this situation. If it happens it's always the crate that relied on logic for safety which is at fault. This is already the case for requirements, and would be the case for guarantees too.

It seems to me you're doing the same mistake that has happened twice above. There's a difference between "a crate trusting the contract of a dependency" and "a crate advertising its contract with clients". I agree the first is subjective and every crate will have different opinions. However the second is not, because there's exactly one party involved (the public API of a crate is defined by that crate, modulo language constraints), while for the first many different crates may have many different opinions about a given dependency.

I agree. In a world with robust this would always be the actual culprit. But in our world (even with safety guarantees), that might be a crate that just happened to use a broken crate. I think that's fine. I distinguish between fixing the issue and blaming the actual culprit. It's not necessary the culprit which will do the fix, since the fix might be to simply stop depending on it, since if it failed once it could fail twice.

I don't understand that whole paragraph. APIs are contracts. APIs are made of types (safety only) and documentation (logic and safety). Both of those are reciprocal trust: "you pass an argument of the given type, I return a result of the given type" and "you pass a proper argument as documented, I return a proper result as documented".

Good, so that's not a good example then. I initially thought so based on:

But then why not say so upfront in their public API, rather than wait until there's undefined behavior somewhere? If they don't know, they just don't say anything (which should mean they don't guarantee it for safety), and clients that need it create a feature request to strengthen the contract by adding that safety guarantee (which is a minor bump).

Ok that's a good argument. So instead of "no safety guarantees by default, clients should create a feature request to negotiate one" it's "logic contract as safety guarantee, when UB happen we decide if it was actually stronger than intended". There's indeed some non-trivial trade-off. It's between "always having to request a guarantee before use" and "only weakening a guarantee when UB happens", which happens (probably significantly) less often. I think I could buy this argument, I'll need to sleep on it.

Wow, lots of discussion happened here. I'll share a few more facts about the mio/tokio case study:

There was never any question about whether it was a bug in mio. After all, mio documents the guarantee quite clearly:

After an explicit call to this method completes, it is guaranteed that the token previously registered to this handle will not be returned by a future poll, so long as a happens-before relationship is established between this call and the poll.

Registry::deregister

The question is whether a bug violating this guarantee is a vulnerability in mio or not.

Mio is already maintained by the Tokio team. It's not really a separate project.

In that case I'd like to hear your take on a different dependency.

I mentioned that the mio CVE was windows specific, and on windows it occurred due to some pretty complex code in mio. But on Linux the situation is quite different. The same guarantee holds on Linux because the epoll API provides said guarantee, and so the proof in mio is "easy": the epoll api works like that.

Now of course, this means that Mio/Tokio also has a robustness dependency on the entirety of the Linux kernel for the exact same guarantee.

So if you run the program on a Linux kernel with a bug such that the epoll API no longer follows this contract, well, you will trigger UB. Is that also unsoundness in Tokio?

1 Like

This question is essentially "do you trust the operating system to uphold the guarantees made in its documentation?", and it's one that bothers me a lot, basically because there is a lot of evidence that you shouldn't trust guarantees made in OS documentation, but also no practical alternative to doing so. (I've had personal experience with system calls not doing what they're supposed to do – in my case, it was Linux's vmsplice without SPLICE_F_GIFT, which documents a copy-on-write behaviour for the spliced pages but, at least at the time, appeared to alias the pages rather than actually copying them.)

There are also plenty of situations in practice where operating systems make "best effort" implementations of an API that end up not implementing all the semantics, so the operation does something approximately like what the documentation suggests should happen, but is not exactly correct. A common consequence of this is that something that is supposed to be atomic actually has race conditions in practice (and it's easy to see how this could lead to a vulnerability if you trust the OS too much).

As such, I think it makes sense to code defensively against potential mistakes made by the operating system, in order to reduce the negative consequences if it does happen. There are of course going to be some operating system mistakes that you can't defend against because they allow your code to be bypassed entirely, but there are also plausible mistakes (like returning stale data) that would be possible to catch (e.g. by storing indexes into a list of valid references rather than the references themselves).

In the case of tokio, therefore, it might make the most sense to depend on epoll working correctly for correctness, but not for soundness (so that if the OS does turn out to be buggy, you simply have a buggy program rather than a vulnerable one); the best tradeoff probably depends on how much performance you'd lose by being defensive, but often this sort of safety check is fairly cheap (especially compared to I/O).

There is no such symmetry between safety requirements and what you're calling "safety guarantees" or "robustness guarantees". The former has a rather precise meaning, the latter is not clear at best or meaningless at worst. I have read your definitions and discussions and I can't make sense of the concept you're trying to define.

Let me explain.

The only real requirements for a caller of a function are the safety requirements. By definition, violating those is the only case where a function has undefined behavior. For all other arguments it has some defined behavior. Not necessarily deterministic behavior, but still, constrained in some way that should optimally be documented.

The distinction is very clear. I normally know exactly whether to mark my functions unsafe or not.

For example:

u32::unchecked_add has actual requirements. That's why it's marked unsafe. If the arguments are bad, that's on the caller. The function can do anything it wants in that case.

u32::strict_add doesn't have any requirements. It has to handle every possible input. The code of the function has to be written differently, so that it works for every possible input.

Now you might informally say that strict_add "has a requirement", it "requires" the inputs be such that the sum doesn't overflow because it has a Panics section and it's going to panic on overflowing inputs. But that's not really a requirement. It can't assume the arguments don't overflow. It still has to handle overflowing arguments. Some user can legitimately pass overflowing inputs and expect everything is going to be fine as defined. It's not expected that such parameters will never be passed by any user.

On the other hand, when a function has a "guarantee", that is supposed to hold 100% of the time. It's not expected that the guarantee will be violated for some user. Otherwise, it wouldn't be called a "guarantee" but rather a "best effort" thing. For instance, Global::allocate will normally allocate memory, but it's not guaranteed: it's best-effort, not guaranteed.

Therefore, there doesn't seem to be any formal distinction between a regular "guarantee" and "robust/safety guarantee", especially if you intend for this to be a clear, well defined thing rather than some fuzzy distinction. As an author of a function I have no idea how you want me to decide whether my guarantees are supposed to be "regular guarantees" or "robust guarantees". I intend all my code to work 100% of the time as documented, otherwise I wouldn't call them "guarantees".

You mentioned at some point that the distinction is supposed to be based on whether the author is "careful". That's a very fuzzy word. So I'm surprised you're claiming the concept isn't fuzzy.

2 Likes

This problem comes up in other languages, regardless whether there's an explicit safe/unsafe boundary.

The problem in general is whether a consumer of a library relies on something that has been documented to work or is a common-sense behavior, or whether the consumer relies on some fragile implementation detail that hasn't been guaranteed (Hyrum's law, etc.)

For the Rust's promise of "safe code can't cause UB", it could get clarified with an asterisks like:

  • it can't cause UB in your code, but you don't control what absurdly fragile things somebody else can put in their unsafe code.
  • if you write unsafe without depending on unreliable things outside of your control, then someone else's buggy safe code won't break you via memory corruption.

or maybe "safe code can't cause UB" should be interpreted not as a description, but as a requirement for authors of unsafe blocks?

Write unsafe code in a way that makes it impossible for safe code to break yours.

Is there a symmetry between pre- and post-conditions? Is there a symmetry between #[requires] and #[ensures] of the contracts experiment? That's exactly the same thing between requirements and guarantees. In particular, those concepts match one-to-one when safety invariants are not violated in APIs.

I've explained this before. You either start with no safety guarantees and wait for unsafe clients to ask you for guarantees (the best option). Or you try to anticipate what unsafe clients might need (you're putting work on your side to avoid having your clients create a feature request, kind of like early optimization).

The definition of "careful" is "obey to the language convention". The language reference specifies that unsafe code should be sound. It is expected from users to be careful and write only sound unsafe code. They can be careless and write safe code incorrect for logic (they wouldn't be using the language wrong in that case).

The language could have had a similar rule for safety guarantees. If you write safe code (or unsafe code for that matter) with safety guarantees, then you must be correct for them (which could also be called "sound") otherwise you're holding the language wrong (you're not careful). But this rule does not exist, because while the language doesn't want a logic bug in a client to become a safety bug in some of its dependencies, the language is fine for a logic bug in a dependency to become a safety bug in some of its clients. In that case, both parties should fight to decide whether the guarantee was for logic only or also for safety.

The problem of relying on undocumented behavior, yes. But the specificity of Rust (which is trying to distinguish logic from safety with an escape hatch) is that there's 2 levels of behavior (safety and logic) which users must abide to for the escape hatch to not invalidate the language guarantees. There are other languages where safety and logic are distinct: essentially all languages with a sound type system. But if they don't provide an escape hatch (like unsafe), then users can't mess with safety, so they only care about logic (like languages without a sound type system). In Rust, because of the escape hatch, any uses of the escape hatch must play nicely with the type system (what Rust calls "soundness" and I call "correct for safety"). So users have to document safety and logic independently. Ideally safe code does not need to document safety because the types already do, so they can only care about logic like in any other language. But for unsafe code, they need to document safety. Today, it's just requirements which is only one half of encapsulation. Ideally it would also be guarantees, which would provide full encapsulation. But as discussed above, Rust is not trying to provide full encapsulation. It is perfectly fine for Rust programs to have undefined behavior due to this lack of full encapsulation. When it happens, involved parties should figure out how to remedy the situation without help from the language.

Those are related. The requirement is how the language proves the property. The requirement today is "unsafe code must not have UB for arbitrary safe clients" and the property is "safe code cannot cause UB without an unsafe client" (which uses both the above requirement and the fact that the type system is sound).

Yes. Pre-conditions = safety requirements. Post-conditions = documented return value or behavior.

For i32::unchecked_neg(x):

  • pre-conditions: x != i32::MIN
  • post-conditions: the return value is -x

For i32::strict_neg(x):

  • pre-conditions: none
  • post-conditions: if x != i32::MIN then the return value is -x, if x == i32::MIN then panic.

We already have pre-conditions and post-conditions today without a separate concept of "robust guarantees".

1 Like

This is simply because you take the logic contract as safety guarantees (as we identified earlier). And that's perfectly fine, because that's actually what the language tells you to do.

Not really, you have 2 notions of pre-conditions and one notion of post-condition:

  • safety pre-condition ("undefined" behavior if violated)
  • logic pre-condition (arbitrary but "defined" behavior if violated while above condition holds)
  • logic post-condition (specified behavior if above condition holds, which implies the one above it)

But anyway, the thing is that if you assume the convention (safety guarantee = logic contract), then you can't see the underlying model where there's a symmetry. And that's fine. You don't need to see it in Rust. (You would in a language with encapsulation.)

Fortunately we have gotten rid of such "arbitrary but defined" language in std documentation because it was close to being an oxymoron and would be completely useless in practice.

2 Likes

Thanks! That's orthogonal to the discussion but an important point. The picture becomes:

if safety_requirement {
    if logic_requirement {
        specified_behavior
    } else {
        reasonable_behavior // instead of arbitrary_behavior
    }
} else {
    undefined_behavior
}

Reasonable behavior means anything non-malicious code could do as part of its specified behavior. In particular, if the code is not expected to do network or file access, it won't access the network or file system as part of its reasonable behavior. So under the assumption of non-malicious code, this is an implicit guarantee (and doesn't need to be documented unless there's something surprising there).