随着区块链技术的发展,区块链安全问题愈发受到各方重视。智能合约作为区块链2.0的核心,其安全性受到更多的关注。形式化符号执行虚拟机FSPVM构建的形式化验证系统能够保障智能合约的安全性,但目前仅有支持验证Solidity编写的以太坊智能合约的形式化验证系统FSPVM-E,且其解释器FEther-E无法支持验证C++编写的EOS智能合约。如何扩展原有的解释器模型结构,使得其支持对EOS智能合约的形式化验证是一个值得研究的问题。本论文以形式化符号执行虚拟机中的解释器FEther为研究目标,将支持Ethereum的实例化FEther在本文中命名为FEther-E,并在原有的解释器模型上做出扩展,提出一种针对EOS智能合约的解释器模型FEther-C++。新模型在中间语言解析器中新增状态分流器模块,使扩展后的模型支持对作用域异常退出操作的形式化;在FEther-E定义的三层语义结构上新增变量语义层,使扩展后的模型支持对变量语法特性的形式化;整合了FEther-E中的各类异常检测代码,通过将异常检测操作分类并制订相应的编写规范,新增了异常检测模块,并细化了异常检测操作;修改了解释器环境变量的结构,新增局部变量作用域表栈和全局变量作用域表,扩展了内存状态寄存器结构,使其支持对作用域变化特性的形式化。本论文给出了两种C++特有的语法特性形式化方案。首先,FEther-C++通过定义变量声明、变量读写和变量销毁操作,以及实现对这三类操作的调用控制流逻辑,完成了对C++变量语法特性的形式化。在第一种语法特性形式化方案基础上,FEther-C++通过构造局部变量和全局变量的形式化定义、实现变量类别的判别逻辑和两种变量访问方式,完成对变量作用域特性的形式化。论文的实验部分给出了两个包含C++语言特性的智能合约代码片段。这两个实验代码片段中包含了变量声明、变量赋值、作用域异常退出、函数参数传递等C++语法特性。该部分实验结果表明通过构造针对EOS智能合约的解释器模型,形式化符号执行虚拟机可以支持验证C++编写的EOS智能合约。同样的由于EOS智能合约语言特性也在其他主流语言如JAVA、Python等中出现,论文提出的框架除了适用于C++编写的EOS智能合约,也可以推广到其他语言编写程序的形式化验证中。