Solvent is a tool to formally verify liquidity properties of Solidity smart contracts.
Liquidity expresses the ideal behaviour of contracts in terms of the exchange of crypto-assets: users want to be guaranteed that, whenever certain states are reached, they can always perform some actions that lead to a desirable asset transfer. While several real-world attacks to smart contracts exploited liquidity vulnerabilities, detecting such vulnerabilities is beyond the reach of current verification tools for Solidity.
As a toy example, consider the following contract:
contract Freezable {
address immutable owner;
bool frozen;
constructor () payable {
owner = msg.sender
}
function freeze() {
require (msg.sender == owner);
frozen = true
}
function pay(int v) {
require (!frozen);
msg.sender.transfer(v)
}
}
Note that the contract allows the owner to set the frozen
flag, making the funds within the contract actually stuck.
We can detect this undesirable behaviour by querying Solvent with the following property:
property liquidity1_nonliquid {
Forall xa
[
true
->
Exists tx [1, xa]
[
<tx>balance[xa] == balance[xa] + balance
]
]
}
Literally, this query asks whether any user xa
can fire a transaction tx
(composed up to 1 method call) whose effect is to increase the ETH balance of xa
by the whole contract balance.
Solvent answers negatively to this query, by finding an execution trace that violates the property:
Contract: freezable_liquidity1_nonliquid.sol
PROPERTY: out/smt2/liquidity1_nonliquid
Passed - NOT LIQUID (counterexample found in 2 steps)
Time: 0.6299567222595215 seconds
The violating trace provided as a counterexample is made of two transactions.
The first transaction is the invocation of the contract constructor (setting the owner to the value 2).
The second transaction is the invocation of the freeze
method by the owner.
In the state resulting from the execution of these transactions, it is not true that any user can fire a transaction whose effect is to withdraw the whole contract balance.
STATE 0
balance = 1
user_balance[0] = 2
user_balance[1] = 2
user_balance[2] = 1
TRANSACTION 0 => 1
msg.sender = 2
msg.value = 1
STATE 1
balance = 2
block.number = 0
err = false
frozen = false
owner = 2
user_balance[0] = 2
user_balance[1] = 2
user_balance[2] = 1
TRANSACTION 1 => 2
f = freeze
msg.sender = 2
msg.value = 0
STATE 2
balance = 2
block.number = 0
err = false
frozen = true
owner = 2
user_balance[0] = 2
user_balance[1] = 2
user_balance[2] = 1
Details on Solvent and on the underlying verification technique are in the following research paper:
- M. Bartoletti, A. Ferrando, E. Lipparini, V. Malvone: Solvent: liquidity verification of smart contracts. iFM, 2024
The data in this repository is structured as follows:
- Subdirectory src contains the source code of the tool;
- Subdirectory contracts contains the benchmark of smart contracts and related liquidity properties that we used to evaluate the effectiveness of Solvent in our paper;
- Subdirectory results contains the results of the experiments (they are discussed in the iFM paper).
Download the docker image from Zenodo. Then, load it from the .tar archive (docker may require sudo root privileges):
docker load < solvent.tar
Upon loading the image, run the container with:
docker run -v `pwd`/output:/tool/output --rm -it solvent
The command above starts the docker container and places you in a bash environment, where you can inspect the source code or run the experiments. -v option will mount output folder in your current directory to the corresponding folder within the container where the evaluation results will be stored. This will allow you to view the generated output even after the container has stopped running. --rm is an optional flag that creates a disposable container that will be deleted upon exit. At this point, you can run the experiments as explained below.
You can exit the container by typing exit
. Output files generated by the evaluation script (logs, tables, plots, etc.) remain available in $PWD/output. Upon finishing your review, you can remove the image from the Docker environment using:
docker rmi solvent
Solvent has the following depencies:
To install them, run:
pip3 install -r requirements.txt
To check that everything is ok, clone the repository and run the regression tests:
python3 evaluate.py --solver cvc5 --only_regression --Timeout 5
To run all the experiments, use:
python3 evaluate.py --solver z3
This runs all the experiments using z3 as a backend, with a default timeout of 400s per verification task (this is the same timeout used in the paper; the execution should take up to 6 hours). If you want instead to use cvc5, run:
python3 evaluate.py --solver cvc5
(Note that if you have installed cvc5 from github through pip3, the version is the 1.2.0, which differs from the 1.1.3-dev.152.701cd63e used for the experiments and installed in the docker.)
You can set the amount of time available for each verification task via the optional argument --Timeout
. For instance, here we reduce the timeout to 100s:
python3 evaluate.py --solver z3 --Timeout 100
If finished successfully, the evaluation script should print:
All experiments were successful.
To compare your results with those in the paper, redirect the output of evaluate.py
. For instance:
python3 evaluate.py --solver z3 > z3.out
Then, to compare your results with those in the paper, run:
git diff --no-index --word-diff results/z3.out z3.out
Note that your results will be different from those in the repository, because of different computational resources. In particular:
- [always] computation times will be different (lines beginning with
Time
); - [very often] experiments resulting in
LIQUID (up to N)
will have a differentN
; - [hardly ever] your experiments resulting in
LIQUID (up to N)
may be tagged asNOT LIQUID (counterexample found in N+1 steps)
in the paper. This is possible because of reduced computational resources w.r.t. those used in our experiments (e.g., a reduced timeout). When this happens,evaluate.py
will output that the test has not passed; - [hardly ever] your experiments resulting in
Timeout
may be tagged asLIQUID
orNOT LIQUID
in the paper. See the previous item.
To check that your results are compatible with those in the repository, you should compare that the outcomes LIQUID
/ NOT LIQUID
are almost always preserved.
To use Solvent on your own contract, open a terminal and run the following:
python3 src/solvent.py <file.sol> <number of transactions> <solver> [-t timeout]
where:
file.sol
is the smart contractnumber of transactions
is the maximum number of transactions to consider in the bounded model checking problemsolver
is the solver to use (eg., z3 or cvc5)timeout
(optional) is the maximum number of seconds the SMT solver can take to complete the verification
To extend the Solidity fragment supported by Solvent, install antlr4 (version 4.7.2). Once this is done, run the following to compile the extended grammar:
antlr4 -Dlanguage=Python3 -visitor TxScript.g4