网络空间安全协议智能形式化自动验证技术

国家自然科学基金项目 2020.01-2023.12

项目背景

现如今，针对网络协议的安全威胁与攻击层出不穷，为了保障协议安全，对其进行安全性检测是必不可少的一环。形式化验证是协议安全性检测技术中最全面、可信度最高的一种手段。但是由于安全协议的复杂性，现有的形式化验证技术并不能自动化证明所有的安全协议和相关安全软件，在证明过程中需要专业验证人员辅助计算机完成证明。过高的人力成本和学习成本阻碍了形式化验证技术的进一步发展和运用。

主要成果

本项目提出了网络安全协议自动形式化验证技术SmartVerif，突破并解决了传统形式化自动验证中的状态空间爆炸问题，打破了数十年来安全协议形式化验证难以自动化的壁垒，实现了对网络安全协议的自动化证明。该成果的核心是将深度强化学习技术与形式化验证技术结合，使用动态策略对安全协议进行验证。

成果反馈

该成果的相关论文发表于安全顶级会议Usenix Security Symposium。审稿人给予如下评价：1.“我认为当前工作朝着协议验证的自动化方向迈出了卓越的一步，具有相当的前景。（I think the current work is an excellent step towards a promising direction for automatic cryptographic protocol verification）”。 2. “我预感这为未来的其它改进工作打开了多扇大门。 （I have a feeling that this approach can open doors for other future work trying to improve upon this current work）”。 3. “本方案看起来显著地超越了当前最先进的工作，因为它可以完成协议的全自动验证。（It seems to push the state of the art forward significantly，since it offers fully automated protocol verification） ”。

应用 1：区块链智能合约的全自动形式化分析

智能合约已在多个行业广泛应用，尤其在金融领域发挥着重要作用。以太坊链上智能合约数量已超过5000万个，然而，自智能合约问世以来，由于安全漏洞问题，智能合约多次给用户带来了巨大的安全隐患，导致了巨额经济损失。我们在以上取得的成果基础上，进一步推动了区块链智能合约形式化分析系统FASVERIF的研发，该系统具有以下显著特点：1）实现形式化建模、属性构建、验证三个阶段的全自动化能力。2）能够覆盖包括无限铸币漏洞在内的6类安全漏洞。3）相较于现有的自动化分析工具，具备更高的通用性和精准度。4）在对1500个仍在线运行的智能合约进行随机选择的测试中，发现了14个合约存在严重的Zero-day金融漏洞。相关结果发表于安全顶级会议Usenix Security Symposium。

应用 2：区块链比特币协议的形式化分析

比特币是一种去中心化的数字货币，基于区块链技术，具有有限供应、挖矿奖励和相对匿名的特点。值得注意的是，虽然比特币在加密货币领域具有重要地位，但也可能面临新的安全漏洞挑战。基于SmartVerif，我们对比特币进行了细粒度的形式化分析，发现在比特币矿池协议中存在一个新型安全漏洞，该漏洞可能被利用来盗取矿工的薪酬。

未来展望

我们发现，上述成果不仅可应用于区块链等热门网络协议的全自动安全性分析，其核心思想也可延伸至系统软件、芯片设计等领域的全自动安全分析。未来，我们将在这些方向进一步探索，期望解决或在很大程度上缓解系统及芯片研发过程中由安全问题带来的阻碍。