Introduction

As a Web3 security company, we’ve spent countless hours dissecting smart contracts and blockchain code bases, looking for vulnerabilities that could make or break a blockchain application. One of the most fundamental aspects of auditing is choosing the right approach to analyze the contract. Do we break it down line by line without running it, or do we put it through rigorous tests to see how it behaves under real-world conditions?

The answer is both.

Static and dynamic analysis are two critical frameworks in our arsenal, and understanding how they work is essential for anyone serious about ensuring smart contract security. Static analysis lets us catch issues before a contract even runs, while dynamic analysis helps us uncover vulnerabilities that only emerge during execution.

Let’s break down what each method brings to the table and why we use both to ensure the program under test (PUT) is bulletproof.

Static Analysis: Identifying Vulnerabilities Before Execution

Static analysis is like performing a security review without ever deploying or executing the contract. It’s usually the first step in any thorough smart contract audit. By going through the code, we can identify vulnerabilities in logic, structure, and security practices that could break or inflict damage on the implementation during compile time.

One of the biggest advantages of static analysis is speed. Automated tools can scan thousands of lines of code in seconds, flagging potential issues such as reentrancy attacks, uninitialized variables, and integer overflows. But as auditors, we don’t just rely on frameworks; instead, once the scanners flag any issues, we manually go through those findings, verify their legitimacy, and build upon those for more complex vulnerabilities that automated scanners might miss.

Key Techniques in Static Analysis

Program Semantics

Program semantics refers to the study of how programs execute and what they mean. It provides a formal framework for understanding program behaviour, ensuring that software (including smart contracts) behaves as expected.

How It Works:

• Operational Semantics: Describes execution behaviour in terms of state changes, often using an abstract machine.
• Denotational Semantics: Represents program meaning as mathematical functions, making it useful for reasoning about correctness.
• Abstract Interpretation: Approximates program behaviour to detect possible errors without executing the code.

Use in Smart Contract Audits:

• Helps formally verify correctness properties, ensuring that contract execution aligns with expectations.
• Enables security proofs, such as verifying that a function always returns the correct value.
• Can be used to model and analyze execution paths to detect unexpected behavior.

Example:

• Operational semantics define how an Ethereum smart contract updates state variables during execution.
• A security researcher could use denotational semantics to mathematically prove that a contract never enters an invalid state.

Dataflow Analysis

Dataflow analysis examines how data moves through a program, helping detect potential issues like unused variables, dead code, and security risks.

How It Works:

• Analyzes variable lifetimes and information flow through a control flow graph.
• Uses techniques like constant propagation, live variable analysis, and taint analysis to detect issues.
• Helps optimize code by identifying redundant calculations and unreachable statements.

Use in Smart Contract Audits:

• Detects dead code, ensuring that unused functions do not introduce attack surfaces.
• Identifies tainted data sources, which may lead to vulnerabilities like unchecked external calls.
• Helps prevent gas inefficiencies by detecting unnecessary storage operations.

Example:

• Reaching Definitions Analysis helps determine whether a variable has been assigned a value before being used in a Solidity contract.
• This can prevent uninitialized variable exploits, where attackers leverage undefined states to manipulate contract execution.

Interprocedural Analysis

Interprocedural analysis examines how data and control flow across multiple functions rather than just within a single function.

How It Works:

• Uses call graphs to map relationships between functions.
• Tracks cross-function dependencies to detect bugs that arise from function interactions.
• Helps identify side effects caused by function calls.

Use in Smart Contract Audits:

• Detects unexpected interactions between contract functions, preventing security flaws.
• Helps optimize contracts by eliminating redundant function calls.
• Ensures proper access control enforcement across multiple contract components.

Example:

• Call Graph Analysis in Solidity smart contracts ensures that a function intended for internal use is not inadvertently exposed to external callers.
• This prevents improper access control vulnerabilities, such as an external attacker exploiting an internal helper function.

Pointer Analysis

Pointer analysis determines how pointers (or references) interact within a program to detect memory errors, aliasing issues, and performance bottlenecks.

How It Works:

