Detecção de Vulnerabilidades em Contratos Inteligentes Utilizando Arvore Sintática Abstrata
Resumo
À medida que avançamos em direção a novas soluções de aplicações descentralizadas, observa-se um crescente número de contratos inteligentes nas redes blockchain, desde implementações mais simples até as mais complexas e valiosas. No entanto, esse aumento significativo traz consigo uma preocupante quantidade de contratos vulneráveis, que estão suscetíveis a ataques de invasores mal-intencionados com o objetivo de roubar recursos ou causar falhas nas aplicações. O objetivo deste artigo é fornecer documentação sobre a detecção das principais vulnerabilidades do Solidity e apresentar uma solução de detecção automatizada que utiliza técnicas de análise estática para identificar vulnerabilidades em grandes conjuntos de dados de contratos inteligentes. Para tanto, foram realizados testes de desempenho e comparações com as principais ferramentas atuais da área de verificação de contratos inteligentes, nesses experimentos a nossa ferramenta apresentou bons resultados tanto em termos de tempo de execução como em capacidade de detecção em relação às demais.
Referências
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.
Publicado
18/09/2023
Como Citar
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: SIMPÓSIO BRASILEIRO DE SEGURANÇA DA INFORMAÇÃO E DE SISTEMAS COMPUTACIONAIS (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.
