小心！智能合约再爆高危漏洞，两大加密货币直接变废纸！

大家都还记得，前一段时间发生的BEC智能合约的安全漏洞问题。近日，智能合约安全问题再次上演，火币Pro发布公告，暂停EDU冲提币业务，随后EDU智能合约被爆出存在严重漏洞！

在智能合约漏洞频出的背景下，我们利用形式化验证工具对上百个智能合约进行深入分析，又发现一个存在严重安全漏洞的智能合约——RMC代币合约！

这一漏洞造成的影响是，直接把曾经市值300多万美元的RMC和一度飙到0.08美元的UET（UselessEthereumToken），变得一文不值！

RMC漏洞发现细节

下图是RemiCoin (RMC)代币中的一段代码：

这段代码实现了ERC20 代币规范中的transferFrom函数，该函数的功能是用户(_from)向另外一个用户(_to)转账一定数量的代币，但是在该函数中却使用了错误的逻辑，在红色框中要求只有：

allowed[from][msg.sender]

的值小于value时，代码才能继续运行，而下面却进行了：

allowed[from][msg.sender] -= value的操作，

造成了溢出错误，让该函数具有严重的漏洞。

而攻击者就可以利用这个漏洞，不需要私钥即可无限制的将任意账户的RMC币转到指定的账户(_to)，从而导致所有持有RMC币的账户都有可能被盗取，严重危害了用户的财产安全。

RMC代币自去年7月进入交易所以来，代币价格最高时达到近2美元，市值300多万美元。12月，有攻击者对该合约进行攻击，并被爆出漏洞，随后，代币价格一路暴跌，跌至4月份的不到0.02美元。

此时，由于该漏洞导致不需要用户的私钥即可对账户余额进行操作，这使得用户手中的RMC代币也变得毫无价值。

无独有偶，与此类似的是，据悉名为UselessEthereumToken的代币，号称世界上第一个100%诚实的以太坊ICO，也出现了严重的安全漏洞：

上图红框中的逻辑是：

balances[_from] <= _value

且：allowed[_from][msg.sender] <= _value

且：balances[_to] + _value <= balances[_to]

才能进行转账操作，而接下来的运算导致：balances[_to]、balances[_from]、allowed[_from][msg.sender]均产生溢出。

攻击者无需任何私钥，只需调用该函数时，把传入的参数_value设置得足够大，即可操纵_from和_to的账户余额。

最终，这个漏洞使得UselessEthereumToken就像其名字一样，变得毫无价值。

截至发稿前，仍有攻击者利用上述漏洞对两个智能合约进行攻击，下图为攻击者利用漏洞大量盗取RMC币：

下图为攻击者利用漏洞大量盗取UET币：

不容忽视的安全问题

在这些漏洞的背后，往往是由于智能合约开发者的经验欠缺。而如何有效地防止此类漏洞的发生，成为了区块链智能合约开发中工作中的一个难题。安全是这场竞赛的核心赛道，对各方而言，都不容忽视。

那么这类安全事件该如何防范呢？各方又该如何避免漏洞的发生呢？

1. 开发者应该提高自己的安全意识。现在发现的漏洞中，大多是因为直接使用普通的加减乘除符号，但却没有对可能溢出的情况作判断，这就造成了数据溢出的隐患，而解决方法也很简单，使用安全的运算库library SafeMath就可以彻底避免数据溢出的问题。

2. 项目方也应建立自己统一的安全标准，并对照安全标准严格执行，进行逐一检查。在完成代币的智能合约编写后，请专业的智能合约审计公司，对合约代码用形式化验证的方法进行审计，并由审计公司给出详细的审计报告。

   形式化验证方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将此方法应用于智能合约的验证，能以逻辑推演的方式来进行系统性的快速审查，高效地解决智能合约安全漏洞问题，避免了存在漏洞的合约发布后，所造成的严重经济损失。

3. 交易平台应该做好对项目方的审核工作和自身安全防护。对交易平台中的项目，应要求其能提供智能合约安全凭证，避免有漏洞的代币对交易平台的信誉产生不良影响。

普通用户该如何选择代币

短短几个月以来，多个智能合约被曝出存在安全漏洞，除了众所周知的BEC、SMT、EDU、BAI之外，多个在交易平台交易的智能合约代币，依旧存在安全隐患。

对广大普通用户来讲，选择有公信力的交易所在一定程度上可以降低风险；但更为重要的是，在投资代币时要擦亮自己的眼睛，对不熟悉的代币在购买时也要更为谨慎，选择通过专业的代码审计平台审计过的代币合约才能有效地保障自己的数字资产的安全，不然就真的一夜回到解放前了。

关于作者：

杨霞，链安科技CEO，电子科技大学副教授，博士后；区块链形式化验证权威专家，形式化验证理论和方法专家；曾为多家军口单位（神州飞船控制系统，导弹控制系统等）研制关键软件的形式化验证；CCF区块链专委会委员，CC国际安全标准成员。曾担任多家公司的创始人。发表30多篇，申请20多项专利。