Solvent: liquidity verification of smart contracts 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] [ 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_nonliquidPassed - 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 Structure 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). Getting Started From the docker image Download the docker image from Zenodo. Then, load it from the .tar archive (docker may require sudo root privileges):docker load z3.out Then, to compare your results with those in the paper, run: git diff --no-index --word-diff results/z3.out z3.outNote that your results will be different from those in the repository, because of different computational resources. In particular:1. [always] computation times will be different (lines beginning with Time);2. [very often] experiments resulting in LIQUID (up to N) will have a different N;3. [hardly ever] your experiments resulting in LIQUID (up to N) may be tagged as NOT 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;4. [hardly ever] your experiments resulting in Timeout may be tagged as LIQUID or NOT 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. Verifying your own contracts To use Solvent on your own contract, open a terminal and run the following: python3 src/solvent.py [-t timeout]where:- file.sol is the smart contract- number of transactions is the maximum number of transactions to consider in the bounded model checking problem- solver 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 Extending Solvent 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