Annotating State Variables with Scribble

Since we released Scribble last December, we have been hard at work adding new features to the language and the tool itself. In this series of posts, we will look at some of the new features we’ve added. Our first post showcases state variable annotations with if_updated.

The problem

During our early usage of Scribble it became apparent that annotations of functions and contracts are nice, but are sometimes insufficient when reasoning about individual state variables. For example, we often want to check that only specific users or entry points can modify certain variables. The simplest example of this is the Ownable contract:

contract Ownable {
    address owner;

    constructor() {
        owner = msg.sender;
    }

    function transferOwnership(address newOwner) public {
        require(msg.sender == owner);
        owner = newOwner;
    }
}

For this contract we want to check that “only the current owner can change the value of Ownable.owner”.

To motivate the need for state variable annotations, let’s first try to check this property without them - i.e. only using function annotations and contract invariants.

To express this property with function annotations, we can start by annotating transferOwnership:

    /// #if_succeeds msg.sender == old(owner) && owner == newOwner;
    function transferOwnership(address newOwner) public {
        require(msg.sender == owner);
        owner = newOwner;
    }

This however is not sufficient - we need to also annotate every other function in the contract and all inheriting contracts, with #if_succeeds old(owner) == owner;, to check that they don’t mess with owner. Clearly that’s a lot of manual effort!

However, even with all this work there is a loop hole! Consider the following case

contract SomeChild is Ownable {
    /// #if_succeeds old(owner) == owner;
    function vulnerable() public {
        address oldOwner = owner;
        owner = address(<some value>);
        this.sensitiveFunction();
        owner = oldOwner;
    }
    
    /// #if_succeeds old(owner) == owner;
    function sensitiveFunction() public {
        ...
    }
}

Even though both vulnerable and sensitiveFunction are annotated to check that owner is updated correctly at the end, and they don’t violate the checks, the property is still broken. sensitiveFunction is called with a different owner, and this can be triggered by actors other than the current owner.

The problem lies in the fact that function annotations don’t check that owner is not temporarily modified incorrectly inside the call.

Trying to achieve this with contract invariants reduces the manual annotations we have to add, but still suffers from the vulnerability shown above.

Clearly, if we want to be strict, we need an annotations that is checked every time a state variable is modified, even in the middle of a function.

The Solution

To achieve this, we introduce the if_updated annotation over state variables. As the name suggests if_updated is evaluated every time a state variable (or a part of it) is modified. Let’s apply it to the above example:

contract Ownable {
    /// #if_updated 
    ///   (msg.sig == bytes4(0xf2fde38b) && old(owner) == msg.sender) ||
    ///   (msg.sig == bytes4(0x00000000));
    address owner;

    constructor() {
        owner = msg.sender;
    }

    function transferOwnership(address newOwner) public {
        require(msg.sender == owner);
        owner = newOwner;
    }
}

The annotation precisely states that owner may ONLY be updated in two cases:

1. If we are calling transferOwnership (0xf2fde38b is the signature hash of transferOwnership) and the old owner is the caller.
2. If we are in the constructor (msg.sig in the constructor is 0x000000)

Scribble will find all locations where owner is modified, including in inheriting contracts, and re-write them to check the above property.

Under the hood

It’s instructive to look in more detail at what are all the syntactic cases of variable modification that Scribble handles.

The simplest update site is a direct assignment. But even that is not as simple as it first seems, since assignments can happen to a part of the variable itself.

contract Foo {
    uint[] arr;
    function foo(uint i, uint j) {
        ...
        arr[i] = j;
        ...
    }
}

State variables can be an arbitrarily complex combination of structs, arrays and maps, and sometimes only a part of the variable gets modified.

A different way to modify a variable is with the delete keyword (which is semantically equivalent to a zeroing-out assignment). Again this applies both to the whole state var, as well as a part of it.

    delete arr[i];

Next we have inline initializers. For those we do some extra work, to insert the annotation check at the beginning of the constructor itself, since we are limited at what we can do in an inline initializer.

contract Foo {
    uint[] arr = [1,2,3];
}

We also handle impure increment/decrement unary operators:

    arr[i]++;
    arr[i]--;

Finally a state var can be indirectly modified by passing it by reference into a function that modifies it. In general we don’t support passing state vars by reference (see the next section for more details). However, we do handle the case where arrays are modified with the builtin push() and pop() functions:

    arr.push(1);
    arr.pop();

A lot of work goes into identifying all of these edge cases, and making sure each one is checked properly.

Limitations

The major limitation of this instrumentation is pointer aliasing. When Scribble detects that an annotated state variable is passed by reference, it will throw an error.

To see why this is difficult consider the contrived example below:

contract Foo {
    /// #if_updated a[0] == 1;
    uint[] a;
    /// #if_updated b[0] == 2;
    uint[] b;
    
    function main(bool flag, uint val) public {
        uint[] storage p = flag ? a : b;
        
        // Which annotation do we check here??
        p[0] = val;
    }
}

The pointer p can point to either a or b, so when we modify p[0] it’s not clear which property we should check. A more practical example of this is using libraries to enhance data types, as shown in the example below.

library ArrUtils {
    function zeroOut(uint[] storage p) public returns (uint) {
        for (uint i = 0; i < p.length; i++) {
            // Which property do we check here?
            p[i] = 0;
        }
    }
}

contract Foo {
    uses ArrUtils for uint[];
    /// #if_updated a[0] == 1;
    uint[] a;
    /// #if_updated b[0] == 2;
    uint[] b;
    
    function main() public {
        a.zeroOut();
        b.zeroOut();
    }
}

The calls to zeroOout() implicitly pass a or b by reference to ArrSum.zeroOut. And within ArrSum.zeroOut, again different properties should be checked depending on the function arguments.

Note that there are some options for reducing this limitation. One option would be to use inline assembly to check at runtime whether a given pointer aliases a specific state variable. Another option is to utilize pointer aliasing analysis to handle some limited cases of aliasing.

However, at the moment this is left as future work and an opportunity to get involved! So please reach out! We’d love to hear what you think!

All posts