Solvent: liquidity verification of smart contracts

• URL: http://arxiv.org/abs/2404.17864v3
• Date: Mon, 23 Sep 2024 10:27:57 GMT
• Title: Solvent: liquidity verification of smart contracts
• Authors: Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini, Vadim Malvone,
• Abstract summary: 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. We propose solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity.
• Score: 2.680854115314008
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Instrumenting Transaction Trace Properties in Smart Contracts: Extending the EVM for Real-Time Security [3.4237310507643706]
  Smart contracts are often instrumented with some safety properties to enhance their security. These safety properties are limited and fail to block certain types of hacks such as those which exploit read-only re-entrancy. We propose to enable smart contracts to validate transaction trace properties in real-time without affecting traditional EVM execution.
  arXiv  Detail & Related papers  (2024-08-26T20:33:22Z)
• Versioned Analysis of Software Quality Indicators and Self-admitted Technical Debt in Ethereum Smart Contracts with Ethstractor [2.052808596154225]
  This paper proposes Ethstractor, the first smart contract collection tool for gathering a dataset of versioned smart contracts. The collected dataset is then used to evaluate the reliability of code metrics as indicators of vulnerabilities in smart contracts.
  arXiv  Detail & Related papers  (2024-07-22T18:27:29Z)
• Vulnerabilities of smart contracts and mitigation schemes: A Comprehensive Survey [0.6554326244334866]
  This paper presents a literature review combined with an experimental report that aims to assist developers in developing secure smarts. It provides a list of frequent vulnerabilities and corresponding mitigation solutions. It evaluates the community most widely used tools by executing and testing them on sample smart contracts.
  arXiv  Detail & Related papers  (2024-03-28T19:36:53Z)
• Vulnerability Scanners for Ethereum Smart Contracts: A Large-Scale Study [44.25093111430751]
  In 2023 alone, such vulnerabilities led to substantial financial losses exceeding a billion of US dollars. Various tools have been developed to detect and mitigate vulnerabilities in smart contracts. This study investigates the gap between the effectiveness of existing security scanners and the vulnerabilities that still persist in practice.
  arXiv  Detail & Related papers  (2023-12-27T11:26:26Z)
• Gradual Verification for Smart Contracts [0.4543820534430522]
  Algos facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities. Traditional verification techniques fall short in providing comprehensive security assurances. This paper introduces an incremental approach: gradual verification.
  arXiv  Detail & Related papers  (2023-11-22T12:42:26Z)
• Token-Level Adversarial Prompt Detection Based on Perplexity Measures and Contextual Information [67.78183175605761]
  Large Language Models are susceptible to adversarial prompt attacks. This vulnerability underscores a significant concern regarding the robustness and reliability of LLMs. We introduce a novel approach to detecting adversarial prompts at a token level.
  arXiv  Detail & Related papers  (2023-11-20T03:17:21Z)
• Formally Verifying a Real World Smart Contract [52.30656867727018]
  We search for a tool capable of formally verifying a real-world smart contract written in a recent version of Solidity. In this article, we present our search for a tool capable of formally verifying a real-world smart contract written in a recent version of Solidity.
  arXiv  Detail & Related papers  (2023-07-05T14:30:21Z)
• Uniswap Liquidity Provision: An Online Learning Approach [49.145538162253594]
  Decentralized Exchanges (DEXs) are new types of marketplaces leveraging technology. One such DEX, Uniswap v3, allows liquidity providers to allocate funds more efficiently by specifying an active price interval for their funds. This introduces the problem of finding an optimal strategy for choosing price intervals. We formalize this problem as an online learning problem with non-stochastic rewards.
  arXiv  Detail & Related papers  (2023-02-01T17:21:40Z)
• Safety Verification of Declarative Smart Contracts [4.303272418564008]
  This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon. Our evaluation on 20 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools.
  arXiv  Detail & Related papers  (2022-11-26T15:02:37Z)
• Smart Contract Vulnerability Detection: From Pure Neural Network to Interpretable Graph Feature and Expert Pattern Fusion [48.744359070088166]
  Conventional smart contract vulnerability detection methods heavily rely on fixed expert rules. Recent deep learning approaches alleviate this issue but fail to encode useful expert knowledge. We develop automatic tools to extract expert patterns from the source code. We then cast the code into a semantic graph to extract deep graph features.
  arXiv  Detail & Related papers  (2021-06-17T07:12:13Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  Existing machine learning-based vulnerability detection methods are limited and only inspect whether the smart contract is vulnerable. We propose ESCORT, the first Deep Neural Network (DNN)-based vulnerability detection framework for smart contracts. We show that ESCORT achieves an average F1-score of 95% on six vulnerability types and the detection time is 0.02 seconds per contract.
  arXiv  Detail & Related papers  (2021-03-23T15:04:44Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.