VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts
Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, Hakjoo Oh

TL;DR
VeriSmart is a highly precise verification tool for Ethereum smart contracts that automatically detects arithmetic bugs with minimal false alarms, improving security and reducing manual review efforts.
Contribution
The paper introduces VeriSmart, a novel exhaustive verification algorithm that leverages transaction invariants for high-precision analysis of smart contracts.
Findings
Detects all arithmetic bugs in real-world contracts
Achieves negligible false alarms
Outperforms existing analyzers in precision and recall
Abstract
We present VeriSmart, a highly precise verifier for ensuring arithmetic safety of Ethereum smart contracts. Writing safe smart contracts without unintended behavior is critically important because smart contracts are immutable and even a single flaw can cause huge financial damage. In particular, ensuring that arithmetic operations are safe is one of the most important and common security concerns of Ethereum smart contracts nowadays. In response, several safety analyzers have been proposed over the past few years, but state-of-the-art is still unsatisfactory; no existing tools achieve high precision and recall at the same time, inherently limited to producing annoying false alarms or missing critical bugs. By contrast, VeriSmart aims for an uncompromising analyzer that performs exhaustive verification without compromising precision or scalability, thereby greatly reducing the burden of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Blockchain Technology Applications and Security · Advanced Malware Detection Techniques
