Key operations

The Merkle tree proof and its state storage in Grug are primarily managed by the code under grug/src/jellyfish-merkle/src and grug/src/db-disk/src.

The key operations within our audit scope are as follows:

1. Applying batches of operations to the Merkle tree. These functions apply batches of operations produced by block processing, which consist of key-value pairs to insert or delete, to the Merkle tree. Applying batches of operations to the database is done in the ABCI FinalizeBlock handler, and they are committed to the database in the ABCI Commit handler.

2. ICS-23 proof generation. These functions implement generation of membership and nonmembership proofs for Grug's state in the ICS-23 format used by IBC. ICS-23 proofs are used for connection, channel, and packet management in the ICS-2, ICS-3, and ICS-4 standards.

Applying batches of operations to the Merkle tree

The application of batch operations resulting from block processing is performed through the flush_but_not_commit function, which calls MERKLE_TREE.apply_raw(...). This function takes four parameters — storage, old_version, new_version, and batch — and invokes the MerkleTree::apply function. The apply function takes the same parameters as apply_raw, except the keys in the batch must have been hashed and sorted by the caller.

The apply function marks the root node of old_version as orphaned if it exists in the nodes, starting from new_version. Then, the MerkleTree::apply_at function is used to apply the appropriate batch operation based on the state of the node at the bits position.

• If it is a leaf node, the MerkleTree::apply_at_leaf function is called, which applies a single insertion/deletion in place, or it creates a subtree if there are multiple insertions/deletions to apply to the leaf's position.

• If it is an internal node, the MerkleTree::apply_at_internal function is called, which partitions the batch into operations that apply to the left/right subtree, and it recurses into those by calling MerkleTree::apply_at_child.

• If the node does not exist, the MerkleTree::create_subtree function is used to create a subtree.

After each function completes its assigned role, the state of the node after the operation is saved, and a flush is performed to record this in the state_commitment function.

ICS-23 proof generation

The DiskDb::ics23_prove function generates proofs that key-value pairs are present or absent from Grug's state. It is intended to be called from IBC packet--processing code, which does not yet appear to be implemented. This function takes two parameters: key and version. It verifies whether the version is valid (i.e., not greater than the latest version or smaller than the oldest version) and retrieves the appropriate state storage for the given version.

If the state storage contains a value corresponding to the key, membership proof is performed using the key via a call to MerkleTree::ics23_prove_existence. If no value is found, a nonmembership proof is conducted by searching neighboring nodes of the nonexistent key and generating membership proofs for those neighboring nodes. This currently does not correctly account for neighbors that may have been deleted; see Finding ref↗.

To perform membership proofs, MerkleTree::ics23_prove_existence traverses child nodes based on the hash of the node's key: if the bit at the current traversal index is 0, the left node is traversed; if it is 1, the right node is traversed. This traversal method is similar to that of a Patricia Merkle tree.

Security considerations

As the ICS-23 reference implementation is used to verify proofs generated by this process, and since the keys are sorted by their hashes when being stored in the tree, soundness of the proofs is provided by the upstream implementation (i.e., chains cannot equivocate between membership and nonmembership of the same key for a given root hash).

Completeness issues arise from incorrect handling of deletions (as in Finding ref↗).

As discussed in Finding ref↗, the MerkleProof::prove function, which is used for Diem-style proofs, fails to perform correct verification when attempting to query the root node in an empty tree, also resulting in incompleteness for that proof format.