Breaking the Tree: Violating Invariants in Semaphore
Welcome back to another Veridise blog post! In this post we talk about contract invariants and why it is so helpful to keep them in mind when checking your code for bugs. As formal methods people, we tend to do this naturally, but its usefulness was made especially clear to us in our recent audit of Semaphore, a foundational protocol in the Ethereum ecosystem for building privacy preserving applications like anonymous voting and safe whistleblowing. By explicitly specifying contract invariants, we were able to quickly find two serious bugs in Semaphore that have been there since its initial release and were missed during previous audits.
Contract Invariants
Some of you might be asking: What are contract invariants? As their name suggests, a contract invariant is a property of the contract that should hold throughout the contract’s lifecycle. For example, consider the example ERC20 token implementation:
contract ExampleToken {
uint initialSupply = 100000000 * (10 ** 18);
uint totalSupply;
mapping(address => uint) balances;
ExampleToken() {
totalSupply = initialSupply;
balances[msg.sender] = totalSupply;
}
function burn(uint _value) {
require(_value <= balances[msg.sender]);
unchecked {
balances[msg.sender] = balances[msg.sender] - _value;
totalSupply = totalSupply - _value;
}
}
function mint(uint _to, uint _value) {
require(totalSupply + _value >= totalSupply);
unchecked {
totalSupply = totalSupply + _value;
balances[_to] = balances[_to] + _value;
}
}
...
}One contract invariant that quickly comes to mind is that totalSupply should always equal the sum of all the values in the balances map. If we look closely, the two require statements in this contract ensure this invariant holds as otherwise, the totalSupply could overflow, breaking the invariant.
In our experience as auditors and researchers, we found violations of contract invariants to be a common source of bugs: while in the weeds of some specific part of the protocol, it can be all to easy to forget some of the global properties that should hold.
One of the first things we, as auditors, do at Veridise is to write down all contract invariants we can think of. In addition to helping us find bugs, contract invariants also help give us a clear picture of what the contract should be doing.
The Semaphore Protocol
Before diving into the contract invariants that helped us find the bugs in Semaphore, let’s briefly go over the protocol, which provides a simple and generic privacy layer for Ethereum DApps. For those already familiar, feel free to skip this section 🙂.
At its core, Semaphore is a zero-knowledge protocol that allows users to create groups, prove membership in a group, or broadcast information to group members without revealing their identity. Each group is represented by an Incremental Merkle Tree which stores the members of the groups at the leaves.
To use Semaphore, users first create a Semaphore Identity offchain. A Semaphore identity is represented by three uint256 values: a nullifier, trapdoor and commitment. You can think of the nullifier and trapdoor as being the user’s private key and the commitment as its corresponding public key. When a user joins a group, their commitment is stored in a leaf node of the group’s Merkle tree.
So where does the privacy come in? To prove their membership in a group without revealing their identity, users call Semaphore’s verifyProof function and pass in a zero-knowledge proof (as a zkSNARK) that they belong to the group. Semaphore then verifies the proof, returning true if the proof is valid and false otherwise.
At a high level, the proof asserts that the user has the nullifier and trapdoor corresponding to a commitment in the tree and that the user knows the path from the Merkle root to the leaf node storing the commitment. The nullifier, trapdoor, commitment, and Merkle tree path are all private inputs in the proof, which means they cannot be revealed to anyone.
Bugs!!
With this background in place, let’s look at the bugs we found and how contract invariants were useful!
Bug 1: Check your commitment is in the field!
When we started our Semaphore audit, one of the first contract invariants we wrote down was the following:
For each group, every commitment in the group must be smaller than the zkSNARK field size used to generate membership proofs.
To give a bit more context, a zkSNARK proof is a polynomial commitment over a prime field, so the values used to generate a valid proof must also lie within the prime field. As the Semaphore commitment is one such value used to generate the proof, it should also be within the field. Semaphore’s proving scheme uses the bn128 curve whose field order is less than the maximum uint256 value. The tricky part here is that commitments are represented as uint256 values, and so the protocol must make sure that no commitment larger than the field size can get added to the tree; otherwise, that member will not be able to prove their membership or broadcast information anonymously.
Once we identified this invariant, the bug finding process became much more directed. We first found all functions which modify the Merkle tree and checked if they added the appropriate checks. Very quickly, we found a missing check in the update function, which allows users to change their commitment in the tree. If we look at the implementation below, we see that the only input that is checked is the current leaf via a call to verify. The newLeaf is not checked and so it can be larger than the prime field!
/// @dev Updates a leaf in the tree.
/// @param self: Tree data.
/// @param leaf: Leaf to be updated.
/// @param newLeaf: New leaf.
/// @param proofSiblings: Array of the sibling nodes of the proof of membership.
/// @param proofPathIndices: Path of the proof of membership.
function update(
IncrementalTreeData storage self,
uint256 leaf,
uint256 newLeaf,
uint256[] calldata proofSiblings,
uint8[] calldata proofPathIndices
) public {
require(
verify(self, leaf, proofSiblings, proofPathIndices),
"IncrementalBinaryTree: leaf is not part of the tree"
);
uint256 depth = self.depth;
uint256 hash = newLeaf;
uint256 updateIndex;
for (uint8 i = 0; i < depth; ) {
updateIndex |= uint256(proofPathIndices[i] & 1) << uint256(i);
...
unchecked {
++i;
}
}
require(updateIndex < self.numberOfLeaves, "IncrementalBinaryTree: leaf index out of range");
}After notifying the developers of this issue they quickly fixed it by including an additional require statement as seen below:
function update(
IncrementalTreeData storage self,
uint256 leaf,
uint256 newLeaf,
uint256[] calldata proofSiblings,
uint8[] calldata proofPathIndices
) public {
require(newLeaf < SNARK_SCALAR_FIELD, "IncrementalBinaryTree: new leaf must be < SNARK_SCALAR_FIELD");
require(
verify(self, leaf, proofSiblings, proofPathIndices),
"IncrementalBinaryTree: leaf is not part of the tree"
);
...
}Consequences. This bug has two interesting consequences. As we mentioned previously, if a user’s commitment is larger than the SNARK field size, then they won’t be able to anonymously prove membership in the group as the inputs to a zk proof must be elements of the field. Second, if a commitment in the tree is larger than the SNARK field size, then that node can never be updated or removed. Prior to removing/updating a node, Semaphore first checks that the leaf node is valid by calling verify on it. As you can see below, verify will revert if the leaf is greater than or equal to the SNARK field size.
function verify(
IncrementalTreeData storage self,
uint256 leaf,
uint256[] calldata proofSiblings,
uint8[] calldata proofPathIndices
) private view returns (bool) {
require(leaf < SNARK_SCALAR_FIELD, "IncrementalBinaryTree: leaf must be < SNARK_SCALAR_FIELD");
uint256 depth = self.depth;
require(
proofPathIndices.length == depth && proofSiblings.length == depth,
"IncrementalBinaryTree: length of path is not correct"
);
uint256 hash = leaf;
for (uint8 i = 0; i < depth; ) {
require(
proofSiblings[i] < SNARK_SCALAR_FIELD,
"IncrementalBinaryTree: sibling node must be < SNARK_SCALAR_FIELD"
);
...
}
...
}Bug 2: Who is in the group?
During our audit, we also wrote contract invariants over the Incremental Merkle Tree data structure which represents a Semaphore Group. Unlike a standard Merkle Tree, which is static, the contents an Incremental Merkle Tree can be updated, meaning that members can be added, removed or changed. Because an Incremental Merkle Tree must be a complete binary tree, the implementation uses a so-called zero value to indicate that a leaf node is empty.
One of the invariants we wrote for the Incremental Merkle Tree is:
Any member of a group can be removed.
To determine if this invariant holds, we first tried to formalize what it means to be a member of a group. One possibility is to consider “any identifier that is added to a group’s Incremental Merkle Tree after its creation” to be a member. However, another possibility is to define member to be “any identifier that can verify they are included in the group’s tree”.
While these definitions should intuitively refer to the same set of accounts, we noticed that they were actually slightly different. There is one account that may not have been explicitly added to the tree but can verify its membership: the identity corresponding to the zero value!
To see why, let’s first consider how the zero value is set. The following code allows a user of the Semaphore protocol to create a group. To do so, they just have to specify the tree’s depth and zero value. It is therefore possible for this creator to specify a value they control i.e, for which they have a nullifier and trapdoor.
/// @dev Creates a new group by initializing the associated tree.
/// @param groupId: Id of the group.
/// @param merkleTreeDepth: Depth of the tree.
/// @param zeroValue: Zero value of the tree.
function _createGroup(
uint256 groupId,
uint256 merkleTreeDepth,
uint256 zeroValue
) internal virtual {
if (getMerkleTreeDepth(groupId) != 0) {
revert Semaphore__GroupAlreadyExists();
}
merkleTree[groupId].init(merkleTreeDepth, zeroValue);
emit GroupCreated(groupId, merkleTreeDepth, zeroValue);
}Now let’s determine if Semaphore strictly disallows the proofs where the indicated leaf is the zero value. To do so, Semaphore would have to perform such validation in their ZK Circuit shown below. Doing so, however, would require that the circuit have knowledge of the zero value as the member’s identity is not included in the proof that is validated on-chain. Since this value is not provided to the circuit, it must not (and does not) perform any such validation.
// nLevels must be < 32.
template Semaphore(nLevels) {
signal input identityNullifier;
signal input identityTrapdoor;
signal input treePathIndices[nLevels];
signal input treeSiblings[nLevels];
signal input signalHash;
signal input externalNullifier;
signal output root;
signal output nullifierHash;
...
}
component main {public [signalHash, externalNullifier]} = Semaphore(20);At this point we’ve established that the zero value can be controlled by a user and it can be used to verify a proof of membership. As such, we can consider it to be an implicit “member” of a group! This member is special though in that it cannot be easily removed from the group since a removal simply replaces the value of the indicated leaf with the zero value as shown below.
function remove(
IncrementalTreeData storage self,
uint256 leaf,
uint256[] calldata proofSiblings,
uint8[] calldata proofPathIndices
) public {
update(self, leaf, self.zeroes[0], proofSiblings, proofPathIndices);
}Consequences. Since this value cannot be removed, it provides (almost) guaranteed access to the group. While other users such as an admin have similar unrestricted access, there are situations under which the admin and the creator may not correspond to the same entity. For example, if the group were managed via a DAO, the contract deployer could ensure their access without an admin’s approval. In addition, since this value is not explicitly added to the group and the identity of a committed proof is not exposed publicly, it would be difficult to determine if it was used to prove group membership.
The Fix. There are two possible ways to fix this issue. One is to specifically disallow a membership proof where the identity corresponds to the zero value. Doing so, however, would require modifications to the ZK-Circuit. The second option is to take away a user’s ability to specify such a value. Doing so isn’t as strong since someone may still discover a way to use the zero value to prove their membership; however, that would require finding a cryptographic hash function collision. Since this is extremely unlikely and required fewer modifications, the Semaphore developers opted to disallow users from setting the zero value as shown below.
/// @dev Creates a new group by initializing the associated tree.
/// @param groupId: Id of the group.
/// @param merkleTreeDepth: Depth of the tree.
function _createGroup(uint256 groupId, uint256 merkleTreeDepth) internal virtual {
if (getMerkleTreeDepth(groupId) != 0) {
revert Semaphore__GroupAlreadyExists();
}
// The zeroValue is in fact an implicit member of the group.
// Although there is a remote possibility that the preimage of
// the hash may be calculated, using this value minimizes the risk.
uint256 zeroValue = uint256(keccak256(abi.encodePacked(groupId))) >> 8;
merkleTree[groupId].init(merkleTreeDepth, zeroValue);
emit GroupCreated(groupId, merkleTreeDepth, zeroValue);
}Parting Thoughts
In short, we find it really helpful to write down contract invariants during our audits here at Veridise. It makes the bug finding process much more directed and ultimately gives us a better idea of what the contract is intending to do. However, this isn’t the whole story: even after specifying the contract invariant, it can be very challenging to manually look through the contract to find violations of the contract invariant, as this requires reasoning about the whole contract and its potential interactions with other contracts. That’s why we are actively developing tools to automatically find such bugs given a high level specification like our contract invariants above.
If you want to learn more, feel free to check out the our full Semaphore audit report and stay tuned for our upcoming blog post where we show how these bugs can be found automatically using Orca, our smart contract fuzzer!
Acknowledgements
We would like to thank the developers of Semaphore including Cedoor and Andy Guzman for their support, insights, and promptly addressing all our questions and fixing the bugs we found during the audit.
About Veridise
Veridise is a blockchain security company that provides audits and software analysis tools for all layers of the blockchain ecosystem, including smart contracts, web3 applications, zero-knowledge circuits, and blockchain implementations. Co-founded by a team of formal verification and software security researchers, Veridise provides state-of-the-art tooling for hardening blockchain security. Our clients can work with us in a variety of ways, including hiring us for security audits, using our automated security analysis tools (for testing, static analysis, formal verification), or a combination of these.
If you’re interested in learning more information, please consider following us on social media or visiting our website:
Website | Twitter | Facebook | LinkedIn | Github | Request Audit
