Rust protects you from bugs, but I don't envision anybody wanting to deliberately advertise that their code may be buggy and users have to protect themselves from such bugs. That would just seem like a rubbish library.
1 Like
Ok, I think that's where our hypotheses differ. I believe there is a comprehensive logic model, it's simply the semantic model of the language. It's low-level in the sense that you talk about observable events (FFI calls, ASM stories, volatile accesses), but for specific platforms you can have higher-level events (read a file, send a UDP packet, etc), on top of which you can build arbitrary user properties. But I agree this is out of scope for this thread. At least we agree on the safety contract part which is on topic 
1 Like
I guess the complexity here is something that @scottmcm brought up in another thread:
I think there's a core tension here between the desirable requirements "a BTreeMap<K,V> for which I know that K's Ord implementation is correct should always be ordered", and "BTreeMap<K,V> should be memory-safe regardless of how badly behaved K's Ord implementation is". Both of these requirements are potenitally important to avoid memory-safety vulnerabilitiies: the latter requirement is required if someone writes a broken Ord, and the former requirement is required if unsafe code relies on a BTreeMap<u32,V> to be correctly ordered.
For the first requirement to hold, btree_map::CursorMut::insert_before_unchecked needs to be unsafe, which effectively declares having an unordered BTreeMap<u32> to be library UB.
For the second requirement to hold, btree_map::CursorMut::insert_before_unchecked needs to be safe: otherwise, giving a BTreeMap a K with a broken Ord implementation is library UB, because it leads to an unsafe method being called without actually upholding its safety requirements.
As such, we basically have a weird case of specialisation here: the implication is that btree_map::<K,V>::CursorMut::insert_before_unchecked is safe whenever K is a downstream type (and that having an incorrectly sorted BTreeMap is library UB in this case), but unsafe whenever K is a standard library type (and that having an incorrectly sorted BTreeMap is not library UB in this case, just a logic error).
I'm not sure that there's any sensible way to cover this gap. (It almost seems as though the "safety level" or "trust level" should be some sort of generic parameter, but I can't think of a way to make that work.)
I don't think there's actually a gap here, because if there is it's the same gap as "well arbitrary safe code correctness is also relevant to soundness", which in the limit means that everything needs to be unsafe, which isn't helpful 
This is wrong. It's OK for the function to exist and be unsafe. It's up to the caller to make sure they don't call it with invalid type / input combinations.
But the caller (BTreeMap) does call it with invalid type/input combinations today, according to its stated safety requirement, if the key type has a broken Ord implementation.
The safety comments in BTreeMap's source code for the calls to insert_before_unchecked assume that Ord is non-broken, which is not a sound assumption given that Ord is a safe trait.
Safety requirements are for external callers from outside of the abstraction boundary. When calling functions in your own module / crate you can ignore documented safety requirements.
2 Likes
I would say that if the type's Ord implementation is incorrect, then insert_before_unchecked's safety requirement should (but is not currently written to) not apply. This resolves the conflict: in the case where nonsensical inserts can happen from safe code, nonsense is sound.
3 Likes
Possibly related to all this: part of the reason I was concerned about all the unsafe in BTreeMap is that it makes it harder to prove it to be sound, and I just came across a bug report demonstrating that BTreeMap does actually double-free with some Ord implementations. (In this case, the incorrect assumption made by Node is that Ord does not panic. an assumption that is wrong even for some standard library types like RefCell<u32>.)
I think the confusion about what unsafe actually means with respect to something like BTreeMap is probably responsible for this. The problem is that Root::split_off, which does not have any stated safety requirements, calls move_suffix, which also does not have any stated safety requirements, but move_suffix actually cause the BTreeMap to get into an invalid state (one in which consuming-iterating over it will cause a double free). This can cause unsoundness in safe code because Root::split_off continues by calling a user-provided trait method (which could panic, and then surrounding code could catch the panic in order to iterate over the invalid-state BTreeMap), but I would put the blame here on move_suffix for not being marked unsafe. (Suspiciously, move_suffix has a large unsafe block with no safety comment above it – but I think that isn't the problem that causes the unsoundness, rather the unsoundness is caused by the fact that it breaks invariants and does not document that it does so.)
The whole BTreeMap implementation seems to have been written using a principle of "let's not care about soundness requirements for our own use internally, and just mark the public APIs as safe or unsafe according to whether use from outside the module would be safe or unsafe", but this means that it isn't benefiting from the Rust compiler helping to catch soundness issues, and thus allows bugs like that to sneak through. I would have hoped for better from the standard library (i.e. using only a minimum of unsafe code that is carefully vetted to ensure soundness).
I would tend to disagree (if I understand you correctly): the main reason to use a BTreeMap rather than a HashMap is when you need sorted entries or even to look at what is before/after a given entry.
The tradeoff is between storing backreferences for every tree node persistently in the data structure (O(number of nodes)), and storing backreferences for every tree node on the route to the object currently being iterated over temporarily in each iterator (O(log(number of nodes) * number of iterators)).
My reasoning is that although you often do use iterators with BTreeMap, you don't normally use very many of them, compared to the number of elements you iterate over. Allocating a small amount of extra memory for each iterator does hurt, but it doesn't hurt as much as allocating extra memory for a backreference in every tree node does (especially given that if you are iterating over the whole tree, you would need to pay the cost of loading all the backreferences from main memory – loading them from the iterator instead is faster, because they would already be in cache).
The extra cost wouldn't be needed for "element before" / "element after" queries, only for iterators and cursors.
1 Like
This is perfectly fine and just a matter of style. This is why I wrote that the concept of unit of implementation is subjective. Within a unit of implementation, there are no contracts (see below for nested contracts). The contracts are at the boundaries of the unit of implementation. And you prove that this unit of implementation is correct with respect to those contracts.
The maximum unit of implementation is the union of a crate with all its pinned dependencies recursively. In large projects like the standard library, it makes sense to consider smaller units of implementation like modules, since it would be too costly to review all of the standard library for correctness when changing arbitrary small and isolated parts. One could obviously push this even further (in particular for large modules) and consider every item (like function definitions) as units of implementation.
Since units of implementation have a natural nesting behavior (a crate with its pinned dependencies is made of crates, which are made of modules, which are made of items), there is naturally a notion of "nested contracts". In particular, an item has an "item-level" contract (its contract when seen as a unit of implementation), but it also has a "module-level" contract (the part of its module contract when that module is seen as a unit of implementation) if it's an item exposed outside the module, and similarly for its "crate-level" contract if it's an item exposed outside the crate. Contracts can always be rewritten into equivalent contracts, such that nested contracts imply the contracts their nested in (item-level implies module-level which implies crate-level). This is a "contract implication" so variance needs to be taken into account between requirements and guarantees.
In the case of insert_before_unchecked, there's at least 2 contracts: the one when seen from outside the standard library and the one when seen from inside. But there could be more depending on how the authors want to split the units of implementation. The problem as you noted, is that the unsafe keyword is unique, so it cannot necessarily match all contracts. The contract it must match is the highest-level contract (highest in the sense of most public, so crate-level for public items). So it's possible that an internally safe function (no safety requirements when used within the module) is marked unsafe because it's publicly unsafe.
What I mean when I say that "safe code cannot cause UB" is that if there's UB, you can always attribute it to an incorrect unsafe block.
I know that you sometimes end up in a situation where the unsafe block looks like this:
let x = library::foo();
// SAFETY: Library is implemented correctly.
unsafe { ub_if_library_is_incorrect(x) };
If that safety comment turns out to be wrong, well shucks. The author of that unsafe block took a risk, and it didn't work out. So this is a scenario where:
- There is UB.
- The fix is to change the safe code, and not the unsafe block.
Given this, was the unsafe block wrong? Well, there is certainly one way in which it's wrong: It had a safety comment saying "library is implemented correctly" and, well, it wasn't implemented correctly, so it had an incorrect safety comment. That makes the unsafe block wrong.
Of course, there's also another way in which it's not wrong: When we fixed the bug, the unsafe code did not change. If it did not change and is now correct, it must have been correct all along?
So given that, I agree the situation is not 100% clear.
However, here's what I think is the right way to look at it: UB is often caused by several things going wrong at the same time. After all, we could fix the UB by changing the unsafe block too! Delete the unsafe { ub_if_library_is_incorrect(x) } line of code, and voilà, no UB. So I guess the UB was caused by that unsafe block after all!? Sure, the bug in library remains, but the UB is gone.
Enough about UB, let's talk about vulnerabilities.
CVE-2024-27308 is an interesting example. Mio documents a guarantee in its docs, and Tokio relied on it in unsafe code. It turns out that the windows implementation violated this contract in some circumstances.
At the time, it was actually argued to me that the CVE should be filed under Tokio because in mio it's just a bug, and it's Tokio that actually triggered UB as a result. However, my take is that this is Rust idealism. There is no other programming language where you would come to the conclusion that the CVE should be filed under Tokio. This conclusion stems purely from the concept of "unsafe" and how closely it's tied with CVEs in our community. Filing it under mio makes much more sense because, for instance, in a CVE you list which versions are affected and also the version in which the bug was fixed. Those questions cannot be answered if it's filed under Tokio because the fix was to change mio.
So did mio cause this CVE or did Tokio cause it? Well, on one hand the bug is in mio and the fix was to change mio, so it seems clear that mio is the cause. However, it's not quite that clear. As the CVE says, versions of Tokio prior to v1.30.0 were not actually vulnerable because prior to v1.30.0, Tokio would use the mio token as a key into a map, rather than cast it to/from a pointer. If we had never made this change in Tokio, then I do not think this mio bug would have been filed as a CVE. It would just have been a bug. So while the unsafe code in Tokio did not cause the bug in mio, it did cause the CVE.
Given an instance of UB, the list of causes that came together to trigger UB may include some causes that are entirely safe code. However, if so, then that cannot be the only cause, and one of the other causes will involve unsafe code.
I do not think wording this as "safe code cannot cause UB" is unreasonable.
14 Likes
I’d say that there is a narrow, pedantic sense in which the unsafe code should change, when viewed at package granularity: its dependency on the library with the bug should be changed to require the fixed version as the minimum version.
Actually I don't think the dependency listing in Tokio should be updated to require the mio version with the fix. That's the wrong tool for the job. The tool I'm actually using to get people who are affected to update is to publish a CVE and RUSTSEC entry for the issue. If someone doesn't want to update mio because, for example, they're not using windows, then that's their prerogative and Tokio shouldn't list a version requirement unless its really needed.
2 Likes
Thanks for this concrete example, which exactly demonstrates where Rust fails to properly distinguish between safety and logic.
This is imprecise. There's 2 ways to understand "incorrect unsafe block":
- The unsafe code fails to uphold the safety requirement of some operation. (This is a result-driven meaning of correct, which only takes the goal into account. So "if the earth is flat, spiders have 10 legs" is incorrect.)
- The unsafe code[1] is incorrect with respect to its safety contract. (This is the theoretical meaning of correct, which also takes hypotheses into account. So "if the earth is flat, spiders have 10 legs" is correct.)
In the first case, you're essentially saying "you can always attribute undefined behavior to where it occurs". So in that case you just need the unsafe keyword for directly-unsafe code. You don't need the concept of unsafe APIs, because you don't need hypotheses (you ignore them). Because Rust does have the concept of unsafe APIs, this can't be the correct interpretation.
In the second case, you need to know which hypotheses are available to that unsafe code, which is the notion of safety guarantees (the safety requirements of an unsafe function become safety guarantees for its body). Since in Rust logic contracts are safety guarantees, you can't always attribute undefined behavior to an incorrect unsafe block, it might be that some safe code had a logic bug. So this also can't be the correct interpretation.
The correct interpretation is: "safe code cannot cause UB in its dependencies" (the italic part being implicit). This is why you need unsafe APIs, to prevent safety properties to become logic properties in clients. The notion of safety requirements propagates safety properties from a unit of implementation to its clients.
To complete the picture (dependency, self, client):
- "safe code can cause UB in its unit of implementation": this is by design and why it's useful to have control over what you consider a unit of implementation (crate, module, function). That's the usual understanding of the scope of unsafe.
- "safe code can cause UB in its clients": This is the main concern. With safety guarantees you can prevent safety properties to become logic properties in dependencies, and thus "safe code cannot cause UB in its clients".
This is again some result-driven meaning of "[in]correct". If Rust thinks that "if the earth is flat then spiders have 10 legs" is an incorrect statement, then this is a more fundamental issue. And we probably shouldn't even talk about contracts at all (because contracts are implications from requirements to guarantees).
Saying "library is implemented correctly" is a hypothesis provided by the language: "logic contracts are safety guarantees". (I obviously disagree with this language decision, and this is the purpose of this thread, making sure it's deliberate and not accidental, since it obviously contradicts the statement that "safe code cannot cause UB".)
Indeed, which is why I believe neither the library nor the unsafe code is wrong, the language is wrong. The situation is not 100% clear because the language is defect. You don't have this issue in C, because C doesn't try (and fail) to distinguish between logic and safety, it only (successfully) have logic.
I think that's another wrong way to look at "cause UB"/"incorrect". When safety contracts are clear, then there's clearly a culprit: the unit of implementation that is incorrect for safety (sure there can be more than one, but that's not shared attribution, they're all completely wrong). The fact that we can work around a culprit in otherwise not-culprit code, doesn't mean the not-culprit code is culprit.
I would not call this idealism, I would call this a defect. The fact that logic contracts are safety guarantees is a language defect, and indeed no other programming language made that mistake.
Indeed, that's what the unsafe mental model tried to fix. You need unsafe code to provide safety guarantees, that's just obvious. And for that you need to be able to choose your safety guarantees (under the constraint that non-robust functions should have no safety guarantees, the same way non-unsafe functions should have no safety requirements).
That's an interesting take. I would generalize it as: while a unit of implementation may be incorrect for safety, it may need another (perfectly correct) unit of implementation to demonstrate that incorrectness. I would not say Tokio caused the CVE, I would say Tokio demonstrated a CVE in Mio. (A CVE that only exists because in Rust "logic contracts are safety guarantees", maybe Mio never wanted to provide such guarantees, but Rust forced it on them.)
This is again result-driven thinking. There is no list of causes. There is a list of unsatisfied properties, but the cause is where a post-condition is unsatisfied while its pre-condition were (there may be multiple such causes, but all of them are equally wrong and don't share attribution). This is a trivial statement that at least one unsatisfied property is in unsafe code, because all directly-unsafe code is unsafe code, and undefined behavior only occurs in directly-unsafe code.
I hope I managed to explained why I believe the opposite.
seen as a unit of implementation, or within a unit of implementation ↩︎
I guess my main concern with your point of view is that I don't think "a unit of implementation should be checked for soundness as a whole" is acceptable in cases where the unit of implementation is too large.
Rust provides a lot of tools to help prove soundness, and in particular, they can be used even within a unit of implementation to help to give more confidence that it is sound. If I have a large unit of implementation – say, a crate together with all its dependencies – and it is using a soundness-checking approach which requires all the internal code to be logically correct (e.g. because it relies on logical correctness of some safe parts of the code to avoid undefined behavior of some unsafe parts of the code), then it is significantly likely that the code will actually be unsound because the surface area that you have to check is too large.
In a way, the promise of Rust is "to prevent a particular class of bugs – those that compromise memory safety – you only have to review unsafe blocks and the code they depend on". To prevent all bugs, you have to review all the code, and this is in general very difficult to do correctly for nontrivial amounts of code. But the hope is that memory-safety bugs can be mostly or even entirely eliminated, by drastically reducing the amount of code that needs reviewing to do that, reducing the effort required to review it to something that humans can reasonably manage.
If the unsafe blocks have large dependencies – e.g. relying on an entire external crate to be implemented correctly – then there's no longer a significant gain from Rust's safety guarantees: the effort of eliminating memory-safety bugs is comparable to the effort of eliminating all bugs, including logical ones, and this amount of effort has historically been proven to be unreachable (or at least economically infeasible) for just about any program.
As such, in the example of the vulnerability @alice linked above, I would put the blame on Tokio for making the soundness of its unsafe code dependent on the correctness of a large dependency. I consider Tokio's unsafe block to be inherently unsound regardless of whether mio is correct or not, because it is too difficult to tell whether mio is correct or not and thus too difficult to tell whether the safety condition is correct. (Or another way of looking at it: for unsafe code you need to be able to prove the safety condition correct, and if it is too complicated, e.g. relying on the correctness of a large dependency, you can't do that.)
The use of unsafe in the programs I write is thus almost entirely at the leaves: I want all the unsafe to be confined to small, self-contained abstractions that I can then build a safe program around, and I want the safety of those unsafe blocks to be as easily proven as possible. (There's one library I'm working on which I ended up entirely rewriting, on the basis that although I was pretty sure it was correct, the unsafe conditions were too complicated for me to be confident. The rewrite changed some of the internls to make the unsafe better-encapsulated and easier to reason about in isolation.) This is why I am horrified at things like the BTreeMap implementation in std/alloc (which I consider problematic enough that I'm seriously considering writing my own version) – I consider it large and complicated enough that it shoul have been designed in a way that doesn't require reasoning about the correctness of the whole to prove the correctness of the unsafe portions (and consider this viewpoint to be supported by the evidence that it was, in fact, unsound).
2 Likes
What you describe is essentially the "Rust Hypothesis" (self-encapsulation: there are no safety guarantees). I also believed this was the convention before I learned that it was not the case and "logic contracts are safety guarantees". I believe this is a good signal that the language should probably take an official stance here.
Note that while the Rust Hypothesis guarantees that "safe code cannot cause UB outside its unit of implementation", it is a bit extreme. It could be refined to authorize the scope of unsafe to leak to dependencies in a controlled way using safety guarantees, exactly like the scope of unsafe is allowed to leak to clients in a controlled way using safety requirements. You can still locally review code for safety (in particular with the robust keyword, which requires unsafe code to provide safety guarantees).
Maybe you missed the part where you get to choose what a unit of implementation is: crate, module, item, etc. I agree that the language should recommend that units of implementation with directly-unsafe code should not exceed 100 lines. In some case that's the crate, in others that's the module, and in the worst case that's the function.
Indeed, that's the current promise. More precisely: to prevent safety bugs, you only need to review unsafe code[1] and the code it depends on. The problem is that that last part is unbounded, and in particular may escape the unit of implementation. So you simply can't review it without pinning those dependencies (which has bad properties). And even with pinning, you may end up extending your unit of implementation beyond what is reasonable to review.
That's not completely correct. You can't review a small dependency either. You would need to pin it first to make it part of your unit of implementation.
Maybe what you're saying with "large dependency" is not that "some of its implementations (past, present, and future) are large" but rather than "its logic contract seems hard to implement correctly". Maybe you could defined it as "there are no correct implementations in less than 100 lines". But then what happens if that dependency decides to write a large implementation for performance, and that implementation ends up being incorrect in a corner case? From their point of view it's just a logic bug. They never claimed to implement the logic contract in less than 100 lines. They never claimed their implementations can be used by unsafe code. Maybe they care more about performance than being correct in all possible corner cases (even unrealistic ones).
A safety contract makes this kind of interaction clearer. A unit of implementation can tell which parts of its API it will prioritize for being absolutely correct, by writing those property as safety contract, and which parts it will prioritize for performance (being possibly incorrect in rare cases), by writing those property as logic contract. I talk about performance but it could be anything else that could trump absolute correctness. As a client of such a unit of implementation, you don't need to guess whether that dependency is able to implement its logic contract correctly, you just assume its safety contract and they will get the CVE if they are incorrect. Also when they get reviewed for safety, those claims will be checked. There's no mixing between logic and safety.
I guess that's what you meant, because unsafe impl and unsafe attributes matter ↩︎
1 Like
I'd actually forgotten that it was possible to depend on a small dependency that's auto-downloaded / auto-updates, because doing that is so far outside my mental model of how programming should work. (I would typically copy the source of a small dependency rather than trying to keep it as a separate library, because there's no reason to share it between projects and because it's common to want to customize them to be a better fit for your own project. The main exception would be if the small dependency is a trait definition that traits use to communicate between each other.) Yes, I know it's commonly done in practice, but didn't bring that thought to mind until you reminded me.
I agree with you that if you are depending on a small dependency from a package manager, that updates independently of your own project, that still doesn't really help from the safety guarantee point of view (and indeed doesn't even guarantee that the dependency will remain small).
2 Likes
I see. Indeed that's an alternative to pinning the dependency. In both cases you extend your unit of implementation to remain self-contained (satisfying the Rust Hypothesis).