当前位置: 玩币族首页 > 区块链资讯 > CertiK：哥大校友会分享问答「从直升机到NASA 军用级安全护盾的区块链应用」

CertiK：哥大校友会分享问答「从直升机到NASA 军用级安全护盾的区块链应用」

2020-07-14 CertiK中国社区来源：区块链网络

2015年夏天，美国亚利桑那州某黑客团队被军方授意攻击波音的“小鸟”（LittleBird）无人军事直升机的计算机系统。“Little Bird”又被称之为“Killer egg”，是由波音公司制造的最轻量级的军用直升机。攻击行为开始前，军方便授予了黑客“小鸟”计算机系统的一部分访问权限。黑客们摩拳擦掌，已被授予访问权限的情况下，如果还没攻下来，怕是不能自称为“Hacker”了。然而戏剧性的是，整整六周时间，这个顶级黑客团队，始终没能攻破“小鸟”的机载飞行控制计算机。这一结果令美国国防部高级研究计划局十分满意。如果为“小鸟”部署的计算机系统可以有效地抵御黑客的攻击，那么这项技术不仅仅适用于军方，而是适用于整个计算机领域。

“小鸟”新系统使用的技术便是形式化验证(formal verification)技术。它的代码就像数学证明一样可靠。

上一篇文章为大家分享了顾荣辉教授在哥大校友活动上发表的演讲，他为大家解答了区块链的安全问题，以及形式化验证如何为区块链安全生态作出建设。演讲中，哥大其他学者对顾荣辉教授进行了采访。下文将走回哥大现场，带你了解那些有关于形式化验证，有关于区块链未来，以及有关于CertiK愿景的答案。
形式化验证特别适合于区块链系统吗？是否有机会在网络安全中更广泛地使用？

顾荣辉教授：形式化验证是一项应用广泛的技术，不仅限于区块链。除区块链外，还可以应用到自动驾驶车辆，以及其他安全性至关重要的设备上，如飞机，火箭等等。目前，形式化验证已被部署到其他技术领域。在区块链中使用形式化验证的特别之处在于：当面对复杂系统时，形式化验证的应用非常困难且成本很高。2016年，我们在减少验证负担方面取得了突破性进展，使其应用起来不再异常昂贵，并且适用范围更广了。形式化验证也非常适用于区块链，它的应用与其他领域和系统应用有很大的不同。一个原因是其他软件系统，可以执行这种运行时监视功能。一旦发生攻击，用户可以很容易地关闭机器以防止被攻击和破坏，这样他们就有时间发现和修复错误、部署补丁、重新启动系统。因此，在这种情况下，即使系统有缺陷，它仍然可以运行，而且你可以找到方法来减轻这些缺陷造成的损失。但是对于区块链系统，情况就不同了。一旦智能合约被上传到区块链中，即使稍后在代码中发现问题(比如TheDAO)，也无法再做进一步的修改。即使是你意识到有问题，你也无能为力。你只能眼睁睁的看着黑客从合约中窃取代币。所以大家都希望智能合约在部署到链上之前是100%正确的，这就是为什么形式化验证非常适合于区块链系统的原因。
你打算将你的技术应用到金融领域吗？这样做对你来说有什么挑战吗？

顾荣辉教授：在区块链和现有的金融机构相关场景中使用我们的技术一定是可行的。今年早些时候被黑客攻击的其中一个智能合约是dForce智能合约，它实际上被认为是一种去中心化金融。该合约对某种金融交易逻辑进行了编码，人们可以参与并使用它进行金融交易。黑客只利用了其中一个漏洞，就窃取了价值2500万美元的加密资产。所以问题可能是：我们可以使用形式化验证来防止这类错误吗?不幸的是，目前答案是否定的。其中一个原因是，一些存在的漏洞，特别是今年早些时候dForce黑客事件中的漏洞，是利用智能合约之间的互连造成的。换句话说，仅仅验证一个智能合约是不够的。我们无法知道在区块链上会部署什么样的金融智能合约。这些未来的合约与已经存在的合约交互，也可能导致漏洞。这就是目前静态形式化验证无法解决这些安全问题的原因。但是我们现在正在哥伦比亚大学研究一些新的方法。其中一种方法是实现智能合约与这些DeFi智能合约交互，但是要将智能合约的后端设计为一个分散的证明引擎。它是动态的，能够提供诸如目前运行的智能合约是否安全等信息。虽然这个概念仍处于早期研究阶段，但我们现在正在探索其可能性。
对较小代码块的验证是否意味着对这些较小代码块之间的交互也进行了验证？如何确保这些项目的所有互动都得到了验证？

顾荣辉教授：让我们回到CertiK证明引擎的工作过程中看一看，如何才能知道最终得到认证的合约确实是经过验证的？我们如何确保每个单独的组成部分都是正确的？

