Challenge 4: Memory safety of BTreeMap's btree::node module

  • Status: Open
  • Tracking Issue: #77
  • Start date: 2024/07/01
  • End date: 2025/04/10
  • Reward: 10,000 USD

Goal

Verify the memory safety of the alloc::collections::btree::node module. This is one of the main modules used for implementing the BTreeMap collection, and it includes a lot of unsafe code.

Success Criteria

The memory safety of all public functions (especially safe ones) containing unsafe code must be verified, e.g.:

  1. LeafNode::new
  2. NodeRef::as_internal_mut
  3. NodeRef::len
  4. NodeRef::ascend
  5. NodeRef::first_edge
  6. NodeRef::last_edge
  7. NodeRef::first_kv
  8. NodeRef::last_kv
  9. NodeRef::into_leaf
  10. NodeRef::keys
  11. NodeRef::as_leaf_mut
  12. NodeRef::into_leaf_mut
  13. NodeRef::as_leaf_dying
  14. NodeRef::pop_internal_level
  15. NodeRef::push
  16. Handle::left_edge
  17. Handle::right_edge
  18. Handle::left_kv
  19. Handle::right_kv
  20. Handle::descend
  21. Handle::into_kv
  22. Handle::key_mut
  23. Handle::into_val_mut
  24. Handle::into_kv_mut
  25. Handle::into_kv_valmut
  26. Handle::kv_mut

Verification must be unbounded for functions that use recursion or contain loops, e.g.

  1. NodeRef::new_internal
  2. Handle::insert_recursing
  3. BalancingContext::do_merge
  4. BalancingContext::merge_tracking_child_edge
  5. BalancingContext::steal_left
  6. BalancingContext::steal_right
  7. BalancingContext::bulk_steal_left
  8. BalancingContext::bulk_steal_right

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.