Solvent: liquidity verification of smart contracts
arxiv(2024)
摘要
Smart contracts are programs executed by blockchains networks to regulate the
exchange of crypto-assets between untrusted users. Due to their immutability,
public accessibility and high value at stake, smart contracts are an attractive
target for attackers, as evidenced by a long history of security incidents.
This has been a driving factor for the application of formal methods to
Ethereum, the leading smart contract platform, and Solidity, its main smart
contract language, which have become the target of dozens of verification tools
with varying objectives. A current limitation of these 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要