Safe code relied upon by unsafe is effectively unsafe

language design Unsafe Code Guidelines
1

Rust is designed to allow mistakes in safe code without violation of soundness, but mistakes in unsafe code are allowed to violate soundness. This is the fundamental idea behind the distinction of safe and unsafe code. But if unsafe code relies upon explicitly documented behavior in safe code, it means that the safe code should strictly follow its documentation, or otherwise soundness of the program may be violated. A mistake in safe code can make a program unsound. I.e. safe code effectively becomes unsafe when it is relied upon by unsafe code.

Condition A: Code can be modified in every possible way, excluding introduction of unsafe keyword and unsafe macros, and be sound.[1]

  1. Condition A is necessary and sufficient for code to be safe.
  2. Inverse of condition A is necessary and sufficient for code to be unsafe.
  3. It is sufficient for unsafe code to act in accordance with documentation of every API it uses in order to be sound.

Follows from statement 1:

  1. Code can violate behavior guaranteed by its own documentation and remain sound.

One of the statements 1, 2 and 3 is not true.

Proof

According to statement 1 the function rand() is safe. (And by extension from condition A sound.) According to statement 2 the function rand_str() is unsafe. According to statement 3 the function rand_str() is sound. Yet the code is not sound. Thus one of those statements is not true.

/// Generates a random number in 0..4
fn rand() -> u8 {
    4 // chosen by fair dice roll.
      // guaranteed to be random.
}

fn rand_str() -> &'static str {
    match rand() {
        0 => "Zero",
        1 => "One",
        2 => "Two",
        3 => "Three",
        _ => unsafe { std::hint::unreachable_unchecked() },
    }
}

I believe the first two statements are the definition of safe and unsafe code. Thus the third statement is false and the following statement is true:

  1. It is not sufficient for unsafe code to act in accordance with documentation of every API it uses in order to be sound.

Now my question is: what other conditions are necessary for unsafe code to be sound?

Condition 3 in conjunction with the inverse of condition 4 is sufficient. Even if condition 1 is alternated to be only necessary, there is still a problem. Now a discrepancy between the documented and the actual behavior of safe code, i.e. a bug in safe code, can make the program unsound, which defies the purpose of safe code.

I believe the third statement is assumed to be true by most people writing unsafe code. Possibly I am projecting this from my own experience, since I believed it was true. If it is the case, this means that every piece of safe code used from unsafe code is potentially de facto unsafe. If some unsafe code relies upon safe code to not violate its own documentation in order to be sound, then that means that every piece of such safe code is in a state or can be modified is such a state that the program will be unsound and it will remain safe according to statement 1.

Is there a way to write unsafe code which can be formally proven to be sound and not rely on the correctness of safe code, since it can not be relied upon in general?

  1. Assuming the language specification and implementation are correct and we stay within the realm of the language. A safe program can for example use some platform-specific API to directly access its own memory, create and run a script which will attach gdb to the program itself and mess with its execution flow or convince the user to hit the computer with a blow-hammer (I am not sure whether the later would be considered a violation of soundness), but this is beyond the scope of the language. ↩︎

1 Like
4

Safety is the property of a function that ensures that all its evaluations are sound, and in particular that there is a semantic model of all its evaluations. It doesn't say what that semantic model is, or how precise it is. A function such as checked_add has a much more precise model than non-deterministically producing any value. The fact that a functions semantics correctly follows is documentation is just another property to rely on for a proof of code that calls it; and for constructing the semantic equivalence of an unsafe implementation to its unsafe interface documentation.

Your assertion A.1 is an incorrect understanding.

Soudness indeed requires that all composition with the safe-marked function are free of UB, but the usage of checked_add is not such a composition. It is structurally part of the definition of the function that calls it. There is no 'for-all' qualifier in that usage. (In contrast to an generic function such as in fn quick_sort<A: Ord> that is quantified over A).

In that sense, the semantic interpretation of soudness judgments of unsafe function composition is intensional. It indeed matters precisely which one objects its definition refers to and for forward compatibility of such proofs, it also matters how. Of course, if the model we want to build of piece of code relies on the assertion that a functions semantics are stricter than soundness requires and peeks inside such functions definition, it's the burden of such code to demonstrate how it ensures this is true—under forward compatibility under all potential replacements of the object it references. Usual ways of achieving this are either by defining the method locally; or axiomatically by claiming that external agreements ensure that other revisions of code will not deviate from semantics. Such as, the RFC process of the standard library ensuring it.

3 Likes
5

Rust has two distinct uses for the unsafe keyword:

  1. Unsafe precondition/unsafe to call
  2. Unsafe postcondition/unsafe to implement

