【得得白话】形式化验证：被注入新灵魂的老技术

区块链行业似乎已经变得波澜不惊了。一边是区块链概念被越来越多的人所知晓，一边是数字货币市场的转凉。虽然潮水已经退去，但在这个过程中，区块链领域也取得了一些实质性的进步。其中，形式化验证（formal verification）的应用就是重要的一个。

两年多前，2016年9月1日，万向区块链实验室肖风在为区块链行业名著《区块链革命》作序时曾写道：“The Dao”事件提醒我们，应该有一个能对智能合约进行事先检验的科学方法，但这方面最先进的技术如形式化验证，目前还处于理论研究阶段。”

但如今，形式化验证已经被正式用于智能合约的安全审计中了。

形式化验证：一套用数学写的法律

谈到形式化验证首先要介绍一下形式化方法。

成都链安科技CEO杨霞曾打了个形象的比方，形式化方法就像一套完备的法律，规定了每个角色能做什么和不能做什么，并对角色之间的关系进行界定。类似于社会系统架构对不同角色进行分类，在承认个体天性的同时，使系统的复杂程度降低了多个维度。

形式化方法最大的特点就是简化和抽象。形式化抽象可以从复杂的事物中抽离出本质，相当于一个精简的解读。举个简单的例子，一个构造复杂的中式凉亭，经过形式化的方法抽象过后，可能只是一个分层的三角形，但这种简化又保留了本质的属性和特征。

形式化抽象过的凉亭

这样看来，形式化方法最大的意义就是简化事物，抽离本质。

而形式化验证，则是用数学中的形式化方法对算法的性质进行证明或证伪，也就是用形式化的代码给检测出算法正确与否。

形式化验证的特性是通过数学或代码的形式制定规范，并对代码进行事先检验。

需要明确的是，形式化验证是一种需要和特定领域结合来发挥价值的一种技术，并不能单独发挥价值。形式化验证并不是一个新技术，但它却可以被不断应用于很多新的领域，包括区块链领域。

专门为系统安全级别高的领域服务，优于传统技术测试

其实形式化验证最开始是被从硬件开始应用的，IBM，AMD，ATMEL，STMicro等等硬件巨头公司都是形式化方法的使用者。另外，军工、航天等领域也广泛应用形式化验证。这些领域的特点都是对系统安全的要求非常高。

早在1994年，形式化验证就被应用于一件硬件公司了，这个公司就是我们熟悉的Intel。

1994年，Intel在奔腾CPU的测试中发现漏洞（FDIV），但考虑到90亿分之一的概率非常之小，奔腾CPU还是被投入了市场。但投入后发现，有不少用户在使用过程中发现中央处理器都不能保证完全正确的运算，导致了用户的恐慌，Intel不得不对奔腾CPU进行了回收。

那一次，Intel损失了47.5亿美金的损失，从那以后，Intel开始广泛使用形式化验证对其硬件产品进行检测，但惨痛的损失无法挽回。

不得不承认，形式化验证比单纯的技术测试的效果要好很多，原因主要在于，形式化验证可以全面地检验系统是否正确，虽然需要更多的时间去建模和燃烧脑细胞。但技术测试一般只是在真实的环境下进行测试，并不能检验出所有的漏洞，漏洞触发的几率也不能与大量投入使用的几率划等号。

形式化验证很适合智能合约

目前，形式化验证已经在区块链领域有了一些落地的应用，主要集中在智能合约的安全验证上。

这也是因为，智能合约安全同样是一个对于系统安全要求非常高的领域,完美与否，在一定程度下，直接决定了人们在区块链上的资产、数据和个人隐私是否安全。

据成都链安科技数据显示，2011年至2018年，由智能合约安全事件导致的经济损失达12.4亿美元。目前，由智能合约安全事件导致的经济损失已经超越交易所，位列第一。智能合约上的一个小小的漏洞，都有可能使投资者的数字资产瞬间归零，无论是The DAO，还是Parity都是如此。

而智能合约又有一旦执行就不可更改的特性，这也就要求智能合约在正是运行之前就保证相对“完美”，而达到这种相对“完美”，形式化验证不失为一个好方法，结合人工检测，可以大程度地搜查出漏洞。形式化验证技术的优势在于，用传统的测试等手段无法穷举所有可能输入，但一旦用数学去验证，整个问题就简单多了。

形式化验证通过数学建模方法对系统进行描述，开发者可以对程序的安全性事先进行审查，排除逻辑漏洞和安全漏洞，从而保证合约的安全，可以有效弥补传统的仅靠人工经验查找代码逻辑漏洞的缺陷。

相对于传统的互联网安全公司的“让Bug展现出来”的安全测试，形式化验证直接从代码自身安全角度出发，防患于未然。而这种“预防”性质的检测正与智能合约的不可更改性相符合。

虽然前期建模过程复杂，需要大量的人力和时间，但对于用户却比较友好，因为模型是事先建好的，所以形式化验证往往操作简单，目前建立的SaaS平台已经可以“一键”搜查智能合约中的漏洞。

但形式化验证也并不是完美的，在一般的情况下，形式化验证可以检测出80%的常规漏洞，但由于很多漏洞是结合业务逻辑的，因此人工符合还是必不可少。

形式化验证虽是军工级别，但是也不能为区块链领域检测出所有的漏洞，漏洞日新月异，不断被挖出，只用不断完善验证模型，结合人工符合以及实况监测，才能最大程度地保证安全。

目前，Imandra、Certik、The Matrix、成都链安、Securify.ch、Runtime Verification、Tezos等区块链领域的公司，都已经开展了智能合约的形式化认证业务，它们通过建立了VaaS平台、公链、以及系统语言将形式化验证应用于区块链领域。至此，形式化验证这个被用于硬件、军工、航空航天的老技术又被赋予了新的灵魂。

相信未来形式化验证会被应用于更多的领域，为更多领域服务，也能更加完善，更加智能。而区块链行业在低谷的时候也能够继续钻研技术，这样才能更加稳健地发展。