DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2024.9

Securing Aptos Framework with Formal Verification

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

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{park_et_al:OASIcs.FMBC.2024.9,
  author =	{Park, Junkil and Zhang, Teng and Grieskamp, Wolfgang and Xu, Meng and Di Giacomo, Gerardo and Chen, Kundu and Lu, Yi and Chen, Robert},
  title =	{{Securing Aptos Framework with Formal Verification}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{9:1--9:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.9},
  URN =		{urn:nbn:de:0030-drops-198741},
  doi =		{10.4230/OASIcs.FMBC.2024.9},
  annote =	{Keywords: Formal verification, Smart contracts, Aptos Network, The Move language, The Move Prover}
}

Search Results

Documents authored by Xu, Meng

Securing Aptos Framework with Formal Verification

Abstract

Cite as

Thanks for your feedback!

Could not send message