Detecção de Vulnerabilidades em Contratos Inteligentes Utilizando Arvore Sintática Abstrata
Abstract
As we move towards new decentralized application solutions, we can observe a growing number of smart contracts on blockchain networks, ranging from more straightforward implementations to more complex and valuable ones. However, this significant increase brings along a concerning amount of vulnerable contracts, susceptible to attacks from malicious actors aiming to steal resources or cause application failures. This paper aims to provide documentation on detecting the main vulnerabilities in Solidity and present an automated detection solution that utilizes static analysis techniques to identify vulnerabilities in large datasets of smart contracts. Based on this, performance tests and comparisons were conducted with the leading current tools in the smart contract verification field, In these experiments, our tool achieved good results in terms of both execution time and detection capability compared to the others.
References
Adrion, W. R., Branstad, M. A., and Cherniavsky, J. C. (1982). Validation, verification, and testing of computer software. ACM Computing Surveys (CSUR), 14(2):159–192.
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., and Tonetta, S. (2014). The nuxmv symbolic model checker. In Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26, pages 334–342. Springer.
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M., et al. (1999). Nusmv: A new symbolic model verifier. In CAV, volume 99, pages 495–499. Citeseer.
Clarke, E. M. (1997). Model checking. In Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17, pages 54–56. Springer.
ConsenSys (2018). Mythril. https://github.com/ConsenSys/mythril. Acessado em: 2023.
Dannen, C. (2017). Introducing Ethereum and solidity, volume 1. Springer.
De Moura, L. and Bjørner, N. (2008). Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, 13 TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14, pages 337–340. Springer.
Durelli, V. H., Durelli, R. S., Borges, S. S., Endo, A. T., Eler, M. M., Dias, D. R., and Guimarães, M. P. (2019). Machine learning applied to software testing: A systematic mapping study. IEEE Transactions on Reliability, 68(3):1189–1212.
El-Far, I. K. and Whittaker, J. A. (2002). Model-based software testing. Encyclopedia of software engineering.
Feist, J., Grieco, G., and Groce, A. (2019). Slither: a static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pages 8–15. IEEE.
Green, C. (1981). Application of theorem proving to problem solving. In Readings in Artificial Intelligence, pages 202–222. Elsevier.
Hasan, O. and Tahar, S. (2015). Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition, pages 7162–7170. IGI global.
King, J. C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7):385–394.
Luu, L., Chu, D.-H., Olickel, H., Saxena, P., and Hobor, A. (2016). Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pages 254–269.
Marijan, D. and Lal, C. (2022). Blockchain verification and validation: Techniques, challenges, and research directions. Computer Science Review, 45:100492.
McMinn, P. (2011). Search-based software testing: Past, present and future. In 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops, pages 153–163. IEEE.
Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., and Dinaburg, A. (2019). Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1186–1189. IEEE.
Ndiaye, M. and Konate, P. K. (2021). Cryptocurrency crime: Behaviors of malicious smart contracts in blockchain. In 2021 International Symposium on Networks, Computers and Communications (ISNCC), pages 1–8. IEEE.
SmartBugs (2020). SmartBugs Curated Repository. https://github.com/smartbugs/smartbugs-curated. Acesso em: 8 de junho de 2023.
SmartContractSecurity (2020). Smart contract weakness classification and test cases. https://swcregistry.io. Acessado em 25 de maio de 2023.
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., and Tonetta, S. (2014). The nuxmv symbolic model checker. In Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26, pages 334–342. Springer.
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M., et al. (1999). Nusmv: A new symbolic model verifier. In CAV, volume 99, pages 495–499. Citeseer.
Clarke, E. M. (1997). Model checking. In Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17, pages 54–56. Springer.
ConsenSys (2018). Mythril. https://github.com/ConsenSys/mythril. Acessado em: 2023.
Dannen, C. (2017). Introducing Ethereum and solidity, volume 1. Springer.
De Moura, L. and Bjørner, N. (2008). Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, 13 TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14, pages 337–340. Springer.
Durelli, V. H., Durelli, R. S., Borges, S. S., Endo, A. T., Eler, M. M., Dias, D. R., and Guimarães, M. P. (2019). Machine learning applied to software testing: A systematic mapping study. IEEE Transactions on Reliability, 68(3):1189–1212.
El-Far, I. K. and Whittaker, J. A. (2002). Model-based software testing. Encyclopedia of software engineering.
Feist, J., Grieco, G., and Groce, A. (2019). Slither: a static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pages 8–15. IEEE.
Green, C. (1981). Application of theorem proving to problem solving. In Readings in Artificial Intelligence, pages 202–222. Elsevier.
Hasan, O. and Tahar, S. (2015). Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition, pages 7162–7170. IGI global.
King, J. C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7):385–394.
Luu, L., Chu, D.-H., Olickel, H., Saxena, P., and Hobor, A. (2016). Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pages 254–269.
Marijan, D. and Lal, C. (2022). Blockchain verification and validation: Techniques, challenges, and research directions. Computer Science Review, 45:100492.
McMinn, P. (2011). Search-based software testing: Past, present and future. In 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops, pages 153–163. IEEE.
Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., and Dinaburg, A. (2019). Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1186–1189. IEEE.
Ndiaye, M. and Konate, P. K. (2021). Cryptocurrency crime: Behaviors of malicious smart contracts in blockchain. In 2021 International Symposium on Networks, Computers and Communications (ISNCC), pages 1–8. IEEE.
SmartBugs (2020). SmartBugs Curated Repository. https://github.com/smartbugs/smartbugs-curated. Acesso em: 8 de junho de 2023.
SmartContractSecurity (2020). Smart contract weakness classification and test cases. https://swcregistry.io. Acessado em 25 de maio de 2023.
Published
2023-09-18
How to Cite
ESQUIVEL, Eduardo V. B.; CAMPOS, Josué Nunes; MENDONÇA, Ronan Dutra; VIEIRA, Alex Borges; NACIF, José Augusto Miranda.
Detecção de Vulnerabilidades em Contratos Inteligentes Utilizando Arvore Sintática Abstrata. In: BRAZILIAN SYMPOSIUM ON CYBERSECURITY (SBSEG), 23. , 2023, Juiz de Fora/MG.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2023
.
p. 335-348.
DOI: https://doi.org/10.5753/sbseg.2023.232866.
