4 effective strategies to come up with Scribble annotations
Coming up with properties can be a difficult task! In this previous post we talked about starting to write Scribble properties. Here I’m going to explore four strategies to accelerate annotating your smart contracts!
As you might already know, Scribble enables you to write properties that you can then test automatically using methods such as fuzzing and symbolic execution.
Sounds awesome, doesn’t it? But how do you come up with those properties? We’ve found that the following four strategies work really well:
- π§ͺ Tests - Base properties on the existing unit tests
- π Documentation - Look at the documentation to find potential properties
- π Copy Pasta - Copy-paste annotations from other similar projects
- π€ Code - Base properties on what you can learn from the code
π§ͺ Tests
The first, and easiest place to start is the test suite that’s usually already there. Unit tests already try to determine if the smart contracts behave as expected. The only thing we’ll need to do is generalise what the unit tests are checking, and formalise it in the Scribble specification language.
Unit tests will often follow a pattern with three stages:
- Arrange - Setup the contract
- Act - Execute the code under test
- Assert - Assert that the result is what we expected
We can write properties based on tests like this with the following approach:
First, we look at the Act section of a test. Specifically, we need to know what function or contract is being executed? This is the function or contract that we’ll need to annotate with Scribble specifications.
Then we have a look at both the Arrange and Assert steps. How do the assertions compare the “input state” after the Arrange step with the state in the Assert phase? There are tons of properties that we could learn from this.
The following are some examples:
Example 1:
// Act
result = someFunction(input)
// Assert
assert result > 0
There is a static assertion that seemingly doesnβt relate to the input. Itβs possible that someFunction()
should only return positive numbers. Let’s add a function specification:
/// if_succeeds {:msg "Returns only positive numbers"} $result > 0;
function someFunction(uint input) returns (uint) { ... }
Example 2:
// Act
result = someFunction(a, b)
// Assert
assert result == a + b
We see here that the input should be the sum of a and b. An annotation will be simple!
/// if_succeeds {:msg "Should add a and b"} $result == a + b;
function someFunction(uint a, uint b) returns (uint) { ... }
Example 3:
// Arrange
contract.setBalance(account[0], 10)
// Act
result = contract.someFunction(account[0], 3)
// Assert
assert contract.balanceOf(account[0]) == 7
Now we see something interesting. It seems like the balance of the contract should be subtracted with the second argument of someFunction
. We can use the old keyword to express this property:
/// if_succeeds {:msg "Should change balance with amount"} old(balanceOf(a)) = balanceOf(a) + amount;
function someFunction(address a, uint amount) returns (uint) { ... }
π Documentation
Documentation is another great place too look for properties. You might find actual natural language specifications, or models describing how the system works. These are the smart contract’s assumptions and properties and will only require a formalisation to Scribble annotations.
Invariants
The documentation usually provides a high-level explanation of the smart contracts. This high-level explanation/ model of the system can hint towards possible invariants:
- Does the documentation describe the various states that smart contracts can be in?
- Are some of the aspects of the contracts constant? Or should they only change under certain conditions?
π‘ If a high-level description includes a sentence of the shape “Property X must always hold over the contracts state variables”, it usually translates directly into Scribble contract invariants!
Function Specifications
Otherwise, the documentation for a project usually walks through how you can work with the code. How you can use the smart contracts, and what you can expect the smart contracts to do. You can use these to figure out the following:
- What kinds of inputs does this function accept? When should the function revert?
- If a particular function succeeds, then what is the effect that we should see?
- What is the relation between the input and the output of the function?
Translate these into if_succeeds
Scribble annotations, as described in the documentation.
π Copy Pasta
One of the most straightforward strategies you can apply is looking at contracts similar to those you’re annotating.
Good Artists Copy; Great Artists Steal
There are bound to be similarities between different smart contracts. You can see this by looking at the sheer amount of ERC20 and ERC721 tokens out there.
These contracts will all have the same, or at least very similar, properties and assumptions. As a result, you might just be able to setup Scribble annotations with just <Ctrl-C>
and <Ctrl-V>
(use Cmd if you’re on Mac π).
π€ Code
The final strategy is one without tricks; it requires you to straight-up understand the code and figure out which properties should hold over it.
Make sure that your properties are sane! The properties should match what a contract is supposed to be doing, not what it actually does!
Luckily, even here, there are some strategies that you can follow. I’ve taken each type of specification that you can currently write with Scribble and highlighted approaches for coming up with properties.
Preconditions
Figuring out pre-conditions is pretty easy; usually, they are already written down as require statements already.
Some prompts you can use:
- Which conditions need to hold for the function to execute successfully?
- Is there an input to this function that should not be accepted? (e.g. transfers to
0x0
) - Is the behaviour of the function depending on the input? (See our documentation on behaviours)
Postconditions
Postconditions are the properties valid after a function is done executing. You can use this to make statements over the result (e.g. the result is an even number). You can also specify the relation between the state before and after the function (e.g. the value of storage variable x is bigger than before).
Some prompts you can use:
- How should this function change the state of the contract?
- How does the result of this function relate to the input to this function?
- The result of a function, is it particular in a certain way? (i.e. it’s always even, or it’s always smaller than this.totalBalance)
Invariants
Invariants are both the easiest and most difficult to come up with. (I know, that doesn’t make any sense π ). These are the properties that describe the entire contract.
These properties can be straightforward and inherent to a contract. For example, an invariant for a token could be that the totalBalance doesn’t change. Easy right?
Sometimes invariants are more difficult to determine and based on complex and/or non-apparent assumptions that a contract has.
Some prompts you can use:
- Are there constant variables in the contract?
- Are there variables protected by access control? ( e.g.
old(x) != x ==> msg.sender == owner
)
Fin
I hope these strategies help you write Scribble annotations! If you have any questions or are looking for help, then hop by on Discord!
Thinking about smart contract security? We can provide training, ongoing advice, and smart contract auditing. Contact us.