区块链安全：合约审计、攻击模式与防御体系

// ❌ 脆弱代码（提款前未扣余额）
function withdraw() external {
    uint256 amount = balances[msg.sender];
    require(amount > 0);
    (bool success, ) = msg.sender.call{value: amount}("");  // 外部调用
    require(success);
    balances[msg.sender] = 0;  // 状态更新在调用之后！
}

contract Attacker {
    VulnerableTarget target;
    
    receive() external payable {
        if (address(target).balance >= 1 ether) {
            target.withdraw();  // 递归重入！
        }
    }
    
    function attack() external {
        target.deposit{value: 1 ether}();
        target.withdraw();  // 第一次触发
    }
}

// ✅ 安全代码（Checks-Effects-Interactions）
function withdraw() external nonReentrant {
    uint256 amount = balances[msg.sender];
    require(amount > 0, "No balance");
    balances[msg.sender] = 0;          // Effect: 先更新状态
    (bool success, ) = msg.sender.call{value: amount}("");
    require(success, "Transfer failed"); // Interaction: 后交互
}

# Slither: 静态分析 pip3 install slither-analyzer
slither contracts/ --filter-paths "node_modules"

# Mythril: 符号执行 pip3 install mythril
myth analyze contracts/Token.sol

# Echidna: 模糊测试（Foundry 内置）
forge test --fuzz-runs 100000

# Certora: 形式化验证 certoraRun contracts/Token.sol --verify Token:specs/Token.spec

// 规范文件: specs/Token.spec
rule transferCorrect(address from, address to, uint256 amount) {
    env e;
    require e.msg.sender == from;
    
    uint256 balanceBefore = balanceOf(from);
    require balanceBefore >= amount;
    
    transfer(e, to, amount);
    
    assert balanceOf(from) == balanceBefore - amount;
    assert balanceOf(to) == balanceOf(to) + amount;
}

rule noBurnUnlessAuthorized(method f) {
    env e;
    calldataarg args;
    uint256 totalBefore = totalSupply();
    
    f(e, args);
    
    assert totalSupply() >= totalBefore || e.msg.sender == owner();
}