Abstract
We present SKLEE, a dynamic symbolic framework to analyse Solidity smart contracts for various safety vulnerabilities. While there are many analysis tools for Solidity contracts, in this work we demonstrate that existing analysis infrastructures for other sequential programming languages, such as C, can be leveraged to construct a competitive analysis framework for Solidity contracts. Notably, SKLEE is bootstrapped on top of KLEE – a dynamic symbolic test-case generation tool for C programs – with modelling for Solidity primitives such as send, call, transfer, and others. Our experiments indicate that SKLEE is indeed competitive with other state-of-the-art tools in terms of (i) the number of bug classes it can identify, and (ii) the number of benchmarks it can analyse in a given time bound.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
SKLEE link: https://github.com/subodhvsharma/SKLEE.
References
Consensys: Mythril: a security analysis tool for ethereum smart contracts. https://github.com/ConsenSys/mythril-classic
Solidity c3 linearization. https://docs.soliditylang.org/en/v0.8.4/contracts.html
Ahrendt, W., et al.: Verification of smart contract business logic - exploiting a Java source code verifier. In: Hojjat, H., Massink, M. (eds.) Fundamentals of Software Engineering - 8th International Conference, FSEN, pp. 228–243 (2019)
Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 66–77 (2018)
Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, pp. 209–224. USENIX Association (2008)
Feist, J., Grieco, G., Groce, A.: Slither: a static analysis framework for smart contracts. In: 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB) (2019)
Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 204–217 (2018)
Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS (2018)
Lu, N., Wang, B., Zhang, Y., Shi, W., Esposito, C.: NeuCheck: a more practical Ethereum smart contract security analysis tool. Softw. Practice Exp. 51(10), 2065–2084 (2019). https://doi.org/10.1002/spe.2745
Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS 2016, pp. 254–269. Association for Computing Machinery (2016)
Mossberg, M., et al.: Manticore: a user-friendly symbolic execution framework for binaries and smart contracts (2019)
Nikolić, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, pp. 653–663. Association for Computing Machinery (2018)
Schneidewind, C., Grishchenko, I., Scherer, M., Maffei, M.: eThor: practical and provably sound static analysis of ethereum smart contracts. In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS 2020, pp. 621–640. Association for Computing Machinery (2020)
Stephens, J., Ferles, K., Mariano, B., Lahiri, S., Dillig, I.: Smartpulse: automated checking of temporal properties in smart contracts. In: 42nd IEEE Symposium on Security and Privacy. IEEE (2021)
Tikhomirov, S., Voskresenskaya, E., Ivanitskiy, I., Takhaviev, R., Marchenko, E., Alexandrov, Y.: Smartcheck: static analysis of Ethereum smart contracts. In: WETSEB 2018, pp. 9–16. Association for Computing Machinery (2018)
Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.: Securify: practical security analysis of smart contracts. In: CCS 2018, New York, NY, USA. Association for Computing Machinery (2018)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Jain, N., Kaneko, K., Sharma, S. (2022). SKLEE: A Dynamic Symbolic Analysis Tool for Ethereum Smart Contracts (Tool Paper). In: Schlingloff, BH., Chai, M. (eds) Software Engineering and Formal Methods. SEFM 2022. Lecture Notes in Computer Science, vol 13550. Springer, Cham. https://doi.org/10.1007/978-3-031-17108-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-031-17108-6_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-17107-9
Online ISBN: 978-3-031-17108-6
eBook Packages: Computer ScienceComputer Science (R0)