Search Results

Documents authored by Park, Junkil

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
DOI: 10.4230/OASIcs.MCPS.2014.94
A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal

Authors: Lu Feng, Andrew L. King, Sanjian Chen, Anaheed Ayoub, Junkil Park, Nicola Bezzo, Oleg Sokolsky, and Insup Lee

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)

Abstract
The emerging network-enabled medical devices impose new challenges for the safety assurance of medical cyber-physical systems (MCPS). In this paper, we present a case study of building a high-level safety argument for a patient-controlled analgesia (PCA) closed-loop system, with the purpose of exploring potential methodologies for assuring the safety of MCPS.
Cite as

Lu Feng, Andrew L. King, Sanjian Chen, Anaheed Ayoub, Junkil Park, Nicola Bezzo, Oleg Sokolsky, and Insup Lee. A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 94-99, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{feng_et_al:OASIcs.MCPS.2014.94,
  author =	{Feng, Lu and King, Andrew L. and Chen, Sanjian and Ayoub, Anaheed and Park, Junkil and Bezzo, Nicola and Sokolsky, Oleg and Lee, Insup},
  title =	{{A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{94--99},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.94},
  URN =		{urn:nbn:de:0030-drops-45263},
  doi =		{10.4230/OASIcs.MCPS.2014.94},
  annote =	{Keywords: Medical Cyber-Physical Systems, Safety Argument, Assurance Cases, Patient-Controlled Analgesia Infusion Pump, Closed-Loop Systems}
}
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 About DROPS Imprint Privacy Contact