research-article

Open access

Towards Automated Safety Vetting of Smart Contracts in Decentralized Applications

Authors:

Mu ZhangAuthors Info & Claims

CCS '22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security

Pages 921 - 935

https://doi.org/10.1145/3548606.3559384

Published: 07 November 2022 Publication History

Abstract

We propose VetSC, a novel UI-driven, program analysis guided model checking technique that can automatically extract contract semantics in DApps so as to enable targeted safety vetting. To facilitate model checking, we extract business model graphs from contract code that capture its intrinsic business and safety logic. To automatically determine what safety specifications to check, we retrieve textual semantics from DApp user interfaces. To exclude untrusted UI text, we also validate the UI-logic consistency and detect any discrepancies. We have implemented VetSC and applied it to 34 real-world DApps. Experiments have demonstrated that VetSC can accurately interpret smart contract code, enable autonomous safety vetting, and discover safety risks in real-world Dapps. Using our tool, we have successfully discovered 19 new safety risks in the wild, such as expired lottery tickets and double voting.

References

[1]

2020. King of the Ether Throne. https://github.com/kieranelby/KingOfTheEtherThrone/. (2020).

[2]

2020. MetaMask: Brings Ethereum to your browser. https://metamask.io/. (2020).

[3]

2020. Octopus: Security Analysis tool for Blockchain Smart Contracts. https: //github.com/quoscient/octopus/. (2020).

[4]

2020. Stanford Log-linear Part-Of-Speech Tagger. https://nlp.stanford.edu/ software/tagger.shtml. (2020).

[5]

2021. Ethereum Virtual Machine Opcodes. https://ethervm.io/. (2021).

[6]

2021. NuSMV: a new symbolic model checker. http://nusmv.fbk.eu/. (2021).

[7]

2022. Block and Transaction Properties. https://docs.soliditylang.org/en/v0.8.11/ units-and-global-variables.html#block-and-transaction-properties/. (2022).

[8]

2022. Discover, collect, and sell extraordinary NFTs. https://opensea.io/. (2022).

[9]

2022. selenium. https://www.selenium.dev/. (2022).

[10]

2022. Uniswap Docs. https://docs.uniswap.org/protocol/V2/concepts/protocol- overview/smart-contracts/. (2022).

[11]

Benjamin Andow, Akhil Acharya, Dengfeng Li, William Enck, Kapil Singh, and Tao Xie. 2017. UiRef: Analysis of Sensitive User Inputs in Android Applications. In Proceedings of the 10th ACM Conference on Security and Privacy in Wireless and Mobile Networks. 23--34.

Digital Library

[12]

Michael Bendersky, W Bruce Croft, and Yanlei Diao. 2011. Quality-Biased Ranking of Web Documents. In Proceedings of the fourth ACM international conference on Web search and Data Mining. 95--104.

Digital Library

[13]

