ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts
Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool, and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.
Tue 10 MayDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:00 | Validation and VerificationDEMO - Demonstrations at ICSE Demo room 1 Chair(s): Allison Sullivan The University of Texas at Arlington | ||
11:00 15mDemonstration | ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts DEMO - Demonstrations Kunjian Song The University of Manchester, Nedas Matulevicius University of Manchester, UK, Eddie Lima Samsung Electronics, Brazil, Lucas C. Cordeiro University of Manchester Pre-print Media Attached | ||
11:15 15mDemonstration | DScribe: Co-generating Unit Tests and Documentation DEMO - Demonstrations Alexa Hernandez McGill University, Mathieu Nassif McGill University, Martin P. Robillard McGill University Link to publication Pre-print Media Attached | ||
11:30 15mDemonstration | SymInfer: Inferring Numerical Invariants using Symbolic States DEMO - Demonstrations ThanhVu Nguyen George Mason University, KimHao Nguyen University of Nebraska-Lincoln, Hai Duong Independent Researcher | ||