Secureum Book
  • 🛡️Secureum Bootcamp
    • 🛡️Secureum Bootcamp
    • 🙌Participate
    • 📜History
  • 📚LEARN
    • Introduction
      • 🔷1. Ethereum Basics
        • 1.1 Ethereum: Concept, Infrastructure & Purpose
        • 1.2 Properties of the Ethereum Infrastructure
        • 1.3 Ethereum vs. Bitcoin
        • 1.4 Ethereum Core Components
        • 1.5 Gas Metering: Solving the Halting Problem
        • 1.6 web2 vs. web3: The Paradigm Shift
        • 1.7 Decentralization
        • 1.8 Cryptography, Digital Signature & Keys
        • 1.9 Ethereum State & Account Types
        • 1.10 Transactions: Properties & Components
        • 1.11 Contract Creation
        • 1.12 Transactions, Messages & Blockchain
        • 1.13 EVM (Ethereum Virtual Machine) in Depth
        • 1.14 Transaction Reverts & Data
        • 1.15 Block Explorer
        • 1.16 Mainnet & Testnets
        • 1.17 ERCs & EIPs
        • 1.18 Legal Aspects in web3: Pseudonymity & DAOs
        • 1.19 Security in web3
        • 1.20 web2 Timescales vs. web3 Timescales
        • 1.21 Test-in-Prod. SSLDC vs. Audits
        • Summary: 101 Keypoints
      • 🌀2. Solidity
        • 2.1 Solidity: Influence, Features & Layout
        • 2.2 SPDX & Pragmas
        • 2.3 Imports
        • 2.4 Comments & NatSpec
        • 2.5 Smart Contracts
        • 2.6 State Variables: Definition, Visibility & Mutability
        • 2.7 Data Location
        • 2.8 Functions
        • 2.9 Events
        • 2.10 Solidity Typing
        • 2.11 Solidity Variables
        • 2.12 Address Type
        • 2.13 Conversions
        • 2.14 Keywords & Shorthand Operators
        • 2.15 Solidity Units
        • 2.16 Block & Transaction Properties
        • 2.17 ABI Encoding & Decoding
        • 2.18 Error Handling
        • 2.19 Mathematical & Cryptographic Functions
        • 2.20 Control Structures
        • 2.21 Style & Conventions
        • 2.22 Inheritance
        • 2.23 EVM Storage
        • 2.24 EVM Memory
        • 2.25 Inline Assembly
        • 2.26 Solidity Version Changes
        • 2.27 Security Checks
        • 2.28 OpenZeppelin Libraries
        • 2.29 DAppSys Libraries
        • 2.30 Important Protocols
        • Summary: 201 Keypoints
      • 🔏3. Security Pitfalls & Best Practices
        • 3.1 Solidity Versions
        • 3.2 Access Control
        • 3.3 Modifiers
        • 3.4 Constructor
        • 3.5 Delegatecall
        • 3.6 Reentrancy
        • 3.7 Private Data
        • 3.8 PRNG & Time
        • 3.9 Math & Logic
        • 3.10 Transaction Order Dependence
        • 3.11 ecrecover
        • 3.12 Unexpected Returns
        • 3.13 Ether Accounting
        • 3.14 Transaction Checks
        • 3.15 Delete Mappings
        • 3.16 State Modification
        • 3.17 Shadowing & Pre-declaration
        • 3.18 Gas & Costs
        • 3.19 Events
        • 3.20 Unary Expressions
        • 3.21 Addresses
        • 3.22 Assertions
        • 3.23 Keywords
        • 3.24 Visibility
        • 3.25 Inheritance
        • 3.26 Reference Parameters
        • 3.27 Arbitrary Jumps
        • 3.28 Hash Collisions & Byte Level Issues
        • 3.29 Unicode RTLO
        • 3.30 Variables
        • 3.31 Pointers
        • 3.32 Out-of-range Enum
        • 3.33 Dead Code & Redundant Statements
        • 3.34 Compiler Bugs
        • 3.35 Proxy Pitfalls
        • 3.36 Token Pitfalls
        • 3.37 Special Token Pitfalls
        • 3.38 Guarded Launch Pitfalls
        • 3.39 System Pitfalls
        • 3.40 Access Control Pitfalls
        • 3.41 Testing, Unused & Redundand Code
        • 3.42 Handling Ether
        • 3.43 Application Logic Pitfalls
        • 3.44 Saltzer & Schroeder's Design Principles
        • Summary: 201 Keypoints
      • 🗜️4. Audit Techniques & Tools
        • 4.1 Audit
        • 4.2 Analysis Techniques
        • 4.3 Specification, Documentation & Testing
        • 4.4 False Positives & Negatives
        • 4.5 Security Tools
        • 4.6 Audit Process
        • Summary: 101 Keypoints
      • ☝️5. Audit Findings
        • 5.1 Criticals
        • 5.2 Highs
        • 5.3 Mediums
        • 5.4 Lows
        • 5.5 Informationals
        • Summary: 201 Keypoints
  • 🌱CARE
    • CARE
      • CARE Reports
  • 🚩CTFs
    • A-MAZE-X CTFs
      • Secureum A-MAZE-X
      • Secureum A-MAZE-X Stanford
      • Secureum A-MAZE-X Maison de la Chimie Paris
