TestingSecurityAudit
The Power of Fuzzing and Formal Verification in Blockchain Security
20 de febrero de 2024•secoalba
- zealynx - 2024-02-20*
1. Introduction
In this article, I want to reveal why implementing fuzzing and formal verification in your projects isn't just important—it's crucial for your success. These advanced security techniques have become the gold standard for industry giants like Uniswap, Optimism, and Aave. The reason? In an ecosystem where a single error can cost millions, security is non-negotiable.
We'll explore how these tools are revolutionizing smart contract security and why industry leaders consider them indispensable. From early vulnerability detection to building trust with investors and users, you'll discover that fuzzing and formal verification aren't exclusive to the big players.
Why should you follow the example of these top-tier protocols? Throughout this article, we'll unravel the benefits of these techniques for projects of any size. I'll show you how they can transform the reliability of your code and elevate your project to the next level of robustness and confidence.
What is Fuzzing?
Fuzzing, or fuzz testing, is a technique where invalid, unexpected, or random data is passed into a system to discover coding errors and security loopholes.
When applied to web applications, fuzzing targets common web vulnerabilities by determining data injection points to identify which entry points might be susceptible to such vulnerabilities.
What is Formal Verification?
Formal Verification (FV) uses mathematical modeling and logical analysis to ensure program security and correctness. A key aspect of FV is symbolic execution, which assigns symbolic values to inputs, allowing the exploration of various program paths in a single analysis.
This technique helps verify if a program can violate certain conditions or reach risky states, using tools like SMT solvers for feasibility assessment. Symbolic execution thus enhances testing, offering a more comprehensive way to establish a program's safety and correctness.
2. Benefits of Fuzzing
Fuzzing represents an advanced security testing methodology that subjects code to an extensive set of inputs, methodically exploring scenarios that could go unnoticed in conventional testing processes.
Key features:
- Executes millions of test cases in relatively short periods
- Offers comprehensive and efficient coverage
The core of fuzzing consists of a sophisticated generator of random or semi-random inputs. This component produces a continuous stream of test data designed to explore the operational limits of the target.
The diverse and often unexpected nature of these inputs allows simulation of a wide range of potential interactions, including those that could challenge typical usage expectations and, consequently, reveal latent vulnerabilities in the program structure.
This method operates as a systematic explorer of the vast spectrum of possible inputs. Each generated data functions as a unique test case, meticulously designed to identify anomalous behaviors or hidden vulnerabilities.
Advantages:
- Comprehensive and continuous test coverage
- Significantly overcomes limitations of manual testing methodologies
- Discovers edge cases and rare errors
- Identifies flaws that escape conventional methods
- Detects subtle anomalies in behavior
3. Benefits of Formal Verification
Imagine a tool capable of examining every corner of your code, meticulously exploring all possible paths it could take. That's exactly what Formal Verification (FV) does.
FV employs a variety of mathematical and logical techniques to analyze code.
Each method provides a unique perspective to the analysis, allowing a deep and multifaceted understanding of the program.
One of the techniques used is symbolic execution, which operates with abstract values instead of concrete data. This allows consideration of multiple scenarios simultaneously, as if we were giving the program a wildcard instead of a specific number.
The result?
A comprehensive and rigorous understanding of your program. FV can categorically demonstrate that certain dangerous conditions are unreachable, offering a security guarantee that surpasses the capabilities of traditional testing. It's like having a team of meticulous detectives examining every possible scenario, no matter how unlikely.
This methodology provides:
- A level of mathematical certainty about program behavior
- Identification of potential hidden vulnerabilities
- Compliance with security specifications and requirements
FV acts as a tireless guardian, thus elevating the reliability and robustness of software to new levels.
4. How can Fuzzing and Formal Verification improve Security Reviews?
The combination of Formal Verification and Fuzzing creates a complementary and powerful approach to security, enhancing traditional Manual Security Reviews.
| Formal Verification | Fuzzing |
|---|---|
| Rigorous and mathematical analysis | Dynamic and comprehensive exploration |
| Precision of static analysis | Breadth of dynamic testing |
The implementation of these techniques in a development project represents a significant advance in security strategy. They integrate the precision of static analysis with the breadth of dynamic testing, providing more complete coverage than either method alone.
In the current context:
- Security is critical
- The adoption of these advanced tools becomes a strategic necessity
- They improve vulnerability detection
- They increase overall reliability
- They demonstrate a serious commitment to product quality and security
The incorporation of Formal Verification and Fuzzing represents an investment in the integrity and robustness of development. In an increasingly complex and threatening digital landscape, these techniques offer a crucial advantage in protecting against vulnerabilities and ensuring the quality of the final product.
| Technique | Strengths | Best For | Key Features |
|---|---|---|---|
| Fuzzing | - Real-world testing - Error discovery - Handling unexpected inputs | - Complex scenarios - Finding edge cases - Detecting anomalies | - Automated input generation - High-speed execution - Dynamic exploration |
| Formal Verification | - Comprehensive analysis - Conceptual correctness - Mathematical proofs | - Security assurance - Proving correctness - Analyzing all states | - Mathematical techniques - Symbolic execution - Static analysis |
The Synergy of Combined Techniques
- Comprehensive Coverage:
- Automated breadth through Fuzzing
- Mathematical depth via Formal Verification
- Contextual insight from Manual Reviews
- Synergistic Strengths:
- Fuzzing: Uncovers non-obvious vulnerabilities
- Formal Verification: Ensures logical correctness and compliance with security properties
- Manual Reviews: Address high-level design issues
- Iterative Improvement:
- Findings from each method inform and enhance the others
- Continuous refinement of security measures
5. Fuzzing vs. Formal Verification: Strengths and Applications
| Feature | Fuzzing | Formal Verification | Unit Test |
|---|---|---|---|
| Approach | Random or unexpected data | Mathematical modeling and logic | Predefined test cases |
| Coverage | High, including edge cases | Complete for given model | Limited to test cases |
| Automation | Highly automated | Partially automated | Variable |
| Complexity | Medium | High | Low to Medium |
| Execution Time | Fast | Can be slow for complex systems | Variable |
| Bug Detection | Effective for unknown bugs | Proves absence of certain errors | Finds known bugs |
| Applicability | Wide, especially in security | Critical for high-security systems | Universal |
4. Benefits for Developers and Businesses
Improved Security and Quality
For Developers
- Discovers edge cases and unexpected behaviors
- Provides mathematical certainty for critical properties
- Facilitates early bug detection in the development cycle
For Businesses
- Enhances protocol security
- Reduces financial risks from potential exploits
- Builds investor and user trust
Difficulty of Fixing Bugs
| Stage | Difficulty |
|---|---|
| Development | Easy |
| Testing | Moderate |
| Production | Difficult |
| Post-Deployment | Extremely Difficult |
Key Benefits Overview
For Developers
- Higher code confidence
- Reduced stress from potential vulnerabilities
- Focus on innovation rather than bug fixing
For Businesses
- Regulatory compliance readiness
- Easier partnerships and integrations
- Increased market differentiation
Our Work
In this section, we present practical examples of how we've integrated Formal Verification and Fuzzing techniques into our blockchain projects. These case studies demonstrate the tangible benefits of these advanced methodologies in enhancing smart contract security and reliability. By sharing our experiences, we aim to illustrate the real-world impact of these tools and inspire their broader adoption in blockchain development.
Possum Labs: Stake yield-bearing assets
- Fuzzing: Foundry
- Invariant testing: Echidna/Medusa
- Formal Verification: Halmos, ItyFuzz
Glif: Liquidity Mining
- Fuzzing: Foundry
- Invariant testing: Echidna/Medusa
- Formal Verification: Halmos, Kontrol, ItyFuzz
Wedefin: Decentralized Index Fund
Revert: AMM Liquidity Providers
Bastion Wallet: ERC-4337, Account Abstraction SDK
- Fuzzing: Foundry-1, Foundry-2
- Invariant testing: Echidna/Medusa
- Formal Verification: Halmos-1, Halmos-2
How These Practices Could Benefit These Protocols
Implementing fuzzing and formal verification in decentralized financial protocols offers significant advantages. These techniques enhance security by identifying subtle vulnerabilities that traditional methods might miss. They increase user trust, reduce economic risks, and allow for continuous security assessment as systems evolve.
Moreover, they prevent potentially catastrophic failures and reputational damage. In a rapidly expanding market, demonstrating robust security measures can provide a competitive edge, attracting more participants and investors.
Why top-tier DeFi protocols are using Fuzzing and Formal Verification?
In this section, I would like to highlight the crucial importance of implementing security tools in your projects, a practice that large protocols have adopted without hesitation.
Before delving deeper, it is fundamental to emphasize the critical role these tools play in the development of any technology. We have all witnessed numerous hacks and vulnerabilities affecting various types of applications, and we are aware of the devastating consequences these incidents can entail.
Numerous institutions, applications, and organizations invest a significant amount of resources to keep their systems as secure as possible. This investment is crucial, as having exceptional code is of little use if a high level of security cannot be guaranteed.
Any breach, no matter how small, can trigger disastrous consequences, such as loss of funds, erosion of user trust, and even the departure of investors. It's important to note that recovering from such problems is usually extremely complicated.
UNISWAP
What reasons made them use fuzzing/Formal verification?
The reasons that drove Uniswap to adopt these techniques over time are directly related to the growing complexity of their new implementations and their commitment to protocol security.
For example, these techniques have been used to:
- Ensure the mathematical correctness of concentrated liquidity algorithms, a fundamental component of Uniswap v3.
- Ensure that their price formation and liquidity management mechanisms function exactly as expected under all possible conditions, thus minimizing the risk of unexpected behaviors or vulnerabilities.
- Continuously improve security throughout the development process by implementing advanced fuzzing techniques. This proactive approach helps identify potential issues in early stages of the development cycle.
These practices not only strengthen the technical integrity of the protocol but also increase user and investor confidence by demonstrating a solid commitment to security in an increasingly complex and competitive DeFi ecosystem.
OPTIMISM
How have they used formal verification to secure their protocol?
Optimism has integrated advanced formal verification into their Continuous Integration (CI) system. This implementation primarily focuses on verifying the pausability mechanism of their L1 contracts.
The verification process centers on:
- Verifying that the pausability mechanism functions correctly, allowing L2-to-L1 transactions to be halted when necessary.
- Ensuring that verification is maintained as the code evolves.
The verification executes symbolic property tests, allowing for exhaustive mathematical verification of all possible inputs, surpassing the limitations of traditional fuzzing.
This integration in Optimism's CI provides continuous verification of critical properties, mitigating risks associated with code changes and improving the overall security of the protocol after deployment.
AAVE
How have they used formal verification to secure their protocol?
Aave uses continuous formal verification to secure their protocol by:
- Implementing ongoing automated verification of all code contributions
- Utilizing advanced formal verification tools integrated into development processes
- Developing a new symbolic execution tool for comprehensive path coverage
- Creating an open-source database of security rules for community contributions
Why this approach?
- It ensures constant security checks on evolving code
- It detects vulnerabilities before deployment
- It mitigates risks from governance-introduced changes
Benefits
- Providing mathematical proofs of critical code areas' security
- Enabling 24/7 analysis of complex specifications
- Allowing rapid detection and prevention of potential vulnerabilities
LIDO
Why do they use fuzzing and formal verification techniques?
Lido implements these advanced security measures primarily due to the critical nature of their staking protocol and the high value of assets they manage.
These techniques allow them to ensure mathematical accuracy of their staking and reward systems, rigorously test operations across different networks, and identify potential vulnerabilities in new features before launch.
With this approach, Lido aims to protect user funds and maintain the stability of their platform.
NASA and Formal Verification: A Model for DeFi Security
While NASA might seem far removed from the world of DeFi, its approach to security and system integrity offers valuable lessons for blockchain protocols.
NASA's Commitment to Formal Verification
NASA has been a pioneer in the use of formal verification techniques, recognizing their critical importance in mission-critical systems where failure is not an option:
- Long-standing Practice: NASA has been using formal methods since the 1970s, with increased emphasis in recent decades.
- Substantial Investment: A significant portion of NASA's budget for software development and verification is allocated to formal methods.
- Wide Application: NASA applies formal verification across various projects, from flight control systems to Mars rover software.
Key Examples of NASA's Formal Verification Use
- Space Shuttle: NASA used formal methods to verify the Space Shuttle's flight control software.
- Mars Curiosity Rover: The mission-critical software for the Mars Science Laboratory, including the Curiosity rover, underwent rigorous formal verification.
- Living with a Star Program: NASA employed formal verification techniques in the development of software for solar observation satellites.
Why Formal Verification is Crucial for NASA
- Zero Tolerance for Errors: In space missions, even minor software errors can lead to catastrophic failures, loss of billion-dollar equipment, or even loss of life.
- Complex Systems: Aerospace systems are incredibly complex, making traditional testing methods insufficient.
- Unreproducible Conditions: Many space scenarios cannot be fully replicated on Earth, making formal proofs of correctness essential.
- Long-term Reliability: Space missions can last for decades, requiring software that remains reliable over extended periods without the possibility of patches or updates.
Lessons for DeFi
The parallels between NASA's needs and those of DeFi protocols are striking:
- Both deal with high-stakes environments where errors can lead to significant financial losses.
- Both operate in complex, often unpredictable environments.
- Both require long-term reliability and security.
By adopting NASA's rigorous approach to formal verification, DeFi protocols can significantly enhance their security posture, potentially preventing catastrophic failures and building greater trust in the ecosystem.
Vulnerabilities Discovered Through the Implementation of Fuzzing and Formal Verification in Well-Known Protocols
Everything mentioned above becomes even more relevant in the blockchain sector. Many protocols in this field handle significant amounts of capital, especially in DeFi projects.
Over time, these protocols have learned a crucial lesson: it's not enough to have a brilliant idea or an innovative product if its long-term security cannot be guaranteed. On these platforms, even the slightest security issue can have devastating consequences.
Compound Finance:
A critical vulnerability was detected in the liquidation system. Under extreme market conditions, incorrect collateral factor calculations could result in unjustified liquidations, putting users' assets at risk.
MakerDAO:
The auction mechanism had a significant flaw. During periods of high volatility, auctions could conclude at prices far below real value, potentially causing substantial fund losses for the protocol.
Uniswap v3:
A subtle error in fee calculation threatened the profitability of liquidity providers. The rounding issue in accumulated fees could result in gradual but significant losses over time.
Aave:
Formal verification prevented a critical vulnerability in flash loans. It was discovered that an attacker could momentarily manipulate asset prices, allowing them to obtain loans under unfairly favorable conditions.
Chainlink:
Potential vulnerabilities were identified in the price aggregation system. These flaws could allow manipulation of input data, compromising the integrity of reported prices across the network.
Synthetix:
Issues were uncovered in the staking and rewards mechanism. In high-volatility scenarios, incorrect reward calculations could result in unfair distribution, affecting token economics and user trust.
Which Protocols Benefit from These Types of Tests
The most prominent projects in the sector, those that have been with us since the beginning, share a common pattern: they have known how to efficiently manage their resources and maintain robust security practices over time.
These protocols conduct periodic audits, combining them with numerous testing campaigns focused on fuzzing and formal verification. A particularly effective strategy is to implement numerous fuzzing tests during protocol development, along with a formal verification approach at the most critical points.
The variety of protocols that benefit from these advanced security practices is surprisingly wide. Below, we present a table that illustrates the diversity of projects that have adopted these techniques, demonstrating how security is a priority:
| Category | Protocols |
|---|---|
| Lending | Aave, Compound, MakerDAO |
| DEX | Uniswap, SushiSwap, PancakeSwap |
| Derivatives | Synthetix, dYdX, Perpetual Protocol |
| Insurance | Nexus Mutual, InsurAce, Etherisc |
| Games and NFTs | Decentraland, OpenSea |
| Yield farming | Yearn Finance, Harvest Finance, Beefy Finance |
| Stablecoins | DAI (MakerDAO), USDC (Centre) |
| Privacy | Tornado Cash, Monero, Zcash |
| Oracles | Chainlink, Band Protocol, API3 |
| Asset Management | Set Protocol, Enzyme Finance, dHEDGE |
| Bridges | Polygon, Avalanche Bridge, Wormhole |
| Identity | Civic, Ontology, SelfKey |
| Storage | Filecoin, Storj, Sia |
| Prediction | Augur, Gnosis, Polymarket |
| Tokenization | RealT, Harbor, Polymath |