这是我们试图用深层规范技术解决的最根本的一个挑战。首先，在确保一份合约被验证时，重点不在于证明技术本身，而在于规范其组成部分。也就是说，如果要证明一个组件是根据规范验证的，那么该组件的所有行为和潜在漏洞都将被规范捕获。然后，当我们进行组合时，我们试图证明组件及其规范之间的交互是正确的，并且能够正确工作。单个组件被组合成经过验证的、更大的组件时，基本上会产生嵌套的证书，一直到你将所有组件组合成一个单一的、经过认证的合约。
DeepSEA工具链是开源的吗？哪些架构是针对DeepSEA的？
有没有计划添加web目标？

顾荣辉教授：DeepSEA工具链（参考链接1）及其编程语言和编译器，是由哥伦比亚--IBM区块链中心、哥伦比亚数据科学研究所和其他哥伦比亚研究所支持的研究项目。当然，它将会成为一个开源工具。CertiK DeepSEA编译器(目前版本为0.9)的下载量已经很多了，任何人都可以使用它来编辑程序。编译器语言是开源的，并且将有文档来帮助建立开发人员社区。为了供那些想了解更多信息的人下载，我们设立了语言参考手册（参考链接2）。CertiK就此项目与各大企业展开合作，其中包括目前规模最大的数字金融机构之一蚂蚁金服。为了提高这个编程语言的适用性，我们将针对多个平台进行功能开发。目前第一个目标平台是EVM-以太坊虚拟机，随后是IBM的Hyperledger Burrow EVM。现在我们正在开发web组件的后端，并预计在2020年内发布。DeepSEA将作为合作项目中的一部分部署于蚂蚁金服发布的公共平台上，因此DeepSEA也将尽快适配于蚂蚁区块链。接下来，DeepSEA将支持更多的区块链平台。

你的研究成果可以申请专利吗？
如果可以，它们受保护吗?

顾荣辉教授：可以的，比如CertiKOS就申请了专利 (PCT/US18/62883)。为了更多人可以获益于CertiKOS，我们会开源CertiKOS的系统代码和生成的机器可检查证明，任何用户都可以使用这个系统，并且检查证明是不是有效。专利仅仅用来保护生成证明的引擎。所以如果版本更新，使用者需要联系CertiK才能生成新的引擎版本和证明版本。DeepSEA也与之类似，该语言和编译器本身是开源的，但生成证明的引擎是受到专利保护的。
你是否看到了通过API开放技术或以某种方式开源的机会？

顾荣辉教授：我们目前没有API，但证明引擎中将会有一些潜在的用例。API现在还并不能投入使用的一个原因是：人们可以识别现有智能合约中的漏洞，并利用这些漏洞来恶意获取不合法收益。CertiK对潜在可能开发的技术都十分谨慎，并在向普通用户提供访问权限方面持保守态度。但CertiK愿意为有特殊需求的企业提供开源机会。考虑到潜在的开发可能，我们应该更加专注于提供像DeepSEA工具链这样的产品。因为它可以直接帮助你开发正确的程序，而不是先开发，然后再采用事后弥补的工具去堵漏洞。这样一来，证明引擎的API访问对于恶意黑客来说就毫无用处了。
目前CertiK团队扩展计划是什么？

顾荣辉教授：目前，除了纽约总部我们拥有各个部门的员工，北京和首尔的分部主要还是由商务人员及市场工作人员组成。因此CertiK的近期计划是在全球招募更多的研究人员和工程师，并在欧洲和亚洲建立一个技术团队。
深度规范有深度学习的网络组件吗?

顾荣辉教授：深度规范本身是独立于深度学习的，它只是一个框架，帮助你为形式化验证编写规范。但是，你可以在此框架的多个步骤中利用深度学习的相关内容，这样可以帮助进一步减少对人工参与的需求。比如我们基于标签的规范系统，CertiK已经开发了一些深度学习技术来学习程序的设计规范。此外，我们还在验证步骤上利用了深度学习，通过我们的技术库和学习框架来验证部分组件。
写在最后

顾荣辉教授是哥伦比亚大学计算机科学系助理教授，CertiK公司的联合创始人。本科毕业于清华大学，于2016年在耶鲁大学获得计算机科学博士学位。顾荣辉教授是操作系统、软件安全以及形式化验证方面的专家，也是CertiKOS的主要设计者和开发者。CertiKOS是世界上第一个被完全证明的并发操作系统内核，也是通向真正可信的系统安全的里程碑。顾荣辉教授因在系统安全领域的贡献获得SOSP最佳论文奖、CACM（国际计算机协会）Research Highlights奖、哥伦比亚大学Packard Fellowship的最终提名、在耶鲁大学获得杰出论文奖并获ACM学位论文奖提名。本次哥大校友活动中，校方选取了六名在自身专业领域成绩突出的教授，邀请他们分享自己进行的工作及科研成果。目前顾教授本人除了传道受业解惑，同时也在不断壮大以其科研成果CertiKOS为核心的CertiK公司的团队。
无论你是想要全职还是兼职，CertiK都欢迎你的加入！
别忘了这个暑假也是实习的好时机！
招聘及职位信息：
https://jobs.lever.co/certik/中国区的职位申请也可以通过邮件联系我们。
商务（BD）、技术及产品职位（全职）申请，请发送简历到：[email protected]
其他职位申请（兼职及实习）请发送简历至：[email protected]
期待你的加入！