Introducing Scribble

Making sure that smart contracts are secure and bug-free has never been more critical. Unfortunately, it remains a difficult task. While there are helpful tools for automatic testing and formal verification, ensuring the correctness of smart contracts continues to be a time-intensive and challenging task. To make things worse, each tool often has a steep learning curve, and it is often uncertain whether it’s even right for the job.

That is why we’ve developed Scribble: a verification language and runtime verification tool. While initially created for automatic property testing during audits, we’ve decided to share this project with the community!

What is Scribble?

When we’re talking about Scribble, we’re talking about two things.

First, Scribble is a specification language for writing properties. \ Second, Scribble is a runtime verification tool. It instruments contracts based on annotations; allowing other tools such as fuzzers, and symbolic executors to automatically test the properties.

Scribble is a language

Scribble defines a domain-specific language for writing properties about smart contracts. We’ve built the language on top of the solidity syntax, to make it easy to learn. This specification language allows you to annotate a solidity smart contract with properties.

📖 A property is a logical statement that you expect to be true, e.g. “All cars are red”. In solidity, you’ll often have properties like: “Only the owner can make a change to X”. Or function sendToken(), should not change this contract’s ether balance".

You can use several annotation types for different kinds of properties. For example, invariants or post-conditions.

This is an example of a Scribble annotation:

/// if_succeeds {:msg "The result should not be zero"} result != 0;
function getBlocknumberOfLatestUpdate() public returns (uint result) {
...
}

As you can see, the annotations take the form of an inline comment placed above a function definition. We’ve added a so-called if_succeeds clause, which checks whether a condition holds after the function is executed. In this case, we check that the result of the function is always non-zero.

📖 If you want to learn more, read our documentation on if_succeeds clauses

We’ve based the Scribble language on proven concepts such as post-conditions, invariants and temporal logic. But we also look at how we can introduce novel ideas to suit the domain-specific problems of smart contracts better.

Scribble is a tool

Scribble can take a contract annotated with properties, and compile it into a new contract. In this new contract, Scribble will have added Solidity code that raises an assertion whenever a property is violated. We call this process instrumentation.

Adding executable code that checks properties is called runtime verification, and makes it easy to work with existing tools without many adaptions. This is the case because most tools will already interpret solidity code and be able to search for property violations right away!

Because you can use existing automatic testing techniques (such as our fuzzer Harvey), you’ll be able to start testing after writing just a single property. We believe that this is a significant benefit; You benefit from automatic testing right away, instead of having to spend a lot of time upfront to gain a critical mass of annotations. Something which is usually necessary with traditional verification approaches.

You can get started testing and analysing a contract quickly, and even decide later on to put in the additional effort to verify a smart contract completely!

Goals

Audit

We’re using Scribble during audits to formulate properties. Using automatic analysis techniques such as fuzzing and symbolic execution, we’ll automatically test and find violations for these properties.

🚀 Reach out to us if you’d like to learn more about fuzzing and property-based testing during audits!

Standard

Scribble aims to work with different tools and techniques; we don’t just want to enable property-based testing, but also easy formal verification. The benefit of using a single universal specification language is that you only put in the effort of writing properties once, but reap the benefit of using multiple tools.

Adoption

With Scribble we are hoping to lower the barrier or entry for automatic testing and formal verification. We also want to reduce the time investment needed to develop correct and secure smart contracts, resulting in a safer ecosystem.

Where can you get it?

We’ve wholly open-sourced Scribble, and it’s available now at GitHub.com/Consensys/Scribble.

⚠️ This is a beta-release, aspects of the language will change, and you might encounter some bugs.

You can easily install Scribble with npm:

npm install --global eth-scribble

Be sure to check out our documentation if you want to learn more about how to use Scribble: https://docs.scribble.codes.

Also, make sure to join our discord community where we’d love to hear your thoughts and feedback!

All posts