符号执行之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。