20億EDU幣被盜？形式化驗證一鍵檢錯！

矽谷Live / 實地探訪 / 熱點探秘/ 深度探討

CertiK:智能合約和區塊鏈系統的形式化驗證平台

區塊鏈時代，智能合約的安全性被無限放大，一個小小的bug就能導致上億美元的損失。EduCoin(EDU)近日被爆出智能合約存在安全漏洞，可被黑客利用盜取任意地址的EDU。幾天內20億枚EDU被盜，引發價格閃崩，甚至牽連整個幣市。

這個安全漏洞其實非常容易被檢測！EDU智能合約中一transferFrom函數, 主要目的是實現EDU的轉賬: 將一定數量(_value)的EDU從源地址(_from)轉賬到接收地址 (_to):

然而此函數並未檢查轉賬的合法性：

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

因此，即使要轉出的金額超過了允許的限制 (allowed[_from][msg.sender])，轉賬也能成功。黑客就是利用這個漏洞將任意地址的EDU無限制地轉到自己的賬戶。也就是說，任何EDU幣持有者都會面對被洗劫一空的風險。從5月23日起，已有超過20億EDU被盜。

事後看來，EduCoin這個看似是個愚蠢的安全漏洞，其實很容易被忽略，而智能合約上一個小小疏忽，就能導致上千萬甚至上億的損失。

形式化驗證技術能有效檢測安全漏洞並避免類似錯誤的產生。小編帶你們來看看CertiK的自動化驗證平台是如何一鍵查錯的。

CertiK的驗證引擎能夠輕易的檢測到EDU的安全漏洞

我們只需要將這段代碼提交到CertiK的驗證引擎，CertiK就能夠在24.9ms內一鍵檢測到EDU的安全漏洞。如果EDU的智能合約在提交之前能夠利用CertiK做代碼檢查，那麼這些損失是完全可以被避免的。

關於CertiK

CertiK 致力於通過全球領先的形式化驗證技術重構大家對於智能合約和區塊鏈的信任。CertiK 能提供最有競爭力的規模化智能合約驗證服務來保證智能合約和區塊鏈系統的安全性。

CertiK 是來自於耶魯大學，哥倫比亞大學和矽谷的精英團隊，聯合創始人邵中是耶魯大學計算機系系主任/終身教授，20餘年安全領域經驗。聯合創始人顧榮輝，哥倫比亞大學助理教授。

請關注CertiK的電報群https://t.me/certikorg， 關於商務合作歡迎聯繫info@certik.org。

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！