使用Securify实现更安全的智能合约

让我们面对现实吧。开发智能合约是困难的。在开发智能合约时,需要考虑多个方面的问题:所有代码都要接受公众的审查,事务维护原始要求可能导致可重入行为,随机性在分布式网络中难以可靠地实现,等等。我们不止一次地看到一些引人注目的智能合约漏洞导致了巨大的损失,更可怕的想法是“我们用这些损失的资金授权给了谁?”。
为了开发更安全的智能合约,来自多方的努力正在进行中——开发人员接受具有最佳实践指导方针的培训,以及“capture the flag””挑战,如Ethernaut或capture the Ether,以及使用更好的工具集和语言(Vyper),以防止意外错误的安全扫描程序和其他问题。更全面的评审可能涉及第三方使用手动评审或正式验证进行的审核,但是,并不是每个人都可以访问这些审核,特别是对于正在引导或业余程序员的团队。对于有抱负的智能合约开发人员,可以立即访问的智能合约检查工具包是安全扫描器,例如Securify by ChainSecurity (https://securify.chainsecurity.com/)或SmartCheck by SmartDec (https://tool.smartdec.net/)。这些是易于使用的在线智能契合约的扫描器,大多数应用程序开发人员都可以使用,两者的主要区别在于,Securify通过语义推断在字节码级别上分析合约的安全违规行为,而SmartCheck则通过解析合约语言进行词汇和语法分析。出于撰写本文的目的,我们将首先关注我们使用Securify的经验,包括基于web的安全扫描器和Securify后端(https://github.com/eth-sri/securify)。
在我们开始之前,我想说的是,在线扫描器的工作基于启发式,并且不能检测超出其预定义列表的漏洞,这是一个有经验的审计团队可以提供的,因此它们不应该被认为是一个广泛审计工作的替代品。永远要记住,你智能合约处理的钱越多,出错的风险就越大。
此外,请注意,对于启发式分析程序来说,预期是过度报告而不是少报告潜在的安全违规行为,因此将会出现一些误报,然后智能合约开发人员应该努力识别是否存在攻击向量。
从一个天真实现的合约钱包开始——它持有一个keccak256哈希值,作为密码,允许从这个合约中检索以太币:
pragma solidity ^0.4.25;
contract simpleWallet {
    
    bytes32 hash;
    
    function commitHash(bytes32 _hash) public payable {
        require(msg.value > 0 && hash == 0x0);
        hash = _hash;
    }
    
    function retrievefromWallet(bytes32 _plaintext) public {
        require(keccak256(abi.encodePacked(_plaintext)) == hash);
        msg.sender.transfer(address(this).balance);
    }
    
    function checkHash(bytes32 _plaintext) public pure returns (bytes32) {
        return keccak256(abi.encodePacked(_plaintext));
    }
}
不要用它来存储资金。一开始,我们就可以看到这个钱包可能很容易受到抢先攻击,commitHash(至少在短时间内)可以由另一方初始化,而不是部署方。让我们把它通过Securify看看它得到了什么:
Securify网站(https://securify.chainsecurity.com/)
使用Securify 网站,只需复制粘贴上述代码即可。点击“Scan Now”,稍等片刻,将返回结果。

共报告5个问题,2个警告。

问题

警告

这些问题以一种相当直观的方式在潜在的易受攻击的代码行上进行了报告,如果单击“info”按钮,还会提供进一步的详细说明和示例。
看看这些问题:
“交易指令影响以太币金额”——这可能是一种过高的估计,因为我们在这里给出了合约持有的全部馀额,而没有预先计算要发送的金额,因此合同要么发送“全额”,要么就“没有”。虽然可能发生的是在同一个块中,但是给定两个有效的事务,第一个事务将提取全额,而第二个事务将得不到任何东西。
在这里,我还期望依赖交易顺序:接收方出现,因为合约应该持有大量的价值,所以使用明文数据侦听一个交易到此的地址,然后抢先运行一个我自己的、GAS价格更高的交易,可能是值得的。
更新:在与Securify团队交谈后,我了解到TOD: Receiver并不是像msg.sender描述的那样,发送方地址保持不变。这将是一个问题,当地址在智能合约中是可变的时候,才可以在提款交易之前更改。那么最重要的问题就是TOD:数量,因为智能合约所持有的金额可以被另一方提取,从而使合法所有者获得0。
“无限制写入存储”——Securify很好地捕捉到了这一点,它警告合约开发人员任何人都可以写入存储,这确实是正确的。虽然合约只在未被赋予值时才允许写操作,但是攻击者可能会在很短的时间内通过插入原始用户而使合约无效。更好的方法可能是将此代码放在构造函数下。
“缺少输入验证”——是相当不言自明的,虽然在合同中并不是非常重要,但是合同开发人员应该注意这一点,特别是对于不同的数据类型。检查传递给合同的地址是不是偶然为0x0以防止资金丢失(假设我们期待合法的交易,而不是将令牌发送到刻录地址 – 这可以在没有这个检查的单独功能中完成)。
无论是“无限制以太流”和“不安全电话不可信合同”是公平的警告,合同可以用合同或账户非故意通信(如醚转让给另一方,而不是合同所有者),所以它是值得的合同开发人员退后一步,看看这是否确实是预期的设计。
Securify Local(https://github.com/eth-sri/securify)
既然Securify有一个web前端,那么为什么要使用Securify的本地实例呢?首先,可以为特定的合约逻辑使用额外的安全模式来扩展Securify(这是我正在研究的问题,可能值得单独写一篇文章),特别是如果存在通用表达式无法捕获的业务域限制。另外,在我玩Securify Web的几个星期中,有一些实例表明它运行缓慢或超时,公平地说,它是一个公共服务,因此拥有一个本地实例是有帮助的。
我用安装了docker的Ubuntu实例部署了Securify,所以我们只需要构建Securify docker映像并将Securify指向我们想要分析的目录。

运行Securify使用.sol合约指向我们的目录

分析完成后:

警告和问题的完整列表

总共检测到5次违规(问题)和4次警告。这里报告的违规和警告不像web版本那样冗长(web版本提供详细说明和示例),而且违规与Securify web报告的违规一致。另一方面,Securify Local似乎为我们提供了额外的警告:LockedEther、DAOConstantGas、TODReceiver和UnhandledException。
我认为这些是贴上警告,因为它们是部分匹配,它们并不完全与Securify中规定的违规模式和安全模式完全匹配。例如,锁定的情况— 合同的确允许以太币被接收,然而,因为转移从地址上转移的金额可能是0,因此Securify不会将其作为违规或安全模式。这些警告作为合约开发人员再次查看的标志,以确保这些不是实际违规。
为了更全面,Securify Local将报告模式的完整列表如下:
1. LockedEther -报告以太币发送该合约的可能性是不可恢复的,因此在合同中被“锁定”了。
2. DAO——报告重入攻击的可能性(类似于DAO情况),更准确地说,这个模式检查是否转发了所有的gas。可以使用transfer()或send()操作来避免只转发2300 gas。
3. DAOConstantGas—报告在执行以太币传输后状态更改可能易受重入攻击的可能性。例如,保存其余以太币的变量仅在发送以太币后才更新。在大多数情况下应该避免使用transfer()或send(),但是更好的做法是使用check – effects – interaction模式
4. TODReceiver—报告存在使用块进行事务排序而更改传输接收器的可能性。例如,如果预期的收件人地址存储为存储变量,并且要根据该地址执行传输,那么如果在传输之前存在这样的事务,则有可能更改或覆盖该地址。
5. TODAmount—报告存在在一个块内的事务排序而可能更改转账金额的可能性。类似于TODReceiver,但是在这种情况下,被转移的金额可能会发生变化。例如,在crowdsale中,代币*接收到的以太币=要发送的代币,其中代币是一个变量,可以在实际发送之前进行更改。
6. UnhandledException——报告在使用call()或send()时,返回值不被处理的可能性。例如,如果发生send()操作,其中接收合约运行一个回退函数,导致一个out of gas错误,那么send()操作将不会恢复,而是返回false。与transfer()不同,transfer()的作用类似于require(send()),它将还原整个事务。
7.Uncontrotedetherflow—当合同允许任意接收以太币时可能出现的问题,特别是防止由于缺少传输操作而导致以太币被锁定的可能性。
8. UnrestrictedWrite——存储变量可能存在任被其他方任意覆盖的可能性,因为它没有所有权限制。
有趣的是,如果我们查看Securify的Github (https://github.com/eth-sri/securify/tree/master/src/main/java/ch/securify/patterns),似乎有更多的模式,其中许多模式已经被注释——可能正在进行中,或者仍在改进中。
请注意,Securify不执行数值分析,因此不存在溢出/下溢检查,尽管这是为将来的版本(如Securify学术论文“限制”一节中所提到的)所计划的。
结语
到目前为止,我使用Securify的经验还不错(除了Securify Web上偶尔出现的“坏网关”之外,不过我还是继续使用我的本地实例)。真正值得称赞的是,ChainSecurity决定在相当宽松的Apache 2.0许可下开源项目,并将Securify免费提供给公共使用,特别是在智能合约安全审计对某些个人来说可能非常昂贵的情况下。
也就是说,启发式分析器只能发现经验所发生的事情,需要显式地覆盖新模式,否则可能会遗漏新模式。在需要进行更广泛审计的地方,使用手工审计进行正式的验证可以证明更加健壮,并且值得研究。