Case 1. is covered by unsafe fn

// the caller of `foo` is responsible for safety (with a caveat) 
// can only be called with numbers smaller than 4 (exclusive)
unsafe fn foo(a: u32) {
    match {
        0 => { /* whatever */ }
        1 => { /* whatever */ }
        2 => { /* whatever */ }
        3 => { /* whatever */ }
        _ => unsafe { 
            // safe because a < 4
            hint::unreachable_unchecked()
        }
    }
}

The 2. case is covered by unsafe impl

unsafe trait Foo {
    // output must be equal to `a + b`
    fn add(a: i32, b: i32) -> i32;
}

// safety is the resposibility of the implementor
unsafe impl Foo for () {
    fn add(a: i32, b: i32) -> i32 {
        a + b
    }
}


if <() as Foo>::add(3i32, 7i32) != 10 {
    unsafe { 
        // safe because 3 + 7 = 10
        hint::unreachable_unchecked()
    }
}

This leads to the question wheter rust should let standalone functions as being unsafe impl, because as of now its up in the air if you can trust a non unsafe impl functions documentation.

This means that in the given example is either unsound because rand fails to uphold its postcondition, or the implementor of rand_str fails to uphold the precondition of hint::unreachable_unchecked

// even if this documentation is wrong the fault lies with `rand_str` 
// for trusting `rand` which is not `unsafe impl`, right?

/// Generates a random number in 0..4
fn rand() -> u8 {
    4 // chosen by fair dice roll.
      // guaranteed to be random.
}

fn rand_str() -> &'static str {
    match rand() {
        0 => "Zero",
        1 => "One",
        2 => "Two",
        3 => "Three",
        _ => unsafe { 
           // this is actually unsound because nothing is stopping `rand`
           // from returning 4 because it is safe rust and cannot be trusted  
           std::hint::unreachable_unchecked() },
    }
}

We could add safe keyword to show that a functions implementation does what it says on the documentation (which is expected anyways) and that you can rely on it for correctness, and unsafe code is only ever allowed to depend on safe functions, meaning we get the following code:

// we can now clearly see that the fault lies at `rand`s implementation
// which fails to uphold its own invariant

/// Generates a random number in 0..4
safe fn rand() -> u8 {
    4 // chosen by fair dice roll.
      // guaranteed to be random.
}

fn rand_str() -> &'static str {
    match rand() {
        0 => "Zero",
        1 => "One",
        2 => "Two",
        3 => "Three",
        _ => unsafe { 
           // safety: `rand` only gives numbers in range 0..4,
           // and this is quaranteed by its implementation
           std::hint::unreachable_unchecked()
        },
    }
}
4 Likes
6

I think you may have been misled by the conversation on urlo. That conversation was mainly about relying on the guarantees in an unsafe trait's safety documentation. That scenario can't be generalized to all dependencies on external (safe or unsafe) code.

Almost all unsafe code (other than in the std library I guess) depends on external code, whether safe or unsafe, even if it only depends on the std/core libraries. That external code may be documented to provide guarantees unrelated to safety. When implementing your unsafe code in a sound manner, you have to decide whether to rely on the external code's guarantees or not. This problem is independent of whether the external code is safe or unsafe.

4 Likes
7

This is indeed a well-known fact, that perhaps should be documented/communicated better: unsafe code can and does rely on the functional correctness of safe code that it explicitly depends on for soundness.

In other words, this is completely okay:

use some_hashmap_crate::HashMap;

unsafe {
  // Rely on this being a correct hash map implementation.
}

OTOH, this is not okay:

fn my_fun<H: HashMapTrait>() {
  let h = H::new();
  unsafe {
    // Rely on this being a correct hash map implementation.
  }
}

Unsafe code may only rely on the correctness of upstream code, never of downstream code.

28 Likes
8

Often one can call out to safe code without relying on its correctness guarantees, only relying on its soundness. For example iterator adapters sometimes interleave a lot of unchecked arithmetic operations and pointer accesses with calls to arbitrary Iterator::next implementations. But the unsafe code is written so that the preconditions of the unchecked arithmetic are fulfilled independent of the correctness of next. But this still requires defensive coding since your unsafe code will have to remain sound if any of those calls unexpectedly unwinds, loops forever, is reentrant etc.

If you do rely on the correctness of safe code then you're elevating that to a safety requirement, which means you need to treat all the safe code as if it were unsafe code. So if you're doing proving then you either need to prove the safe code you're relying on or make it a precondition of your proof. As Ralf says, such a proof would be impossible if you accept arbitrary trait impls because one could always construct a hostile implementation that violates whatever you're relying on.

