Slither, Mythril, Echidna ” las herramientas que usan los mejores auditores del mundo
# Mythril analiza rutas de ejecución simbólicamente # Detecta: reentrancy, integer overflow, unprotected selfdestruct $ myth analyze VulnerableBank.sol ==== Reentrancy ===== SWC ID: 107 Severity: High Contract: VulnerableBank Function name: withdraw(uint256) PC address: 0x4a2 Description: External call to user-supplied address followed by state change. An attacker may cause a reentrant call to VulnerableBank.withdraw(). Initial State: Account: [ATTACKER] Balance: 1 ETH Transaction Sequence: 1. VulnerableBank.deposit() value=1 ETH 2. AttackContract.attack() Triggers: VulnerableBank.withdraw(1000000000000000000) ReEnters: VulnerableBank.withdraw(1000000000000000000) [× 10] Drains: 10 ETH total ==== Integer Overflow (no detectado en Solidity 0.8+) ==== SWC ID: 101 Note: SafeMath built-in desde Solidity 0.8.0
// echidna-test.sol ” Propiedades que SIEMPRE deben cumplirse contract BankTest is VulnerableBank { // Echidna buscará inputs que violen esta propiedad function echidna_balance_invariant() public view returns (bool) { // El balance del contrato nunca debe bajar a 0 si hay depósitos return address(this).balance >= totalDeposits; } function echidna_no_free_money() public view returns (bool) { // Nadie puede retirar más de lo que depositó return withdrawals[msg.sender] <= deposits[msg.sender]; } } # Ejecutar: $ echidna BankTest.sol --contract BankTest --config echidna.yaml # echidna.yaml: # testLimit: 50000 # seqLen: 100 # shrinkLimit: 5000