VERISMART: A highly precise safety verifier for ethereum smart contracts

Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, Hakjoo Oh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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 manually checking undiscovered or incorrectly-reported issues. To achieve this goal, we present a new domain-specific algorithm for verifying smart contracts, which is able to automatically discover and leverage transaction invariants that are essential for precisely analyzing smart contracts. Evaluation with real-world smart contracts shows that VERISMART can detect all arithmetic bugs with a negligible number of false alarms, far outperforming existing analyzers.

Original languageEnglish
Title of host publicationProceedings - 2020 IEEE Symposium on Security and Privacy, SP 2020
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1678-1694
Number of pages17
ISBN (Electronic)9781728134970
DOIs
Publication statusPublished - 2020 May
Event41st IEEE Symposium on Security and Privacy, SP 2020 - San Francisco, United States
Duration: 2020 May 182020 May 21

Publication series

NameProceedings - IEEE Symposium on Security and Privacy
Volume2020-May
ISSN (Print)1081-6011

Conference

Conference41st IEEE Symposium on Security and Privacy, SP 2020
CountryUnited States
CitySan Francisco
Period20/5/1820/5/21

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Software
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'VERISMART: A highly precise safety verifier for ethereum smart contracts'. Together they form a unique fingerprint.

  • Cite this

    So, S., Lee, M., Park, J., Lee, H., & Oh, H. (2020). VERISMART: A highly precise safety verifier for ethereum smart contracts. In Proceedings - 2020 IEEE Symposium on Security and Privacy, SP 2020 (pp. 1678-1694). [9152689] (Proceedings - IEEE Symposium on Security and Privacy; Vol. 2020-May). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/SP40000.2020.00032