Difficulty: Advanced
A smart contract audit is a systematic review of source code to identify security vulnerabilities, logic errors, gas inefficiencies, and compliance with best practices. Given the immutable and financially consequential nature of deployed smart contracts, auditing is essential for any project handling significant value. Professional audits take 1-4 weeks and are conducted by firms like Trail of Bits, OpenZeppelin, Consensys Diligence, and Spearbit. Even with a professional audit, no code is guaranteed bug-free - audits reduce risk but cannot eliminate it.
Manual review is the backbone of thorough auditing. Auditors begin by understanding the protocol design through documentation and architecture diagrams. They then perform line-by-line review focusing on access control, external interactions, state management, arithmetic, and protocol-specific logic. Experienced auditors use threat modeling - thinking like an attacker and systematically evaluating each function for exploit vectors. They trace fund flows, check invariants, verify edge cases, and identify logic errors that automated tools miss. The output is a detailed report categorizing findings by severity (Critical, High, Medium, Low, Informational).
Automated tools complement manual review. Slither (Trail of Bits) is a static analysis framework with 80+ detectors for common vulnerabilities - it runs in seconds and should be in every CI/CD pipeline. Mythril (Consensys) uses symbolic execution to explore all possible execution paths, finding issues like unchecked calls and ether leaks. Echidna (Trail of Bits) is a property-based fuzzer that tests invariants by generating random inputs and call sequences. Each tool has different strengths: Slither for fast pattern matching, Mythril for deep path exploration, Echidna for invariant testing.
Formal verification uses mathematical proofs to verify contract behavior matches specification for all possible inputs and states. Tools like Certora Prover and Halmos let developers write formal specifications and automatically verify them. You can prove that 'total supply always equals sum of all balances' or 'no user's balance exceeds total supply.' While formal verification provides the strongest guarantees, it's expensive and requires specialized expertise, so it's typically used for the most critical DeFi components.
Bug bounty programs provide ongoing security after deployment. Platforms like Immunefi host programs with rewards from $1,000 to $10,000,000+ for critical vulnerabilities. A well-structured program includes clear scope, severity criteria, response SLAs, and competitive rewards. Immunefi has facilitated over $100M in payouts. For protocols with significant TVL, continuous bug bounties are essential as the last line of defense.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
// Run: slither . --print human-summary
// Common Slither detectors and fixes:
interface IERC20 {
function transfer(address to, uint256 amount) external returns (bool);
}
contract SlitherExamples {
address public owner;
uint256 public totalSupply = 1000;
mapping(address => uint256) public balances;
// Detector: missing-zero-address-check
function setOwnerBad(address _owner) external {
owner = _owner; // Slither warns: missing zero check
}
function setOwnerGood(address _owner) external {
require(_owner != address(0), "Zero address");
owner = _owner;
}
// Detector: reentrancy-eth
function withdrawBad() external {
uint256 amount = balances[msg.sender];
(bool success, ) = msg.sender.call{value: amount}("");
require(success);
balances[msg.sender] = 0; // Slither: reentrancy!
}
function withdrawGood() external {
uint256 amount = balances[msg.sender];
balances[msg.sender] = 0; // Update first
(bool success, ) = msg.sender.call{value: amount}("");
require(success);
}
// Detector: shadowing-local
function calculateBad() external view returns (uint256) {
uint256 totalSupply = 500; // Shadows state variable!
return totalSupply;
}
function calculateGood() external view returns (uint256) {
uint256 localSupply = 500; // No shadowing
return localSupply + totalSupply;
}
// Detector: unused-return
function transferBad(address token, address to) external {
IERC20(token).transfer(to, 100); // Return value ignored!
}
function transferGood(address token, address to) external {
bool success = IERC20(token).transfer(to, 100);
require(success, "Transfer failed");
}
}Shows common issues Slither detects with their fixes: missing zero-address checks, reentrancy from incorrect state update order, variable shadowing, and unchecked return values. Run Slither in CI/CD to catch these automatically.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
// Run: echidna . --contract TestToken --config echidna.yaml
contract TokenToTest {
mapping(address => uint256) public balances;
uint256 public totalSupply;
function mint(address to, uint256 amount) external {
balances[to] += amount;
totalSupply += amount;
}
function burn(address from, uint256 amount) external {
require(balances[from] >= amount, "Insufficient");
balances[from] -= amount;
totalSupply -= amount;
}
function transfer(address from, address to, uint256 amount) external {
require(balances[from] >= amount, "Insufficient");
balances[from] -= amount;
balances[to] += amount;
}
}
contract TestToken is TokenToTest {
address constant USER1 = address(0x10000);
address constant USER2 = address(0x20000);
address constant USER3 = address(0x30000);
// INVARIANT 1: Total supply == sum of all balances
function echidna_total_supply_invariant() public view returns (bool) {
return totalSupply ==
balances[USER1] + balances[USER2] + balances[USER3] +
balances[address(this)] + balances[msg.sender];
}
// INVARIANT 2: No balance exceeds total supply
function echidna_no_balance_exceeds_supply() public view returns (bool) {
return balances[USER1] <= totalSupply &&
balances[USER2] <= totalSupply &&
balances[USER3] <= totalSupply;
}
// INVARIANT 3: Transfer preserves total supply
function echidna_transfer_preserves_supply() public view returns (bool) {
// If Echidna can break this, transfer has a bug
return true; // Simplified - real invariant would compare before/after
}
}
// echidna.yaml:
// testMode: assertion
// testLimit: 100000
// seqLen: 100
// sender: ["0x10000", "0x20000", "0x30000"]Echidna tests invariants by generating random call sequences with random inputs. The echidna_ functions define properties that should ALWAYS hold true. If Echidna finds a violating sequence, it reports it. This is more powerful than unit tests because it explores unexpected operation combinations.
// JavaScript: Professional audit workflow
const auditWorkflow = {
phase1_scoping: {
duration: '1-2 days',
activities: [
'Review documentation and specifications',
'Understand protocol architecture and trust assumptions',
'Identify critical components and attack surfaces',
'Define scope: contracts, functions, version',
'Set up development environment and run existing tests',
],
},
phase2_automated: {
duration: '1-2 days',
tools: {
slither: 'Static analysis, 80+ detectors, runs in seconds',
mythril: 'Symbolic execution, deep path exploration, minutes-hours',
echidna: 'Property-based fuzzing, invariant testing, hours',
solhint: 'Code style and best practice linting',
},
},
phase3_manual: {
duration: '5-15 days',
focusAreas: [
'Access control and authorization',
'External call safety (reentrancy, return values)',
'Arithmetic correctness and precision',
'Oracle integration and price manipulation',
'Flash loan attack vectors',
'Upgrade safety (proxy patterns)',
'Economic/game theory attacks',
'Edge cases and boundary conditions',
],
},
phase4_reporting: {
severity: {
Critical: 'Direct loss of funds or permanent DoS',
High: 'Significant impact, possible fund loss under conditions',
Medium: 'Moderate impact, unlikely but possible fund loss',
Low: 'Minor impact, best practice violation',
Informational: 'Code quality, readability, gas optimization',
},
structure: [
'Executive Summary',
'Scope and Methodology',
'System Overview',
'Findings by severity',
'Each: Title, Severity, Description, Impact, Recommendation, Status',
],
},
phase5_remediation: {
duration: '1-5 days',
activities: [
'Team implements fixes',
'Auditor reviews fixes (remediation review)',
'Final report with fix verification',
],
},
};
console.log('Audit Phases:');
for (const [phase, details] of Object.entries(auditWorkflow)) {
console.log(`\n${phase} (${details.duration})`);
if (details.activities) details.activities.forEach(a => console.log(` - ${a}`));
if (details.tools) {
for (const [tool, desc] of Object.entries(details.tools)) {
console.log(` ${tool}: ${desc}`);
}
}
}A professional audit follows five phases: scoping, automated analysis, manual review, reporting, and remediation. The severity classification helps teams prioritize fixes. Multiple audit firms should review high-value protocols for maximum coverage.
Smart Contract Audit, Slither, Mythril, Echidna, Formal Verification, Bug Bounty