• Identifies aliasing, where multiple variables refer to the same memory location.
• Detects dangling references, which could lead to security vulnerabilities.
• Used in languages like C, C++, and low-level bytecode analysis but also applies to storage pointer management in smart contracts.

Use in Smart Contract Audits:

• Ensures secure memory and calldata stack handling in EVM-based contracts.
• Helps detect unexpected contract state modifications due to aliasing.
• Aids in gas optimization by identifying unnecessary storage operations.

Example:

• In Solidity, mapping types serve as references to random storage locations. Improper handling can lead to data corruption or unintended writes to storage.
• Pointer analysis techniques can identify cases where one mapping accidentally overwrites another due to improper index calculation.

Bytecode Analysis

Bytecode analysis involves examining the low-level representation of a program executed by a virtual machine (e.g., Ethereum Virtual Machine). It is crucial for verifying smart contracts post-compilation.

How It Works:

• Analyzes compiled EVM bytecode to detect vulnerabilities not visible at the source-code level.
• Uses pattern matching, control flow analysis, and symbolic execution.
• Helps ensure that optimizations do not introduce security risks.

Use in Smart Contract Audits:

• Detects obfuscated vulnerabilities that static analysis tools might miss at the source-code level.
• Helps verify compiler correctness, ensuring that Solidity-to-EVM conversion does not introduce flaws.
• Identifies mis-compilation issues, preventing unintended opcode behaviours.

Example:

• Bytecode Analysis of a Solidity Smart Contract can uncover unexpected gas usage patterns, ensuring the contract adheres to best practices.
• It can also detect hidden backdoors, such as self-destruct calls that were not present in the original source code but introduced via bytecode modifications.

Limitations of Static Analysis

While static analysis is great for finding issues early, it isn’t perfect. It tends to produce false positives, meaning it sometimes flags issues that aren’t actually exploitable. Also, it doesn’t tell us how the contract behaves in a real blockchain environment. Some vulnerabilities only appear when the contract methods are executed, when interaction with other smart contracts, when variable blockchain environment states occur, or when there is unpredictable user input.

Dynamic Analysis: Putting Contracts to the Test

If static analysis is reading the blueprint of a building, dynamic analysis is testing the actual building’s structure internally and externally. This method involves executing the contract in different environments to observe how it behaves under various conditions. It helps us catch issues like unexpected state changes, gas inefficiencies, and execution failures that static analysis might miss.

When we conduct dynamic analysis, we look at how the contract handles edge cases, stress testing it against high transaction volumes and unpredictable inputs. This method provides real-world insights that are crucial for ensuring security and reliability.

Key Techniques in Dynamic Analysis

Symbolic Execution

Symbolic execution is a powerful technique used in smart contract security analysis to systematically explore a contract’s execution paths and detect vulnerabilities before deployment. Instead of executing the contract with actual values, it uses symbolic variables to represent inputs, allowing auditors to analyze all possible execution paths without manually testing each scenario.

How It Works

1. Symbolic Input Assignment
   • Instead of using real transaction inputs (e.g., msg.sender = 0x123…), the contract is executed with symbolic variables (X, Y, Z).
   • This means every function and condition is evaluated for all possible values, making it easier to detect edge cases.
2. Path Exploration & Constraint Solving
   • The execution engine systematically explores all feasible execution paths.
   • Each condition (e.g., if (balance > 100)) creates a branch, leading to different possible outcomes.
   • A Satisfiability Modulo Theories (SMT) solver determines whether each path can be executed.
3. Vulnerability Detection
   • The tool flags unreachable code, invalid state transitions, integer overflows, and access control flaws.
   • If a path leads to an unsafe state (e.g., allowing unauthorized access), it generates a test case demonstrating the exploit.

Example

Vulnerable Code:

Using symbolic execution, we set:

• a = X (symbolic value)
• b = Y (symbolic value)

The solver checks if X + Y > 2^256 – 1, confirming whether an overflow is possible.

Satisfiability Modulo Theories (SMT) Based Techniques

SMT-based techniques involve using automated reasoning to analyze smart contracts by solving logical constraints. These techniques leverage SMT solvers to verify the correctness, security, and functional behaviour of contracts by encoding contract logic as mathematical formulas.

