Using automatic analysis tools with MakerDAO contracts (original) (raw)

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.