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}
}

Document

Short Paper

DOI: 10.4230/LIPIcs.GISCIENCE.2018.42

The Use of Particle Swarm Optimization for a Vector Cellular Automata Model of Land Use Change (Short Paper)

Authors: Yi Lu and Shawn Laffan

Published in: LIPIcs, Volume 114, 10th International Conference on Geographic Information Science (GIScience 2018)

Abstract

Cellular automata (CA) is an important area of research in GIScience, with recent research developing vector-based models in addition to the traditional raster data formats. One active area of research is the calibration of transition rules, particularly when applied to vector CA. Here we evaluate a particle swarm optimization (PSO) process to calibrate a vector CA model of land use change for a sub-region of Ipswich in Queensland, Australia, for the period 1999-2016. We compare the results with those for a raster CA of the same dataset. The spatial indices of the vector PSO-CA model exceed that of the raster model, with spatial accuracies being 82.45% and 76.47%, respectively. In addition, the vector PSO-CA model achieved a higher kappa coefficient. Vector-based PSO-CA model can be used for the exploration of urbanization process and provide a better understanding of land use change.

Cite as

Yi Lu and Shawn Laffan. The Use of Particle Swarm Optimization for a Vector Cellular Automata Model of Land Use Change (Short Paper). In 10th International Conference on Geographic Information Science (GIScience 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 114, pp. 42:1-42:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lu_et_al:LIPIcs.GISCIENCE.2018.42,
  author =	{Lu, Yi and Laffan, Shawn},
  title =	{{The Use of Particle Swarm Optimization for a Vector Cellular Automata Model of Land Use Change}},
  booktitle =	{10th International Conference on Geographic Information Science (GIScience 2018)},
  pages =	{42:1--42:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-083-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{114},
  editor =	{Winter, Stephan and Griffin, Amy and Sester, Monika},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GISCIENCE.2018.42},
  URN =		{urn:nbn:de:0030-drops-93702},
  doi =		{10.4230/LIPIcs.GISCIENCE.2018.42},
  annote =	{Keywords: Vector cellular automata (CA), Particle swarm optimization (PSO), Land use simulation, Ipswich}
}

Search Results

Documents authored by Lu, Yi

Securing Aptos Framework with Formal Verification

Abstract

Cite as

The Use of Particle Swarm Optimization for a Vector Cellular Automata Model of Land Use Change (Short Paper)

Abstract

Cite as

Thanks for your feedback!

Could not send message