Scribble Exercise 4

In this exercise we're going to have a look at a vulnerable initializable smart contract. We'll use Scribble to annotate and find a bug in the initialisation logic!

Handy Links

Scribble Repository -> https://github.com/ConsenSys/Scribble

Mythril Repository -> https://github.com/ConsenSys/Mythril

Scribble Docs 📚 -> https://docs.scribble.codes/

MythX Dashboard -> https://dashboard.mythx.io

Installation

# We'll need the mythx-cli client:
pip3 install mythx-cli

# Make sure to use node 12-14
npm install eth-scribble --global

Also you will need a developer MythX account and the associated API key.

Setting up the target

git clone git@github.com:ConsenSys/scribble-4.git
cd scribble-exercise-4

Finding the vulnerability

The "bug" in this exercise is very straightforward. It shows you how you can use global if_succeeds annotations to describe valid state transitions.

Global if succeeds annotations are great as they allow us to specify this on the contract level. This means that we won't have to go into every function, of every contract inheriting from initializable to make sure the property holds. Scribble will do it for us!

The vulnerability in this example is the Example contract which "unintentionally" violates the propety of singular initialisation.

 contract Example is Initializable {
    function accidentalUninitialisation() {
        initialized = false;
    }
}

Adding annotations

Now we can add a thre annotations that will ensure that Initializable, and all contracts inheriting from it are correct.

The first annotation is a global if_succeeds property which will ensure that initialized remains true once the contract is initialized.

/// #if_succeeds old(initialized) ==> initialized;
contract Initializable {
    ...
}

The second and third annotation will ensure that initialize is only called whenever initialised is false, and that initialized is true afterwards.

    /// #if_succeeds !old(initialized);
    /// #if_succeeds initialized;
    function initialize() public {

Together these three properties ensure that initialize() can only be called once.