Assessment reports>Initia>Critical findings>Unsound native-function declaration leading to critical verifier bypass
Category: Coding Mistakes

Unsound native-function declaration leading to critical verifier bypass

Critical Severity
Critical Impact
High Likelihood

Description

The table.move module defines functions that can be used to maintain tables containing elements indexed by a key (also known as hashmaps in other contexts).

The module exposes functionality to iterate over the elements of a table, in a mutable or immutable fashion. The intended usage of the mutable version of this feature is as follows:

// t is a Table<K, V>
// start and end are Option<bytes> which constrain the start and end of the iteration
// order determines whether iteration should occur in ascending or descending order (sorted by the BCS serialized key)
let iter = table::iter_mut(&t, start, end, order);
loop {
    if (!table::prepare_mut<K, V>(&mut iter)) {
        break;
    }

    let (key, value) = table::next_mut<K, V>(&mut iter);
} 

Most of the functionality of the module is supported by native functions, including iterators. In particular, iter and iter_mut use the new_table_iter and new_table_iter_mut native functions, which create an object in the VM memory and return an identifier that refers to the object:

native fun new_table_iter<K: copy + drop, V, B>(
    table: &Table<K, V>,
    start: vector<u8>,
    end: vector<u8>,
    order: u8
): u64;

native fun new_table_iter_mut<K: copy + drop, V, B>(
    table: &mut Table<K, V>,
    start: vector<u8>,
    end: vector<u8>,
    order: u8
): u64;

Due to how the native functions are defined, the Move verifier is unable to correctly track the relationship between the table object passed to the new_table_iter[_mut] function and the returned iterator. This makes the reference safety verifier ineffective.

Impact

This issue allows to mount a critical bypass for the security invariants enforced by the reference safety verifier, allowing for an instance to obtain two independent mutable references to the same object or to retain a mutable reference to an object even after it is transferred.

The appendix (ref) contains a proof-of-concept test that demonstrates the issue.

Recommendations

Change the implementation of the iterator functionality to allow the reference safety verifier to correctly track reference relationships. In practice, this can be achieved by ensuring to receive the type of the table (or table values) as input and returning a reference to the type of the table (or table values) as output.

Remediation

Zellic © 2024Back to top ↑