Unitimes 第二期AMA前瞻： 安全领域的新星如何拯救区块链生态？

请看以下案例：

• 2018年4月22日，BEC市场瞬间蒸发64亿人民币，黑客利用以太坊ERC-20智能合约中BatchOverFlow漏洞，攻击了美链BEC的智能合约；

• 2018年4月25日，各大交易所暂停SmartMesh(SMT)的充值和提现交易， SMT也曝出存在安全漏洞；

• 2018年5月23日，EDU(EduCoin)被爆出现合约漏洞，多达数十亿代币被盗；

• 2018年7月9日，加密货币交易平台Bancor因调查其“安全漏洞”停止运营，被盗代币的价值超过1200万美元。

“据网络安全公司Carbon Black的调查数据显示，2018年上半年，有价值约11亿美元的数字加密货币被盗，且在全球范围内因区块链安全事件损失金额还在不断攀升。”

——腾讯安全《2018上半年区块链安全报告》

众所周知，区块链安全问题一直为人诟病。那么，到底如何构建一个安全的区块链生态？

或许，CertiK能给你答案。

CertiK是一家智能合约及区块链生态安全服务提供商，采用形式化验证将智能合约转化为数学模型，通过逻辑上的推理演算来验证模型，从而证明智能合约的安全性。其核心产品为CertiKOS防黑客操作系统。

基于CertiK技术构建的CertiKOS，是世界上第一个被完成形式化验证的操作系统内核，被称作“无漏洞且防黑客的系统”，曾引起国内外轰动，被部署在多个安全领域。

在区块链应用中，由于区块链的不可篡改性，智能合约一旦上线并出现安全隐患，对用户造成的损失是巨大且不可挽回的。一旦出现黑客事件，需要整个社区的共识才能回滚交易，所以每次遭受攻击都回滚交易也是不现实的。因此，区块链应用开发的过程需要用大量的测试和检验以获取足够的安全性。

传统的验证方法主要是模拟和测试，即通过实验对系统进行查错。一般的方法是，在一端按系统要求或者自定义输入，观察在另一点的输出。这种方法耗费大量的时间，而且由于实验所能涵盖的系统行为有限，很难找出所有的潜在错误。

而形式化验证是使用数学方法严格证明一个程序正确性的过程。形式化验证方法可以检查程序的各种属性，如公平性、可达性、有界性和无状态二义性等，从理论上对程序做了全面检验，合格即被认为安全。

CeriK系统利用形式化验证理论，希望帮助用户构建无法被黑客攻破的智能合约，其运作步骤是：

1. CertiK客户端将智能合约源代码提交给CertiK系统；

2. CertiK将代码的验证问题转换成类似的数学问题，将问题分解成子任务并广播到CertiK网络；

3. CertiK节点协作解决这些数学问题以换取奖励；

4. CertiK汇总各节点发现的问题及解决方案；

5. CertiK将这些解决方案组装成原始问题的结论，并发回客户端；

6. 最终得出结论代码是否无缺陷，或提示潜在的风险和漏洞。

被誉为“安全领域新星”的CertiK，为解决区块链安全问题带来了巨大希望。

Unitimes非常高兴地宣布，9月2日（周日）晚，CertiK联合创始人顾荣辉教授将应邀参加第二期线上AMA（Ask Me Anything）活动。本期AMA主题为“形式化验证”，具体时间点明天将以海报形式公布，敬请关注！

顾荣辉是哥伦比亚大学计算机科学系终身助理教授。他本科就读于清华大学，2016年在耶鲁大学获得计算机科学博士学位，他还获得了耶鲁大学优秀论文奖和ACM论文奖提名。顾教授是系统软件形式验证方面的专家，是CertiKOS的主要设计者和开发者。

这是一次与顶尖大学教授对话的机会；

这是一个技术探讨和学习的线上课堂；

这一次，你可以来问他关于形式化验证的任何问题！

参与方式：添加社群管理员微信unitimes2017，备注“姓名+第二期AMA"。