Document Open Access Logo

Towards Benchmarking of Solidity Verification Tools

Authors Massimo Bartoletti , Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau, Franco Sainas

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.6.pdf
  • Filesize: 0.66 MB
  • 15 pages

Document Identifiers

Author Details

Massimo Bartoletti
  • University of Cagliari, Italy
Fabio Fioravanti
  • University of Chieti-Pescara, Italy
Giulia Matricardi
  • University of Chieti-Pescara, Italy
Roberto Pettinau
  • Technical University of Denmark, Lyngby, Denmark
Franco Sainas
  • EPFL, Lausanne, Switzerland

Funding

  • Bartoletti, Massimo: Partially supported by project SERICS (PE00000014) and PRIN 2022 DeLiCE (F53D23009130001) under the MUR National Recovery and Resilience Plan funded by the European Union - NextGenerationEU.

Cite AsGet BibTex

Massimo Bartoletti, Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau, and Franco Sainas. Towards Benchmarking of Solidity Verification Tools. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.FMBC.2024.6

Abstract

Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them. Most of the current research on the verification of contracts revolves around Solidity, the main high-level language supported by Ethereum and other leading blockchains. Although bug detection tools for Solidity have been proliferating almost since the inception of Ethereum, only in the last few years we have seen verification tools capable of proving that a contract respects some desirable properties. An open issue is how to evaluate and compare the effectiveness of these tools: indeed, the existing benchmarks for general-purpose programming languages cannot be adapted to Solidity, given substantial differences in the programming model and in the desirable properties. We address this problem by proposing an open benchmark for Solidity verification tools. By exploiting our benchmark, we compare two leading tools, SolCMC and Certora, discussing their completeness, soundness and expressiveness limitations.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Smart contracts
  • Ethereum
  • Verification
  • Blockchain

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Leonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, and Natasha Sharygina. Solcmc: Cav 2022 artifact. https://github.com/leonardoalt/cav_2022_artifact/tree/main, 2022.
  2. Leonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, and Natasha Sharygina. Solcmc: Solidity compiler’s model checker. In Computer Aided Verification (CAV), volume 13371 of LNCS, pages 325-338. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_16.
  3. Monika Di Angelo and Gernot Salzer. Consolidation of ground truth sets for weakness detection in smart contracts. In Financial Cryptography Workshops, volume 13953 of LNCS, pages 439-455. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-48806-1_28.
  4. Shaun Azzopardi, Joshua Ellul, and Gordon J. Pace. Monitoring smart contracts: ContractLarva and open challenges beyond. In Runtime Verification, volume 11237 of LNCS, pages 113-137. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03769-7_8.
  5. Massimo Bartoletti, Stefano Lande, Maurizio Murgia, and Roberto Zunino. Verifying liquidity of recursive Bitcoin contracts. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/LMCS-18(1:22)2022.
  6. Thomas Bernardi, Nurit Dor, Anastasia Fedotov, Shelly Grossman, Neil Immerman, Daniel Jackson, Alexander Nutz, Lior Oppenheim, Or Pistiner, Noam Rinetzky, Mooly Sagiv, Marcelo Taube, John A. Toman, and James R. Wilcox. WIP: Finding bugs automatically in smart contracts with parameterized invariants. https://groups.csail.mit.edu/sdg/pubs/2020/sbc2020.pdf, 2020.
  7. Dirk Beyer. Competition on software verification and witness validation: SV-COMP 2023. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 13994 of LNCS, pages 495-522. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_29.
  8. N. Bjørner, A. Gurfinkel, K. L. McMillan, and A. Rybalchenko. Horn clause solvers for program verification. In Fields of Logic and Computation (II), volume 9300 of LNCS, pages 24-51. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23534-9_2.
  9. Certora. The Certora Verification Language. https://docs.certora.com/en/latest/docs/cvl/index.html, 2022.
  10. Certora. Formal verification of OpenZeppelin (may-june 2022). https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/certora/reports/2022-05.pdf, 2022.
  11. Certora. Certora prover documentation: invariants. https://docs.certora.com/en/latest/docs/cvl/invariants.html, 2023.
  12. Certora. Certora prover documentation: Prover approximations. https://docs.certora.com/en/latest/docs/prover/approx/index.html, 2023.
  13. Certora report: CallWrapper. https://prover.certora.com/output/95211/e265c818d176463cbaa6f53e4d0fe394?anonymousKey=7d67af6ba7eedc4f099a133a04f4d36953f377dc, 2024.
  14. Stefanos Chaliasos, Marcos Antonios Charalambous, Liyi Zhou, Rafaila Galanopoulou, Arthur Gervais, Dimitris Mitropoulos, and Ben Livshits. Smart contract and DeFi security: Insights from tool evaluations and practitioner surveys. In ICSE, pages 60:1-60:13, 2024. URL: https://doi.org/10.1145/3597503.3623302.
  15. Consensys. Write smart contract specifications using Scribble. https://consensys.io/diligence/scribble/, 2023.
  16. E. De Angelis, F. Fioravanti, J. P. Gallagher, M. V. Hermenegildo, A. Pettorossi, and M. Proietti. Analysis and transformation of constrained Horn clauses for program verification. Theory Pract. Log. Program., 22(6):974-1042, 2022. URL: https://doi.org/10.1017/S1471068421000211.
  17. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  18. Bruno Dias, Naghmeh Ivaki, and Nuno Laranjeiro. An empirical evaluation of the effectiveness of smart contract verification tools. In Pacific Rim International Symposium on Dependable Computing (PRDC), pages 17-26, 2021. URL: https://doi.org/10.1109/PRDC53464.2021.00013.
  19. Enterprise Ethereum Alliance. Smart contract weakness classification (SWC). https://swcregistry.io/, 2020.
  20. Josselin Feist, Gustavo Grieco, and Alex Groce. Slither: a static analysis framework for smart contracts. In Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pages 8-15. IEEE/ACM, 2019. URL: https://doi.org/10.1109/WETSEB.2019.00008.
  21. Ikram Garfatta, Kais Klai, Walid Gaaloul, and Mohamed Graiet. A survey on formal verification for Solidity smart contracts. In Australasian Computer Science Week Multiconference, pages 3:1-3:10. ACM, 2021. URL: https://doi.org/10.1145/3437378.3437879.
  22. Hossein Hojjat and Philipp Rümmer. The ELDARICA Horn solver. 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1-7, 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603013.
  23. Nikolay Ivanov, Chenning Li, Qiben Yan, Zhiyuan Sun, Zhichao Cao, and Xiapu Luo. Security threat mitigation for smart contracts: A comprehensive survey. ACM Comput. Surv., 55(14s):326:1-326:37, 2023. URL: https://doi.org/10.1145/3593293.
  24. Daniel Jackson, Chandrakana Nandi, and Mooly Sagiv. Certora technology white paper. https://docs.certora.com/en/latest/docs/whitepaper/index.html, 2022.
  25. Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. SMT-based Model Checking for Recursive Programs. Formal Methods in System Design, pages 175-225, 2016. URL: https://doi.org/10.1007/s10703-016-0249-4.
  26. Satpal Singh Kushwaha, Sandeep Joshi, Dilbag Singh, Manjit Kaur, and Heung-No Lee. Ethereum smart contract analysis tools: A systematic review. IEEE Access, 10:57037-57062, 2022. URL: https://doi.org/10.1109/ACCESS.2022.3169902.
  27. Cosimo Laneve. Liquidity analysis in resource-aware programming. J. Log. Algebraic Methods Program., 135:100889, 2023. URL: https://doi.org/10.1016/J.JLAMP.2023.100889.
  28. OpenZeppelin. Utilities / address. https://docs.openzeppelin.com/contracts/4.x/api/utils#Address, 2024.
  29. Anton Permenev, Dimitar K. Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin T. Vechev. VerX: Safety verification of smart contracts. In IEEE Symposium on Security and Privacy, pages 1661-1677. IEEE, 2020. URL: https://doi.org/10.1109/SP40000.2020.00024.
  30. Clara Schneidewind, Ilya Grishchenko, Markus Scherer, and Matteo Maffei. eThor: Practical and provably sound static analysis of Ethereum smart contracts. In ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 621-640. ACM, 2020. URL: https://doi.org/10.1145/3372297.3417250.
  31. The Solidity Authors. SMTChecker and formal verification: contract balance. https://docs.soliditylang.org/en/v0.8.24/smtchecker.html#contract-balance, 2023.
  32. The Solidity Authors. SMTChecker and formal verification: untrusted calls and reentrancy. https://docs.soliditylang.org/en/latest/smtchecker.html#trusted-external-calls, 2023.
  33. Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin T. Vechev. Securify: Practical security analysis of smart contracts. In ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 67-82. ACM, 2018. URL: https://doi.org/10.1145/3243734.3243780.
  34. Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, and Arie Gurfinkel. Verifying Solidity smart contracts via communication abstraction in SmartACE. In Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 13182 of LNCS, pages 425-449. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-94583-1_21.
  35. Scott Wesley and Valentin Wüstholz. Verify OpenZeppelin. https://github.com/contract-ace/verify-openzeppelin, 2022.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact