Using automatic analysis tools with MakerDAO contracts

Security
3

Hi there !

I’m the developer of Pakala and I took a look at its behavior running your example.

First of all, its model of the EVM is pretty limited compared to Mythril or Manticore. This is to keep it simple and because I don’t have the resource, or see the point in making another tool like the two I just mentioned.

Your original contract is too complex and my analysis is too unoptimized for it to lead interesting results, because it has to simulate a pretty long chain of transactions. That’s why it was unsuccessful, but maybe it could work if you would wait long enough.

However, unlike the others, Pakala is currently able to flag the same bug in the simplified contract Dan mentionned above: (slightly modified so the contract kills itself):

contract ReturnMemory {
    mapping(bytes32=>address) public slates;
    bool everMatched = false;

    function etch(address yay) public returns (bytes32 slate) {
        bytes32 hash = keccak256(abi.encodePacked(yay));
        slates[hash] = yay;
        return hash;
    }

    function lookup(bytes32 slate, address nay) public {
    if (nay != address(0x0)) {
        everMatched = slates[slate] == nay;
    }
    }
    
    function selfdestruct_if_invariant_broken() public returns (bool) {
        if(everMatched) selfdestruct(msg.sender);
    }
}

You can run it this way:

solc --bin-runtime test.sol | tail -n 1 | pakala -

And it will find the etch->lookup->selfdestruct sequence.

As Dan said, Z3 needs to be taught about hashes, and that’s non-trivial. However I have a wrapper around Z3 that is able to handle most of these simple cases.

It works by noticing that:

  • if “keccak(a) == keccak(b)” must be true, then “a == b” must also be true
  • if “keccak(a) != keccak(b)” must be true, then “a != b” must also be true.
    This way we can add supplemental constraint on hash inputs, and do that recursively, which can often constrain the hash input enough so that there is a single solution.
    When the input only has a single solution, we can compute the concrete hash value.

So here, we want a storage key equality: “keccak(keccak(yay)) == keccak(slate)”.
As per above, “keccak(yay) == slate” must be true.
Because there are still multiple possibilities for yay, we arbitrarily constraint it to 1 (for example). Then slate must be equal to keccak(1). And we have our solution. This is basically what Pakala does.

Also I found a minor bug in the way I handled hashes because I wasn’t concretizing dependent hash first. I published the fix. Before it, it would work but find a longer transaction chain.

6 Likes