Scribble: an inline verification language for Solidity

Tooling and Languages
, ,
1

Former colleagues of mine recently released Scribble which I believe is a very exciting step forward for the usability of specification and verification techniques on Solidity smart contracts.

The major benefit is that it allows developers to write properties using inline comments their code, with no need to manage a separate set of test files.

Scribble is first and foremost a language, but also includes a tool for processing and instrumenting solidity code.

Here’s a basic example:

contract Foo {
    int x;

    /// if_succeeds {:msg "test"} x == old(x) + y;
    function add(int y) public {
        require(y > 0);
        x += y;
    }
}

The text following the /// is written in Scribble, it defines the property to check:

  1. If the function returns properly (ie. without INVALID or REVERT)
  2. then the new value of x should incremented by the amount y.
  3. if the property does not hold, then an event will be emitted with the text “test”.

The scribble tool can then instrument the code, to emit an AssertionFailed event if the property is broken (an assert is also added by default, but can be optionally removed which is advantageous for fuzzing campaigns).

contract Foo {
    event AssertionFailed(string message);

    struct vars0 {
        int256 old_0;
    }

    int internal x;

    function add(int y) public {
        vars0 memory _v;
        _v.old_0 = x;
        _original_Foo_add(y);
        if ((!((x == (_v.old_0 + y))))) {
            emit AssertionFailed("0: test");
            assert(false);
        }
    }

    function _original_Foo_add(int y) private {
        require((y > 0));
        x += y;
    }
}

I’ll let my colleagues know I’ve posted this here, and would love to see feedback and discussion.

7 Likes
2

@maurelian Thanks for joining SCRF and for your post.

Scribble seems like a very interesting tool, and its use together with Mythril is indeed a great idea.

After reading this post, a few questions popped in my head, and your insights would be much appreciated:

  • If used together with Mythril, I guess my first question is how scalable that is. Do you have any data on scalability of Scribble + Mythril when used together?
  • If used solo, Scribble will generate bytecode that will end up using more gas. I know this is dependent on the types of annotations, but is there any available data showing specific examples and how much more gas was needed?
  • Is there any reuse mechanism built-in into the DSL? Or do I have to clone annotations if I want to reuse them?
  • What happens in the case of reusable contracts (e.g., OpenZeppelin) and overriding inherited functions? Do invariants apply to overriden functions?

Once again, thanks for your post and welcome to SCRF :slight_smile:

2 Likes
3

Those are some interesting questions! Let me try to answer them!

On the scalability of Mythril and Scribble:

Most (if not all) of the optimisations that went into Mythril are to improve its primary use-case (Finding vulnerabilities that we have written particular modules for).

We could do some optimisations/ tweaks when just testing properties.

For example, Mythril can take a modular approach analysing functions in isolation instead of the contract’s entire state space.

We do not have concrete data on the Scalability of Scribble+Mythril, but I would assume that it is close to the scalability of Mythril on its own.

We are currently designing the implementation of specification language features like aggregation and quantification (e.g. sum, avg), and trying to optimise instrumentation for analysis techniques such as symbolic execution (by limiting the use of loops for example).

Finally, we are exploring the use of symbolic execution and fuzzing at diligence.

On gas usage:

Our primary goal currently is to enable automatic property testing. In this scenario, gas costs are not a significant factor. As a result, we have not put in much effort measuring the gas impact of annotations.

I would also add that Scribble is still in the early stages of development, so the annotations’ gas footprint is bound to change.

On re-use mechanisms:

We do not have an easy code re-use mechanism yet, but we are working on it! It seems like many contracts will have similar properties, so being able to easily re-use properties is super valuable!

We are currently thinking of implementing a method based on macros and predicates, to be used throughout Scribble annotations. If you have any ideas or feedback here, we would love to hear!

Finally on overriding:

Invariants do apply to overridden functions. Essentially we expect an inheriting contract not to violate the assumptions of the contracts that it is inheriting. This is necessary because the correctness of non-overridden functions can depend on these invariants.

3 Likes
4

@walker Thanks for the clarifications :)