Martim Carbone, Weidong Cui, Long Lu, Wenke Lee, Marcus Peinado, and Xuxian Jiang. 2009. Mapping Kernel Objects to Enable Systematic Integrity Checking. In Proceedings of the 16th ACM Conference on Computer and Communications Security (CCS'09).

Digital Library

[14]

Chain Security. 2021. VerX API. (2021). http://verx.ch/docs/api.html

[15]

Mihai Christodorescu, Somesh Jha, Sanjit A Seshia, Dawn Song, and Randal E Bryant. 2005. Semantics-Aware Malware Detection. In 2005 IEEE Symposium on Security and Privacy (S&P'05). IEEE, 32--46.

[16]

Weidong Cui, Marcus Peinado, Zhilei Xu, and Ellick Chan. 2012. Tracking Rootkit Footprints with a Practical Memory Analysis System. In Proceedings of the 21st USENIX Conference on Security Symposium (USENIX Security'12).

Digital Library

[17]

Michael del Castillo. 2016. The DAO Attacked: Code Issue Leads to $60 Million Ether Theft. https://www.coindesk.com/dao-attacked-code-issue-leads-60-million-ether-theft. (2016).

[18]

B. Dolan-Gavitt, T. Leek, M. Zhivich, J. Giffin, and W. Lee. 2011. Virtuoso: Narrowing the Semantic Gap in Virtual Machine Introspection. In 2011 IEEE Symposium on Security and Privacy.

[19]

Brendan Dolan-Gavitt, Abhinav Srivastava, Patrick Traynor, and Jonathon Giffin. 2009. Robust Signatures for Kernel Data Structures. In Proceedings of the 16th ACM Conference on Computer and Communications Security (CCS'09).

Digital Library

[20]

Ebay. 2022. Ebay: Ending a listing. https://www.ebay.com/help/selling/listings/ creating-managing-listings/cancelling-listing?id=4146/. (2022).

[21]

Ethereum. 2021. INTRODUCTION TO DAPPS. https://ethereum.org/en/ developers/docs/dapps/. (2021).

[22]

Ittay Eyal and Emin Gün Sirer. 2014. Majority is Not Enough: Bitcoin Mining is Vulnerable. In International Conference on Financial Cryptography and Data Security. Springer, 436--454.

[23]

Joel Frank, Cornelius Aschermann, and Thorsten Holz. 2020. {ETHBMC}: A Bounded Model Checker for Smart Contracts. In 29th USENIX Security Symposium (USENIX Security 20).

[24]

Jake Frankenfield. 2019. 51% Attack. https://www.investopedia.com/terms/1/51- attack.asp. (2019).

[25]

Tal Garfinkel, Mendel Rosenblum, et al. 2003. A Virtual Machine Introspection based Architecture for Intrusion Detection. In NDSS. 191--206.

[26]

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2018. Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. In Procceedings of The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).

Digital Library

[27]

Ethan Heilman, Alison Kendler, Aviv Zohar, and Sharon Goldberg. 2015. Eclipse Attacks on Bitcoin's Peer-to-Peer Network. In 24th USENIX Security Symposium (USENIX Security 15). 129--144.

[28]

Jianjun Huang, Zhichun Li, Xusheng Xiao, Zhenyu Wu, Kangjie Lu, Xiangyu Zhang, and Guofei Jiang. 2015. {SUPOR}: Precise and Scalable Sensitive User Input Detection for Android Apps. In 24th USENIX Security Symposium (USENIX Security 15). 977--992.

[29]

Jianjun Huang, Xiangyu Zhang, Lin Tan, Peng Wang, and Bin Liang. 2014. AsDroid: Detecting Stealthy Behaviors in Android Applications by User Interface and Program Behavior Contradiction (ICSE 2014).

[30]

Christopher D. Manning Jeffrey Pennington, Richard Socher. 2020. GloVe: Global Vectors for Word Representation. https://nlp.stanford.edu/projects/glove/. (2020).

[31]

Xuxian Jiang, Xinyuan Wang, and Dongyan Xu. 2007. Stealthy Malware De- tection Through Vmm-based "Out-of-the-box" Semantic View Reconstruction. In Proceedings of the 14th ACM Conference on Computer and Communications Security (CCS'07).

[32]

Hongyan Jing and Evelyne Tzoukermann. 1999. Information Retrieval Based on Context Distance and Morphology. In Proceedings of the 22nd annual international ACM SIGIR conference on Research and Development in Information Retrieval. 90--96.

Digital Library

[33]

Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. In Proceedings of the 2018 Network and Distributed System Security Symposium.

[34]

Johannes Krupp and Christian Rossow. 2018. TEETHER: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In Proceedings of the 27th USENIX Conference on Security Symposium (USENIX Security'18).

[35]

JongHyup Lee, Thanassis Avgerinos, and David Brumley. 2011. TIE: Principled Reverse Engineering of Types in Binary Programs. In Proceedings of the 18th Annual Network and Distributed System Security Symposium (NDSS'11).

[36]

Zhiqiang Lin, Junghwan Rhee, Chao Wu, Xiangyu Zhang, and Dongyan Xu. 2012. Dimsum: Discovering Semantic Data of Interest from Un-mappable Memory with Confidence. In Proceedings of NDSS Symposium 2012.

[37]

Zhiqiang Lin, Junghwan Rhee, Xiangyu Zhang, Dongyan Xu, and Xuxian Jiang. 2011. SigGraph: Brute Force Scanning of Kernel Data Structure Instances Using Graph-based Signatures. In Proceedings of the 18th Annual Network and Distributed System Security Symposium (NDSS'11).

[38]

Ye Liu, Yi Li, Shang-Wei Lin, and Rong Zhao. 2020. Towards Automated Verification of Smart Contract Fairness. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 666--677.

Digital Library

[39]

Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS'16).

Digital Library

[40]

Stephen McLaughlin and Patrick McDaniel. 2012. SABOT: Specification-based Payload Generation for Programmable Logic Controllers. In Proceedings of the 2012 ACM Conference on Computer and Communications Security (CCS'12).

Digital Library

[41]

Yuhong Nan, Min Yang, Zhemin Yang, Shunfan Zhou, Guofei Gu, and XiaoFeng Wang. 2015. Uipicker: User-input Privacy Identification in Mobile Applications. In 24th USENIX Security Symposium (USENIX Security 15). 993--1008.

[42]

State of the DApps. 2022. DApp Statistics. https://www.stateofthedapps.com/stats. (2022).

[43]

Harrie Oosterhuis and Maarten de Rijke. 2018. Ranking for Relevance and Display Preferences in Complex Presentation Layouts. In The 41st International ACM SIGIR Conference on Research & Development in Information Retrieval (SIGIR '18).

[44]

Rahul Pandita, Xusheng Xiao, Wei Yang, William Enck, and Tao Xie. 2013. WHYPER: Towards Automating Risk Assessment of Mobile Applications. In Proceedings of the 22nd USENIX Conference on Security (USENIX Security 13).

[45]

Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. 2020. VerX: Safety Verification of Smart Contracts. In 2020 IEEE Symposium on Security and Privacy (Oakland).

[46]

Giuseppe Petracca, Ahmad-Atamli Reineh, Yuqiong Sun, Jens Grossklags, and Trent Jaeger. 2017. Aware: Preventing Abuse of Privacy-Sensitive Sensors via Operation Bindings. In 26th USENIX Security Symposium (USENIX Security 17). 379--396.

[47]

Giuseppe Petracca, Yuqiong Sun, Ahmad-Atamli Reineh, Patrick McDaniel, Jens Grossklags, and Trent Jaeger. 2019. Entrust: Regulating Sensor Access by Cooperating Programs via Delegation Graphs. In 28th USENIX Security Symposium (USENIX Security 19). 567--584.

[48]

Zhengyang Qu, Vaibhav Rastogi, Xinyi Zhang, Yan Chen, Tiantian Zhu, and Zhong Chen. 2014. AutoCog: Measuring the Description-to-Permission Fidelity in Android Applications. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (CCS '14).

Digital Library

[49]

Talia Ringer, Dan Grossman, and Franziska Roesner. 2016. Audacious: User-driven Access Control With Unmodified Operating Systems. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. 204--216.

Digital Library

[50]

Michael Rodler, Wenting Li, Ghassan O. Karame, and Lucas Davi. 2019. Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. In Proceedings of the 2019 Network and Distributed System Security Symposium.

[51]

Franziska Roesner, Tadayoshi Kohno, Alexander Moshchuk, Bryan Parno, Helen J Wang, and Crispin Cowan. 2012. User-driven Access Control: Rethinking Permission Granting in Modern Operating Systems. In 2012 IEEE Symposium on Security and Privacy. IEEE, 224--238.

[52]

Evgeniy Shishkin. 2019. Debugging Smart Contract's Business Logic Using Symbolic Model Checking. Programming and Computer Software 45, 8 (2019), 590--599.

Digital Library

[53]

Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, and Hakjoo Oh. 2020. VERIS- MART: A Highly Precise Safety Verifier for Ethereum Smart Contracts. In 2020 IEEE Symposium on Security and Privacy (Oakland).

[54]

Solidity. 2020. Solidity. https://solidity.readthedocs.io/en/v0.6.1/. (2020).

[55]

David Sounthiraraj, Justin Sahs, Garret Greenwood, Zhiqiang Lin, and Latifur Khan. 2014. SMV-Hunter: Large Scale, Automated Detection of SSL/TLS Man- in-the-Middle Vulnerabilities in Android Apps. In NDSS.

[56]

Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, and Isil Dillig. 2021. SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. In IEEE S&P.

[57]

Yuan Tian, Nan Zhang, Yueh-Hsun Lin, Xiao Feng Wang, Blase Ur, Xian Zheng Guo, and Patrick Tague. 2017. Smartauth: User-Centered Authorization for the Internet of Things. In Proceedings of the 26th USENIX Conference on Security Symposium (USENIX Security 17).

[58]

Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS'18).

Digital Library

[59]

Yuepeng Wang, Shuvendu K Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, and Immad Naseer. 2018. Formal Specification and Verification of Smart Contracts for Azure Blockchain. arXiv preprint arXiv:1812.08829 (2018).

[60]

Siwei Wu, Dabao Wang, Jianting He, Yajin Zhou, Lei Wu, Xingliang Yuan, Qinming He, and Kui Ren. 2021. DeFiRanger: Detecting Price Manipulation Attacks on DeFi Applications. arXiv preprint arXiv:2104.15068 (2021).

[61]

Xusheng Xiao, Xiaoyin Wang, Zhihao Cao, Hanlin Wang, and Peng Gao. 2019. Iconintent: Automatic Identification of Sensitive UI Widgets Based on Icon Classification for Android Apps. In 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). IEEE, 257--268.

[62]

Zethyr. 2021. Zethyr Exchange. https://www.dapp.com/app/zethyr-exchange/. (2021).

Cited By

Li XYang JChen JTang YGao XChua TNgo CKa-Wei Lee RKumar RLauw H(2024)Characterizing Ethereum Upgradable Smart Contracts and Their Security ImplicationsProceedings of the ACM Web Conference 202410.1145/3589334.3645640(1847-1858)Online publication date: 13-May-2024
https://dl.acm.org/doi/10.1145/3589334.3645640
Ibba GDestefanis GNeykova ROrtu MAufiero SBartolucci S(2024)DAI: A Dependencies Analyzer and Installer for Solidity Smart Contracts2024 IEEE International Conference on Software Analysis, Evolution and Reengineering - Companion (SANER-C)10.1109/SANER-C62648.2024.00015(72-75)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER-C62648.2024.00015
Li PWang GXing XZhu JGu WZhai G(2024)A smart contract vulnerability detection method based on deep learning with opcode sequencesPeer-to-Peer Networking and Applications10.1007/s12083-024-01750-717:5(3222-3238)Online publication date: 27-Jun-2024
https://doi.org/10.1007/s12083-024-01750-7
Show More Cited By

Index Terms

Towards Automated Safety Vetting of Smart Contracts in Decentralized Applications
1. Security and privacy
  1. Software and application security

Recommendations

SAFEVM: a safety verifier for Ethereum smart contracts
ISSTA 2019: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis

Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use ...
Formal Modeling and Verification of Smart Contracts
ICSCA '18: Proceedings of the 2018 7th International Conference on Software and Computer Applications

Smart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an ...
Formal Verification of Smart Contracts: Short Paper
PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security

Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security

November 2022

3598 pages

ISBN:9781450394505

DOI:10.1145/3548606

General Chairs:
Heng Yin
University of California, Riverside
,
Angelos Stavrou
Virginia Tech
,
Program Chairs:
Cas Cremers
CISPA Helmholtz Center for Information Security
,
Elaine Shi
Carnegie Mellon University

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 November 2022

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

CCS '22

Sponsor:

SIGSAC

CCS '22: 2022 ACM SIGSAC Conference on Computer and Communications Security

November 7 - 11, 2022

CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
1,801
Total Downloads

Downloads (Last 12 months)691
Downloads (Last 6 weeks)77

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li XYang JChen JTang YGao XChua TNgo CKa-Wei Lee RKumar RLauw H(2024)Characterizing Ethereum Upgradable Smart Contracts and Their Security ImplicationsProceedings of the ACM Web Conference 202410.1145/3589334.3645640(1847-1858)Online publication date: 13-May-2024
https://dl.acm.org/doi/10.1145/3589334.3645640
Ibba GDestefanis GNeykova ROrtu MAufiero SBartolucci S(2024)DAI: A Dependencies Analyzer and Installer for Solidity Smart Contracts2024 IEEE International Conference on Software Analysis, Evolution and Reengineering - Companion (SANER-C)10.1109/SANER-C62648.2024.00015(72-75)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER-C62648.2024.00015
Li PWang GXing XZhu JGu WZhai G(2024)A smart contract vulnerability detection method based on deep learning with opcode sequencesPeer-to-Peer Networking and Applications10.1007/s12083-024-01750-717:5(3222-3238)Online publication date: 27-Jun-2024
https://doi.org/10.1007/s12083-024-01750-7
Bärtl M(2023)A statistical examination of utilization trends in decentralized applicationsFrontiers in Blockchain10.3389/fbloc.2023.12063306Online publication date: 16-Aug-2023
https://doi.org/10.3389/fbloc.2023.1206330
Ye MNan YZheng ZWu DLi HJust RFraser G(2023)Detecting State Inconsistency Bugs in DApps via On-Chain Transaction Replay and FuzzingProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598057(298-309)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598057
Zhu JXing XWang GLi P(2023)Opcode Sequences-Based Smart Contract Vulnerabilities Detection Using Deep Learning2023 IEEE 22nd International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom)10.1109/TrustCom60117.2023.00057(284-291)Online publication date: 1-Nov-2023
https://doi.org/10.1109/TrustCom60117.2023.00057

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents