一行代码蒸发64亿？！形式化验证帮你一秒避免悲剧

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

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

区块链时代，智能合约的安全性被无限放大，一个小小的bug就能导致上亿美元的损失。美链(BEC)近日被爆出安全漏洞，被黑客用以太坊ERC-20智能合约中BatchOverFlow漏洞攻击，引发价格闪崩，当日币价几乎归0。除了美链，据英国和新加坡的研究人员统计，超过34000个智能合约都有可被利用的安全隐患。

智能合约的安全问题频频亮红灯，黑客简单的一串数字就能套利千万，让人血本无归。想要保证智能合约能够100%的正确，只有形式化验证（Formal Verification)可以确保这些漏洞完全被检测。具体的方式我们用美链来探讨一下。

美链到底出了什么安全漏洞？

美链这个安全漏洞其实非常简单！美链智能合约中一个batchTransfer函数, 主要目的是实现BEC token的批量转账: 将固定整数数量(_value) 转账到一批接收账号的数组里 (_receivers). 为了实现这样的批量转账, BEC的开发人员, 首先计算需要转账的总金额, 计算的公式是:

总金额 (amount) = 需要给每个接收方转账的额度(_value) x 总共需要转账的账户个数 (_cnt)

然后在确保发送方拥有足够的余额后, 给每个接收方发送转账的额度.

但是, 出了什么问题呢?

在计算 amount = _value x _cnt 的过程中, 开发人员并没有考虑到256位整数数据溢出的可能性.

因此黑客们, 依靠这个漏洞, 成功的余额不足的情况下, 依然从账户中转走了总计2²⁵⁶个BEC Token.

用形式化验证方法轻松检测漏洞

事后看来好像美链这个安全漏洞看起来是个愚蠢的错误，但是类似BEC的安全漏洞其实很容易忽略，而智能合约上一个小的程序上的疏忽，就能导致上千万甚至上亿的损失。

自动化的形式化验证平台很可能能帮助检测和避免类似的错误。来看看Certik的自动化形式化验证平台是如何做到的。

CertiK 的验证引擎能够轻易的检测到BEC的溢出错误

将这段代码提交到CertiK的验证引擎，添加几个标签，Certik的自动化验证引擎能够轻易的检测到BEC的溢出错误。

Certik的形式化验证引擎能够处理这些标签并且能够根据标签来检查代码实现的正确性。如果美链的智能合约提交之前能够被CertiK做安全检测，那么这上亿的损失就能被避免。

关于 CertiK

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

CertiK 是来自于耶鲁大学，哥伦比亚大学和硅谷的精英团队，联合创始人邵中是耶鲁大学计算机系系主任/终身教授、中科大名誉院长、清华大学大师讲习团成员，20余年安全领域经验。联合创始人顾荣辉，清华大学本科、耶鲁大学博士、哥伦比亚大学助理教授。

关于商务合作欢迎联系 info@certik.org

推荐阅读

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

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

卫哲 | 姚劲波 | 胡海泉 

垂直种植 | 无人车

王者荣耀 | 返老还童 

---