Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems
In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order logic theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering f...
| Κύριοι συγγραφείς: | , |
|---|---|
| Μορφή: | Άρθρο |
| Γλώσσα: | English |
| Έκδοση: |
IEEE
2018-01-01
|
| Σειρά: | IEEE Access |
| Θέματα: | |
| Διαθέσιμο Online: | https://ieeexplore.ieee.org/document/8531607/ |
| _version_ | 1828977212463775744 |
|---|---|
| author | Zheng Yang Hang Lei |
| author_facet | Zheng Yang Hang Lei |
| author_sort | Zheng Yang |
| collection | DOAJ |
| description | In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order logic theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering from standard issues surrounding reusability, consistency, and automation. A specific FSPVM, denoted as FSPVM-E, was developed in Coq based on a general, extensible, and reusable formal memory framework, an extensible and universal formal intermediate programming language, denoted as Lolisa, and a corresponding formally verified interpreter for Lolisa, denoted as FEther. However, our past work has demonstrated that the execution efficiency of the standard development of FEther is extremely low. As a result, FSPVM-E fails to achieve its expected verification effect. This paper addresses this issue by first identifying three root causes of the low execution efficiency of formal interpreters. We then build abstract models of these causes, and present respective optimization schemes for rectifying the identified conditions. Finally, we apply these optimization schemes to FEther, and demonstrate that its execution efficiency has been improved significantly. |
| first_indexed | 2024-12-14T14:53:21Z |
| format | Article |
| id | doaj.art-67b08bd7be3c4b64a4e564e9cb15b6ee |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-14T14:53:21Z |
| publishDate | 2018-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-67b08bd7be3c4b64a4e564e9cb15b6ee2022-12-21T22:57:03ZengIEEEIEEE Access2169-35362018-01-016703317034810.1109/ACCESS.2018.28806928531607Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving SystemsZheng Yang0https://orcid.org/0000-0002-0165-0000Hang Lei1School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, ChinaSchool of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, ChinaIn recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order logic theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering from standard issues surrounding reusability, consistency, and automation. A specific FSPVM, denoted as FSPVM-E, was developed in Coq based on a general, extensible, and reusable formal memory framework, an extensible and universal formal intermediate programming language, denoted as Lolisa, and a corresponding formally verified interpreter for Lolisa, denoted as FEther. However, our past work has demonstrated that the execution efficiency of the standard development of FEther is extremely low. As a result, FSPVM-E fails to achieve its expected verification effect. This paper addresses this issue by first identifying three root causes of the low execution efficiency of formal interpreters. We then build abstract models of these causes, and present respective optimization schemes for rectifying the identified conditions. Finally, we apply these optimization schemes to FEther, and demonstrate that its execution efficiency has been improved significantly.https://ieeexplore.ieee.org/document/8531607/Formal verificationsmart contractsevaluation strategyinterpreterhigher-order logic theorem provingsecurity |
| spellingShingle | Zheng Yang Hang Lei Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems IEEE Access Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security |
| title | Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems |
| title_full | Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems |
| title_fullStr | Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems |
| title_full_unstemmed | Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems |
| title_short | Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems |
| title_sort | optimization of executable formal interpreters developed in higher order logic theorem proving systems |
| topic | Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security |
| url | https://ieeexplore.ieee.org/document/8531607/ |
| work_keys_str_mv | AT zhengyang optimizationofexecutableformalinterpretersdevelopedinhigherorderlogictheoremprovingsystems AT hanglei optimizationofexecutableformalinterpretersdevelopedinhigherorderlogictheoremprovingsystems |