Document Open Access Logo

Securing Aptos Framework with Formal Verification

Authors Junkil Park, Teng Zhang, Wolfgang Grieskamp, Meng Xu, Gerardo Di Giacomo, Kundu Chen, Yi Lu, Robert Chen

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.9.pdf
  • Filesize: 0.6 MB
  • 16 pages

Document Identifiers

Author Details

Junkil Park
  • Aptos Labs, Palo Alto, CA, USA
Teng Zhang
  • Aptos Labs, Palo Alto, CA, USA
Wolfgang Grieskamp
  • Aptos Labs, Palo Alto, CA, USA
Meng Xu
  • University of Waterloo, Canada
Gerardo Di Giacomo
  • Aptos Labs, Palo Alto, CA, USA
Kundu Chen
  • MoveBit, Hong Kong, China
Yi Lu
  • Bitslab, Singapore, Singapore
Robert Chen
  • OtterSec, Bellevue, WA, USA

Cite AsGet BibTex

Junkil Park, Teng Zhang, Wolfgang Grieskamp, Meng Xu, Gerardo Di Giacomo, Kundu Chen, Yi Lu, and Robert Chen. Securing Aptos Framework with Formal Verification. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.FMBC.2024.9

Abstract

The Aptos Framework is a collection of smart contracts written in the Move language that define standard and common on-chain actions for the Aptos Network. As the security and safety of the Aptos Framework is of utmost importance, it has continuously undergone rigorous testing and comprehensive auditing. To further increase the level of assurance, we have formally verified its security and correctness. This involves identifying critical security requirements for each module, creating formal specifications, and subsequently verifying them using the Move Prover. To the best of our knowledge, this represents one of the first instances of formal verification being applied on such a large scale in a smart contract framework. This paper discusses how this rigorous effort ensures a high level of quality assurance for the Aptos Framework.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Formal verification
  • Smart contracts
  • Aptos Network
  • The Move language
  • The Move Prover

Metrics

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

Supplementary Materials

References

  1. Aptos. The Aptos Blockchain. https://aptos.dev/aptos-white-paper, 2022.
  2. Aptos Labs, MoveBit, and OtterSec. Securing the Aptos Framework through formal verification. https://medium.com/aptoslabs/securing-the-aptos-framework-through-formal-verification-14124d1ed660, 2024.
  3. Mike Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter. The Spec# Programming System: Challenges and Directions, pages 144-152. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-69149-5_16.
  4. Certora. Certora Prover Documentation. https://docs.certora.com/en/latest/index.html, 2022.
  5. ConsenSys. Mythril Classic: Security analysis tool for Ethereum smart contracts. URL: https://github.com/skylightcyber/mythril-classic.
  6. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  7. E. W. Dijkstra. On the Reliability of Programs, pages 359-370. Association for Computing Machinery, New York, NY, USA, 1 edition, 2022. URL: https://doi.org/10.1145/3544585.3544608.
  8. David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, and Jingyi Emma Zhong. Fast and reliable formal verification of smart contracts with the move prover (extended version). CoRR, abs/2110.08362, 2021. URL: https://doi.org/10.48550/arXiv.2110.08362.
  9. Ethereum Foundation. Solidity documentation, 2018. URL: http://solidity.readthedocs.io.
  10. Wolfgang Grieskamp, Nicolas Kicillof, Keith Stobie, and Víctor A. Braberman. Model-based quality assurance of protocol documentation: tools and methodology. Softw. Test. Verification Reliab., 21(1):55-71, 2011. URL: https://doi.org/10.1002/STVR.427.
  11. Ákos Hajdu and Dejan Jovanovic. solc-verify: A modular verifier for solidity smart contracts. CoRR, abs/1907.04262, 2019. URL: https://doi.org/10.48550/arXiv.1907.04262.
  12. Ákos Hajdu and Dejan Jovanovic. SMT-Friendly Formalization of the Solidity Memory Model. In ESOP, volume 12075 of Lecture Notes in Computer Science, pages 224-250. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_9.
  13. K. M. Leino. Accessible software verification with dafny. IEEE Software, 34(06):94-97, nov 2017. URL: https://doi.org/10.1109/MS.2017.4121212.
  14. K. Rustan M. Leino and Philipp Rümmer. A polymorphic intermediate verification language: Design and logical encoding. In Javier Esparza and Rupak Majumdar, editors, TACAS, pages 312-327, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-12002-2_26.
  15. Jing Liu and Zhentian Liu. A survey on security verification of blockchain smart contracts. IEEE Access, 7:77894-77904, 2019. URL: https://doi.org/10.1109/ACCESS.2019.2921624.
  16. Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making smart contracts smarter. In ACM Conference on Computer and Communications Security, pages 254-269. ACM, 2016. URL: https://doi.org/10.1145/2976749.2978309.
  17. Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. Finding the greedy, prodigal, and suicidal contracts at scale. In ACSAC, pages 653-663. ACM, 2018. URL: https://doi.org/10.1145/3274694.3274743.
  18. The CVC Team. CVC5. URL: https://github.com/cvc5/cvc5.
  19. Palina Tolmach, Yi Li, Shang-Wei Lin, Yang Liu, and Zengxiang Li. A survey of smart contract formal specification and verification. CoRR, abs/2008.02712, 2020. URL: https://doi.org/10.48550/arXiv.2008.02712.
  20. 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 Conference on Computer and Communications Security, pages 67-82. ACM, 2018. URL: https://doi.org/10.1145/3243734.3243780.
  21. Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett, and David L. Dill. The Move Prover. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification, pages 137-150. Springer International Publishing, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_7.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact