Related papers: Formally Verifying a Real World Smart Contract

Formally Verifying a Real World Smart Contract

URL: http://arxiv.org/abs/2307.02325v1
Date: Wed, 5 Jul 2023 14:30:21 GMT
Title: Formally Verifying a Real World Smart Contract
Authors: Alexandre Mota, Fei Yang, Cristiano Teixeira
Abstract summary: 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.
Score: 52.30656867727018
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Nowadays, smart contracts have become increasingly popular and, as with software development in general, testing is the standard method for verifying their correctness. However, smart contracts require a higher level of certainty regarding correctness because they are diffcult to modify once deployed and errors can result in significant financial losses. Therefore, formal verification is essential. 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.

Related papers

Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
arXiv Detail & Related papers (2024-10-05T05:21:48Z)
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)
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)
CONTRACTFIX: A Framework for Automatically Fixing Vulnerabilities in Smart Contracts [12.68736241704817]
ContractFix is a framework that automatically generates security patches for vulnerable smart contracts. Users can use it as a security fix-it tool that automatically applies patches and verifies the patched contracts.
arXiv Detail & Related papers (2023-07-18T01:14:31Z)
Vera: A General-Purpose Plausibility Estimation Model for Commonsense Statements [135.09277663808322]
We introduce Vera, a general-purpose model that estimates the plausibility of declarative statements based on commonsense knowledge. trained on 7M commonsense statements created from 19 QA datasets and two large-scale knowledge bases. We find that Vera excels at filtering LM-generated commonsense knowledge and is useful in detecting erroneous commonsense statements generated by models like ChatGPT in real-world settings.
arXiv Detail & Related papers (2023-05-05T17:15:32Z)
Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
arXiv Detail & Related papers (2023-01-05T18:18:46Z)
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)
Editing Factual Knowledge in Language Models [51.947280241185]
We present KnowledgeEditor, a method that can be used to edit this knowledge. Besides being computationally efficient, KnowledgeEditor does not require any modifications in LM pre-training. We show KnowledgeEditor's efficacy with two popular architectures and knowledge-intensive tasks.
arXiv Detail & Related papers (2021-04-16T15:24:42Z)
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.