EN
专访 | CertiK联合创始人顾荣辉：从源头开始 阻断黑客之路
“虽然程序漏洞的检测和验证已经引起业界的高度重视，但在区块链行业内，安全问题仍旧频繁发生。如果只检测已经存在的漏洞的话，永远存在被黑客抢先一步的风险。既然这样，我们有没有办法直接开发出一个没有程序漏洞的、可以完全被信赖的智能合约呢？”
CertiK联合创始人顾荣辉在开发者大会上提到了智能合约安全的源头问题。
这无疑是一个非常大胆的想法。毕竟对于软件开发者们来说，开发一个编程语言，意味着还要编写对应的编译器使其能够在不同语言层级的环境下运行，这项工程复杂且庞大，无论是从理论基础还是实操能力方面对都具备极大的挑战。此外，智能合约语言又由于其独特属性以及较高的安全要求，技术壁垒更加难以攻克，让很多资深的开发者都望而却步。
直击源头
2013年，智能合约作为以太坊生态系统的一部分被引入，它允许在不需要第三方的情况下，执行可追溯、不可逆转和安全的交易。然而，由于代码开源、一旦部署则难以修改等特性，智能合约很快成为区块链安全事件的重灾区。黑客利用交易过程中智能合约程序代码出现的漏洞，发起各式各样的攻击。仅2018年一年间，被报道的攻击损失就达到了上亿美元。
大量资金的流失引起了安全公司的注意，进而安全审计、安全验证、漏洞检测等安全手段竞相加入区块链安全赛道。针对现有的智能合约，大部分安全公司都提出了安全解决方案与改进建议。可是对于编写智能合约的的语言本身，即代码漏洞问题的真正“源头”所在，并未得到普遍关注。
一般来说，为了编写智能合约，必须使用智能合约语言（SCL）。在以太坊虚拟机（EVM）上运行的编程语言是Solidity，它是一种面向合约的高级语言。在以太坊网络上编写智能合约的主要步骤是：用以太坊高级语言编写，接着用EVM编译器编译成字节码，最后用以太坊客户端上传到区块链网络。
对已经编写好的程序进行漏洞检查就如同在“事中”预防，却有可能错过“事前”就存在的错误。例如用Solidity来进行以太坊智能合约开发，即使Solidity源代码正确，但在编译阶段，因为编译器版本不同，最后编译到EVM等机器语言中生成代码时，编译器引入新的漏洞，执行依然会出现问题。顾荣辉说： “所以我们的想法是从代码的编写阶段就提高它的安全性，从源头找到就这些存在的安全漏洞并解决它。”
DeepSEA项目为了攻克这些更加底层可能出现的问题与隐患而诞生。
据顾荣辉介绍，DeepSEA是CertiK与耶鲁大学和哥伦比亚大学的科研团队共同主导推进的项目。得益于顾荣辉和另一位联合创始人邵中教授在网络安全、编程语言、形式化验证等领域的深度积累，DeepSEA[L1] 团队具备了发起了技术攻坚战的能力。
DeepSEA致力于构建跨平台的、可信赖的智能合约框架，令使用高级语言编写的智能合约能够准确无误的在例如以太坊虚拟机（EVM）和超级账本（Hyperledger）等平台上进行编译并且保证没有任何安全漏洞，为开发者提供一个值得信赖的开发环境。
作为现下唯一的专门为区块链安全而诞生的编程语言，DeepSEA在与CertiK公司的形式化验证技术做了结合之后，其源代码和编写的智能合约能够输出对应的数学模型，从而转化为可被形式化验证的对象和框架。该模型能被导入到Coq证明辅助器中，让用户能够在Coq中对程序进行基于数学模型的手动或者半自动的证明。该证明辅助器具有非常高的灵活性，可以凭此进行一些非常复杂的安全验证，确保了智能合约从源头到输出过程的安全性。
DeepSEA目前主要包括两部分：一是DeepSEA语言，二是经过验证的安全可靠的编译器。顾荣辉指出，用DeepSEA语言编写的智能合约，能够生成与开发者意图相符的代码规范。当智能合约产生更高级别的安全需求时，可以与CertiK开发的形式化验证技术相结合进行二次验证，用以证明合约的安全性，相当于双层保障。
“我们在语言的设计上引入的还是编程语言的思路，包括它是一个函数式的强类型的编程语言，在设计上更加安全，也更容易帮助使用者找到程序上的安全漏洞。”顾荣辉说道。
总结来说，DeepSEA的优势有三点，首先，DeepSEA语言可以帮助开发者避免不必要的错误，让代码的编写过程更加安全和高效。其次，DeepSEA编译器可以使程序语言安全、准确地从源代码级别被转译到字节码级别，用户不用担心编译器在编译过程会引入新的漏洞。最后，用户可以通过加标签的的方式编写程序规范，能够保证程序规范与开发者的意图没有出入。
“因为源代码的开发其实是在表达一件事，就是告诉我们，如何实现一个合约。而我们则是让开发者来写合约到底是去做什么，到底是什么，从开始的地方，根源处去解决问题。”顾荣辉称。
未来不止于此
尽管当前看来，智能合约因成为区块链安全的“重症灾区”而吸引了大部分的眼球，但作为因区块链安全而生的语言以及编译器，DeepSEA的想像空间显然可以比智能合约更大、更广。
对此，顾荣辉表示：“我们希望DeepSEA不局限于一个区块链的平台上，而是跨平台、全面性的。”
具体的应用场景上，在程序开发层面，DeepSEA框架的搭建从早期就标明该语言可以有效处理编程中的“固有冲突”。如今的主流操作系统和虚拟机管理程序仍然是用类似于C语言的低级语言编写的，而高级的形式化推理和低级的系统编程之间存在着一些固有冲突（inherent Conflict），比如前者是依赖于高抽象级别的丰富理论，后者却必须操控和管理低级别的硬件资源。DeepSEA编译器的出现能够有效解决这个问题。
在应用层面， DeepSEA语言对于自带金融属性的智能合约比如货币交易平台、支付网络，多重签名钱包等提供了安全壁垒加持，能够有效保护用户的数字资产不受侵犯。
据顾荣辉透露，DeepSEA项目得到了包括哥伦比亚大学-IBM区块链中心、以太坊基金会、QTUM量子链在内的科研基金支持。除去资金支持，这些平台还将为DeepSEA提供社区支持，对DeepSEA的各类Demo做社区反馈，帮助其更新迭代。第二是在DeepSEA完成初步设计进行开源化后，能够得到各个平台、开源社区、开发者们的支持。第三是与IBM、以太坊基金会的核心开发人员进行长期的沟通，对DeepSEA未来的应用场景进行探讨。
并且，DeepSEA已经和由IBM、英特尔、埃森哲、JPMorgan等联合提出的区块链开源项目“超级账本”（ Hyperledger）达成了合作关系，可以将DeepSEA对接到超级账本的平台上。
根据DeepSEA的路线规划，将在今年内公布第一个DeepSEA语言版本，完成对首批科研支持伙伴Hyperledger、以太坊、量子链的对接工作。在得到各个平台、生态的支持和反馈以及更多开发者的声音后，预计在明年完善DeepSEA的语言，完成DeepSEA编译器的安全验证工作，并且真正的应用DeepSEA语言编写比较重要的智能合约，进而部署到以上几个平台中。
“未来希望能够对接到更多像以太坊、量子链这样的知名公链上，通过智能合约的语言来打通不同区块链生态，实现智能合约从各个区块链生态或是各个区块链平台上的移植。”面对还有些遥远的未来，年轻的DeepSEA已经按下“enter”键，开始了一往无前的区块链之路。
