Using automatic analysis tools with MakerDAO contracts

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 Zeppelin 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 Zeppelin article first :slight_smile:

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:

  1. Manticore: Ran out of memory quickly.

  2. Oyente: Reports that the assert can throw, but to make sure that it isn’t a false positive, we added require(wad == 0) in lock and it reports the same issue, so we assume it’s a false positive.

  3. 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.

  1. Echidna: Replaced the assert with an echidna property similar to what I did for Securify, and the tool couldn’t find the issue.

  2. 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.

  3. Pakala: Again replaced the assert with a msg.sender.transfer(address(this).balance), but we were still unsuccessful.

  4. Mythril: Only false positives.

  5. MythX: Still unsuccessful.

  6. 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.

18 Likes

Thanks for trying out our tools, Echidna and Manticore! This is a great example for why we make our tools flexible. It was a fun challenge to test our tools and see if they could discover this bug. Identifying minimal examples of failure helps us improve them. I’m also glad we’re finally talking about reachability; not reentrancy or other trivial "bug classes.”

The Bug in DSChief

Let’s start by explaining why this bug is difficult for automated tools to find.

There are many sequences of transactions to falsify the invariant, however, they all share a specific call to voteSlate with a hashed address. Instead of using the original SimpleDSChief contract, take a look at the following code:

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 echidna_checkAnInvariant() public returns (bool) {
        return !everMatched;
    }
}

That’s the simplified “essence” of the bug: using a hash as an argument. You need to find two values, such that the first one is the hash of the second.

Fuzzer mode

Is this bug fuzzable? If exploring a codepath requires a specific 256-bit value that depends on an earlier input, then it’s kind of obvious that a fuzzer will be ill-suited to overcome it. There is good discussion of these “gates” in our 2016 presentation about the DARPA CGC.

You can modify the code so it’s more amenable to fuzzing. If you’re testing a conventional target, then you would NOP out magic number checks so AFL can overcome them, or you would directly target a specific function with libFuzzer. BoringSSL’s “fuzzer mode” is a great example. You have to figure out how to plumb your fuzzer into the logic of the program to use a fuzzer effectively.

Luckily, that’s not too hard with Echidna because it’s usually just a little bit of extra Solidity to help it overcome these “gates” in the program and reach more states.

DSChief with “fuzzer mode”

As an example of that approach, here is an Echidna script that detects the vulnerability. It includes a new function called voteSlate_using_address. Echidna calls this function during the fuzzing campaign to execute proper calls to voteSlates. This makes it possible to randomly generate valid values that represent hashed addresses:

function voteSlate_using_address(address yay) public {
    voteSlate(keccak256(abi.encodePacked(yay)));
}

Echidna can detect the bug once you provide it with this helper function:

$ echidna-test SimpleDSChief.sol --config SimpleDSChief.yaml 
...
Analyzing contract: ds.sol:SimpleDSChief
echidna_checkAnInvariant: failed!💥  
  Call sequence:
    lock(191561942608236107294793378393788647952342390272950272)
    voteSlate_using_address(42)
    etch(42)

This is an example of a pattern that a lot of automated tools have problems with. However, they are problems that a smart engineer doing a deliberate audit could work around.

Automating a solution

We’re talking about tools that produce transactions. To find this bug, you have to produce a transaction with a constant that is calculated by hashing another input. This is a fun example of the boundaries of automated reasoning. However, we realized you don’t need to get lost in the hashing or calculations happening here: it’s just the output of an earlier call.

You’re supposed to use this API to make calls that give you back a value, that you then use again later. This pattern occurs frequently enough that we can automate it out of existence. It’s not difficult, it’s just a case we hadn’t thought about yet (except Gustavo, who was inspired to consider this feature a year ago). I’m happy to report that Echidna is just going to find tricky bugs like this by default now.

Echidna now mines constants from return values

For Echidna, we added constant mining to extract return values. Echidna is now capable of finding bugs of this type without assistance. Here it is running on the original code sample:

$ echidna-test SimpleDSChief.sol 
...
Analyzing contract: SimpleDSChief.sol:SimpleDSChief
echidna_checkAnInvariant: failed!💥  
  Call sequence:
    lock(25503647802596573024641331103917583752275218414108811802173174404990563651242)
 voteSlate("\148\187\n\149v\237H~\222\158\135\162\133c\200\241\234\128\&1m\185\156N\134Q\241\ACK\228\SOH\128\134\255")
    etch(fcc4f2a007b6393c0b73cb690089d48c33842a39)

We’re excited to take this Echidna capability out for a spin and find new bugs with it.

Key Takeaways

We enjoyed this opportunity to stress and improve our tools! This conversation is proceeding in the right direction: we should focus on reachability of codepaths. I’m glad we built our tools so we can easily add new strategies that enhance their coverage.

This also demonstrates why SaaS services for bug discovery are a necessary but insufficient solution for securing your code. It’s easy to write programs that are unintentionally hard to test. Your code probably has “gates” exactly like this bug. You still need an expert to effectively apply testing techniques in context with your codebase.

Finally, this shows that smart contract program analysis is not conventional program analysis. AFL and KLEE would never solve a problem like this one. Unlike regular programs that you give some bytes and they segfault or don’t, smart contracts make sequential atomic transactions. They don’t crash, they just get into a bad state. We can get richer results by building knowledge of the transaction model into our testing tools. In this case, we found an inter-transaction relationship and enhanced our model to move information from the execution of one transaction into the generation of another.

Epilogue: Manticore

We’re pleased that our symbolic execution engine correctly executes the transaction trace of the exploit. We were able to debug the exploit in Manticore’s concrete mode, verifying it is indeed a problem. This is a great result. It demonstrates that we have a correct model of the EVM in Manticore, and this fidelity lets us execute transactions if we know what they are first.

That leaves us with the question: If Manticore can execute the code perfectly given the transaction sequence, why can’t it generate the transaction sequence on its own? We don’t want to just execute the transactions. We want to synthesize them from thin air. The answer is, again, domain knowledge.

The Z3 solver, which Manticore depends on, knows nothing about hashes out-of-the-box. It needs rules, some might say a “theory,” of how hashes work that it can mix into its regular behavior. People use hashes in the real world so we have added rules to Manticore that reason about them. These let us solve many problems that include hashes, however, we don’t have a “comprehensive theory” of one-way functions to rely on.

This bug exposed a need for an evolution in our current strategy for hashes. It is far from game-over. We need to add a rule that we don’t have right now. We know what the rule is, it makes sense, and we’re going to add it. We’ll explain further in the next post to this thread, and you’ll see this enhanced domain knowledge in the next release of Manticore.

Authors of this post include: Gustavo Grieco, JP Smith, Alex Groce, Felipe Manzano, Ryan Stortz, Jay Little, and Dan Guido.

9 Likes

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

Hi Dan. I’m sorry for such a late response.

I’ve really enjoyed the answer to our post. Thanks you and the other guys for putting together such a clear explanation about your tools and for conceptualizing some of the challenges arising in the example that Vera had presented.

I agree with you: reachability properties are much more interesting! :-). Also about the fact that push-button tools or services may fail short in some cases… We advocate for combined “human intelligence + machine power” approach. A good and adaptable set of tools used wisely can make auditors much more effective in their tasks, but auditors are still the ones driving the whole process!

Thanks a lot for your post and we look forward to keeping talking about tools, their underlying techniques and the challenges of auditing software relying on tools.

5 Likes