项目动态 | CertiK 与 OKEX 联合举办全球大学联会

11 月 11 日在哥伦比亚大学，CertiK 与 OKEX 携手举办全球大学联会。联会现场齐聚众多重量级来宾，人潮涌动，场面异常火爆，由于场地限制，部分来宾甚至置身会场外倾听宣讲，此次活动旨在思维的碰撞，共同探讨区块链领域的发展趋势及未来。
CertiK 团队联合创始人顾荣辉教授在接受专访时表示，拥有百分百的安全及信任才可以构建一个健康的区块链生态系统。
区块链的技术在不断的发展，对于很多行业来说，区块链技术的应用为产业带来了大量的收益，但网络安全问题也产生了大量的损失。

TheDAO：因双花攻击导致直接损失 5000 万美元

BEC：整数溢出漏洞带来 50 亿美元的损失
EduCoin：整数溢出漏洞带来 20 亿代币的损失
仅仅在 2017 年 12 月这一月中，区块链领域就因黑客损失了 6.3 亿美元

那么解决办法是什么？

当前市场对于智能合约安全问题的检验途径主要有以下三种：
1. 程序测试 ：用运行程序的方法，通过输入各种不同的可能性来检测是否存在整数溢出等漏洞问题。这种检测方法的缺点是通常无法百分之百覆盖所有可能的情形，因而不能排除有未能被检测到的漏洞存在。
2. 人工审计： 人工审计主要是依靠专家的专业知识去审核代码，筛查可能会出现的漏洞和潜在的规范性问题。但是人工审核的时间成本较为昂贵，并且无论专家的专业知识到达了什么水平，都难免会出现疏漏。
3. 形式化验证： 形式化验证是用数学模型的方式证明合约中没有漏洞。形式化验证会在两个层次上对合约进行保证：

• 用数学推理的方法捕捉、覆盖合约的所有行为，覆盖所有的可能性，从而保证合约没有漏洞。

• 公开透明，证明合约的创建者不仅要说明合约做了什么，还要证明合约确实按照创建者的意图执行。

与另外两种检验方式相比，形式化验证的专业化程度更高，它还能从数学层面上证明整个代码的安全性和正确性。因此通过对所有变量的每个可能值进行计算，形式化验证可以对程序进行全面、彻底的检查。
CertiK 团队根据此项技术研发，做到了世界上第一个黑客无法攻击的并发操作系统。团队专门提供严格的形式化验证服务，通过使用独有的形式化验证技术，结合静态分析及人工复核等方式全面检测合约的漏洞及逻辑错误。
在区块链领域内，安全是永恒的重心。此次全球大学联会更是将这个主题提升到了新的高度。

CertiK 作者

内容仅供参考 不作为投资建议 风险自担

版权所有 未经允许 严禁转载

☟☟☟