符号执行之manticore工具演练

参考资料：SANS SEC 554
https://docs.soliditylang.org/en/v0.8.0/
ziion虚拟机：区块链智能合约中的kali(ziion涵盖演练中所以提及到的工具)

动静态之分

IDA是静态分析工具，常用于检测脆弱性；manticore是动态分析工具，常用于编写漏洞利用(符号执行：即执行动态的二进制)，毕竟要证明危害性嘛，所以动态执行并验证结果。

演练目标
• 使用符号执行来查找安全漏洞。
• 使用manticore 对可利用的合约进行分析。
• 识别基于算术的漏洞。
• 了解manticore 符号执行运行的输出文件。

第一步
创建 Solidity 文件，文件后缀名 test.sol 源码如下：

pragma solidity ^0.4.26;

contract Ownership{
    address owner = msg.sender;
    function Owner() public{
        owner = msg.sender;
    }
    modifier isOwner(){
        require(owner == msg.sender);
        _;  }}
contract Pausable is Ownership{
    bool is_paused;
    modifier ifNotPaused(){
        require(!is_paused);
        _;  }
    function paused() isOwner public{
        is_paused = true;   }
    function resume() isOwner public{
        is_paused = false;  }}
contract SEC554_CoinBank is Pausable{
    mapping(address => uint) public balances;
    function transfer(address to, uint value) ifNotPaused public{
        balances[msg.sender] -= value;
        balances[to] += value;
    }

第二步

设置编译器版本（代码第一行有版本号）
sudo solc-select 0.4.26

第三步

运行符号执行
运行 manticore 时，请确保选择开关 --txlimit 1 和 --limit-loops，否则测试将运行很长时间（或者可能永远不会完成）（这一点在B站上的UP主：甜品专家《南京大学《软件分析》课程》中有只言片语的描述）
结果类似于下图，并且可能需要几分钟才能完成。

第四步

分析 Manticore 的发现
完成后，查看检测到的漏洞。结果在以 mcore_ 开头的文件夹中

看一下 manticore 创建的文件。符号执行有许多输出文件，显示日志、摘要、跟踪和结果。

打开global.findings文件查看汇总结果

Manticore 发现了多个漏洞，其中包括几个整数溢出漏洞。

Balances[to] += 和balances[to] -= 的代码段会产生算术漏洞。

整数溢出/上溢/下溢（算术攻击）

缓冲区溢出，算术运算达到类型的最大(上溢)或最小(下溢)值时，就会发生整数上溢或下溢。比如一个数字是uint8类型存储，那么它存储的范围是0到2^8-1的8位无符号数。超过范围即漏洞。
使用安全数学库代替各种运算符(例如加法、减法和乘法)，OpenZeppelin 的安全数学库是避免上溢/下溢漏洞的当前技术。
使用数学库代替标准运算符，例如加法、减法和乘法。请注意，不包括除法，因为 EVM 不允许除以 0。

526互联

符号执行manticore工具演练之发现缓冲区溢出漏洞

符号执行之manticore工具演练