As I mentioned in the introductions thread, I’m doing a research internship at OpenZeppelin, working on my master’s thesis with my advisor, Diego Garbervetsky, trying to figure out how can automatic analysis tools benefit smart contract’s auditors.
Because in the past months I’ve been using artificial contracts to try out the tools, Diego suggested that we might want to simplify a real one, to avoid some of the support and scalability issues of the tools, but still get a better idea of how they perform with real life code. Considering the recent vulnerability OpenZeppelin auditors found on it, I tried them on a simplified version of the faulty MakerDAO contract.
In this post I’m going to assume everyone is familiar with the MakerDAO vulnerability, so I recommend you to take a look at the OpenZeppelin article first 
Our first simplified version only had the original logic related to voting, because that’s the main goal of the contract, and where the vulnerability is found, but we had to simplify it even further to reduce the work that had to be done to debug the tools we were trying to use, so, the contract that we used only allowed users to vote for a single option:
contract SimpleDSChief {
mapping(bytes32=>address) public slates;
mapping(address=>bytes32) public votes;
mapping(address=>uint256) public approvals;
mapping(address=>uint256) public deposits;
function lock(uint wad) public {
deposits[msg.sender] = add(deposits[msg.sender], wad);
addWeight(wad, votes[msg.sender]);
}
function free(uint wad) public {
deposits[msg.sender] = sub(deposits[msg.sender], wad);
subWeight(wad, votes[msg.sender]);
}
function voteYays(address yay) public returns (bytes32){
bytes32 slate = etch(yay);
voteSlate(slate);
return slate;
}
function etch(address yay) public returns (bytes32 slate) {
bytes32 hash = keccak256(abi.encodePacked(yay));
slates[hash] = yay;
return hash;
}
function voteSlate(bytes32 slate) public {
uint weight = deposits[msg.sender];
subWeight(weight, votes[msg.sender]);
votes[msg.sender] = slate;
addWeight(weight, votes[msg.sender]);
}
function addWeight(uint weight, bytes32 slate) internal {
address yay = slates[slate];
approvals[yay] = add(approvals[yay], weight);
}
function subWeight(uint weight, bytes32 slate) internal {
address yay = slates[slate];
approvals[yay] = sub(approvals[yay], weight);
}
function add(uint x, uint y) internal pure returns (uint z) {
require((z = x + y) >= x);
}
function sub(uint x, uint y) internal pure returns (uint z) {
require((z = x - y) <= x);
}
}
Then, the main goal was to find a way to easily express a property that represents how the voting system is supposed to work, because most tools try to find a counterexample for a property, and/or try to prove that it always holds.
The best one that I could come up with using the contract’s state variables in Solidity was this one:
function checkAnInvariant() public {
bytes32 senderSlate = votes[msg.sender];
address option = slates[senderSlate];
uint256 senderDeposit = deposits[msg.sender];
assert(approvals[option] >= senderDeposit);
}
Ideally, we would want to check that approvals[anOption] only has the sum of the valid votes for that option, but at this stage we didn’t want to further change the original contract, and without further instrumentation we don’t have a way to check that with a function inside the contract. So, in a given transaction without a specific parameter, the only mapping that we can access is votes using msg.sender, that’s why we only check that pretty weak property. I say “weak” because it can hold and approvals contain an invalid value anyways, but if it’s false there’s an issue with the votes.
After choosing that property I took all the available tools that I had and tried to run them on the simplified contract extended with checkAnInvariant(), unsuccessfully in most cases:
-
Manticore: Ran out of memory quickly.
-
Oyente: Reports that the assert can throw, but to make sure that it isn’t a false positive, we added
require(wad == 0)inlockand it reports the same issue, so we assume it’s a false positive. -
Securify: I modified the contract to check for the property like so:
function checkAnInvariant(int aParam) public { bytes32 senderSlate = votes[msg.sender]; address option = slates[senderSlate]; uint256 senderDeposit = deposits[msg.sender]; if (approvals[option] < senderDeposit) { aVar = aParam; } }
Being aVar a public state variable of the contract. I made this change because Securify checks for specific properties, and one of those is unrestricted writes. It reports the assignment as a warning, instead of a violation, so it isn’t sure that it’s possible, and it doesn’t give any further information.
-
Echidna: Replaced the assert with an echidna property similar to what I did for Securify, and the tool couldn’t find the issue.
-
Maian: Replaced the assert with a
suicide, like in Securify, because that’s what the tool searches for, and again it couldn’t find the issue. -
Pakala: Again replaced the assert with a
msg.sender.transfer(address(this).balance), but we were still unsuccessful. -
Mythril: Only false positives.
-
MythX: Still unsuccessful.
-
teEther: The process died before giving an output.
In finding this error we were luckier with VeriSol. We got a wrong trace at first (free -> checkAnInvariant), and looking more into it we realized it wasn’t properly handling uints, so we added many require(anUint >= 0) in the contract and tried again. Again, we got a trace that didn’t make much sense and we realized it wasn’t properly initializing the mappings, the votes mapping wasn’t initialized with zeros, so Diego added that into the Boogie representation of the contract that VeriSol generates. Again, we got a weird trace, and I realized it was assuming it could find a value that after being hashed would be all zero bytes. In some cases that could be an issue but in this it wasn’t, so we changed the Boogie representation again to avoid this and tried again. Finally it worked, we got: victim.lock -> victim.voteSlate -> attacker.voteYays -> victim.free. It shows the issue with the contract, even though this particular case would be very hard to exploit by an attacker, because the victim has to use the contract in a way that isn’t intended to be used, and the attacker should know which option corresponds to the hash the victim used.
After another minor change to the Boogie representation we got a different interesting trace: victim.lock -> victim.voteSlate -> victim.etch, that also shows the problem.
This is not meant to be a fair general comparison between the tools, because some of them are probably not intended to be used like this, but I thought this could give everyone an idea of the issues faced when using these tools.