Powered by GitBook
On this page
  • Static Analysis
  • Fuzzing
  • Symbolic Checking
  • Formal Verification
  • Manual Analysis
  1. LEARN
  2. Introduction
  3. 4. Audit Techniques & Tools

4.2 Analysis Techniques

The analysis techniques used in audits involve a combination of different methods that are applied to the project codebase along with any accompanying specification and documentation. Many are automated analysis performed with tools with some level of manual assistance and there are generally eight broad categories:

  • There's specification analysis that is completely manual.

  • There's documentation analysis that's also manual.

  • There's software testing which is automated.

  • Static analysis again automated.

  • Fuzzing.

  • Combination.

  • Automated techniques.

    • Symbolic checking.

    • Formal verification s automated with some level of manual assistance.

  • Manual analysis (that is entirely manual).

Let's discuss each of these categories in some detail.

Static Analysis

Static analysis is a technique for analyzing program properties without actually executing the program. This contrasts to software testing, where programs are actually executed or run with different inputs to examine their behavior.

With smart contracts, static analysis can be performed on the Solidity code directly or on the EVM bytecode, and it is usually a combination of control flow and Data Flow analysis.

Some of the most widely used static analysis tools with smart contracts are Slither (which is a static analysis tool from Trail of Bits) and Maru (which is a static analysis tool from ConsenSys Diligence), both of which analyze intermediate representations derived from Solidity code of smart contracts.

Fuzzing

Fuzzing (or fuzz testing) is an automated software testing technique that involves providing invalid, unexpected or random data as inputs to software. This contrasts again with software testing in general where chosen and valid data is used for testing.

So, firstly these invalid, unexpected or random data are provided as inputs, then the program is monitored for exceptions such as crashes, failing built-in code assertions or potential memory leaks.

Fuzzing is especially relevant to smart contracts because anyone can interact with them on the blockchain by providing random inputs without necessarily having a valid reason to do so, or any expectation from such an interaction. This is in the context of arbitrary Byzantine fault behavior that we have discussed multiple times earlier. The widely used Fuzzing tools for smart contracts are Echidna from Trail of Bits, Harvey from ConsenSys Diligence and most recently, Foundry's Fuzz testing.

Symbolic Checking

Symbolic checking is a technique of checking for program correctness by using symbolic inputs to represent a set of states and transitions instead of using real inputs and enumerating all the individual states or transitions separately. The related concept of model checking (or property checking) is a technique for checking whether a finite state model of a system meets a given specification, and in order to solve such a problem algorithmically both the model of the system and its specification are formulated in some precise mathematical language.

The problem itself is formulated as a task in logic with the goal of solving that formula. There is decades of research and development in this domain and I would encourage anyone interested to explore the many references available. Here, for smart contracts, Manticore from Trail of Bits and Mythril from Consensys Diligence are two widely used symbolic checkers which we will touch upon in later.

Formal Verification

Formal verification is the act of proving or disproving the correctness of algorithms underlying the system with respect to a certain formal specification of a property using formal methods of mathematics.

Formal verification is effective at detecting complex bugs, which are generally hard to detect manually or using simpler automated tools. Formal verification needs a specification of the program being verified and techniques to compare the specification with the actual implementation. Some of the tools in this space are Certora's Prover and Chain Security's VerX. kEVM from Runtime Verification is a formal verification framework that models EVM semantics.

Manual Analysis

Manual analysis is complementary to automated analysis using tools. It serves a critical need in smart contact audits. Today, automated analysis using tools is cheap because it typically uses open source software that is free to use. Automated analysis is also fast deterministic and scalable, however it's only as good as the properties it is made aware of, which is typically limited to those concerning Solidity and EVM related constraints.

Manual analysis on the other hand is expensive, slow, non-deterministic and not scalable because human expertise in smart contract security is a rare and expensive skillset today, and we are slower, more prone to error and also inconsistent. Manual analysis however is the only way today to infer and evaluate business logic and application level constraints which is where a majority of the serious vulnerabilities are being found.

Previous4.1 AuditNext4.3 Specification, Documentation & Testing

Last updated 1 year ago

📚
🗜️