那些被一行代码蒸发1个亿的智能合约，形式化验证了解一下？ | 人物志

「人物志」为区块链大本营（ID：blockchain_camp）着力打造的人物栏目，以「趣味而不失专业，可读而不失深度」为宗旨，每期邀请区块链领域的顶级专家和开发者就行业、投融资、开发、案例、项目实践等展开探讨。

作为以太坊生态的核心，智能合约这几年发展迅速。最早的智能合约，可以追溯到1995年，由密码学家尼克萨博首次提出。智能合约在多方参与、复杂交易的场景中有明显优势。

然而，近期随着智能合约安全问题的频繁出现，智能合约的劣势也愈发明显，包括智能合约如何对实体资产进行控制，从而保证其有效地执行合约；以及如何保证代码完全反应合约方的意志而不出现漏洞等。这些问题所引起的漏洞，使DAO、Parity、BEC等著名项目的市值几乎一夜归零。

再加上智能合约一旦上传即公开且不可更改，因此现在的区块链项目，对于安全性的需求更加迫切。

针对这些安全问题，成都链安科技尝试将原本应用于军工领域的「形式化验证」方法，应用于智能合约安全审计。形式化验证（formal verification）是基于数学建模方法对系统进行描述，通过形式化验证，开发者可以对程序的安全性事先进行审查，排除逻辑漏洞和安全漏洞，从而保证合约的安全。

关于形式化验证的更多细节，近日，我们采访了链安科技创始人/CEO杨霞，就形式化验证的现状、原理以及市场情况作了深入探讨。

以下是与杨霞对话实录。

偶然打开的区块链新世界大门

区块链大本营：我了解到你的主要身份是电子科技大学的教授，在从事区块链之前有怎样的人生经历？

杨霞：我从本科到研究生到博士，一直都在电子科技大学，而且是一路保送过来的，有人说我这是「坐飞机」（笑），之后就顺理成章的留校当老师了。2012年9月开始做形式化验证；2013年，我在美国一所大学的国际级安全实验室以访问学者身份工作和学习了一年。

我为什么要做形式化验证呢？原因在于，我之前一直研究嵌入式操作系统的安全保障技术，别人就问我你怎么证明你的系统是安全的？是不是得找一个方法来证明？于是我开始探索对系统安全性和功能进行证明的方法，于是发现了形式化验证方法。其实形式化验证本来是一个很冷门的领域，受众范围也没那么广，所以基本都是在高校和研究所里在研究。我也将此技术应用于航天、航空、军事等领域的安全关键软件中。

区块链大本营：作为教师，从教育工作到一个区块链企业的创业者，是出于怎样的契机？

杨霞：我接触区块链是2016年著名的DAO系统安全事件，其实那个时候真的没有太在意。不过我有一个朋友在搞区块链，他跟我说你搞形式化验证，能不能去验证一下智能合约的安全，比如针对Dao系统的安全事件。我觉得挺有趣的就去试了一下。那时候我们还没有自动化的工具，只能靠人工进行代码的形式化描述，然后去证明。最后发现，形式化验证方法应用于智能合约安全审计效果不错。

然后我又找来了一个IBM的捐款智能合约（当时的合约不多），也验证了一下，发现了一个「Unchecked Send返回值」的漏洞。所以我们当时觉得，在区块链领域，形式化验证是大有作为的。在去年9月，万向组织的第三届全球区块链峰会上，主办方邀请我做了一个「智能合约形式化验证」的主题演讲，当时引起了大家的关注。

不过那个时候，我们还没有做自动化的工具，要靠人工来做。但人也会犯错，我就想如何提高自动化的能力，减少人工参与度，并且兼容更多区块链平台。这就是VaaS平台建立的原因。

区块链大本营：请简单介绍一下VaaS这个平台。

杨霞：VaaS（Verification as a Services）作为第一个同时支持EOS和以太坊区块链的高度自动化形式化验证平台，具有验证效率高、自动化程度高、人工参与度低、易于使用、支持多个合约开发语言等优点。

主要用于对智能合约进行安全审计，通过对这种「军事级」的安全验证，以提高区块链生态系统的安全性，同时，达到有效控制漏洞风险的目的。VaaS平台的“一键式”形式化验证工具，可精确定位到有风险的代码位置和风险原因，有效的验证智能合约或区块链应用的常规安全漏洞、安全属性和功能正确性，从而提高其安全等级。相关研究成果已申请软件发明专利5项。

揭秘形式化验证技术

区块链大本营：形式化验证跟传统互联网安全公司的做法有什么不同？

杨霞：传统的互联网安全公司是「以攻促防」，而我们是直接从代码自身安全角度出发，来防止不安全事件发生。举个例子，就像一个是西医，有病的时候给你治病，而一个是中医，强调自身抵抗力的提升，自己身体更健康了，就很难生病了。

区块链大本营：形式化验证的原理到底是什么？

杨霞：形式化验证是一种基于数学和逻辑学的方法。具体来讲，在智能合约部署之前，对其代码和文档进行形式化建模，然后通过数学的手段对代码的安全性和功能正确性进行严格的证明，可有效检测出智能合约是否存在安全漏洞和逻辑漏洞。该方法可以有效弥补传统的靠人工经验查找代码逻辑漏洞的缺陷。形式化验证技术的优势在于，用传统的测试等手段无法穷举所有可能输入，而我们用数学证明的角度，就能克服这一问题。

区块链大本营：能举个例子进一步说明一下吗？

