Automated Invariant Generation for Solidity Smart Contracts

• URL: http://arxiv.org/abs/2401.00650v1
• Date: Mon, 1 Jan 2024 03:37:30 GMT
• Title: Automated Invariant Generation for Solidity Smart Contracts
• Authors: Ye Liu, Chengxuan Zhang, Yi Li. (Nanyang Technological University, Singapore)
• Abstract summary: 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.
• Score: 2.4181711081104282
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program invariants are properties that are always preserved throughout the execution, which characterize an important aspect of the program behaviors. In this paper, 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 based on both dynamic inference and static verification. Unlike INVCON+, InvCon only produces likely invariants, which have a high probability to hold, yet are still not verified against the contract code. Particularly, INVCON+ is able to infer more expressive invariants that capture richer semantic relations of contract code. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks. The experimental results indicate that INVCON+ efficiently produces high-quality invariant specifications, which can be used to secure smart contracts from common vulnerabilities.

Related papers

• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  We introduce SolBench, a benchmark for evaluating the functional correctness of Solidity smart contracts generated by code completion models. We propose a Retrieval-Augmented Code Repair framework to verify functional correctness of smart contracts. Results show that code repair and retrieval techniques effectively enhance the correctness of smart contract completion while reducing computational costs.
  arXiv  Detail & Related papers  (2025-03-03T01:55:20Z)
• SmartInv: Multimodal Learning for Smart Contract Invariant Inference [10.468390413756863]
  We present SmartInv, an accurate and fast smart contract invariant inference framework. Our key insight is that the expected behavior of smart contracts relies on understanding and reasoning across multimodal information. We evaluate SmartInv on real-world contracts and re-discover bugs that resulted in multi-million dollar losses.
  arXiv  Detail & Related papers  (2024-11-14T06:28:57Z)
• 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)
• Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions [8.32630869646569]
  We present a viable technological roadmap for the community toward this ambitious goal. Our technology, called Theorem-Carrying-Transaction (TCT), combines the benefits of concrete execution and symbolic proofs. Our prototype incurs a negligible runtime overhead, two orders of magnitude lower than a state-of-the-art approach.
  arXiv  Detail & Related papers  (2024-08-12T20:27:41Z)
• 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)
• Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
  We propose a specification mining approach to infer contract specifications from past transaction histories. Our approach derives high-level behavioral automata of function invocations, accompanied by program invariants statistically inferred from the transaction histories. Experiments show that SMCON mines reasonably accurate specifications that can be used to enhance symbolic analysis of smart contracts achieving higher code coverage and up to 56% speedup.
  arXiv  Detail & Related papers  (2024-03-20T03:39:51Z)
• Contract Usage and Evolution in Android Mobile Applications [45.44831696628473]
  We present the first large-scale empirical study on the presence and use of contracts in Android applications, written in Java or Kotlin. We analyzed 2,390 Android applications from the F-Droid repository and processed more than 51,749 KLOC. Our findings show that it would be desirable to have libraries that standardize contract specifications in Java and Kotlin.
  arXiv  Detail & Related papers  (2024-01-25T15:36:49Z)
• 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)
• Enhancing Smart Contract Security Analysis with Execution Property Graphs [48.31617821205042]
  We introduce Clue, a dynamic analysis framework specifically designed for a runtime virtual machine. Clue captures critical information during contract executions, employing a novel graph-based representation, the Execution Property Graph. evaluation results reveal Clue's superior performance with high true positive rates and low false positive rates, outperforming state-of-the-art tools.
  arXiv  Detail & Related papers  (2023-05-23T13:16:42Z)
• Toward Adversarial Training on Contextualized Language Representation [78.39805974043321]
  This paper investigates adversarial training (AT) from the perspective of the contextualized language representation outputted by PLM encoders. We propose textitContextualized representation-Adversarial Training (CreAT) in which the attack is explicitly optimized to deviate the contextualized representation of the encoder. CreAT produces consistent performance gains on a wider range of tasks and is proven to be more effective for language pre-training where only the encoder part is kept for downstream tasks.
  arXiv  Detail & Related papers  (2023-05-08T08:56:51Z)
• 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)
• ContrastVAE: Contrastive Variational AutoEncoder for Sequential Recommendation [58.02630582309427]
  We propose to incorporate contrastive learning into the framework of Variational AutoEncoders. We introduce ContrastELBO, a novel training objective that extends the conventional single-view ELBO to two-view case. We also propose ContrastVAE, a two-branched VAE model with contrastive regularization as an embodiment of ContrastELBO for sequential recommendation.
  arXiv  Detail & Related papers  (2022-08-27T03:35:00Z)
• Speculative Decoding: Exploiting Speculative Execution for Accelerating Seq2seq Generation [80.2267931231335]
  We propose Speculative Decoding (SpecDec) to study exploiting the idea of speculative execution to accelerate autoregressive (AR) decoding. SpecDec has two innovations: Spec-Drafter -- an independent model specially optimized for efficient drafting, and Spec-Verification -- a reliable method for verifying the drafted tokens efficiently.
  arXiv  Detail & Related papers  (2022-03-30T17:27:09Z)
• HCC: A Language-Independent Hardening Contract Compiler for Smart Contracts [5.379572824182189]
  We propose the first practical smart contract compiler, called HCC. HCC inserts security hardening checks at the source-code level based on a novel and language-independent code property graph (CPG) notation.
  arXiv  Detail & Related papers  (2022-03-01T11:25:32Z)
• 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)
• Profiling Gas Consumption in Solidity Smart Contracts [3.0378875015087567]
  We propose GasMet, a suite of metrics for statically evaluating the code quality of a smart contract from the gas consumption perspective. An experiment involving 2,186 smart contracts demonstrates that the proposed metrics have direct associations with deployment costs.
  arXiv  Detail & Related papers  (2020-08-12T17:26:55Z)

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.