Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strengthening Solidity Invariant Generation: From Post- to Pre-Deployment

Kartik Kaushik, Raju Halder, Samrat Mondal

TL;DR

This work tackles the problem of ensuring Solidity smart contract correctness before deployment by generating invariants without relying on post-deployment transaction histories. It introduces InvSol, a Solidity-to-Java transcompiler-based framework that annotates code with JML specifications, uses a dynamic invariant explorer (Daikon) and loop invariant detector (GIN-DYN), and employs a Test Crafter to generate coverage-rich tests, all under static verification. Its key contributions include pre-deployment invariant synthesis, loop invariant coverage, a broad set of blockchain-specific invariant templates (gas, reentrancy, time locks, access control, etc.), and a comprehensive evaluation showing InvSol outperforms state-of-the-art tools like InvCon, InvCon+, and Trace2Inv across multiple datasets. This approach enables earlier, safer deployment of contracts and provides a practical, auditable toolchain for developers and auditors in the blockchain ecosystem.

Abstract

Invariants are essential for ensuring the security and correctness of Solidity smart contracts, particularly in the context of blockchain's immutability and decentralized execution. This paper introduces InvSol, a novel framework for pre-deployment invariant generation tailored specifically for Solidity smart contracts. Unlike existing solutions, namely InvCon, InvCon+, and Trace2Inv, that rely on post-deployment transaction histories on Ethereum mainnet, InvSol identifies invariants before deployment and offers comprehensive coverage of Solidity language constructs, including loops. Additionally, InvSol incorporates custom templates to effectively prevent critical issues such as reentrancy, out-of-gas errors, and exceptions during invariant generation. We rigorously evaluate InvSol using a benchmark set of smart contracts and compare its performance with state-of-the-art solutions. Our findings reveal that InvSol significantly outperforms these tools, demonstrating its effectiveness in handling new contracts with limited transaction histories. Notably, InvSol achieves a 15% improvement in identifying common vulnerabilities compared to InvCon+ and is able to address certain crucial vulnerabilities using specific invariant templates, better than Trace2Inv.

Strengthening Solidity Invariant Generation: From Post- to Pre-Deployment

TL;DR

This work tackles the problem of ensuring Solidity smart contract correctness before deployment by generating invariants without relying on post-deployment transaction histories. It introduces InvSol, a Solidity-to-Java transcompiler-based framework that annotates code with JML specifications, uses a dynamic invariant explorer (Daikon) and loop invariant detector (GIN-DYN), and employs a Test Crafter to generate coverage-rich tests, all under static verification. Its key contributions include pre-deployment invariant synthesis, loop invariant coverage, a broad set of blockchain-specific invariant templates (gas, reentrancy, time locks, access control, etc.), and a comprehensive evaluation showing InvSol outperforms state-of-the-art tools like InvCon, InvCon+, and Trace2Inv across multiple datasets. This approach enables earlier, safer deployment of contracts and provides a practical, auditable toolchain for developers and auditors in the blockchain ecosystem.

Abstract

Invariants are essential for ensuring the security and correctness of Solidity smart contracts, particularly in the context of blockchain's immutability and decentralized execution. This paper introduces InvSol, a novel framework for pre-deployment invariant generation tailored specifically for Solidity smart contracts. Unlike existing solutions, namely InvCon, InvCon+, and Trace2Inv, that rely on post-deployment transaction histories on Ethereum mainnet, InvSol identifies invariants before deployment and offers comprehensive coverage of Solidity language constructs, including loops. Additionally, InvSol incorporates custom templates to effectively prevent critical issues such as reentrancy, out-of-gas errors, and exceptions during invariant generation. We rigorously evaluate InvSol using a benchmark set of smart contracts and compare its performance with state-of-the-art solutions. Our findings reveal that InvSol significantly outperforms these tools, demonstrating its effectiveness in handling new contracts with limited transaction histories. Notably, InvSol achieves a 15% improvement in identifying common vulnerabilities compared to InvCon+ and is able to address certain crucial vulnerabilities using specific invariant templates, better than Trace2Inv.
Paper Structure (23 sections, 1 theorem, 9 equations, 10 figures, 13 tables, 2 algorithms)

This paper contains 23 sections, 1 theorem, 9 equations, 10 figures, 13 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Hoare Logic and Smart Contract Correctness
  3. Contract Vulnerabilities and Invariants
  4. Invariant Synthesis and Execution
  5. Overview
  6. Code Transcompiler
  7. Post Processor
  8. Transcompilation Formalism
  9. AutoJML
  10. Test Crafter
  11. Invariant Generation Module
  12. Static Code Auditor
  13. Specific invariant templates to address vulnerability concerns
  14. Experimental Evaluation
  15. Benchmark Datasets
  16. ...and 8 more sections

Key Result

Theorem 1

Let $\mathcal{S}_{\text{sol}}$ and $\mathcal{S}_{\text{java}}$ be the state transition semantic functions for Solidity and Java languages respectively. Given a Solidity state $\rho_{\text{sol}}$ and a Java state $\rho_{\text{java}}$, let $\mathbb{T}_\rho\llbracket \rho_{\text{sol}} \rrbracket = \rho

Figures (10)

  • Figure 1: A code snippet for distribute function
  • Figure 2: Solidity code for transferring asset ownership, ensuring that only the owner can initiate the transfer.
  • Figure 3: InvSol System Architecture
  • Figure 4: Overview of custom classes in Post Processor
  • Figure 5: Comparative core grammars of Solidity and Java programming languages
  • ...and 5 more figures

Theorems & Definitions (2)

  • Theorem 1: Semantics Equivalence
  • proof