Safety Verification of Declarative Smart Contracts

• URL: http://arxiv.org/abs/2211.14585v3
• Date: Wed, 2 Aug 2023 09:43:06 GMT
• Title: Safety Verification of Declarative Smart Contracts
• Authors: Haoxian Chen, Lan Lu, Brendan Massey, Yuepeng Wang, Boon Thau Loo
• Abstract summary: 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.
• Score: 4.303272418564008
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. 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. Furthermore, DCV significantly outperforms baseline tools in verification time.

Related papers

• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  We present the Code-Development Benchmark (Codev-Bench), a fine-grained, real-world, repository-level, and developer-centric evaluation framework. Codev-Agent is an agent-based system that automates repository crawling, constructs execution environments, extracts dynamic calling chains from existing unit tests, and generates new test samples to avoid data leakage.
  arXiv  Detail & Related papers  (2024-10-02T09:11:10Z)
• 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)
• Effective Targeted Testing of Smart Contracts [0.0]
  Since smart contracts are immutable, their bugs cannot be fixed, which may lead to significant monetary losses. Our framework, Griffin, tackles this deficiency by employing a targeted symbolic execution technique for generating test data. This paper discusses how smart contracts differ from legacy software in targeted symbolic execution and how these differences can affect the tool structure.
  arXiv  Detail & Related papers  (2024-07-05T04:38:11Z)
• Solvent: liquidity verification of smart contracts [2.680854115314008]
  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.
  arXiv  Detail & Related papers  (2024-04-27T10:54:50Z)
• 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)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Automated Invariant Generation for Solidity Smart Contracts [2.4181711081104282]
  We propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks.
  arXiv  Detail & Related papers  (2024-01-01T03:37:30Z)
• 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)
• Detecting Logical Relation In Contract Clauses [94.85352502638081]
  We develop an approach to automate the extraction of logical relations between clauses in a contract. The resulting approach should help contract authors detecting potential logical conflicts between clauses.
  arXiv  Detail & Related papers  (2021-11-02T19:26:32Z)
• Exploring Robustness of Unsupervised Domain Adaptation in Semantic Segmentation [74.05906222376608]
  We propose adversarial self-supervision UDA (or ASSUDA) that maximizes the agreement between clean images and their adversarial examples by a contrastive loss in the output space. This paper is rooted in two observations: (i) the robustness of UDA methods in semantic segmentation remains unexplored, which pose a security concern in this field; and (ii) although commonly used self-supervision (e.g., rotation and jigsaw) benefits image tasks such as classification and recognition, they fail to provide the critical supervision signals that could learn discriminative representation for segmentation tasks.
  arXiv  Detail & Related papers  (2021-05-23T01:50:44Z)
• 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.