VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts

Explore a highly precise safety verifier for Ethereum smart contracts in this 17-minute IEEE conference talk. Delve into the pressing issue of ensuring smart contract safety and learn about VeriSmart, an exhaustive, precise, and fully automated verification tool. Discover the key features of VeriSmart, including its inference and use of transaction invariants. Examine the algorithm behind VeriSmart and its experimental setup. Compare its performance against bug-finders and explore incorrect CVE reports identified by the tool. Gain insights into the general applicability of VeriSmart and understand its potential impact on improving smart contract security in the Ethereum ecosystem.

VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts
Smart Contract • Digital contract written in programming languages
Pressing Issue: Ensuring Safety of Smart Contracts
Goal:Automatic Safety Verification of Smart Contracts
SmartMesh (CVE-2018-10376)
Shortcomings of Existing Approaches
VeriSmart: Exhaustive, Precise, Fully Automated Smart Contract Safety Verifier
Result Highlight
Key Feature of VeriSmart: Inference and Use of Transaction Invariant
Verification with Transaction Invariants
VeriSmart Algorithm
Experimental Setup
vs. Bug-finders
Incorrect CVE reports Found by VeriSmart
General Applicability of VeriSmart
Summary