Academic Journal
Securing Aptos Framework with Formal Verification
| العنوان: | Securing Aptos Framework with Formal Verification |
|---|---|
| المؤلفون: | Park, Junkil, Zhang, Teng, Grieskamp, Wolfgang, Xu, Meng, Di Giacomo, Gerardo, Chen, Kundu, Lu, Yi, Chen, Robert |
| المساهمون: | Junkil Park and Teng Zhang and Wolfgang Grieskamp and Meng Xu and Gerardo Di Giacomo and Kundu Chen and Yi Lu and Robert Chen |
| بيانات النشر: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| سنة النشر: | 2024 |
| المجموعة: | DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
| مصطلحات موضوعية: | Formal verification, Smart contracts, Aptos Network, The Move language, The Move Prover |
| الوصف: | 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. |
| نوع الوثيقة: | article in journal/newspaper conference object |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | Is Part Of OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024); https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.9 |
| DOI: | 10.4230/OASIcs.FMBC.2024.9 |
| الاتاحة: | https://doi.org/10.4230/OASIcs.FMBC.2024.9 https://nbn-resolving.org/urn:nbn:de:0030-drops-198741 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.9 |
| Rights: | https://creativecommons.org/licenses/by/4.0/legalcode |
| رقم الانضمام: | edsbas.65358040 |
| قاعدة البيانات: | BASE |
| DOI: | 10.4230/OASIcs.FMBC.2024.9 |
|---|