【专访】 “寻找代码的圣杯”——程序能证明自己没有 bug 吗？

 “  有人说，数学证明是特别纯粹的，证出来是对就是对，是错就是错。其实这个说法是错误的。我们可能永远都找不到圣杯。归根到底，我们总要依赖于一点点其他的东西。你总需要一个小小的支点。这个支点已经是人类文明的精华了，但它永远做不到 100% 可靠。

寻找软件世界的圣杯

口述 | 郭宇

采访、整理 | 橙皮书

对很多没听说过「形式化验证」的人，你可能暂时没办法理解它背后一些很美的东西。

没关系，今天我想用一个故事向你们介绍这种美。如果你觉得有意思的话，可能也会顺带理解区块链美的地方在哪。

 1 

对我来说，形式化验证是在追寻计算机领域里的圣杯。它要解决的问题，是怎么保证软件里没有 bug 。你肯定会很惊讶，软件有 bug 这件事几乎是一定的。只要涉及到复杂代码，就很难避免出错。

怎么保证它没有 bug 呢？

从计算机出现开始就有很多人在研究这个问题，但一直没人能给出答案。所以，它是一个圣杯。就像一本谁都没看过的武林秘籍。

我大概是 05 年开始搞这个东西的。形式化验证是一个非常小众的研究方向。当时我在安徽的中国科学技术大学里，我们实验室想招研究生，非常难招。因为同学们都跑去研究人工智能了。而形式化验证他们很多人压根就没听说过。

但最近两年，这个非常冷门的研究方向突然火了。主要还是因为区块链横空出世，吸引了很多人进来研究。就像密码学跟着区块链火起来一样。以太坊创始人 V 神一定程度上也助推了「形式化验证」的发展。

那么，到底什么是形式化验证？

我们都知道，代码和程序是逻辑性很强的东西。既然逻辑性很强，那我们当然也可以用逻辑来推理它，论证这个软件到底安不安全、有没有 bug。只不过平常我们所理解的“推理”，可能都是在自己的大脑里进行的。像柯南破案那样，一步步地推演。但现在我们需要把这个推理的过程，用更严谨、更标准的数学和数理逻辑的方式表达出来，让计算机能够看懂——这个东西就叫形式化验证。

 2 

为什么形式化验证会非常小众？

除了因为本身在寻找圣杯外，还有一个原因是它对技术门槛的要求比较高。

如果你想研究形式化验证，首先需要先弄懂这套逻辑系统的“语言”。人们平常沟通的时候，讲话用的是自然语言和文字，很直接，很简单，彼此也很容易听懂。但逻辑语言全部都是符号。你必须先弄懂符号是什么意思。然后，你还要理解怎么把你平常说的话，用这些符号表达出来。这个东西是最花时间的。

一般一个 PHD 刚入门，需要先花上很长的时间，不断看东西，培养这种用符号表达的感觉。像小时候刚开始学造句一样。等你会造句了，最后一步才是开始写作文。也就是把整个推理的逻辑论证出来。“推理”本身又会涉及到很多理论深度的东西。所以总结起来，它对门槛的要求确实比较高。

我研究这个东西十几年了。我是 01 年在科大读研，05 开始研究，07 年 PHD 毕业，然后留在科大当老师。读研的时候，最开始一段时期做的是网络研究，后来才做的形式化验证。做了之后我发现，形式化验证里面有很多特别美的东西。它背后有很多特别美的数学理论。但很少有人能触及到这种美。因为你在触及到这种美之前，需要花费非常多的时间来琢磨。

这点感觉跟区块链挺像的。区块链初看很简单，但是你深入研究，反复去做、去试验，花上一些时间，你才能慢慢领略到区块链背后美妙的地方在哪。

 3 

当时研究形式化验证，我最大的苦恼是一直没能找到合适的应用场景。

我们尝试过很多方向的应用，大多数是操作系统内核的验证，包括很多实时性的内核，比如工业控制、医疗设备、专用芯片这些东西。

我们还尝试过存储芯片方面的应用。闪存芯片上有一层很薄的软件，这层软件非常关键，不能有 bug，因为它要用来确保存储和读取时候不会出错。你平常用 u 盘如果没有在操作系统里退出直接硬拔出来，它就有可能会触及到这层软件的 bug，导致数据丢失。

我们希望把形式化验证那套东西拿过来用，确保这些软件代码里没有 bug。这些应用场景的代码量比较短又足够复杂，所以适合拿来做验证。

只有代码足够复杂才值得做形式化验证，如果代码太简单就不需要了，你让程序员肉眼看一下就能判断有没有 bug 了。

但即使是这样，我们仍然觉得形式化验证在工业应用上的性价比很低。因为工程的变化速度太快了，理论距离实际使用，其实还是有不少的差距。

 4 

这个让人苦恼的现象一直持续到 16 年。那时我开始研究区块链的底层技术。

我看了比特币和以太坊。当以太坊出现后，智能合约冒出水面。我很敏锐地察觉到，这里面其实有一些很适合我们的新机会。智能合约是形式化验证非常理想的一个应用场景。

我马上就和一位朋友商量，要不要一起出来干这件事：用形式化验证的方式搞区块链安全。那个朋友之前在 360 工作，他跟我说，要干，不干你将来一定后悔。他本身也有连续创业的经验，所以我当时就决定：出来创业。

于是今年 4 月份，我们拿了一点钱，就组建了一个团队开始搞。这个团队也是以我之前在中科大的几个学弟为主，还有一些早期就对区块链非常感兴趣的 90 后的小朋友。

 5 

现在很多形式化验证惯用的方法是：弄一个黑盒，然后丢一段代码进去，黑盒再吐出来一个结果：yes or no。

如果是 yes，那就说明丢进去的这段代码没有问题。如果是 no ，就说明代码里有 bug。但这种方式的问题在于，这个盒子本身是个黑盒。你没办法证明黑盒的正确性。所以这种方式更多还是用来找 bug。

比如芯片上的形式化验证就是用“黑盒模式”找漏洞。你把芯片设计图丢进黑盒里，它尽可能去遍历所有的状态，然后找出一个反例，告诉你这里有 bug，在某种情况下可能会出现什么问题等等——但如果找不出来 bug 呢？是代码本身没有 bug 吗？还是黑盒的能力不够，找不出 bug？

所以这一类形式化验证，你需要依赖于黑盒本身的正确性。当然你可以把这个黑盒开源，让全世界的人帮你检查看有没有错误。但很少人有人能这么做。因为这块技术目前还没有做到那么好。

 6 

我们从 05 年开始研究时，采用的是另一种最古老、最传统、也是最笨的办法。但这种方式有一个好处是，当它回答 yes 的时候，它会给出一个证据。这个证据是一个数学证明。就像你小时候在黑板上证数学题那样，把证明过程写出来就没办法造假。老师和同学都可以看到。所有人都可以检查。

理论上这套方法是可以这样做的，但实际上我们还做不到自动化。你肯定希望最理想的情况是直接把代码扔进盒子里，然后就能自动吐出来一个证明。但现在还做不到。这是理论的天花板。

我们现在是半自动化来做这件事。你想象下这个盒子上有一些辅助的把手，当你发现盒子转不动的时候，就需要人工手动去摇一摇，丢进一段代码，吐出来一段证明。这是一个通过人操控的盒子。

其实这个盒子是非常复杂的，上面有很多的把手，需要大量做研究的人不停地摇，而且需要摇上好几年。我们当时跟很多国内的团队聊，他们称我们是原教旨主义。因为像我们这样干的人很少。这种传统的做法没法工业化应用。懂得怎么摇盒子把手的人其实很少很少。但我当时就很坚信，这个看似传统的方法才是未来。

这里面很多人误解了，觉得由人去摇把手很累，但这其实是人类体现自我价值的意义。就像证明“哥德巴赫猜想”是人应该要做的事情，不可能让机器来做。人存在的意义就是在盒子卡住的关键时候去推动一下。

从一开始我就很接受这种哲学观。它就应该这么做。但另一方面，你摇上那么几年这个问题怎么解决？当时我认为，人摇的时间一定是越来越快的。把手会越来越少，盒子会越来越简单。

事实也的确如此。经过十几年的发展，这个方法反而被越来越多的人接纳。因为这个东西跟其他计算机技术的发展是一样的。人们写软件是用一层一层的 stack ，“堆栈”，不断垒起来。这种传统的证明方式之所以低效，是因为它没有软件栈，用的全部是最底层的技术，类似 if、else、and、or 这种非常底层的证明语言，那当然会很累。

但如果你有对应的软件堆栈，有相应的框架和工具，你在很高的抽象层上去做证明，那就不会很累了。你不能因为现在还没有这种技术栈，就说这条方向没有前途。这是我从一开始就非常相信的。事实也验证了是正确的。现在很多人都在往这个方向走。

 7 

为什么智能合约出现后我会非常激动呢？

因为智能合约的代码量也是比较短的，但它对安全性的要求更高。智能合约一旦部署到区块链上就不能再修改，所以它一定不能出错。这些基本的特性就决定了它对形式化验证是有需求的。

再加上区块链的设计哲学是去中心化的，所以想要保证「智能合约的代码里没有 bug」 ，这件事必须用一种去中心化的方式去证明。

也就是说，智能合约发布到网上，如果它能自带一个证明，就是最好的。

我们研究的那套形式化验证的方法，移植到智能合约上就是要去琢磨，怎么做出一些自带数学证明的智能合约模版。

这种自带证明的方式，跟「一个中心化的黑盒直接吐出 yes or no 的结果」相比，它跟区块链的思想是一致的。通过某一个机构为智能合约做安全审计也不是未来。因为它仍然依赖于机构的中心化的权威，无法确保智能合约可信。

而从另一方面来说，这种去中心化的方式效率上会更高。因为生成证明是非常难的，需要大量人类的智慧，但检验证明是很简单的。机器非常容易做。检验的难度，跟代码的行数成正比。哪怕要验证的代码有一亿行，用机器来做检查仍然会非常快，因为可以并行做。

所以我非常坚信，智能合约是我们这种传统的形式化验证方法一个绝佳应用场景。它去中心化的精神也和区块链很像。

8

在我的脑海里，未来所有的智能合约发布到网上都必须带一个自己的数学证明，

这个证明用来：

• 证明你干了什么事

• 证明你的管理员权限

• 证明你的合约对参与各方都是公平的

• 证明你没有后门、你的分红、锁仓机制到底是什么样的

• ……

这是让智能合约更可信必须要做的事情。

带了这个数学证明，对于用户来说，哪怕你看不懂证明过程到底是怎么样的，你也可以随时就用另外的工具去检查这个证明是否正确。

这套检查的工具可以由其他不同的人提供，所有人都可以来做这样的工具。这样就给了用户一个选择，让发布智能合约的人，和负责审计的人，都没办法作弊。

9

很多人听到这里肯定会有一个疑问：这样是不是就解决了我们一开始提到的“圣杯”问题？

其实远远不是。

为一个程序带上一个证明，这个证明写了数学推理的过程，用来论证程序自身没有 bug——但我们都知道，数学推理需要有一些公理作为前提，然后才能往后进行推导。

如果这个前提本身是错误的，推理是不是也就不成立了？

举个例子：密码学里的加密问题。

椭圆曲线签名算法里有一个假设叫离散对数难题。加密算法的安全性依赖于这么一件事：解离散域上的对数是非常非常难的，它的解空间非常大，最后解出来的概率，会远小于一个非常非常小的数。就像在大海里捞针。但如果量子计算机造出来，这个问题就不存在了。所以，「基于这个假设去证明这套密码学是安全的」这件事本身也不可靠了。

在程序里面也是一样的。

比如我想证明 EVM （以太坊虚拟机）里面的一段代码跑出来的返回结果是“1”，那么我需要先把程序的语义表达出来，而这就是代码级的形式化验证会遇到的一个问题：很多编程语言的手册很不完善，因此程序的语义翻译很难做到 100% 精准。

一套编程语言的设计，语义往往会存在模糊的地方。因此，形式化语义的时候就会遇到一个巨大的鸿沟。

EVM 的设计水平已经算是比较高的了，以太坊黄皮书对语义的描述写得很清楚，所以它可能是有 99.99%的准确度，但也不是 100%。最终翻译到形式化验证里，理论上还是有可能存在问题。如果有问题，推理的过程和实际在 EVM 上跑的过程，二者就不一致了。这样推理过程本身就不可靠，所有的证明就没有意义了。这个偏差是一定存在的。

形式化验证还有一个严重的依赖，是推理的逻辑本身。换句话说，就是推理的逻辑本身有没有问题。这点也是有可能会受到质疑的。

逻辑学至今已经发展了好几百年，有本神书叫 GEB ——《哥德尔、艾舍尔、巴赫》，里面也谈到了这个问题。哥德尔是个超级聪明的人，他在 1931 年提出一个定理叫“哥德尔第二不完备性定理”。这个定理在说一个什么事情呢？给定一个逻辑推理系统，你需要证明这个系统自洽不自洽。

所谓的“自洽”是指在这个逻辑系统里没有前提的情况下无法推出 False。用人话来说，你的逻辑不能前后矛盾。所谓的自洽系统，就是你永远不可能说出自相矛盾的话。但“自洽”是需要证明出来的。一旦你要证明这个逻辑系统是自洽的，你就必须用一个更复杂的逻辑系统来证明。这个更复杂的逻辑系统又需要一个超级复杂的逻辑系统来证明它的自洽。

哥德尔第二不完备性定理明确提出：不可能有一个系统能证明自己自洽。它甚至很明确的找到反例说，如果你找到了一个系统能证明自己的系统逻辑自洽，那么你的逻辑就不自洽。GEB 这本神书就在谈论这个问题背后的整套哲学系统，整本书大概七百多页，非常长，也很深，到现在我也才看了三分之一。

我们在形式化验证里用来推理程序所用的逻辑，它有没有问题呢？其实它也是个黑盒。但这个黑盒跟我上面说的那个黑盒不太一样。它相对比较稳定，不怎么变化。但它背后依赖的数学理论，“自洽性”也还没有人证明过。只是有几个数学家说，这里面大概是没有问题的。

其实在逻辑学上，有很多公理是互相矛盾的。

严格来说，必须真的有人证出来两个公理是不矛盾的、可以一起用，我们才可以去使用这些公理。但这些东西太复杂了，很多至今都没有人能搞懂。

有人说，数学证明是特别纯粹的。证出来是对就是对，是错就是错。其实是因为他可能不太理解这套东西。搞逻辑学的人都知道，很多公理单独使用可能没有问题，但你再加入一个公理，这个系统还能否自洽就是未知的了。因此，很多数学家会凭着自己的直觉加进去，觉得没问题，但具体有没有证明过呢？需要另一套更复杂的逻辑。

这里面是有很多开放性的问题。有很多不同的选择。我们在做的时候，倾向于不去轻易引入一些甚至很有名的公理。能不用就不用。比如反证法，反正法会跟很多公理发生矛盾，如果用了，说不定哪天就出问题了。

10

所以，我们可能永远都找不到圣杯。

归根到底，我们总要依赖于一点点其他的东西。你总需要一个小小的支点。而所依赖的这个支点，需要做到尽量可靠。但你永远做不到 100% 可靠。

当然，我觉得这个支点已经是人类文明的精华了。因此还是比较可靠的。

这里面还有很多非常有意思的故事。这也是为什么我会说它们背后有很多很美的东西。只是了解的人不多而已。

11

那么，形式化验证跟大家更熟悉的密码学，他们之间有关系吗？

有关系。

我个人觉得，密码学这套历史有一条线，可以把它分隔成两半。在这条线之后，密码学所有东西你要证明可靠；而在之前，你往往不需要证明，全靠经验。

如果你现在随便去买一本密码学的书，大概率翻开，第一章会讲“对称加密”、第二章讲“非对称加密”、第三章讲“哈希、随机数”。这些东西都是没有证明的，只是教你怎么用而已。所以到头来，你可能只是背了一堆的算法。这叫前密码学。

但现在不一样了。现在如果你自己想提出一个密码学的东西，你必须先证明它的安全性。所以从某个时候开始，这在学术上称作 Provable Security，“可证安全性”。如果现在新提出一个哈希函数是没证明过的，那没有人敢用。现代一点的密码学的书，从一开始就要证明「为什么是安全的」。

所以就需要先定义什么叫“安全”。

有很多不同种类的攻击模型。“安全”指的是在某一种攻击模型下的安全。也就是说，一个算法在某个攻击模型下被证明是安全的了，那在现实生活中也不一定是安全的。因为实际的安全环境，可能跟理论上的攻击模型会不一样。比如零知识证明、多方安全计算，都有他们各自的安全模型前提。你选了一个密码学算法，你就要知道算法的安全模型是什么。你必须搞懂每一种安全的前提和假设，才能不出错。

每一个后现代密码学书，英文书居多，一上来就要证明安全性。一直证明到，某个算法在某种攻击模型下被攻破的几率，小于一个可忽略值，一般是 2 的 n 次方之一，才可以。

近年来密码学开始逐渐有了更多现代化的工具去做证明。这种证明不是写在纸上那种，因为里面的逻辑是越来越复杂的，写在纸上没人看得懂，万一跳步了怎么办呢？所以要用特殊的程序和工具去证明，保证每一步都执行。而且每一步的引理都必须写得非常清楚，不能有模糊的地方。

密码学现在几乎都是这样。你要提出新东西，都必须要证明。包括分布式协议也要证明。如果不证，就说明它有的地方没考虑清楚。有证明，才代表一个协议所有的角落都排查过了。

所以我认为，未来在区块链领域，证明也是会越来越重要的。

12

对区块链行业来说，未来成熟的生态里，智能合约必须具备三个关键要素：

1、安全。

保证代码没有漏洞。这是大部分搞安全的人正在做的事情，也是比较基础的东西。但我个人觉得，这件事其实并没有那么有趣。

2、可信。

可信其实是目的。就是让用户信任某个智能合约。比如最近 fomo3d 很热，但没人知道这个合约对所有人是否都是公平的。它里面部署了很多不同的合约，有的合约是不开源的。即使开源了，里面的逻辑比较复杂也没那么容易能看懂。因此智能合约想要可信，最好合约作者的每个声明都必须有配套的证明。这个证明必须和代码挂钩在一起，不管是源代码还是编译后的字节码。

3、规范。

现在很多项目需要多个合约互相交互，所以不同合约之间就必须要有规范。比如，去中心化交易所其实就是一个智能合约。这个智能合约与其他 ERC20 代币的合约进行交互，互相兑换。去中心化交易所要上通证时候，审计智能合约有时候会重点去看，这个代币的管理员有没有权限冻结 token。如果有权限，那就很危险。

所以我们发现一个很有意思的现象，国外很多做金融 DApp 的公司，到最后都变成了一个合约审计的公司。因为没有审计公司能帮他们干，他们自己审核了一堆智能合约后，就有这个能力去帮别人审计合约，就可以去接这块业务了。现在的智能合约本质上都不存在规范。ERC20、ERC721 这些标准都很粗糙。我们手上有形式化验证的工具，也会帮去中心化交易所审计合约的代码，这样效率会比较高。

我们发现规范性这个问题是很严重的。太多的智能合约缺少规范，因此很容易产生很多兼容性问题。比如我们都知道 ERC20 里有一个变量叫 symbol，是用来表示代币的名字，是叫“比特币”还是“以太币”。这个 symbol 的字母大小写完全是混乱的，因为它没有具体的规范，规定必须怎么写。再比如函数执行失败要不要return false，还是不return？这里也有很多东西没写清楚。因为没写清楚，大家就各做各的，导致最终的接口不一致。于是很多合约充值就会有漏洞。

我认为合约只有规范了，DApp 才能真正繁荣起来。不仅仅只是 ERC20 这个合约标准，还有许多合约标准都有规范性问题。未来我们很有可能会在 ERC20 上面再搭一个栈，比如去中心化交易所，然后去中心化交易所上面再搭一个金融借贷类的栈，再往上还可以搭金融衍生品、资产管理——但你每往上搭一层，每一层都必须规范。只有每一层都打牢固了，才能造出高楼。

13

我个人相信，区块链安全会是一个细分行业。而且它一定会不断细分下去。

区块链公司跟很多传统公司不一样。传统公司一定要做大，要把很多业务进行整合，因为只有整合才能发挥优势。就像 BAT，每家都做外卖，每家都做支付，什么业务都有。归根到底，它只有把自己整合起来变成怪兽才能胜出。

但区块链行业反而是，做好自己最擅长的事情就是最好的。因为区块链本来就是用来解决生产关系的。传统公司需要有一个老板发号施令让员工往同一个方向走。区块链行业是发现一个规律能挣钱，那大家就会自发往那走。

所以通过区块链已经可以解决传统公司的一些问题了。很多时候，你和别人之间是互惠关系。这种互惠关系加上 token 绑定，就会成为一个小圈子。

就像现在的链圈，它不是一个公司，就是一个小圈子，组织形式非常松散，但又有一致的利益绑定。这种运作方式远比一个公司的效率来得高。为什么区块链行业发展速度都很快也是因为这个原因。没有老板，三人成军。发展非常灵活。所以我认为，区块链公司不一定需要做大。

智能合约让人们协作的成本变得很低。这也是我们选择以智能合约为中心做形式化验证业务的一个原因。只不过现阶段它还不挣钱。但这个方向，它跟传统 BAT 的业务不太一样。所以这些巨头公司也没办法进来。

智能合约天生对协作就是友好的。而大公司想的是一定要把别人收购，这样我们才能一条心。但同时，大公司各部门间的协作又会产生很多内耗。这是传统公司不可避免的弊病。所以从这个角度来看，小公司也许更有优势。未来我们认为会出现越来越多的小公司。

14

公链的安全和智能合约底层的安全，其实仅仅只是区块链安全领域的一小部分。未来更重要的部分也许是上层业务逻辑的安全。

现阶段我们看到的大部分的漏洞是底层的漏洞，比如各种溢出。这是因为现在大家还不了解区块链技术，行业里的程序员没有经过行业的教育。但未来大家会变得越来越聪明，底层非常低级的安全漏洞会越来越少。

而上层业务会随着整个行业的发展变得越来越复杂，可能出现的漏洞也会越来越多。代码的行数在变大，智能合约的数量也在增加。而业务漏洞是安全审计公司做不来的，工具也做不到自动化检查。因为工具无法理解高层的业务意图，传统的安全公司也没办法解决这个问题。没有完善的工具，配套人才非常稀缺。因此，区块链安全是一片蓝海。

今年 9 月初，我会在一个学术会议上做报告，给高校的人讲「什么是智能合约」。他们很多都没听说过智能合约，但一旦他们听说了，很多人可能就会进来这个行业。因为这些做形式化验证研究的老师，他们会很敏感地察觉到，智能合约是一个大金矿。现在还没有多少人在挖。我可能不需要跟他们讲具体怎么在智能合约上做形式化验证，只需要给他们讲智能合约现在面临哪些问题，他们就能意识到这一点。因此，很多高校类的老师出来创业，这可能也会成为区块链的一个趋势。

能读完文章的都是真爱。如果你希望了解更多关于「形式化验证」与「区块链安全」的秘密，转发这篇文章到朋友圈并配上文中最打动你的一段话，截屏发给小安姐姐（微信号secbit_xiaoanbi），她会把你加入到 SECBIT 区块链爱好者的群里。

安比（SECBIT）实验室专注于区块链与智能合约安全问题，全方位监控智能合约安全漏洞、提供专业合约安全审计服务，在智能合约安全技术上开展全方位深入研究，致力于参与共建共识、可信、有序的区块链经济体。

安比（SECBIT）实验室创始人郭宇，中国科学技术大学博士、耶鲁大学访问学者、曾任中科大副教授。专注于形式化证明与系统软件研究领域十余年，具有丰富的金融安全产品研发经验，是国内早期关注并研究比特币与区块链技术的科研人员之一。研究专长：区块链技术、形式化验证、程序语言理论、操作系统内核、计算机病毒。

安比(SECBIT)实验室

info@secbit.io