Static Analysis Tools
Overview of Static Analysis
Static analysis examines code without executing it, identifying potential vulnerabilities through syntax analysis, control flow examination, and pattern recognition. These tools form the foundation of our automated security assessment process.
Key Static Analysis Tools
Slither
Description: Slither is a Solidity static analysis framework written in Python. It runs a suite of vulnerability detectors, prints visual information about contract details, and provides an API to easily write custom analyses.
Use Cases:
- Detecting common vulnerabilities
- Visualization of contract inheritance and function call graphs
- Custom detector development for project-specific issues
- Automated report generation
Key Features:
- Extensive vulnerability detector suite (70+ detectors)
- Contract summarization
- Inheritance graph generation
- Function call visualization
- Highly customizable
Integration in Our Process: We run Slither as a first-pass analysis on all smart contract codebases, often with custom detectors tailored to the project's specific needs.
Mythril
Description: Mythril is a security analysis tool for EVM bytecode. It uses symbolic execution, SMT solving, and taint analysis to detect various contract vulnerabilities.
Use Cases:
- Identifying complex vulnerability patterns
- Detecting issues that require runtime path analysis
- Generating proof-of-concept attack transactions
- Finding edge case vulnerabilities
Key Features:
- Symbolic execution engine
- Control flow analysis
- Constraint solver integration
- Detailed exploit generation
Integration in Our Process: We use Mythril to perform deep analysis on critical contract components, particularly where complex state transitions need verification.
Securify
Description: Securify is a security scanner for Ethereum smart contracts that uses formal verification techniques to analyze code for security issues.
Use Cases:
- Analyzing contract security properties
- Checking compliance with security patterns
- Identifying violations of security best practices
Key Features:
- Formal verification approach
- Pattern-based vulnerability detection
- Low false-positive rate for supported vulnerability classes
Integration in Our Process: We apply Securify as a complementary analysis tool, particularly for its strengths in analyzing compliance with security patterns.
Manticore
Description: Manticore is a symbolic execution tool for analysis of smart contracts and binaries that can verify source code integrity and detect vulnerabilities.
Use Cases:
- Verification of critical security properties
- Discovery of unexpected execution paths
- Generation of test cases for edge conditions
Key Features:
- Fine-grained control over execution
- State space exploration
- Custom constraint solving
- Python API for custom analyses
Integration in Our Process: We use Manticore for in-depth analysis of specific functions or modules where precision is critical and the state space is manageable.
Certora Prover
Description: The Certora Prover uses formal verification to mathematically prove that a smart contract implementation satisfies a set of specified rules or properties.
Use Cases:
- Proving security properties of critical contracts
- Verifying implementation against specifications
- Ensuring correctness of complex state transitions
Key Features:
- Formal specification language
- Verification of complex properties
- Exhaustive analysis of all possible states
- Counter-example generation
Integration in Our Process: For critical infrastructure or high-value contracts, we use Certora to formally verify key security properties when appropriate.
Custom Static Analysis
Beyond off-the-shelf tools, we develop custom static analyzers for specific projects:
Protocol-Specific Analyzers
We create custom tools to check for vulnerabilities specific to certain protocol designs, such as:
- AMM-specific vulnerability checkers
- Lending protocol collateral validators
- Staking and reward mechanism analyzers
Code Quality Analyzers
We use and extend linting tools to enforce best practices:
Limitations of Static Analysis
While powerful, static analysis has inherent limitations:
- May produce false positives requiring manual verification
- Cannot fully assess runtime or economic vulnerabilities
- Limited understanding of developer intent
- May miss vulnerabilities dependent on external state
We address these limitations by:
- Combining multiple tools with different approaches
- Supplementing with dynamic analysis and testing
- Applying manual review to validate findings
- Using economic and game-theoretic analysis
Integration into CI/CD
For ongoing projects, we help integrate static analysis into development workflows:
- GitHub Actions integration
- Pre-commit and pre-push hooks
- Automated reporting and ticketing
- Security gate enforcement
Static analysis tools provide a critical first line of defense in identifying potential security issues, but they are most effective when combined with other testing methodologies and expert review.