Smart Contract Security Testing: Slither, Mythril, and Static Analysis

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-analyzer

Basic 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-informational

Understanding 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 integration

Every 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 modifiers

Mythril: 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/myth

Basic 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.sol

What 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/echidna

Writing 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.json

Pre-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.

Read more