安全聚焦 | CertiK携手OKEX，聚焦区块链技术及业务发展的未来
11月11日在哥伦比亚大学，CertiK与OKEX携手举办全球大学联会。联会现场齐聚众多重量级来宾，人潮涌动，场面异常火爆，由于场地限制，部分来宾甚至置身会场外倾听宣讲，此次活动旨在思维的碰撞，共同探讨区块链领域的发展趋势及未来。
CertiK团队联合创始人顾荣辉教授在接受专访时表示，拥有百分百的安全及信任才可以构建一个健康的区块链生态系统。
区块链的技术在不断的发展，对于很多行业来说，区块链技术的应用为产业带来了大量的收益，但网络安全问题也产生了大量的损失。
TheDAO：因双花攻击导致直接损失5000万美元
BEC：整数溢出漏洞带来50亿美元的损失
EduCoin：整数溢出漏洞带来20亿代币的损失
仅仅在2017年12月这一月中，区块链领域就因黑客损失了6.3亿美元
那么解决办法是什么？
当前市场对于智能合约安全问题的检验途径主要有以下三种：
程序测试：用运行程序的方法，通过输入各种不同的可能性来检测是否存在整数溢出等漏洞问题。这种检测方法的缺点是通常无法百分之百覆盖所有可能的情形，因而不能排除有未能被检测到的漏洞存在。
人工审计：人工审计主要是依靠专家的专业知识去审核代码，筛查可能会出现的漏洞和潜在的规范性问题。但是人工审核的时间成本较为昂贵，并且无论专家的专业知识到达了什么水平，都难免会出现疏漏。
形式化验证：
形式化验证是用数学模型的方式证明合约中没有漏洞。形式化验证会在两个层次上对合约进行保证：
用数学推理的方法捕捉、覆盖合约的所有行为，覆盖所有的可能性，从而保证合约没有漏洞。
公开透明，证明合约的创建者不仅要说明合约做了什么，还要证明合约确实按照创建者的意图执行。
与另外两种检验方式相比，形式化验证的专业化程度更高，它还能从数学层面上证明整个代码的安全性和正确性。因此通过对所有变量的每个可能值进行计算，形式化验证可以对程序进行全面、彻底的检查。
CertiK团队根据此项技术研发，做到了世界上第一个黑客无法攻击的并发操作系统。团队专门提供严格的形式化验证服务，通过使用独有的形式化验证技术，结合静态分析及人工复核等方式全面检测合约的漏洞及逻辑错误。
在区块链领域内，安全是永恒的重心。此次全球大学联会更是将这个主题提升到了新的高度。
我们绝不仅仅是寻找漏洞，而是要消除哪怕只有0.00000001%被攻击的可能性。
了解更多
General Information: info@certik.org
Audit & Partnerships: bd@certik.org
Website: certik.org
Twitter: @certik.org
Telegram: t.me/certik.org
Medium:medium.com/certik
币乎：bihu.com/people/1093109
往期回顾
请点击“阅读原文”访问CertiK官网