Challenge 10: Memory safety of String

  • Status: Open
  • Tracking Issue: #61
  • Start date: 2024/08/19
  • End date: 2025/04/10
  • Reward: N/A

Goal

In this challenge, the goal is to verify the memory safety of std::string::String. Even though the majority of String methods are safe, many of them are safe abstractions over unsafe code.

For instance, the insert method is implemented as follows in v1.80.1:

pub fn insert(&mut self, idx: usize, ch: char) {
    assert!(self.is_char_boundary(idx));
    let mut bits = [0; 4];
    let bits = ch.encode_utf8(&mut bits).as_bytes();

    unsafe {
        self.insert_bytes(idx, bits);
    }
}

where insert_bytes has the following implementation:

unsafe fn insert_bytes(&mut self, idx: usize, bytes: &[u8]) {
    let len = self.len();
    let amt = bytes.len();
    self.vec.reserve(amt);

    unsafe {
        ptr::copy(self.vec.as_ptr().add(idx), self.vec.as_mut_ptr().add(idx + amt), len - idx);
        ptr::copy_nonoverlapping(bytes.as_ptr(), self.vec.as_mut_ptr().add(idx), amt);
        self.vec.set_len(len + amt);
    }
}

The call to the unsafe insert_bytes method (which itself contains unsafe code) makes insert susceptible to undefined behavior.

Success Criteria

Verify the memory safety of all public functions that are safe abstractions over unsafe code:

  1. from_utf16le (unbounded)
  2. from_utf16le_lossy(unbounded)
  3. from_utf16be (unbounded)
  4. from_utf16be_lossy (unbounded)
  5. pop
  6. remove
  7. remove_matches (unbounded)
  8. retain (unbounded)
  9. insert
  10. insert_str (unbounded)
  11. split_off (unbounded)
  12. drain
  13. replace_range (unbounded)
  14. into_boxed_str
  15. leak

Ones marked as unbounded must be verified for any string/slice length.

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors:

  • Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
  • Reading from uninitialized memory.
  • Mutating immutable bytes.
  • Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.