Catching weird security bugs in Solidity smart contracts with global invariant checks
Contract invariants are properties of the program program state that are expected to always hold true. In my previous article I discussed the use of Solidity assertions to check contract invariants. This article expands on the use of invariants and provides a couple of additional examples.
An interesting property of invariant checking on the bytecode level is that it allows you to detect low-level issues, including issues caused by compiler optimisation or idiosyncrasies of the programming language, from high-level rules. For instance, in the last article we saw that the invariant “the contract should always remain unlocked” could be broken by exploiting Solidity storage addressing. Let’s look at some more examples.
Example 1: Integer rounding
Integer divisions in Solidity round down to the nearest integer. Failure to consider this rounding behaviour can lead to bugs and vulnerabilities. Consider the example from Sigma Prime’s blog post which also has a great writeup on this bug class:
pragma solidity ^0.5.0;contract FunWithNumbers {
uint constant public tokensPerEth = 10;
uint constant public weiPerEth = 1e18;
mapping(address => uint) public balances;function buyTokens() public payable {
uint tokens = msg.value/weiPerEth*tokensPerEth; // convert wei to eth, then multiply by token rate
balances[msg.sender] += tokens;
}function sellTokens(uint tokens) public {
require(balances[msg.sender] >= tokens);
uint eth = tokens/tokensPerEth;
balances[msg.sender] -= tokens;
msg.sender.transfer(eth*weiPerEth);
}
}
Let’s put on the auditor’s hat and come up with some meaningful properties to check. Amongst other things we could assert that, when comparing the contract account state at the beginning and end of a transaction, the following should always be true:
- The token balance of msg.sender increases when the contract account balance increases;
- The contract account balance increases when the token balance of msg.sender increases;
- The token balance of msg.sender decreases when the contract account balance decreases;
- The contract account balance decreases when the token balance of msg.sender decreases.
This could be generalised even more (e.g. the sum of all token balances increases if and only if the contract balance increases) and supplemented with additional checks (balance always increases by the right amount, …) to catch more possible bugs.
MythX supports standard Solidity assertions and the MythX AssertionFailed event which allows you to add a custom error message. One way of checking contract invariants is by creating a modifier to wrap all public and external functions. This ensures that the invariant holds at the end of all internal message calls and transactions. This approach has some limitations but let’s roll with it for now (support for inline specifications is coming to MythX soon™).
Typically we’ll create a modifier along the following lines:
modifier checkInvariants { // Save old state uint sender_balance_old = balances[msg.sender]; // Execute the function body
_; // MythX AssertionFailed event if (--- this should never occur ---) {
emit AssertionFailed("Some error message");
} // Solidity assertion assert(--- this should always hold ---);
}
We’ll add the checks by creating a wrapper contract and overriding the public functions in FunWithNumbers:
contract VerifyFunWithNumbers is FunWithNumbers {
uint contract_balance_old;
constructor() public {
contract_balance_old = address(this).balance;
}
event AssertionFailed(string message);
modifier checkInvariants {
uint sender_balance_old = balances[msg.sender];
_;
if (address(this).balance > contract_balance_old && balances[msg.sender] <= sender_balance_old) {
emit AssertionFailed("Invariant violation: Sender token balance must increase when contract account balance increases");
}
if (balances[msg.sender] > sender_balance_old && contract_balance_old >= address(this).balance) {
emit AssertionFailed("Invariant violation: Contract account balance must increase when sender token balance increases");
}
if (address(this).balance < contract_balance_old && balances[msg.sender] >= sender_balance_old) {
emit AssertionFailed("Invariant violation: Sender token balance must decrease when contract account balance decreases");
}
if (balances[msg.sender] < sender_balance_old && address(this).balance >= contract_balance_old) {
emit AssertionFailed("Invariant violation: Contract account balance must decrease when sender token balance decreases");
}
contract_balance_old = address(this).balance;
}function buyTokens() public payable checkInvariants {
super.buyTokens();
}
function sellTokens(uint tokens) public checkInvariants {
super.sellTokens(tokens);
}
}
Running this contract through the MythX Remix plugin detects two invariant violations. Let’s have a closer look at the reported issues.
The first counterexample produced by MythX shows a user attempting to buy tokens with a very low call value of 6 Wei. In this case, the 6 Wei get added to the contract balance but the balance of the user does not increase.
Taking another look at the code, we can see that if less than 1 Ether is sent when calling buyTokens(), the result of the division msg.value/weiPerEth will be rounded down to 0 and the subsequent multiplication with tokensPerEth will likewise return 0.
The second counterexample shows a user first buying one Ether (1000000000000000000 Wei) worth of tokens (transaction 2), then selling 6 tokens (transaction 3). This deducts 6 tokens from the user’s balance but does not transfer any Ether to the user due to the rounding error in sellTokens(uint tokens) : uint eth = tokens/tokensPerEth will be rounded down to 0 if tokens is lower than 10 or to the nearest multiple of 10 otherwise.
Example 2: Arbitrary storage writes via large-sized arrays
A couple of years ago I wrote about proving security properties using the open-source tool Mythril. By checking contract invariants with MythX you can achieve similar results. It is however important to point out the difference between the two methods:
- The method shown previously was based on under-constrained symbolic execution of the runtime bytecode (using an older version of Mythril) whereby storage variables were initialised as symbolic variables. This method detects all instances of a bug but also returns false positives.
- MythX combines symbolic execution and input fuzzing after partially initialising the contract account state with the concrete values. By doing this it avoids false positives but there’s a residual risk of false negatives. The risk of missing bugs declines the longer the tools are allowed to run.
With that said, let’s revisit the example shown in the old article which was based on Doug Hoyte’s classic USCC submission. This smart contract contains a hidden method of overwriting the owner state variable:
pragma solidity ^0.5.0;contract Pwnable {
address public owner;
uint[] private bonusCodes;
constructor() public {
bonusCodes = new uint[](0);
owner = msg.sender;
}
function PushBonusCode(uint c) public {
bonusCodes.push(c);
}
function PopBonusCode() public {
require(0 <= bonusCodes.length);
bonusCodes.length--;
}
function UpdateBonusCodeAt(uint idx, uint c) public {
require(idx < bonusCodes.length);
bonusCodes[idx] = c;
}
}
To catch improper modifications of the owner variable we can informally define the property:
- The owner must not change in the course of the transaction unless the transaction sender matches the existing owner.
Which translates to the following Solidity assertion:
assert(owner == old_owner || msg.sender == old_owner);Using the aforementioned method of creating a wrapper around the Pwnable contract, we get:
contract VerifyPwnable is Pwnable { modifier checkInvariants {
address old_owner = owner; _; assert(msg.sender == old_owner || owner == old_owner);
}
function PushBonusCode(uint c) public checkInvariants {
super.PushBonusCode(c);
} function PopBonusCode() public checkInvariants {
super.PopBonusCode();
} function UpdateBonusCodeAt(uint idx, uint c) public checkInvariants {
super.UpdateBonusCodeAt(idx, c);
}}
This time MythX detects one assert violation in the code:
Apparently there is a way to change the contract owner even though the state variable owner is not explicitly accessed anywhere in the code. This happens due to the way dynamically sized arrays are laid out in storage:
- The length of the array
uint[] bonusCodesis stored at storage slot 1; - Accessing array element
npoints to storage addresskeccak(1) + n.
The state variable owner lives at storage slot 0. To access it, one must first underflow the unsigned integer variable bonusCodes.length which happens in the first function call:
PopBonusCode()
In the second call we write to the array index that equals(MAX_UINT — keccak(1)). This will result in a write to the storage address keccak(1)+(MAX_UINT — keccak(1)) which overflows into 0:
UpdateBonusCodeAt(35707666377435648211887908874984608119992236509074197713628505308453184860938, 0)
Voila! The owner is now set to the zero address (to set it to any other address, convert it to an unsigned integer and pass it with the second argument). You can try this out with the Remix JavaScript VM or Ganache to verify that it works.
It’s worth pointing out that even without the assertion, MythX automatically detects the two individual flaws that make the owner overwrite possible. The first issue is the integer overflow caused by decreasing bonusCodes.length. Note that this is not possible anymore with solc 6.0 or higher which makes the array length read-only.
Additionally, MythX reports that a writes to an arbitrary storage location are possible following the length underflow:
TL;DR
By checking high-level invariants using symbolic execution and input fuzzing you can verify assumptions about how your code behaves. This can uncover unexpected bugs caused by peculiarities of the Solidity programming language, such as rounding errors, unsafe integer arithmetics and addressing of elements in storage.
By the way, all examples in this article can be reproduced using the free version of MythX. You should try it out!
