State Machine Testing with Echidna

Property-based testing is a powerful technique for verifying arbitrary properties of a program via execution on a large set of inputs, typically generated stochastically. Echidna is a library and executable I’ve been working on for applying property-based testing to EVM code (particularly code written in Solidity).

Echidna is a library for generating random sequences of calls against a given smart contract’s ABI and making sure that their evaluation preserves some user-defined invariants (e.g.: the balance in this wallet must never go down). If you’re from a more conventional security background, you can think of it as a fuzzer, with the caveat that it looks for user-specified logic bugs rather than crashes (as programs written for the EVM don’t “crash” in any conventional way).

The property-based testing functionality in Echidna is implemented with Hedgehog, a property-based testing library by Jacob Stanley. Think of Hedgehog as a nicer version of QuickCheck. It’s an extremely powerful library, providing automatic minimal testcase generation (“shrinking”), well-designed abstractions for things like ranges, and most importantly for this blog post, abstract state machine testing tools.

After reading a particularly excellent blog post by Tim Humphries (“State machine testing with Hedgehog,” which I’ll refer to as the “Hedgehog post” from now on) about testing a simple state machine with this functionality, I was curious if the same techniques could be extended to the EVM. Many contracts I see in the wild are just implementations of some textbook state machine, and the ability to write tests against that invariant-rich representation would be invaluable.

The rest of this blog post assumes at least a degree of familiarity with Hedgehog’s state machine testing functionality. If you’re unfamiliar with the software, I’d recommend reading Humphries’s blog post first. It’s also worth noting that the below code demonstrates advanced usage of Echidna’s API, and you can also use it to test code without writing a line of Haskell.

First, we’ll describe our state machine’s states, then its transitions, and once we’ve done that we’ll use it to actually find some bugs in contracts implementing it. If you’d like to follow along on your own, all the Haskell code is in examples/state-machine and all the Solidity code is in solidity/turnstile.

Step 0: Build the model

Fig. 1: A turnstile state machine

The state machine in the Hedgehog post is a turnstile with two states (locked and unlocked) and two actions (inserting a coin and pushing the turnstile), with “locked” as its initial state. We can copy this code verbatim.

data ModelState (v :: * -> *) = TLocked                              | TUnlocked                              deriving (Eq, Ord, Show)initialState :: ModelState vinitialState = TLocked

However, in the Hedgehog post the effectful implementation of this abstract model was a mutable variable that required I/O to access. We can instead use a simple Solidity program.

