Smart Contract Security Testing: Slither, Mythril, and Static Analysis
Security testing for smart contracts requires both automated tools and manual review. Slither performs fast static analysis and catches a wide range of common vulnerabilities. Mythril uses symbolic execution to find logical flaws that static analysis misses. Echidna performs property-based fuzzing to verify that invariants hold under adversarial conditions. All three should run in CI before any deployment.
Key Takeaways
Static analysis is fast and should run on every commit. Slither analyzes Solidity without executing code and catches reentrancy, unchecked returns, integer issues, and access control flaws in seconds.
Symbolic execution explores all code paths mathematically. Mythril reasons about program behavior symbolically rather than with specific inputs, finding vulnerabilities that neither static analysis nor regular testing will catch.
Echidna finds property violations through targeted fuzzing. Unlike random fuzz testing, Echidna uses feedback-driven fuzzing specifically designed for smart contracts — it focuses on paths that change state and approach boundary conditions.
Automated tools are not a substitute for manual audit. Tools catch known vulnerability patterns. Novel attack vectors, business logic flaws, and economic exploits require human expertise.
The pre-audit checklist is as important as the audit itself. Resolving all tool findings before the audit lets auditors focus on logic-level issues rather than mechanical problems.
Why Automated Security Analysis Matters
Manual code review is expensive and slow. A senior Solidity auditor reviewing 2,000 lines of code takes days. Slither reviews those same 2,000 lines in under a minute and catches a well-defined set of common vulnerability patterns with high accuracy.
The workflow is not automated tools instead of manual review — it is automated tools first, then manual review. Running Slither and Mythril before engaging an auditor means the auditor's time is spent on business logic, economic design, and novel attack vectors rather than catching unchecked arithmetic or visible reentrancy.
Slither: Static Analysis
Slither is developed by Trail of Bits and is the most widely used static analysis tool for Solidity. It works by analyzing the contract's AST and control flow graph without executing code.
Installation
pip3 install slither-analyzer
# Or with pipx (recommended for isolation)
pipx install slither-analyzerBasic Usage
# Analyze a single file
slither contracts/MyContract.sol
<span class="hljs-comment"># Analyze an entire Hardhat project
slither .
<span class="hljs-comment"># Analyze with specific Solidity version
slither . --solc-remaps <span class="hljs-string">"@openzeppelin=node_modules/@openzeppelin"
<span class="hljs-comment"># Output in JSON for CI integration
slither . --json results.json
<span class="hljs-comment"># Filter to specific severity levels
slither . --filter-paths <span class="hljs-string">"node_modules|test" --exclude-informationalUnderstanding Detector Output
INFO:Detectors:
Reentrancy in Vault.withdraw(uint256) (contracts/Vault.sol#42-52):
External calls:
- token.transfer(msg.sender,amount) (contracts/Vault.sol#49)
State variables written after the call:
- balances[msg.sender] -= amount (contracts/Vault.sol#50)
- totalDeposited -= amount (contracts/Vault.sol#51)
Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#reentrancy-eth
INFO:Slither:contracts/Vault.sol analyzed (3 contracts with 12 detectors)
INFO:Slither:Use https://crytic.io/ to get access to additional detectors and GitHub integrationEvery finding includes: the vulnerability type, the exact code location, which external calls precede which state changes, and a link to documentation.
Common Detectors and What They Find
Reentrancy (reentrancy-eth, reentrancy-no-eth): State changes after external calls.
// VULNERABLE: state changed AFTER external call
function withdraw(uint256 amount) external {
require(balances[msg.sender] >= amount);
token.transfer(msg.sender, amount); // external call
balances[msg.sender] -= amount; // state change AFTER — reentrancy!
}
// FIXED: state changed BEFORE external call (CEI pattern)
function withdraw(uint256 amount) external {
require(balances[msg.sender] >= amount);
balances[msg.sender] -= amount; // state change BEFORE
token.transfer(msg.sender, amount); // external call after
}Unchecked low-level calls (unchecked-lowlevel): Return values from call, send, delegatecall not checked.
// VULNERABLE
address(recipient).call{value: amount}("");
// FIXED
(bool success, ) = address(recipient).call{value: amount}("");
require(success, "ETH transfer failed");Dangerous use of tx.origin (tx-origin): Using tx.origin for authorization allows phishing attacks.
Uninitialized local variables (uninitialized-local): Variables used before assignment.
Arbitrary from in transferFrom (arbitrary-send-erc20): transferFrom called with an from address controlled by the caller.
Suppressing False Positives
// slither-disable-next-line reentrancy-no-eth
token.transfer(msg.sender, amount);Document every suppression with a reason. Suppressing a real finding to silence the tool is a security vulnerability.
Slither Printers
Slither includes printers for understanding contract structure:
slither . --print call-graph <span class="hljs-comment"># function call graph as DOT file
slither . --<span class="hljs-built_in">print inheritance <span class="hljs-comment"># inheritance hierarchy
slither . --<span class="hljs-built_in">print data-dependency <span class="hljs-comment"># variable dependency analysis
slither . --<span class="hljs-built_in">print function-summary <span class="hljs-comment"># function visibility and modifiersMythril: Symbolic Execution
Mythril uses symbolic execution and SMT solving to reason about all possible execution paths. Where Slither is fast but pattern-based, Mythril is slower but mathematically exhaustive within its analysis scope.
Installation
pip3 install mythril
# Or with Docker (recommended for consistent results)
docker pull mythril/mythBasic Usage
# Analyze a contract file
myth analyze contracts/MyContract.sol
<span class="hljs-comment"># With Solidity remappings
myth analyze contracts/MyContract.sol \
--solc-json remappings.json
<span class="hljs-comment"># Set timeout (default is 86400s — too long for CI)
myth analyze contracts/MyContract.sol --<span class="hljs-built_in">timeout 300
<span class="hljs-comment"># Output as JSON
myth analyze contracts/MyContract.sol -o json
<span class="hljs-comment"># Via Docker
docker run -v $(<span class="hljs-built_in">pwd):/code mythril/myth analyze /code/contracts/MyContract.solWhat Mythril Detects
Integer arithmetic issues: Overflow and underflow even in code that passes casual review.
// Mythril will find this if the unchecked block allows overflow
function calculateReward(uint256 stake, uint256 multiplier)
public pure returns (uint256) {
unchecked {
return stake * multiplier; // could overflow
}
}Unprotected Ether withdrawal: Any path where an attacker can drain ETH.
Delegatecall to user-supplied address: A classic proxy vulnerability.
// VULNERABLE: caller controls 'target'
function execute(address target, bytes calldata data) external {
(bool success, ) = target.delegatecall(data);
require(success);
}Timestamp dependence: Logic that depends on block.timestamp in ways that miners can manipulate.
Transaction order dependence: Race conditions exploitable by frontrunning.
Interpreting Mythril Output
==== Integer Arithmetic Bugs ====
SWC ID: 101
Severity: High
Contract: Vault
Function name: calculateShares(uint256,uint256)
PC address: 340
Estimated Gas Usage: 5456 - 26000
The arithmetic operator can overflow. It is possible to cause an integer overflow or underflow
in the arithmetic operation.
--------------------
In file: contracts/Vault.sol:87
shares = (amount * totalShares) / totalAssets
--------------------Common Vulnerabilities to Test For
Reentrancy
Write a test that deploys an attacking contract and verifies your contract resists reentrant calls:
// test/ReentrancyTest.t.sol
contract MaliciousReceiver {
Vault target;
uint256 attackCount;
constructor(Vault _target) {
target = _target;
}
// Called when ETH is sent to this contract
receive() external payable {
if (attackCount < 3 && address(target).balance > 0) {
attackCount++;
target.withdraw(1 ether); // attempt reentrant call
}
}
function attack() external payable {
target.deposit{value: msg.value}();
target.withdraw(1 ether);
}
}
contract ReentrancyTest is Test {
Vault vault;
MaliciousReceiver attacker;
function setUp() public {
vault = new Vault();
attacker = new MaliciousReceiver(vault);
// Fund vault with legitimate deposits
vm.deal(address(this), 10 ether);
vault.deposit{value: 10 ether}();
}
function test_ResistsReentrancy() public {
vm.deal(address(attacker), 1 ether);
uint256 vaultBalanceBefore = address(vault).balance;
attacker.attack{value: 1 ether}();
// Vault should only have lost the attacker's legitimate deposit
assertEq(address(vault).balance, vaultBalanceBefore);
assertEq(attacker.attackCount(), 0); // no reentrant calls succeeded
}
}Access Control
function test_AccessControl_AllFunctions() public {
address nobody = makeAddr("nobody");
// Test every privileged function
vm.startPrank(nobody);
vm.expectRevert();
vault.pause();
vm.expectRevert();
vault.setFee(500);
vm.expectRevert();
vault.emergencyWithdraw(address(this));
vm.stopPrank();
}Integer Overflow (Solidity < 0.8.0)
For pre-0.8.0 contracts or code using unchecked:
function testFuzz_NoOverflow(uint256 a, uint256 b) public {
// If a + b overflows, the result should be caught
if (a > type(uint256).max - b) {
vm.expectRevert();
myContract.add(a, b);
} else {
assertEq(myContract.add(a, b), a + b);
}
}Echidna: Property-Based Fuzzing for Security
Echidna is a Haskell-based fuzzer developed by Trail of Bits specifically for smart contract security. Unlike Foundry's built-in fuzzer (which is general purpose), Echidna is tuned for finding security violations.
Installation
# Using Docker (simplest)
docker pull trailofbits/echidnaWriting Echidna Properties
// test/VaultEchidna.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
import "../src/Vault.sol";
import "../src/MockERC20.sol";
contract VaultEchidna {
Vault vault;
MockERC20 token;
address constant ECHIDNA_CALLER = address(0x10000);
constructor() {
token = new MockERC20("T", "T", 18);
vault = new Vault(address(token));
token.mint(ECHIDNA_CALLER, 1000000e18);
token.approve(address(vault), type(uint256).max);
}
// Invariant: user balance in vault never exceeds what they deposited
function echidna_balances_consistent() public view returns (bool) {
return vault.balances(ECHIDNA_CALLER) <= token.balanceOf(address(vault));
}
// Invariant: total deposited equals sum of all balances (simplified: one user)
function echidna_total_deposited_matches() public view returns (bool) {
return vault.totalDeposited() == vault.balances(ECHIDNA_CALLER);
}
// Invariant: vault token balance never decreases without a withdrawal event
function echidna_no_free_drain() public view returns (bool) {
return token.balanceOf(address(vault)) >= vault.totalDeposited();
}
}Run Echidna:
docker run -v $(pwd):/code trailofbits/echidna \
/code/test/VaultEchidna.sol \
--contract VaultEchidna \
--config /code/echidna.yaml# echidna.yaml
testLimit: 50000
seqLen: 100
timeout: 300
deployer: "0x10000"
sender: ["0x10000"]Integrating Security Tools in CI
# .github/workflows/security.yml
name: Security Analysis
on: [push, pull_request]
jobs:
slither:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: actions/setup-python@v5
with:
python-version: "3.11"
- run: pip install slither-analyzer
- uses: actions/setup-node@v4
with:
node-version: 20
- run: npm ci
- name: Run Slither
run: |
slither . \
--filter-paths "node_modules|test|lib" \
--exclude-informational \
--json slither-results.json
continue-on-error: true # don't fail CI for informational findings
- uses: actions/upload-artifact@v4
with:
name: slither-results
path: slither-results.json
mythril:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Run Mythril
run: |
docker run -v $(pwd):/code mythril/myth \
analyze /code/contracts/Vault.sol \
--timeout 120 \
-o json > mythril-results.json
- uses: actions/upload-artifact@v4
with:
name: mythril-results
path: mythril-results.jsonPre-Audit Checklist
Before engaging a professional auditor, verify:
Security Testing Checklist
==========================
Static Analysis
[ ] Slither passes with 0 high/medium severity findings
[ ] All suppressed findings have documented justifications
[ ] Mythril analysis run on all critical contracts
Test Coverage
[ ] 100% branch coverage on all state-mutating functions
[ ] Every custom error is exercised by at least one test
[ ] Reentrancy tests for all external call sequences
[ ] Access control tests for all privileged functions
[ ] Fuzz tests on all numeric operations
[ ] Invariant tests for core protocol properties
Code Quality
[ ] No floating pragma (pin to exact version)
[ ] No assembly unless absolutely necessary and audited separately
[ ] All TODO/FIXME comments resolved
[ ] Events emitted for all state changes
[ ] NatSpec documentation on all external/public functions
Known Vulnerability Patterns
[ ] CEI (Checks-Effects-Interactions) pattern followed throughout
[ ] No tx.origin authorization
[ ] No block.timestamp for precise timing
[ ] No assumption about msg.value in loops
[ ] No delegatecall to user-controlled addresses
[ ] No selfdestruct (deprecated in EIP-6780)Summary
Smart contract security testing requires a layered approach: Slither for fast static analysis on every commit, Mythril for deeper symbolic execution on critical contracts, Echidna for property-based security fuzzing, and manual security-focused test cases for known vulnerability patterns. None of these tools replaces a professional audit, but using all of them before the audit means auditors spend their time finding novel issues rather than catching mechanical errors that automated tools already know how to find.