A Survey of Smart Contract Formal Specification and Verification
arXiv:2008.02712
Abstract
A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview in order to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.
References in corpus (30)
- An Overview on Smart Contracts: Challenges, Advances and Platforms
- ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection
- Ekiden: A Platform for Confidentiality-Preserving, Trustworthy, and Performant Smart Contract Execution
- Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts
- Vandal: A Scalable Security Analysis Framework for Smart Contracts
- SmartEmbed: A Tool for Clone and Bug Detection in Smart Contracts through Structural Code Embedding
- Towards Safer Smart Contracts: A Survey of Languages and Verification Methods
- Towards Safer Smart Contracts: A Sequence Learning Approach to Detecting Security Threats
- Smart Contract Vulnerabilities: Vulnerable Does Not Imply Exploited
- Thou Shalt is not You Will
- Raziel: Private and Verifiable Smart Contracts on Blockchains
- Security Analysis Methods on Ethereum Smart Contract Vulnerabilities: A Survey
- Precise Attack Synthesis for Smart Contracts
- SMT-Friendly Formalization of the Solidity Memory Model
- EVulHunter: Detecting Fake Transfer Vulnerabilities for EOSIO's Smart Contracts at Webassembly-level
- Oracle-Supported Dynamic Exploit Generation for Smart Contracts
- Security Analysis of EOSIO Smart Contracts
- Obsidian: Typestate and Assets for Safer Blockchain Programming
- Deductive Proof of Ethereum Smart Contracts Using Why3
- Bug Searching in Smart Contract
- Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity
- Formal Analysis of Composable DeFi Protocols
- Formal Verification of Solidity contracts in Event-B
- Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph
- WhylSon: Proving your Michelson Smart Contracts in Why3
- Resources: A Safe Language Abstraction for Money
- A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
- Smart Contract Design Meets State Machine Synthesis: Case Studies
- Building Executable Secure Design Models for Smart Contracts with Formal Methods
- Pluralize: a Trustworthy Framework for High-Level Smart Contract-Draft