形式化验证是用数学的方法去证明系统的完备性。当前的形式化验证已经成功用于网络安全协议的证明,并发现了许多漏洞。但是现有的形式化验证方法主要是手工的验证和半自动化的验证。因为协议状态空间的过大会导致内存爆炸的情况发生,因此,对网络安全协议的自动化验证仍是一个挑战。智能合约是一种能根据接收到的信息自动履行合同条款的协议,随着以智能合约为代表的区块链应用的增长,其频发的安全事件也严重威胁着大众的经济财产安全。本文中,为了能对网络安全协议进行自动化验证,作者提出了一款能自动化验证协议的通用框架,我们采用了动态策略的方法,辅助形式化验证工具智能的在定理树上进行路径搜索。与现有的静态策略相比,该方法具有更灵活且不需要人工学习成本的特点。动态策略在经过训练后,能够根据协议自动的对神经网络进行优化,且不需要人工辅助,提高了验证成功的概率。为了解决智能合约中待验证合约数量多且需要较高安全等级的验证的问题,本文提出了一种代币智能合约的形式化建模方法,对5个存在整数溢出漏洞的智能合约进行建模,并使用了本文提出的自动验证框架形式化验证,成功且高效的找出了其存在的整数溢出漏洞。本文所提出的形式化验证框架的动态策略设计思想是:当在定理树中进行随机的路径搜索时,如果定理树中某个节点代表的引理不在正确的路径上时,我们应该给它赋予一个较低的权值。因此我们引入了一种强化学习算法DQN(Deep Q Network)来实现该策略。本文所提出的智能合约形式化建模方法需先对程序的一系列逻辑代码进行建模,再通过演算的方法,证明其安全属性是否得到满足或者是破坏。本文开展的主要工作有:1.为了能让强化学习中的神经网络能对形式化验证逻辑进行学习,本文设计了一种形式化数据提取技术。该技术对验证工具自动生成的中间定理进行了剪枝,提取了相应的逻辑语句来简化描述验证过程,解决了现有的形式化验证数据难以与神经网络直接进行交互的问题。并构建了定理树的存储结构,通过对冗余数据的剪枝以及使用神经网络来辅助定理树进行递归的构建,解决了定理树存储时容易造成状态空间爆炸的问题。2.为了解决监督学习及无监督学习算法因缺少数据集难以进行网络训练的问题,本文引入强化学习中的DQN神经网络到形式化验证中,并提出了一种特征向量的提取方法和判断循环检测的算法。提高了神经网络的通用性以及路径选择的成功率。与监督学习方法相比,该方法不需要提供数据集进行神经网络的训练。3.为了展示本文提出的自动形式化验证框架的应用场景,同时解决智能合约中存在的安全性问题,本文提出了一种代币智能合约的形式化建模方法。通过对智能合约的逻辑代码进行建模,来分析其安全属性是否得到满足或者是破坏。并通过本文的自动化验证框架进行验证后,成功且高效地发现了其存在的漏洞。