Hints
Providing hints to backend tools with annotations
The main use case for scribble properties is to instrument them as actual assertions in the code and allow a backend tool (such as a fuzzer or symbolic execution engine) to check the instrumetned code. A lot of backend tools explore parts of the possible input state space of the contract, trying to find a trace violating the properties. Since this state space is usually huge, backend tools can only explore a small fraction of the input space, and can sometimes waste time on uninteresting inputs. In such case it can be helpful for the user to provide guidance to the backend tools.
In scribble v0.5.7 we added two new annotations that provide guidance to backend tools. Note that these are not properties to be checked, and are thus not part of the "specification" of the contract. Also while we tried to keep these annotations as general as possible, not all tools may be able to make use of them. So far we have been using them with our fuzzer (Harvey), but most tools that are guided by coverage should be able to use these annotations.
The first annotation limits the set of inputs that a tool may try for a given contract. Its looks and behaves exactly as Solidity's
require() statement:/// #require {:msg "description"} <solidity boolean expression>
A
#require annotation can be inserted before a function or before any statement inside of a function.
When inserted before a function, it can talk about the arguments/returns of the function and is instrumented as a require() statement at the beginning of the function.When inserted before a statement, it can talk about any local variables in scope, as well as function argument/returns and state variables. It is instrumented as a
require() inserted before the target statement.For example, consider the below contract that has an 'upgradable' model for interest rate:
interface IInterestRateModel {
function getInterstRate() external view return (uint256);
}
contract Pool {
IInterestRateModel intrestRateModel;
function upgradeInterestRateModel(IInterestRateModel newModel) onlyOwner external {
this.interestRateModel = newModel;
}
}
The interest rate is modeled by a contract implementing
IInterestRateModel and can be upgraded by calling Pool.upgradeInterestRateModel. In our experience our fuzzer can often trigger the upgrade path with a random address, thus breaking the contract (the fuzzer is allowed to try things as the owner as well). Once this invalid upgrade is performed, and the contract is in an invalid state a lot of followup false positives are triggered.
We'd like to limit the fuzzer from triggering an invalid upgrade. We can do so with the following #require annotation: function upgradeInterestRateModel(IInterestRateModel newModel) onlyOwner external {
/// #require(newModel == <address of valid model>);
this.interestRateModel = newModel;
}
Since this is translated as a
require(), if the fuzzer tries to use an invalid address here, the transaction reverting will not be treated as a property violation.In certain cases the backend tool may need to guess/compute a very specific set of inputs to make progress. In such cases it may be useful for the user to suggest input values for the backend tool to try. We support this with the synonymous annotation
#try:/// #try {:msg "description"} <solidity boolean expression>
#try can be inserted before a function or before a given statement. It allows the user to write a boolean expression over the inputs, that aims to help the backend tool. For example consider the following contrived MultiTokenPool contract, that holds funds on behalf of a user for multiple different tokens. The pool provides a function for withdrawing funds from just one token - withrdawSingleToken.contract MultiTokenPool {
function withdrawSingleToken(address token) {
require(isValidToken(token));
...
}
}
If the underlying tool attempts random bits as arguments to
withdrawSingleToken, without realizing that a valid token address is needed, then its unlikely that it will be able to cover this function. In such cases a user can suggest specific inputs for the tool to try with the following #try annotation: function withdrawSingleToken(address token) {
/// #try token == <Token1 addr>;
/// #try token == <Token2 addr>;
require(isValidToken(token));
...
}
The above annotation gets translated as the following
ifs:
function withdrawSingleToken(address token) {
if (token == <Token1 addr>) {
// dummy statement
}
if (token == <Token2 addr) {
// dummy statement
}
require(isValidToken(token));
...
}
The added
ifs are designed to have no actual effect on the exectuion of the program, but still to not be optimized away by the compiler.
The idea behind them is that if the underlying tool is trying to maximize coverage by exploring more paths, then it will attempt to reach the bodies of the if statemets. Reaching those bodies requires solving the relatively easy constraints token == <Token1 addr> and token == <Token2 addr>. Solving these constraints allows the tool to try exactly the inputs that we wanted it to try.
Note that unlike the #require annotation, #try does not limit the backend tool to only use the inputs we suggested - the annotation allows any other possible input as well.Last modified 1yr ago