长按二维码,关注官方公众号
RK87 - 智能合约验证工具（翡翠宴会厅A）
以太坊引入了智能合约的理念，开启了区块链上经济建设的新时代。然而，智能合约只不过是一串代码 —— 既然是代码，，存在缺陷就是在所难免的事。据报道，许多攻击已导致数百万 ETH 被盗，安全问题已经成为智能合约部署中最大问题之一。
为了发现智能合约漏洞，我们开发了许多审查工具，但这些工具都存在一定缺陷。可以使用符号执行工具（如 Manticore 和 Mythril）审查目标智能合约的二进制文件，但是需要手工设置每个二进制文件。基于模式的属性行为分析器（Securify）只能检测模式漏洞，无法检测出整数溢出和逻辑错误。基于调用路径条件的分析器（OyTune）无法处理多事务调用中的错误。
该课程介绍了一种使用非基于模式的符号执行来查找智能合约中的缺陷。我们开发了一款名为 RK97 的专用工具，用以自动验证 ERC20 合约，无需人与人之间的交互。早期结果喜人：RK87 可以准确检测出 2018 年报道的大多数缺陷，还能帮助我们找出许多尚未公布的缺陷。
