高阶定理证明系统中形式解释器的优化
Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems
摘要：
在最近的出版物中，我们提出了一种新的正式符号过程虚拟机（FSPVM）框架，该框架结合了高阶定理证明和符号执行，用于验证以太坊区块链系统中开发的智能合约的可靠性和安全性，而不会遇到围绕可重用性，一致性和自动化的标准问题。在Coq中基于通用的、可扩展的和可重用的形式存储器（GERM）框架、可扩展的和通用的形式中间程序设计语言（表示为Lolisa，其是使用广义代数数据库的Solidity程序设计语言的大子集）和用于Lolisa的对应的形式验证的解释器（表示为FEther）开发了表示为FSPVM-E的特定FSPVM。它是FSPVM-E的关键组成部分。然而，我们过去的工作表明，FEther标准开发的执行效率非常低。因此，FSPVM-E未能达到预期的验证效果。目前的工作解决这个问题，首先确定三个根本原因的执行效率低的正式解释。然后，我们建立这些原因的抽象模型，并提出相应的优化方案，以纠正所确定的条件。最后，我们将这些优化方案应用于FEther，并证明其执行效率得到了显着提高。
英文摘要：
In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering the 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 (GERM) framework, an extensible and universal formal intermediate programming language, denoted as Lolisa, which is a large subset of the Solidity programming language that uses generalized algebraic datatypes, and a corresponding formally verified interpreter for Lolisa, denoted as FEther, which serves as a crucial component of FSPVM-E. 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. The present work 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
