Towards Safer Smart Contracts: A Survey of Languages and Verification Methods
arXiv:1809.09805
Abstract
With a market capitalisation of over USD 205 billion in just under ten years, public distributed ledgers have experienced significant adoption. Apart from novel consensus mechanisms, their success is also accountable to smart contracts. These programs allow distrusting parties to enter agreements that are executed autonomously. However, implementation issues in smart contracts caused severe losses to the users of such contracts. Significant efforts are taken to improve their security by introducing new programming languages and advance verification methods. We provide a survey of those efforts in two parts. First, we introduce several smart contract languages focussing on security features. To that end, we present an overview concerning paradigm, type, instruction set, semantics, and metering. Second, we examine verification tools and methods for smart contract and distributed ledgers. Accordingly, we introduce their verification approach, level of automation, coverage, and supported languages. Last, we present future research directions including formal semantics, verified compilers, and automated verification.
References in corpus (2)
Cited by in corpus (14)
- An Overview on Smart Contracts: Challenges, Advances and Platforms
- A comprehensive survey on smart contract construction and execution: paradigms, tools, and systems
- A Survey on Ethereum Systems Security: Vulnerabilities, Attacks and Defenses
- Security Defense For Smart Contracts: A Comprehensive Survey
- Smart Contract Vulnerabilities: Vulnerable Does Not Imply Exploited
- Security Analysis Methods on Ethereum Smart Contract Vulnerabilities: A Survey
- Maintaining Smart Contracts on Ethereum: Issues, Techniques, and Future Challenges
- A Survey of Smart Contract Formal Specification and Verification
- Oracle-Supported Dynamic Exploit Generation for Smart Contracts
- Using Fault Injection to Assess Blockchain Systems in Presence of Faulty Smart Contracts
- Obsidian: Typestate and Assets for Safer Blockchain Programming
- Formal Modelling and Security Analysis of Bitcoin's Payment Protocol
- Flash Crash for Cash: Cyber Threats in Decentralized Finance
- Verification of a Smart Contract for a Simple Casino