20亿EDU币被盗？形式化验证一键检错！

硅谷Live / 实地探访 / 热点探秘 / 深度探讨

---

CertiK:智能合约和区块链系统的形式化验证平台

 

区块链时代，智能合约的安全性被无限放大，一个小小的bug就能导致上亿美元的损失。EduCoin(EDU)近日被爆出智能合约存在安全漏洞，可被黑客利用盗取任意地址的EDU。几天内20亿枚EDU被盗，引发价格闪崩，甚至牵连整个币市。

 

EDU到底出了什么安全漏洞？

这个安全漏洞其实非常容易被检测！EDU智能合约中一transferFrom函数, 主要目的是实现EDU的转账: 将一定数量(_value)的EDU从源地址(_from)转账到接收地址 (_to):

然而此函数并未检查转账的合法性：

allowed[_from][msg.sender] -= _value; 

 

因此，即使要转出的金额超过了允许的限制 (allowed[_from][msg.sender])，转账也能成功。黑客就是利用这个漏洞将任意地址的EDU无限制地转到自己的账户。也就是说，任何EDU币持有者都会面对被洗劫一空的风险。从5月23日起，已有超过20亿EDU被盗。

 

用CertiK一键检测漏洞，让漏洞无处藏身

 

事后看来，EduCoin这个看似是个愚蠢的安全漏洞，其实很容易被忽略，而智能合约上一个小小疏忽，就能导致上千万甚至上亿的损失。

 

形式化验证技术能有效检测安全漏洞并避免类似错误的产生。小编带你们来看看CertiK的自动化验证平台是如何一键查错的。

CertiK的验证引擎能够轻易的检测到EDU的安全漏洞

 

我们只需要将这段代码提交到CertiK的验证引擎，CertiK就能够在24.9ms内一键检测到EDU的安全漏洞。如果EDU的智能合约在提交之前能够利用CertiK做代码检查，那么这些损失是完全可以被避免的。

关于CertiK

CertiK 致力于通过全球领先的形式化验证技术重构大家对于智能合约和区块链的信任。CertiK 能提供最有竞争力的规模化智能合约验证服务来保证智能合约和区块链系统的安全性。

 

CertiK 是来自于耶鲁大学，哥伦比亚大学和硅谷的精英团队，联合创始人邵中是耶鲁大学计算机系系主任/终身教授，20余年安全领域经验。联合创始人顾荣辉，哥伦比亚大学助理教授。

 

请关注CertiK的电报群https://t.me/certikorg， 关于商务合作欢迎联系info@certik.org。

---

推荐阅读

区块链报告 | 脑机接口报告 

硅谷人工智能 | 斯坦福校长

卫哲 | 姚劲波 | 胡海泉 

垂直种植 | 无人车

王者荣耀 | 返老还童 

---