An SMT solver is a tool that determines whether a given logical formula is satisfiable, meaning whether there exists an assignment of values that makes the formula true.

How It Works:

1. Formal Representation of Code:
   • The contract’s logic is translated into logical formulas involving mathematical theories (e.g., arithmetic, bitwise operations, and boolean logic).
   • This is done using Intermediate Representation (IR) techniques.
2. Constraint Generation:
   • The execution paths of the smart contract are encoded as constraints.
   • These constraints define conditions under which certain vulnerabilities might occur (e.g., “Under what conditions can an overflow happen?”).
3. Automated Reasoning:
   • An SMT solver (e.g., Z3, CVC4, Yices) attempts to prove or disprove the existence of vulnerabilities by solving the constraints.
   • If a satisfiable solution exists for an unsafe state, the contract is vulnerable.
   • If the solver proves no solution exists, the contract is safe against that particular issue.

Common Theories Used in SMT-Based Analysis

SMT solvers handle multiple mathematical theories simultaneously. In smart contract analysis, the most relevant ones include:

Concolic Testing

Concolic testing (a combination of concrete and symbolic execution) is a technique used to automatically generate test cases by analyzing both real inputs (concrete execution) and abstract symbolic values (symbolic execution). It is particularly useful for detecting edge cases and maximizing code coverage.

How It Works:

• Concrete Execution: The program runs with real inputs to observe how it behaves under normal conditions.
• Symbolic Execution: The same execution path is analyzed with symbolic variables instead of concrete values. This helps determine alternative execution paths that were not covered in the original test.
• Constraint Solving: The system generates new test cases by solving constraints derived from symbolic execution, ensuring that new paths in the program are explored.
• Iterative Refinement: The process repeats, gradually increasing test coverage and identifying hard-to-reach vulnerabilities.

Use in Smart Contract Audits:

• Detecting Edge Cases: Concolic testing helps uncover corner-case vulnerabilities in smart contracts, such as integer overflows, reentrancy, and access control flaws.
• Maximizing Code Coverage: Ensures that as many execution paths as possible are tested, making security audits more robust.
• Improving Fuzz Testing: Works well alongside fuzzing by providing a more structured way to explore execution paths.

Example:

• A concolic testing tool for Solidity executes a smart contract with both real and symbolic inputs. If a transaction normally executes without failure, but symbolic execution reveals a hidden vulnerability only triggered under specific conditions, the tool generates a new test case to confirm the issue.
• For instance, if a function behaves correctly for most users but fails when the sender’s address has a specific byte pattern, concolic testing can discover this rare but exploitable flaw.

Limitations of Dynamic Analysis

While dynamic analysis is powerful, it comes with challenges. It requires more computational resources and time, making it less scalable than static analysis for large codebases. Plus, we can’t test every possible execution path, meaning some vulnerabilities might still go undetected.Static vs. Dynamic Analysis: Which One Wins?

The truth is, neither method alone is enough. As auditors, we’ve seen cases where static analysis flagged potential issues that dynamic analysis proved harmless and cases where dynamic analysis revealed security flaws that static analysis completely missed.

Here’s a quick comparison of the two approaches:

Why We Should Use Both

It is advisable to never rely on just one approach. Static analysis helps to identify potential vulnerabilities early in the process, while dynamic analysis validates those findings and uncovers additional issues that only appear during execution. Using both techniques together allows for a more thorough and effective audit.

By combining static and dynamic analysis, we can:

• Detect vulnerabilities that exist in both code structure and execution.
• Validate whether theoretical vulnerabilities pose real threats.
• Strengthen smart contract security before and after deployment.
• Minimize the risk of undetected vulnerabilities that could lead to exploits.

Final Thoughts

Smart contract security isn’t just about running tools or following a checklist. It requires a deep understanding of both code and execution behaviour. Static and dynamic analysis are two sides of the same coin, each playing a crucial role in securing blockchain applications.

As auditors, our goal should be to ensure that every smart contract we review is as secure as possible before it goes live. By leveraging both static and dynamic analysis, we can build more resilient, trustworthy, and efficient smart contracts that stand the test of time in the ever-evolving world of Web3.