State Variable Annotations
Properties that hold when state variables are written to
State variable specifications allow us to describe how a smart contract is allowed to change state variables and under which circumstances.
This allows us to specify generically how all functions of the smart contract should be allowed to modify state. We highlight two use cases to demonstrate how this enables effective specification writing:
Access Control
You can write access control specifications using State Specifications. For example, we can define properties that say "only the owner can change this". Checking this property will ensure that none of the functions in the smart contract allow a non-owner to change that variable.
💡 We discuss this example in greater detail below
Integrity
Using State Specifications we can also make sure that the integrity of the state is maintained by all the functions in the smart contract.
For example, we can say that some variables shouldn't be changed, which we can use to state that the totalBalance of a non de-/inflationary token should stay constant. If we accidentally make the mint function of a contract public and unprotected, then this property would be violated.
Variable Updates
The if_updated
specification enables properties that will be checked at any point where a variable is updated. These properties follow the following structure and are placed above state variable declarations
The following property states that a variable shouldn't be updated.
The Ownable case study
Sometimes it's more convenient to reason about properties of the contract's state variable. For example, consider the Ownable
contract below:
You may want to express the following property:
The value of
owner
may only be set at contract creation, OR changed by the current owner by callingtransfer
Note that we want this property to also hold for all contracts that inherit from Ownable
. You can do this by adding an if_succeeds
annotation on all functions OTHER than transferOwnership
. However, this is fragile; what if we miss one?
We currently cannot express this as a contract-wide invariant, as those don't support old()
and don't (yet) support temporal predicates. Even if we specified this as a contract invariant, a function inside the contract can temporarily re-assign onlyOwner
and then restore it before returning.
Fundamentally, we want our property to be checked every time owner
is modified, which is precisely what you can do with the new if_updated
annotation:
There are several things to unpack here.
The if_updated
annotation appears right above the declaration of the owner
variable. This property will ensure that the condition following if_updated
will be checked on every write to the owner variable. This condition has two clauses that describe the conditions where the owner variable is allowed to be updated.
Clause 1
The first clause msg.sig == 0x0 && owner == msg.sender
describes the case when we are in the constructor (in that case msg.sig == 0x0
), and states that in that case, after the assignment owner
must equal to the msg.sender
(i.e., the contract creator).
Clause 2
The second clause specifies several things: a) we need to be in a call to transferOwnership
(which is specified by msg.sig == <signature-of-transferOwnership>
) b) The caller must be the current owner (msg.sender == old(owner)
). Note the use, of old()
to refer to the value of owner
before the assignment c) The new value of owner
must be what was passed in to transferOwnership
(owner == newOwner
).
The two clauses together precisely specify the property that we had in mind in the beginning, without any manual annotations required at every location where owner
is modified
In Summary:
if_updated
annotations appaer in docstrings right before a variable declarationIn an
if_updated
annotation you can useold()
to refer to the value of an expression before the assignment.Scribble automatically finds all places where the variable is modified and inserts the check there.
Note that "variable modification" is not just limited to assignments. A variable may be also modified due to
delete
operations, unary increment/decrement operations (++
/--
), etc.Scribble can only instrument state variables that are not aliased. A state variable is aliased if it (or any part of it) is assigned to a storage pointer variable on the stack. For example in the below code
arr
is aliased, and cannot be annotated:
Last updated