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余年安全领域经验。联合创始人顾荣辉，哥伦比亚大学助理教授。
