Solvent: liquidity verification of smart contracts

TL;DR

Solvent is a verification tool designed to check liquidity properties in smart contracts, addressing limitations of existing tools in expressing and verifying asset exchange security properties.

Contribution

It introduces Solvent, a novel verification approach specifically targeting liquidity and asset exchange properties in Solidity smart contracts.

Findings

Solvent effectively verifies liquidity properties in smart contracts.

It demonstrates good performance on a standard benchmark.

The tool uncovers potential security issues related to asset withdrawal.

Abstract

Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts.