对话哥伦比亚大学教授——带你深入了解形式化验证技术

下面由小编针对对话哥伦比亚大学教授——带你深入了解形式化验证技术为您答疑解惑，希望能给您带来有一些有效参考。

在智能合约框架下，事先检查合约本身是否存在机制漏洞，是解决其安全问题的关键。

而形式化验证（Formal Verification）正是用数学方法验证程序的正确性，为智能合约和区块链应用提供安全服务的技术。

9月2日晚8点，Unitimes成功举办第二期区块链技术与应用AMA活动。

我们有幸邀请到了CertiK联合创始人、哥伦比亚大学教授顾荣辉为大家带来了主题为“带你深入了解形式化验证技术”的分享。

本次AMA分为两个环节：固定问答环节自由问答环节固定问答——顾教授从形式化验证的概念说起，图文并茂地介绍了CertiK是如何使用这项技术来为智能合约和区块链应用保驾护航的。

此外，他谈到了CertiK团队的情况及其社区建设的计划。

最后，顾教授还对形式化验证技术的学习和研究者提出了寄语。

以下为具体内容：Q1、顾教授您好，欢迎参加Unitimes区块链技术与应用AMA。

能简要地介绍一下您自己以及您的团队吗？顾：大家好，我是顾荣辉，现在是哥伦比亚大学CS助理教授。

2011年本科毕业于清华大学，2016年博士毕业于耶鲁大学。

致力于软件系统形式化验证的研究，联合创建了CertiK项目，致力于通过深度规范技术，构建可靠安全的区块链生态。

CertiK的另一位联合创始人邵中教授，是耶鲁大学计算机系系主任、终身冠名教授，是形式化验证领域的世界级专家。

2016年，我和邵中教授一起设计并开发了首个经过完全验证的并发操作系统内核CertiKOS。

CertiK有16位工程师，大多是之前Google、Facebook的资深工程师。

我们目前有三位科研人员，我和邵教授在耶鲁与哥大的实验室也会为CertiK持续提供科研成果，光邵教授的实验室就有20位左右的博士生、博士后以及访问学者。

Q2、本期主题是形式化验证，可能有些成员不是特别了解什么是形式化验证，您能用简单易懂的语言解释一下吗？顾：简而言之，“形式化验证”就是通过数学的方法证明程序是“正确的”。

这里的正确性，指的是，程序的实现，与程序员的设计或意图（我们称作规范）是相符的。

V神说过，所有程序的bug，都是由“程序的实现，与程序员的意图之间有区别”导致的。

形式化验证，就是希望通过数学方法，证明没有这种“区别”。

我这里举一个例子：假设左边的是程序员的意图，实现一个算(x+1)的平方。

右边是一段程序，完成了指定的计算。

普通的安全测试，就是找几个输入，看看输出是不是相符。

例如：比如x = 0, x= 1。

如果不相符，立刻就可以找到bug。

可是即使所有测试都满足，也未必说明是正确的。

例如，下面这个错误的程序也满足所有测试。

形式化验证，是试图证明，在所有情况下，两者都相符，证明的过程如下：先用数学上的“结合律”，然后提取公因式，然后交换律，再提取公因数，最后根据平方的定义，可证。

形式化验证，看起来很cool，但是实际非常困难。

之前大家普遍认为“一个像并发式操作系统内核那样复杂的系统，是很难甚至无法完全形式化验证的”。

2016年，在OSDI16（顶级计算机会议）上，我和邵中教授一起展示了CertiKOS，第一次让大家确认并发式操作系统内核是可以被完全形式化证明的。

Q3、您刚刚在介绍中提到了并发操作系统内核CertiKOS，请问您的团队是在什么样的背景下开发了这个系统？顾：首先，操作系统内核，可以被看做当前计算机系统的基础，它的地位相当于区块链世界的公链（或者虚拟机）。

安全性的保证至关重要，传统的安全测试无法满足要求。

可是，对于多核的、并发的操作系统内核，因为太过复杂，之前一直无法通过数学的方法被完全证明。

像我刚才所说，很多科学家认为“一个像并发式操作系统内核那样复杂的系统，是很难甚至无法完全形式化验证的”。

2015年我和邵中教授一起提出了“深度规范”的概念，大概的想法是“形式化验证”的瓶颈，不是在“如何证明”，而是在“如何写出好的意图（或规范）”。

利用这套技术，我们可以把一个复杂系统（并发的，或者分布式的）进行解构、分层，从而更加自动化的进行证明。

我们利用深度规范，实现了CertiKOS，最后被部署到了一个未来机器人上。

当时验收方请来了由谷歌工程师组成的黑客团队进行评测，给出的报告对CertiKOS的描述是“无懈可击”。

Q4、CertiKOS是如何保护区块链项目的？能否举几个具体的例子？顾：CertiK的目标是构建完全可信的区块链生态，我们正在做的事情有如下几件：1）最简单的，我们可以帮助项目方，验证智能合约，保证安全性。

2）其次，我们正在开发一套新的智能合约语言，DeepSea。

在9月8日香港举行ETHIS上，我们的首席科学家Vilhelm Sj?berg会第一次展示这个语言。

DeepSea可以帮助开发者开发更加安全高效的智能合约，并且通过我们设计的被完全验证过的编译器，被编译成bytecode的过程，也是正确的。

3）我们可以与公链合作，保证公链生态的健康发展。

比如我们和NEO、星云链、量子链、本体、ICON、Waves等的合作。