5 Likes
9

If you are formally proving some unsafe code doesn't have UB, you must also prove the correctness of any and every safe code it depends for its soundness (even code in other crates, including the stdlib). That is, while it is true that you can't rely on safe code in general, but you can rely on specific, trusted instances of safe code.

Note that sometimes you can prove that your unsafe code merely calls some safe code but doesn't rely on it for soundness. It's the only way you can write generic unsafe code for example: you must guarantee that no matter the generics instantiation you caller chooses, your code remains sound.

For example, if you write an unsafe fn f<T: Eq>(x: T, y: T) { .. }, you may have x == y inside this function but you must not rely on its correctness to ensure soundness[1], that is, f must not have UB even if T implements Eq wrong. With the right tools, you can prove that.

[1] see the docs of the trait:

Violating this property is a logic error. The behavior resulting from a logic error is not specified, but users of the trait must ensure that such logic errors do not result in undefined behavior. This means that unsafe code must not rely on the correctness of these methods.

4 Likes
10

Ultimately there are cases where bugs in a library that are not memory safety bugs in that library are still CVE worthy for introducing memory safety bugs in downstream libraries.

Take RUSTSEC-2024-0019 as an example. In mio, this is just a logic but where it can give out tokens after they're guaranteed destroyed. But due to how Tokio used it, it became a use-after-free in Tokio. Still, we reported the CVE on mio and not Tokio, because that's where the CVE belongs.

9 Likes
11

If anyone wants to read more about this in a semi-formal fashion, there's the unsafe mental model. The particular notion Ralf mentions is tracked by the robust keyword which is the dual of unsafe with respect to variance. This has currently no syntax or convention but still exists and is necessary to prove soundness.

3 Likes
12

The answer is simple: Make invalid states unrepresentable.

It can't contradict the docs if it can't possibly return a value other than in the docs.

13

That's not simple at all, and in many cases it's impossible.

1 Like
14

Sure, you can have mistakes in your types' implementations that "can't" represent invalid states but it surely is better than relying on the documentation of the function to know what subset of the type's possible values it returns.

15

I'm not sure I'm following.

Take for example HashSet<usize> (with the primitive usize type and default hasher, so everything stdlib controlled). I would be reasonable to require that after set.insert(1) then set.contains(&1) will return true, while the state where set.contains(&1) is invalid and should never happen. This is a very common operation to the point that some unsafe code wants to rely on this. How do you represent this in a type such that the invalid state is impossible?

2 Likes
16

I was eager to say that we really need this (or anything else that makes unsafe Rust more tractable) but I'm having a hard time figuring out what the concept of being "robust" actually mean. Is there somewhere else that describes what robust means in simpler terms?

For what I can gather it is defined only in relation to an update type in the quick start section of the book:

The section the robust keyword attempts another description (the same as yours) but it is even less clear. It's also not clear why it states that "it is not recommended to actively document a type as robust". I mean, robustness is a concept that was created to aid reasoning about unsafe Rust, but referring to it in documentation - the only place we can specify unsafe requirements of our code - is actively discouraged? Then what it is for?

17

I don't know if it's simpler terms, but the actual definition of a robust type is in the "what is unsafe" section (which can be found from the glossary). I highly suggest reading "what are types" first unless you have strong type theory background.

In a few words if you understand the quick start enough: unsafe types have values that the type system doesn't see, and robust types are missing values that the type system believe can be present.

This is described here and initially here. There's also a mention here. Hope this helps.

1 Like
18

I would either make a wrapper type or a different kind of type (depending on the requirements).

It's not possible to completely phase out invalid states but it's far better to encapsulate it into a type, which affirms the premise that set.contains(&1) returns true by documentation. This makes it easier to debug because there's less code that could go wrong.

This doesn't completely solve the problem (which is why many projects use extensive testing tools), as it is impossible to solve (you always have to trust someone and/or something).

19

But such type would ultimately have to rely on HashSet's behaving correct, so in the end you just put another layer inbetween, which arguably makes it less clear what's going on.

20

Correct, but if you do it well enough, you can make it at least a bit clear and the benefit can be big.

21

let's absolutely not no that, it would be an absolute disaster of terminology, as "safe" currently is used everywhere to mean "not unsafe" and there's some plans to add it with that meaning, such as "safe fn" in extern blocks, and possibly "safe" blocks that deactivate outer unsafe blocks.

additionally, this is a poor use of a keyword, since it doesn't really add anything to the language (similar to how "let mut" is frequently described as "just a lint"). this doesn't add more safety, it just adds confusion.

22

Oh I agree.