contract Turnstile {  bool private locked = true; // initial state is locked  function coin() {    locked = false;  }  function push() returns (bool) {    if (locked) {      return(false);    } else {      locked = true;      return(true);    }  }}

At this point, we have an abstract model that just describes the states, not the transitions, and some Solidity code we claim implements a state machine. In order to test it, we still have to describe this machine’s transitions and invariants.

Step 1: Write some commands

To write these tests, we need to make explicit how we can execute the implementation of our model. The examples given in the Hedgehog post work in any MonadIO, as they deal with IORefs. However, since EVM execution is deterministic, we can work instead in any MonadState VM.

The simplest command is inserting a coin. This should always result in the turnstile being unlocked.

s_coin :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelStates_coin = Command (\_ -> Just $ pure Coin)                 -- Regardless of initial state, we can always insert a coin  (\Coin -> cleanUp >> execCall ("coin", []))  -- Inserting a coin is just calling coin() in the contract  -- We need cleanUp to chain multiple calls together  [ Update $ \_ Coin _ -> TUnlocked    -- Inserting a coin sets the state to unlocked  , Ensure $ \_ s Coin _ -> s === TUnlocked    -- After inserting a coin, the state should be unlocked  ]

Since the push function in our implementation returns a boolean value we care about (whether or not pushing “worked”), we need a way to parse EVM output. execCall has type MonadState VM => SolCall -> m VMResult, so we need a way to check whether a given VMResult is true, false, or something else entirely. This turns out to be pretty trivial.

match :: VMResult -> Bool -> Boolmatch (VMSuccess (B s)) b = s == encodeAbiValue (AbiBool b)match _ _ = False

Now that we can check the results of pushing, we have everything we need to write the rest of the model. As before, we’ll write two Commands; modeling pushing while the turnstile is locked and unlocked, respectively. Pushing while locked should succeed, and result in the turnstile becoming locked. Pushing while unlocked should fail, and leave the turnstile locked.

s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelStates_push_locked = Command (\s -> if s == TLocked then Just $ pure Push else Nothing)                        -- We can only run this command when the turnstile is locked  (\Push -> cleanUp >> execCall ("push", []))  -- Pushing is just calling push()  [ Require $ \s Push -> s == TLocked    -- Before we push, the turnstile should be locked  , Update $ \_ Push _ -> TLocked    -- After we push, the turnstile should be locked  , Ensure $ \before after Push b -> do before === TLocked                                        -- As before                                        assert (match b False)                                        -- Pushing should fail                                        after === TLocked                                        -- As before  ]
s_push_unlocked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelStates_push_unlocked = Command (\s -> if s == TUnlocked then Just $ pure Push else Nothing)                          -- We can only run this command when the turnstile is unlocked  (\Push -> cleanUp >> execCall ("push", []))  -- Pushing is just calling push()  [ Require $ \s Push -> s == TUnlocked    -- Before we push, the turnstile should be unlocked  , Update $ \_ Push _ -> TLocked    -- After we push, the turnstile should be locked  , Ensure $ \before after Push b -> do before === TUnlocked                                        -- As before                                        assert (match b True)                                        -- Pushing should succeed                                        after === TLocked                                        -- As before  ]

If you can recall the image from Step 0, you can think of the states we enumerated there as the shapes and the transitions we wrote here as the arrows. Our arrows are also equipped with some rigid invariants about the conditions that must be satisfied to make each state transition (that’s our Ensure above). We now have a language that totally describes our state machine, and we can simply describe how its statements compose to get a Property!

Step 2: Write a property

This composition is actually fairly simple, we just tell Echidna to execute our actions sequentially, and since the invariants are captured in the actions themselves, that’s all that’s required to test! The only thing we need now is the actual subject of our testing, which, since we work in any MonadState VM, is just a VM, which we can parametrize the property on.

prop_turnstile :: VM -> propertyprop_turnstile v = property $ do  actions <- forAll $ Gen.sequential (Range.linear 1 100) initialState    [s_coin, s_push_locked, s_push_unlocked  -- Generate between 1 and 100 actions, starting with a locked (model) turnstile  evalStateT (executeSequential initialState actions) v  -- Execute them sequentially on the given VM.

You can think of the above code as a function that takes an EVM state and returns a hedgehog-checkable assertion that it implements our (haskell) state machine definition.

Step 3: Test

With this property written, we’re ready to test some Solidity! Let’s spin up ghci to check this property with Echidna.

λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile.sol" <span style="font-weight: 400;">-- set up a VM with our contract loaded</span>λ> check $ prop_turnstile v <span style="font-weight: 400;">-- check that the property we just defined holds</span>  ✓ passed 10000 tests.Trueλ>

It works! The Solidity we wrote implements our model of the turnstile state machine. Echidna evaluated 10,000 random call sequences without finding anything wrong.

Now, let’s find some failures. Suppose we initialize the contract with the turnstile unlocked, as below. This should be a pretty easy failure to detect, since it’s now possible to push successfully without putting a coin in first.

We can just slightly modify our initial contract as below:

contract Turnstile {  bool private locked = false; // initial state is unlocked  function coin() {    locked = false;  }  function push() returns (bool) {    if (locked) {      return(false);    } else {      locked = true;      return(true);    }  }}

And now we can use the exact same ghci commands as before:

λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile_badinit.sol" λ> check $ prop_turnstile v  ✗ failed after 1 test.       ┏━━ examples/state-machine/StateMachine.hs ━━━    49 ┃ s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState    50 ┃ s_push_locked = Command (\s -> if s == TLocked then Just $ pure Push else Nothing)    51 ┃   (\Push -> cleanUp >> execCall ("push", []))    52 ┃   [ Require $ \s Push -> s == TLocked    53 ┃   , Update $ \_ Push _ -> TLocked    54 ┃   , Ensure $ \before after Push b -> do before === TLocked    55 ┃                                         assert (match b False)       ┃                                         ^^^^^^^^^^^^^^^^^^^^^^    56 ┃                                         after === TLocked    57 ┃ ]       ┏━━ examples/state-machine/StateMachine.hs ━━━    69 ┃ prop_turnstile :: VM -> property    70 ┃ prop_turnstile v = property $ do    71 ┃   actions <- forAll $ Gen.sequential (Range.linear 1 100) initialState 72 ┃ [s_coin, s_push_locked, s_push_unlocked] ┃ │ Var 0 = Push 73 ┃ evalStateT (executeSequential initialState actions) v This failure can be reproduced by running: > recheck (Size 0) (Seed 3606927596287211471 (-1511786221238791673))Falseλ>

As we’d expect, our property isn’t satisfied. The first time we push it should fail, as the model thinks the turnstile is locked, but it actually succeeds. This is exactly the result we expected above!

We can try the same thing with some other buggy contracts as well. Consider the below Turnstile, which doesn’t lock after a successful push.

contract Turnstile {  bool private locked = true; // initial state is locked  function coin() {    locked = false;  }  function push() returns (bool) {    if (locked) {      return(false);    } else {      return(true);    }  }}

Let’s use those same ghci commands one more time

λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile_nolock.sol" λ> check $ prop_turnstile v  ✗ failed after 4 tests and 1 shrink.       ┏━━ examples/state-machine/StateMachine.hs ━━━    49 ┃ s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState    50 ┃ s_push_locked = Command (\s -> if s == TLocked then Just $ pure Push else Nothing)    51 ┃   (\Push -> cleanUp >> execCall ("push", []))    52 ┃   [ Require $ \s Push -> s == TLocked    53 ┃   , Update $ \_ Push _ -> TLocked    54 ┃   , Ensure $ \before after Push b -> do before === TLocked    55 ┃                                         assert (match b False)       ┃                                         ^^^^^^^^^^^^^^^^^^^^^^    56 ┃                                         after === TLocked    57 ┃  ]       ┏━━ examples/state-machine/StateMachine.hs ━━━    69 ┃ prop_turnstile :: VM -> property    70 ┃ prop_turnstile v = property $ do    72 ┃   [s_coin, s_push_locked, s_push_unlocked]       ┃   │ Var 0 = Coin       ┃   │ Var 1 = Push       ┃   │ Var 3 = Push    73 ┃   evalStateT (executeSequential initialState actions) v    This failure can be reproduced by running:    > recheck (Size 3) (Seed 133816964769084861 (-8105329698605641335))Falseλ>

When we insert a coin then push twice, the second should fail. Instead, it succeeds. Note that in all these failures, Echidna finds the minimal sequence of actions that demonstrates the failing behavior. This is because of Hedgehog’s shrinking features, which provide this behavior by default.

More broadly, we now have a tool that will accept arbitrary contracts (that implement the push/coin ABI), check whether they implement our specified state machine correctly, and return either a minimal falsifying counterexample if they do not. As a Solidity developer working on a turnstile contract, I can run this on every commit and get a simple explanation of any regression that occurs.

Concluding Notes

Hopefully the above presents a motivating example for testing with Echidna. We wrote a simple description of a state machine, then tested four different contracts against it; each case yielded either a minimal proof the contract did not implement the machine or a statement of assurance that it did.

If you’d like to try implementing this kind of testing yourself on a canal lock, use this exercise we wrote for a workshop.



*** This is a Security Bloggers Network syndicated blog from Trail of Bits Blog authored by JP Smith. Read the original post at: https://blog.trailofbits.com/2018/05/03/state-machine-testing-with-echidna/