manticore符号执行漏洞分析问题

Question

我通过manticore符号执行带有漏洞的合约得到以下文件（下方有图），但是我不知道如何去根据这些文件分析合约中存在哪些漏洞，具体代码如下：

我想问我这样编写代码是否正确，大家能否给我提供一个你们用来分析并成功的脚本和合约源码的例子，我想参考一下看看我错在哪里。我这里运行的时候只会报：

2024-02-13 20:03:15,942: [20196] m.c.plugin:WARNING: 
Caught will_solve in state None, but failed to capture its initialization
2024-02-13 20:03:16,034: [20195] m.c.plugin:WARNING: 
Caught will_solve in state None, but failed to capture its initialization

from manticore.ethereum import ManticoreEVM
# 创建Manticore实例
m = ManticoreEVM()
# 创建账号/合约所有者
owner = m.create_account(balance=100000000000000000000)
# 创建受攻击者账号
attacker = m.create_account(balance=100000000000000000000)
# 部署合约
contract = m.solidity_create_contract('VulnerableContract.sol', owner=owner)
# 设置参数的符号变量
to = m.make_symbolic_value()
amount = m.make_symbolic_value()
# 调用合约函数
contract.transfer(attacker, amount)
# 设置分析参数
m.finalize()
# 获取生成的测试状态
states = m.ready_states
# 对测试状态进行一些操作，比如访问符号变量的具体取值
for state in states:
    to_value = state.solve_one(to)
    amount_value = state.solve_one(amount)
    print(f"Test case: to={to_value}, amount={amount_value}")

https://img-blog.csdnimg.cn/direct/2df8fc07c29f4b44a930a834196dae73.png

Answer 1

参考通义千问和郭老师的小迷弟雅思莫了-编写提供，主要是为了帮助您快速解决问题，如下回答，您可以参考下，如有问题，评论区留言。

你提供的代码是使用 Manticore 进行以太坊智能合约符号执行的基础部分，看起来基本正确。但是，从日志信息来看，Manticore 在处理某些状态时未能捕获初始化问题，这可能是因为你的合约或测试场景触发了某种边界条件或其他异常情况。

要分析合约中的漏洞，你需要根据生成的输出（状态）来检查是否存在不期望的行为或者违反安全属性的情况。比如在 Solidity 合约中常见的整数溢出、重入攻击、权限控制失效等问题。

以下是一个简化的示例，展示如何分析一个包含潜在整数溢出漏洞的合约：

from manticore.ethereum import ManticoreEVM

# 假设 VulnerableContract.sol 包含如下有整数溢出风险的函数：
# contract VulnerableContract {
#     function unsafeAdd(uint a, uint b) public returns (uint c) {
#         c = a + b;
#     }
# }

m = ManticoreEVM()

owner = m.create_account(balance=100000000000000000000)
contract = m.solidity_create_contract('VulnerableContract.sol', owner=owner)

# 符号化输入
a = m.make_symbolic_value()
b = m.make_symbolic_value()

# 调用可能存在漏洞的函数
c = contract.unsafeAdd(a, b)

# 添加约束条件来查找溢出情况
overflowed = m.cpu.memory.load(c, 32) == 0  # 如果结果为零，则可能发生溢出

# 执行并获取满足约束条件的状态
m.finalize()
overflow_states = [s for s in m.ready_states if s.satisfies(overflowed)]

for state in overflow_states:
    a_value, b_value = state.solve([a, b])
    print(f"Overflow detected: a={a_value}, b={b_value}")

# 对于其他类型的漏洞，你需要构造相应的约束条件和检查方法

请注意，实际的漏洞分析过程通常会更复杂，需要结合具体的合约逻辑和安全知识进行深入分析。对于上述例子，虽然我们找到了可能导致溢出的输入组合，但要进一步确认是否真的存在漏洞，还需要进一步查看 EVM 字节码执行的过程和结果。