杨霞：通过对合约文档和和代码进行形式化的建模，通过数学推理和证明的方式验证智能合约的功能正确性和安全属性。可以发现代码的逻辑漏洞和安全漏洞，弥补人工方式对逻辑漏洞查找的不足。

以近期频发的溢出类安全漏洞属性检查为例，如检查代码

int8 c=a+b

是否存在溢出漏洞，下面展示对这行代码的功能正确性和安全属性的证明过程。

首先，我们对整数类型建模，定义形式化规则：

Int8.repr: Z -> int8

该规则通过截取纯数学整数（取值范围从无穷小到无穷大）的低8位数值得到一个8位长度的机器整数。然后写加法运算的形式化规范，如下：

{a:int8,b:int8} //

设置代码执行的前提条件，保证a和b的类型是8位有符号机器整数;

{c = a + b;} //

加法运算的源码程序；

{(int8.repr(a+b)) /\ ((Int8.repr (a+b)) = (a+b))} ; //

设置代码正确执行的后置条件。

其中，(int8.repr(a+b))描述，

是为了证明代码的功能正确性是否满足，即需要证明源代码是对a和b进行求和而不是求差或任何其他运算逻辑，并且将运算结果转换为int8类型。此外，需要对是否溢出的安全属性进行证明，因此添加后置条件：

((Int8.repr (a+b)) = (a+b))

因为一旦

a+b>int8.max_singed 或

a+b<int8.min_signed 都将导致

(Int8.repr (a+b)) ≠ (a+b)。

最后，根据前置条件证明代码的执行是否满足上述后置条件。如果产生一个不可证明结果，说明程序功能不正确，或者存在溢出安全漏洞。然后根据证明结果，对源程序进行分析修改，然后再重新证明，直到证明通过为止。我们采用这种数学的证明方式将代码形式化描述为公式，并对其属性进行同样对其他逻辑漏洞和安全漏洞进行证明，基于此原理，我们实现了自动化的验证工具，能够方便、快速地验证出代码的功能正确性和安全属性。

巨头来抄怎么办？不怕！

区块链大本营：形式化验证平台的竞争门槛是什么？如何防止被巨头抄袭？

杨霞：一个是门槛比较高，其他人想进来的话可能也不是短期就能进来的，在形式化验证领域，需要有多年的积累。

另外，我认为行业不排斥更多人进来啊，大家在里面都找到各自的位置，市场不是一家就能做完的，谁做的更好，谁做的更快，谁就能占据更多的会场份额。我们已经研制了高度自动化的区块链形式化验证平台，申请多项专利，也跟知名企业开展了合作，例如比原链、布比、火币等。我们对自己的产品有信心，只有高度自动化的智能合约安全审计才能保障审计的准确性和效率。

区块链大本营：在这一领域，目前有哪些公司跟你们有竞争关系，区别在哪？

杨霞：目前国内还没有采用形式化验证的方法进行智能合约安全审计的，我们是第一家，因为我们起步较早。

区块链大本营：你认为从技术角度来看，形式化验证在国内外的差异是否存在？

杨霞：技术上来讲，差别不大。中国人的优势是做事很拼，整个区块链领域，我们的技术发展程度跟国外的差异都不大。而在安全方面，我们这样的公司瞄准的比国外更早，积累也更多。比如我们率先做出了同时支持以太坊和EOS的自动化合约审计工具。

区块链大本营：在研发这套系统的过程中，你们遇到的最大的技术挑战是什么？你们是如何应对的？

杨霞：对于我们来讲，最麻烦的就是区块链的验证跟传统的操作系统等软件的形式化验证不一样，区块链存在的问题是，多个区块链平台，而且存在于多种智能合约开发语言，甚至有的区块链平台，提供多种合约开发语言。这是最大的挑战。

关于应对，只能是一个坑一个坑的去填。虽然我们也做了一个中间的框架层，能更快速的对各个平台的支持，但还是有一些技术的工作要一个个去完成。比如换一个平台之后，要去跟平台适配，为了把我们的工具移植到更多的平台，还是有很多工作要去做。

开发者，别让小白错误毁了大生意

区块链大本营：在你们接手的项目中，比较典型的安全漏洞有哪些？

杨霞：目前看来，还是小白级的错误居多。比如BEC的那个溢出漏洞。还有就是之前爆出来的以太坊平台资深的漏洞，比如短地址攻击，以及拒绝服务攻击等。这些漏洞通过形式化验证都能找出来。

区块链大本营：既然平台都那么不安全，我们该怎样看待这些问题？

杨霞：安全是多方面的，智能合约就不说了，80%都有安全问题；还有DApp层面的，比如前段时间爆出的BiYong漏洞，用明文传送用户信息。剩下一个就是平台自身的安全漏洞了。

就像Windows系统一样，用的人越多，爆出的漏洞越多，被补上的就越多，但其实背后意味着这个平台逐步变得更安全。就像以太坊，大家每天都在骂不安全，但大家都还在用。

区块链大本营：下一步你们有哪些打算？

杨霞：下一步我们会建立技术社区，让所有开发者共同来建立一个安全的区块链生态，把它做得更好。同时，我们将支持更多的区块链平台，解决更多的区块链安全问题，为行业提供更多的安全服务。

区块链大本营：最后一个问题，请以创业者的身份，对那些想要入门区块链的人说几句心里话。

杨霞：其实我最想说的就是，大家要踏踏实实地静下心来做点实事，戒骄戒躁。可能这感觉有点像老师在说教（笑）。区块链是很有意思的一个技术，我将会坚定的把这条路走下去，因为我相信坚持做下去的人会取得最终的胜利！