巨额数字背后，各种原因导致的安全事件还在不断增加。如何构建安全可靠的区块链生态，变得越来越刻不容缓。
近日，腾讯安全联合知道创宇发布《2018上半年区块链安全报告》。《报告》显示，区块链自身机制安全、生态安全和使用者安全三个方面造成的经济损失分别为12.5亿、14.2亿和0.56亿美元，共计高达27亿美元。
巨额数字背后，各种原因导致的安全事件还在不断增加。如何构建安全可靠的区块链生态，变得越来越刻不容缓。
8月5日13:00，应「火星财经创始学习群」轮值群主任铮、副群主廖志宇邀请，CertiK联合创始人顾荣辉做了主题为“CertiK，构建安全可靠的区块链生态”的分享。
他表示，区块链世界一直安全事故频发，但传统的安全技术很难满足要求，CertiK采用了形式化的验证，将智能合约转化为数学模型，通过逻辑上的推理演算来验证模型，从而证明智能合约的安全性。
目前CertiK正在努力更大程度自动化智能合约的验证工作，从而提高验证速度，减少人工介入。
以下为顾荣辉分享原文，由火星财经（ID：hxcj24h）整理：
CertiK一开始是实验室的项目。当时我和邵中教授想研发一个“没有漏洞、无法攻破”的并发式操作系统内核，因为传统的测试技术和形式化验证技术都达不到要求。
2015年我们提出了“深度规范”的概念，并用这套技术做了CertiKOS，最后被部署到了一个未来机器人上。当时验收方请来了由谷歌工程师组成的黑客团队进行评测，给出的报告对CertiKOS的描述是“无懈可击”。
区块链世界一直安全事故频发，但传统的安全技术都无法满足要求，一些知名公链意识到形式化验证对区块链潜在的重要性，联系到我和邵教授的实验室，后来就创建了CertiK公司，致力于提高区块链生态的安全性与可靠性。
邵教授是CertiK的联合创始人，同时也是耶鲁大学计算机系系主任、终身冠名教授，是形式化验证领域的世界级专家。我目前是哥伦比亚大学计算机系助理教授，本科毕业于清华大学，博士毕业于耶鲁大学。
CertiK有16位工程师，大多是之前Google、Facebook的资深工程师。我们目前有三位科研人员，我和邵教授在耶鲁与哥大的实验室也会为CertiK持续提供科研成果，光邵教授的实验室就有20位左右的博士生、博士后以及访问学者。
CertiKOS是利用CertiK技术构建的世界上第一个并发式操作系统内核。从字面上可以看出，CertiKOS=CertiK+OS。
虽然我们一直对社群的发展缺乏经验，但目前CertiK社群规模也已达4万人，推特有8千人关注。我们的投资机构有传统VC（光速中国，经纬中国，丹华等），矿主（比特大陆，嘉楠耘智旗下基金等），交易所（币安Labs，OK，KuCoin，Gate等），加密货币基金（FBG，节点，Kenetic，NGC，SigNum等），以及各大公链平台（NEO，星云链，量子链，本体，ICON，Waves等）。
我们的安全验证服务从5月份开始上线，已经与多家交易所达成了安全战略合作，比如火币、OKEx、Fcoin、Gate、KuCoin、币信等。CertiK已经为多家机构完全了安全验证工作，包括之前登陆币安的Iotex与Quarkchain，以及首发火币的ContentBox。
公链平台方面，我们与NEO、星云、本体、Quarkchain都有安全战略合作。Aelf创新联盟也将我们选作首家安全合作伙伴。
之前大家普遍认为“一个像并发式操作系统内核那样复杂的系统，是很难甚至无法完全形式化验证的”。2016年，在OSDI16（顶级计算机会议）上，我和邵中教授一起展示了CertiKOS，第一次让大家确认并发式操作系统内核是可以被完全形式化证明的。
两年过去了，我们的科研团队仍然是唯一拥有这项技术的。我们认为，区块链系统，比如EVM，是至少与并发式操作系统内核同等复杂，甚至是更加复杂的。所以，相比较于其他团队（包括其他顶级科研单位比如MIT、普林斯顿等），CertiK可能是距离这个目标最近的。
因为智能合约相对来讲比较简单，即使是很老的技术，也是可以进行验证的。目前CertiK正在努力更大程度自动化智能合约的验证工作，已经开始了smartlabeling工作的研发，即自动对合约进行标注，最大程度提高我们的验证速度，减少人工介入。
问答环节：
Q1:Demo里面如何使用的机器学习技术？如何做到自动标注？机器如何知道代码的功能？
A1:CertiK?这个自动化的问题，好像很多从业者还是用比较人工的方式在做验证。嵌入式系统相对较为简单，但像CertiKOS这种通用并发操作系统已经非常困难了。
简而言之，CertiKOS的处理方法是把并发式系统通过分层转化为“分布式系统”的验证，所以和区块链系统的验证工作较为接近。更多细节，可以参考我们最新的PLDI18以及OSDI16的文章。
Q2:目前国际验证平台的情况是怎样的？CertiK的技术优势在什么地方？验证流程如何？如何去解决相对复杂智能合约的验证？如何解决多平台的智能合约验证？如何根据用户的需求来检验智能合约的准确性？
A2:目前国际验证平台有比如Quant Stamp和Open Zeppelin，他们也为很多客户提供了服务，但是他们科研团队的支持较为有限，很难对复杂系统，比如EVM的实现进行验证。
另外比较知名的有runtime verification，他们的创始人Grigore Rosu是UIUC的教授，也是我和邵教授的好朋友。他们使用的技术叫做KFramework，对于并发的及分布式的复杂系统处理能力不够。
关于跨平台的问题，我们的技术理论上是和平台或者编程语言无关的，但是实际中，是需要根据各个平台编写对应的前端，也是为什么我们和很多知名公链有合作，为他们提供定制化的安全验证服务。
在目前的智能合约领域，理论上是不可能完全自动生成代码的，但可以借助机器学习技术添加部分标注，降低人力成本。有两类可以学习的标注：一是对于像loop invariants的这种特殊结构的标注，可以关注我们深度规范社区，很快会有这方面的论文发表；二是对于有较多验证库的合约，比如发币的合约。
Q3:平台会开源吗？在分析eos的webassembly时，有发现什么问题吗？
A3:这套自动化的验证引擎，smart labeling标注手段等都会在之后开源。我们的核心竞争力还是在深度规范技术的专利，这块更多的是服务复杂系统（比如EVM等），短期不会开源。我们觉得为区块链生态提供的基础的安全服务layer是有开源必要的，至少没有闭源的必要。
关于EOS的webassembly，在与EOS官方合作前，我们应该不会主动宣布任何与其相关的漏洞。在此呼吁一下区块链的安全社区，要肩负起社会责任感。
另外，CertiK正在开展一项更为基础的研发工作。我们认为即使是多验证了几个智能合约，多服务了几个交易所，甚至是多弄几个报漏洞得奖励的平台，都不能从根本上改变区块链世界的安全危机。我们在致力于通过区块链系统结构的改变，大幅度提升各个区块链生态的可靠性，更多消息将在年底或明年年初发布。
嘉宾简介
顾荣辉/CertiK联合创始人
哥伦比亚大学助理教授。2011年本科毕业于清华大学，2016年博士毕业于耶鲁大学。致力于软件系统形式化验证的研究，与耶鲁大学邵中教授一起设计并开发了首个经过完全验证的并发操作系统内核CertiKOS。联合创建了CertiK项目，致力于通过深度规范技术，构建可靠安全的区块链生态。
►
本文为火星财经原创稿件，
转载请添加微信：huyalu08，须
在文章标题后注明：“文章来源：火星财经（ID：hxcj24h）”。
点 击 关 键 字 查 阅
[
火星公开课墙裂推荐
]
超脑链郭睿
|
CK-Lab张十一
|
币牛牛
黄锦
BGogo王启恒
|
币优陈勇
|
Chaince吴子臻
|
爱思虫哥
