Just Accepted
SmartExecutor: Coverage-Driven Symbolic Execution Guided via State Prioritization and Function Selection
Authors: 
Qiping Wei, Fadul Sikder, Huadong Feng, Yu Lei, Raghu Kacker, Richard KuhnAuthors Info & Claims
Accepted on 19 June 2024
Abstract
Symbolic execution of smart contracts suffers from sequence explosion. Some existing tools limit the sequence length, thus being unable to adequately evaluate some functions. In this paper, we propose a symbolic execution approach without limiting the sequence length. In our approach, the symbolic execution process is a two-phase model that maximizes code coverage while reducing the number of sequences to be executed. The first phase executes all sequences up to a length limit to identify the not-fully covered functions while the second attempts to cover these functions according to state evaluation and a function graph structure. We have developed a tool called SmartExecutor and conducted an experimental evaluation on the SGUARD dataset. The experimental results indicate that compared with state-of-the-art tools, SmartExecutor achieves higher code coverage with less time. It also detects more vulnerabilities than Mythril, a state-of-the-art symbolic execution tool.
References
[1]
Jaeseung Choi, Doyeon Kim, Soomin Kim, Gustavo Grieco, Alex Groce, and Sang Kil Cha. 2021. SMARTIAN: Enhancing Smart Contract Fuzzing with Static and Dynamic Data-Flow Analyses. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE). 227–239. https://doi.org/10.1109/ASE51524.2021.9678888
[2]
ConsenSys. 2015. ConsenSys is a market-leading blockchain technology company. https://consensys.net/about/ Last accessed 20 November 2023.
[3]
contractAnalysis. 2023. Case studies on Mpro. https://github.com/contractAnalysis/smartExecutor_exp_data/tree/smartExecutor_paper/mpro_case_study.
[4]
contractAnalysis. 2023. SmartExecutor. https://github.com/contractAnalysis/smartExecutor.
[5]
contractAnalysis. 2023. SmartExecutor experiment data preparation. https://github.com/contractAnalysis/smartExecutor_exp_data.
[6]
Joseph Cook. last edit July 31, 2023. Ethereum Accounts. https://ethereum.org/en/developers/docs/accounts/ Last accessed 20 November 2023.
[7]
ConsenSys Diligence. 2019. Analysis Modules(detection capabilities). https://mythril-classic.readthedocs.io/en/master/analysis-modules.html.
[8]
Ethereum. 2016. Solidity. https://docs.soliditylang.org/en/v0.8.7/ Last accessed 20 November 2023.
[9]
Etherscan. 2015. The Ethereum Blockchain Explorer. https://etherscan.io/ Last accessed 20 November 2023.
[10]
Josselin Feist, Gustavo Greico, and Alex Groce. 2019. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In Proceedings of the 34nd IEEE/ACM International Conference on Automated Software Engineering (ASE’19).
[11]
Shane Fontaine. 2019. Understanding Bytecode on Ethereum. https://medium.com/authereum/bytecode-and-init-code-and-runtime-code-oh-my-7bcd89065904 Last accessed 20 November 2023.
[12]
fravoll. 2018. Tight Variable Packing. https://fravoll.github.io/solidity-patterns/tight_variable_packing.html Last accessed 19 November 2023.
[13]
Asem Ghaleb and Karthik Pattabiraman. 2020. Slither: A Static Analysis Framework for Smart Contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis.
[14]
Masoud Ghorbanzadeh. Last edit July 7, 2023. TRANSACTIONS. https://ethereum.org/en/developers/docs/transactions/ Last accessed 20 November 2023.
[15]
Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust, Lujo Bauer and Ralf Küsters (Eds.). Springer International Publishing, Cham.
[16]
Jingxuan He, Mislav Balunović, Nodar Ambroladze, Petar Tsankov, and Martin Vechev. 2019. Learning to Fuzz from Symbolic Execution with Application to Smart Contracts. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS’19).
[17]
Holo. 2018. Token HoloToken. https://etherscan.io/token/0x6c6ee5e31d828de241282b9606c8e98ea48526e2 Last accessed 20 November 2023.
[18]
Jianjun Huang, Jiasheng Jiang, Wei You, and Bin Liang. 2022. Precise Dynamic Symbolic Execution for Nonuniform Data Access in Smart Contracts. IEEE Trans. Comput. 71, 7 (2022), 1551–1563. https://doi.org/10.1109/TC.2021.3092639
[19]
Sylabs Inc. 2017. Apptainer User Guide. https://apptainer.org/docs/user/latest/ Last accessed 20 November 2023.
[20]
Wayne Jones. 2022. The DAO Attack: Understanding What Happened. https://crypto.news/learn/the-dao-attack-understanding-what-happened/.
[21]
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.
[22]
Ning Lu, Bin Wang, Yongxin Zhang, Wenbo Shi, and Christian Esposito. 2019. NeuCheck: A more practical Ethereum smart contract security analysis tool. In Software: Practice and Experience.
[23]
Bernhard Mueller. 2018. Smashing Ethereum Smart Contracts for Fun and Real Profit. https://tinyurl.com/y827tk72 Last accessed 20 November 2023.
[24]
Bernhard Mueller. 2018. Smashing Smart Contracts. https://github.com/muellerberndt/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf.
[25]
Tai D. Nguyen, Long H. Pham, and Jun Sun. 2021. SGUARD: Towards Fixing Vulnerable Smart Contracts Automatically. In 42nd IEEE Symposium on Security and Privacy, SP 2021. IEEE. https://doi.org/10.1109/SP40001.2021.00057
[26]
Chigozie Oduah. 2023. What Are Solidity Modifiers? Explained with Examples. https://www.freecodecamp.org/news/what-are-solidity-modifiers/ Last accessed 20 November 2023.
[27]
Trail of Bits. 2019. A symbolic execution tool for analysis of smart contracts and binaries. https://github.com/trailofbits/manticore.
[28]
The University of Texas at Austin. [n. d.]. Texas Advanced Computing Center (TACC). http://www.tacc.utexas.edu.
[29]
Bernard Peh. 2017. Solidity Bytecode and Opcode Basics. https://medium.com/@blockchain101/solidity-bytecode-and-opcode-basics-672e9b1a88c2 Last accessed 20 November 2023.
[30]
rakita. last edit September 2, 2023. Ethereum Virtual Machine (EVM). https://ethereum.org/en/developers/docs/evm/ Last accessed 20 November 2023.
[31]
Sunbeom So, Seongjoon Hong, and Hakjoo Oh. 2021. SmarTest: Effectively Hunting Vulnerable Transaction Sequences in Smart Contracts through Language Model-Guided Symbolic Execution. In Proceedings of the 30th USENIX Security Symposium.
[32]
ConsenSys Software. 2018. A security analysis tool for EVM bytecode. https://github.com/ConsenSys/mythril.
[33]
Qiping Wei, Fadul Sikder, Huadong Feng, Yu Lei, Raghu Kacker, and Richard Kuhn. 2023. SmartExecutor: Coverage-Driven Symbolic Execution Guided by a Function Dependency Graph. In 5th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS).
[34]
Maximilian Wohrer and Uwe Zdun. 2018. Smart contracts: security patterns in the ethereum ecosystem and solidity. In 2018 International Workshop on Blockchain Oriented Software Engineering (IWBOSE). 2–8. https://doi.org/10.1109/IWBOSE.2018.8327565
[35]
GAVIN WOOD. 2022. Ethereum Yellow Paper. https://ethereum.github.io/yellowpaper/paper.pdf.
[36]
Xiao Liang Yu. 2017. An Analysis Tool for Smart Contracts. https://github.com/enzymefinance/oyente.
[37]
Abdullah A. Zarir, Gustavo A. Oliva, Zhen M. (Jack) Jiang, and Ahmed E. Hassan. 2021. Developing Cost-Effective Blockchain-Powered Applications: A Case Study of the Gas Usage of Smart Contract Transactions in the Ethereum Blockchain Platform. ACM Trans. Softw. Eng. Methodol. 30, 3, Article 28 (mar 2021), 38 pages. https://doi.org/10.1145/3431726
[38]
William Zhang, Sebastian Banescu, Leonardo Pasos, Steven Stewart, and Vijay Ganesh. 2019. MPro: Combining Static and Symbolic Analysis for Scalable Testing of Smart Contract. In 2019 IEEE 30th International Symposium on Software Reliability Engineering (ISSRE). 456–462. https://doi.org/10.1109/ISSRE.2019.00052
[39]
Zibin Zheng, Shaoan Xie, Hong-Ning Dai, Weili Chen, Xiangping Chen, Jian Weng, and Muhammad Imran. 2020. An overview on smart contracts: Challenges, advances and platforms. Future Generation Computer Systems 105 (2020), 475–491. https://doi.org/10.1016/j.future.2019.12.019
Index Terms
- SmartExecutor: Coverage-Driven Symbolic Execution Guided via State Prioritization and Function Selection
Recommendations
Concrete Constraint Guided Symbolic Execution
ICSE '24: Proceedings of the IEEE/ACM 46th International Conference on Software EngineeringSymbolic execution is a popular program analysis technique. It systematically explores all feasible paths of a program but its scalability is largely limited by the path explosion problem, which causes the number of paths proliferates at runtime. A key ...
Running symbolic execution forever
ISSTA 2020: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and AnalysisWhen symbolic execution is used to analyse real-world applications, it often consumes all available memory in a relatively short amount of time, sometimes making it impossible to analyse an application for an extended period. In this paper, we present a ...
Efficient state merging in symbolic execution
PLDI '12Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
EISSN:2769-6480
Table of ContentsCopyright © 2024 Copyright held by the owner/author(s).
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Online AM: 15 July 2024
Accepted: 19 June 2024
Revised: 11 May 2024
Received: 01 December 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 147Total Downloads
- Downloads (Last 12 months)147
- Downloads (Last 6 weeks)41
Reflects downloads up to 19 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in