TY - GEN
T1 - VERISMART
T2 - 41st IEEE Symposium on Security and Privacy, SP 2020
AU - So, Sunbeom
AU - Lee, Myungho
AU - Park, Jisu
AU - Lee, Heejo
AU - Oh, Hakjoo
N1 - Funding Information:
We thank Junhee Lee and Minseok Jeon for their valuable comments on Proposition 1 and Appendix A. This work was supported by Institute of Information & communications Technology Planning & Evaluation(IITP) grant funded by the Korea government(MSIT) (No.2019-0-01697, Development of Automated Vulnerability Discovery Technologies for Blockchain Platform Security and No.2019-0-00099, Formal Specification of Smart Contract).
Publisher Copyright:
© 2020 IEEE.
PY - 2020/5
Y1 - 2020/5
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85088920725&partnerID=8YFLogxK
U2 - 10.1109/SP40000.2020.00032
DO - 10.1109/SP40000.2020.00032
M3 - Conference contribution
AN - SCOPUS:85088920725
T3 - Proceedings - IEEE Symposium on Security and Privacy
SP - 1678
EP - 1694
BT - Proceedings - 2020 IEEE Symposium on Security and Privacy, SP 2020
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 18 May 2020 through 21 May 2020
ER -