文/羊城晚报全媒体记者 李钢

今天聊一个新技术，一个被中国科学家突破的重要技术-通用全自动形式化验证。

看不懂这个名词没关系，除了计算机领域的工作者以外，能一眼看懂的为数不多。

先说说验证什么。

协议，软件，芯片，计算机的世界里，扩展，缺陷无处不在。设计者有心或无意，都有可能。

但是，由于裂缝，缺陷的存在，小则造成的财产损失，重则带来灾难，甚至会威胁到国家安全。著名的如波音的737MAX坠机事件，说明就是因为新设计的飞控软件有BUG。

那么，为了保证安全，就要对协议，软件和芯片在事前进行数学推理尺度上的证明以完成安全突破的发现（这也是国际安全评估的最高标准），这就是形式化验证的意义。

先从区块链链说起

区块链是保护数字系统安全的，但它本身绝对安全么？未必。只要是人造的技术，都会有裂缝。

通常，由于缺乏灵活性，以目前越来越流行的智能合约（区块链的应用层协议）为例，每年都会因为智能合约的安全漏洞而导致数以亿计的经济损失。

通常情况下，作为一种网络协议，智能合约就需要通过协议安全形式化验证替代，来发现其隐藏的漏洞，缺陷。

目前，我们有三种方式，来做协议安全形式化验证：

第一，手工形式化验证-工作量大，人工成本高，理论基础强，自动化程度差，而且不通用；

第二，半自动形式化验证-利用一些工具静态或动态地人工添加规则，自动化程度稍高，但通用性差，很难形式化验证具有复杂的状态的协议；

第三，当前协议安全形式化验证系统-没有一个全自动，通用的通信协议安全形式化验证系统。

破折号后面的内容，就说明了现有的三种方式，有各自的不足。

既然有难点，就会有人去攻关

于是，通用自动形式化验证技术由中国科技大学熊焰团队完成了突破，完成了安全协议通用自动形式化验证系统。

这一技术突破了有史以来网络协议无法进行通用全面形式化验证的壁垒，并且解决了验证状态爆炸的问题。所谓验证状态爆炸，简单来说，就是要对极其复杂的可能逐一进行尝试而导致几年，几十年，甚至几百年无法完成验证。

对智能合约做形式化验证可以分为二个层次：

第一层称为智能合约源程序自动转换为形式化安全模型的系统SMARTMODLE。

第二层称为安全协议通用自动形式化验证系统SMARTVERIF。

这一系统可以自动发现智能合约所有已知和未知类型的安全漏洞，可以广泛扩展广大区块链智能合约的自动形式化验证。

之所以叫做形式化验证，那么就是一种基于数学的验证技术，可以在数学模型上证明协议有没有安全漏洞。其背后的数学理论基础是基于图灵奖得主罗宾·米勒提出的π演算模型。

当下的安全测试（例如，模糊测试）

形象相当于相当于抽检，有可能出现一些安全突破没有被抽检到的情况。

因此，形式化验证在软件的安全评估标准中处于最高等级。经过了形式化验证的软件，协议，芯片，其可信赖度可以保证最高，但也不能说是绝对可信。

熊焰团队的技术突破，将逻辑推理证明和神经网络技术结合在了一起。

作为逻辑推理证明的形式化验证，无法解决状态爆炸问题，而神经网络能够解决状态爆炸问题，但它是一个黑匣子，无法进行逻辑推理证明。

两强相加，各取其长，实现了安全协议的形式化验证。

SmartVerif是一个通用，自动协议安全形式化系统，对于任意一个协议，给定一个安全目标，类似自动挖掘出其所有安全漏洞，可以广泛使用各种复杂协议安全的形式化验证，如WIFI ，5G，区块链链等。

而且，既然是自动化，那么验证的时长将大大降低，实现了“一万年太久，只争朝夕”。

这一技术突破的前景不止于此

前文提到了，该技术也适用于软件和芯片的验证。

熊焰说，软件形式化验证要比安全协议形式化验证的状态爆炸要大的多，目前其主要关键技术已经突破，团队正在开发软件通用自动形式化验证系统，准备不久的将来，对受邀的国内某大型自主操作系统进行形式化验证。

想想看，每天都有多少新软件，特别是安全性要求非常高的软件问世，软件通用自动形式化验证的作用和意义就有多大。

芯片，将是这一技术另一个重要的可以大展身手的领域。

芯片的设计，同样需要高效的形式化验证技术保障其安全可用。

有可能，由于设计缺陷，设计人员所设计的芯片中潜藏着会会影响芯片功能性的逻辑错误，但该错误在流片前提示发现，应用这样的芯片在敏感而安全性要求极高的系统上，会给系统带来潜在的毁灭性危险。最终，当发现逻辑错误后，重新进行流片，会造成巨大的经济损失。

结果，集成电路都是通过国外EDA软件来设计的，这些EDA套件有可能在设计阶段将植入特殊功能的逻辑，称为芯片木马或者。硬件木马。在满足一定条件的时候，可能会实施改变功能，窃取信息，物理破坏，控制系统等攻击行为。

你可能不知道的是，某超级大国曾经实施一个监控项目-即使电脑不联网也能被监控，其背后的原理就是，这些芯片的硬件电路中存在木马或者后门，集成电路芯片中的这些恶意电路可以绕过系统软件的安全防御和用户的设防，实施“电子间谍”行为。

面对这些隐患，传统的芯片功能验证，测试方法很难检测出恶意电路，而传统的集成电路设计流程和方法学也无相应设计安全的措施和手段保障。

而熊焰团队正在突破其关键技术的芯片形式化验证技术，将采用穷尽搜索的方法验证系统，相较与传统的模拟和测试方法，其最大的优点是具有完备性，能够实现全面，彻底的电路验证。(更多新闻资讯，请关注羊城派 pai.ycwb.com)

了解前沿科技，加入羊晚科技爱好者交流群

来源 | 羊城晚报·羊城派
责编 | 陈倩