Learn how to fuzz like a pro: Introduction to fuzzing

Echidna Workshop Streaming Series Part 1

This is the first part of a six-part series on Echidna, where the basics of Echidna are covered. The speaker talks about some housekeeping items and provides an overview of what will be covered in this workshop.

Introduction

• The workshop begins with music.

• The speaker introduces himself and welcomes everyone to the first Echidna Workshop streaming series.

• The speaker talks about the agenda for today's workshop and what will be covered in each section.

How to Find Bugs

• The speaker discusses different methodologies that can be employed to find bugs in code.

Fuzzing Methodologies

• The speaker explains what fuzzing is and how it fits into testing methodologies.

Interactive Exercises

• The speaker demonstrates how to use Echidna for fuzzing through interactive exercises.

Defining Good Invariance

• The last section covers how to define good invariance, which sets up for next week's workshop.

Overall, this transcript covers the introduction of the first part of a six-part series on Echidna. It includes information on finding bugs, fuzzing methodologies, interactive exercises using Echidna, and defining good invariance.

Introduction to Testing Techniques

This section introduces different testing techniques that can be used to find bugs in smart contracts. The speaker discusses the benefits and limitations of each technique.

Unit Testing

• Unit testing is a well-known technique that covers expected values.

• It has limitations as it may miss unexpected values, leading to edge cases.

• A unit test is just a dot on the input space line, unable to cover the entire breadth of input space.

• Edge cases are usually found through other testing methodologies.

Manual Review

• Manual review theoretically finds every possible bug in the code base.

• However, it's time-consuming, requires specific skill sets, and does not track code changes.

• Security audits are an example of manual review but are snapshots in time.

Fully Automated Analysis

• Fully automated analysis is quick and easy to use.

• Slither is an example of fully automated analysis but has limitations on how many types of bugs it can find.

Semi-Automated Analysis

• Semi-Automated Analysis is great for logic-related bugs that cannot be found easily with previous methodologies.

• Echidna is a semi-automatic analysis technique where humans guide the automated piece to do certain things well.

• It requires someone like you or me to look at the code and guide Echidna.

Bug Finding Journey with Echidna

In this section, we will go through a journey together using Echidna to find a bug in smart contract code.

Bug Finding Journey with Echidna

• The speaker shows a piece of code with a bug in it that we will use Echidna to find.

• The exchange rate is one E3 to 10 tokens, but the bug causes the transaction to revert, and you don't get any tokens.

• Echidna can be used to find this bug.

Conclusion

This transcript introduces different testing techniques that can be used to find bugs in smart contracts. Unit testing, manual review, fully automated analysis, and semi-automated analysis are discussed with their benefits and limitations. The bug finding journey with Echidna shows how it can be used to find bugs in smart contract code.

Introduction to Fuzz Testing

In this section, the speaker introduces fuzz testing and explains how it differs from traditional testing. They also introduce property-based testing as a way to approach fuzz testing in the smart contract world.

Fuzz Testing vs Traditional Testing

• Fuzz testing is different from traditional testing because it doesn't aim to crash the program with random inputs.

• Smart contracts don't technically have crashes, so we need a different approach to fuzzing.

• Property-based testing is a way to approach fuzzing in the smart contract world.

What is Property-Based Testing?

• Property-based testing involves defining properties that should always be true given some preconditions.

• The fuzzer generates random values and tests whether the properties hold or not.

• The goal of property-based testing is to test whether the system behaves as expected.

Examples of Properties

• An example invariant for an ERC20 token is that no user's balance should exceed the total supply of tokens.

• System properties define the expected behavior of a system or function.

Introduction to Echidna

In this section, the speaker introduces Echidna, an open-source tool used for semi-automated analysis in audits. The speaker explains that Echidna requires a target contract and properties to test.

How Echidna Works

• Echidna needs a Target contract and properties to test.

• The Target contract is what Echidna is fuzzing, while the properties are what it's trying to validate.

• With these two inputs, Echidna can try to validate the system behavior by checking if it violates any of the provided properties.

Summary of Finding Bugs with Semi-Automated Analysis

In this section, the speaker summarizes how to find bugs using semi-automated analysis and introduces property-based testing as a way of validating system behavior.

Finding Bugs with Semi-Automated Analysis

• The goal is to figure out properties that describe system behavior and use Echidna to validate or invalidate them.

• Property-based testing is better at finding hard-to-find bugs in code bases than other testing methodologies.

Key Considerations When Using Echidna

In this section, the speaker highlights key considerations when using Echidna for semi-automated analysis.

Key Considerations

• Think of Echidna as an externally owned account that sends transactions really fast with random values.

• It calls a sequence of functions with random inputs on both the Target and inherited contracts.

• Properties are resolved to a truthy value, meaning they must be true.

Exercise One: Checking for Correct Arithmetic

In this section, the instructor introduces exercise one and explains that they will be using Solidity 0.7 to check for correct arithmetic. They also discuss the Target contract and the transfer function.

Introduction to Exercise One

• Exercise one involves checking for correct arithmetic using Solidity 0.7.

• The Target contract is introduced, along with the token contract which inherits ownership.

• The transfer function is discussed as being important for exercise one.

Goals of Exercise One

• Goal 1: Add a property to check that Echidna caller cannot have more than an initial balance of 10,000 tokens.

• Echidna caller is defined as message.sender or the person sending transactions to the Target contract.

• Goal 2: Fix any bugs found and recheck properties with Echidna.

Setting Up Test Token Contract

• A new file called niche.soul is created with Solidity version set to 0.7.

• The token.sol file is imported into niche.soul.

• Inheritance is used so that test token inherits all functions from token and ownership from plausible.

Setting Up Echidna

• Setup involves defining Echidna caller's initial balance as ten thousand tokens in balances mapping.

• Constructor is used to define setup in test token contract.

Writing Properties for Echidna

• Properties must follow a specific format: a function with Echidna_asterisk or wildcard structure that takes in no functions and returns a Boolean.

• Echidna checks all state-changing functions to find properties with the Echidna_wildcard structure.

Introduction to Property-Based Testing

In this section, the speaker introduces property-based testing and explains how it differs from traditional testing methods. They also provide an example of a property test.

What is Property-Based Testing?

• Property-based testing is a type of testing that focuses on testing properties or invariants of a system rather than specific inputs and outputs.

• It involves generating random inputs to test the system against, which can help uncover edge cases and potential bugs.

• The goal is to ensure that the system behaves correctly under all possible inputs, not just the ones that are explicitly tested.

Example: Writing a Property Test

• The speaker challenges Echidna to write a property test for the balance function in their code.

• The property they want to test is whether Echidna's caller's balance will always be less than or equal to 10,000.

• Echidna must either validate this or find an edge case where it is not valid.

Finding Bugs with Echidna

• Echidna is a tool used for property-based testing in Solidity code.

• When running tests with Echidna, it will generate random inputs and try to find bugs by violating the specified properties.

• In this example, Echidna found an arithmetic overflow bug in the transfer function when sending more than 10,000 tokens.

Fixing Bugs Found by Echidna

• The speaker explains how they fixed the arithmetic overflow bug found by Echidna in their transfer function.

• They caution that their fix may not be optimal and recommend using a newer version of Solidity instead.

Running Echidna on a Target Contract

In this section, the speaker discusses how to run Echidna on a target contract and provides properties for testing.

Setting up Exercise 1

• The speaker shows the template that was set up for Exercise 1.

• A property was set, and Echidna broke it by sending a value of more than 10,000 which caused an underflow.

Validating Rob Bytecode with Echidna

• Echidna needs an ABI in addition to bytecode to validate Rob bytecode.

• Providing both the bytecode and ABI is equivalent since the ABI helps determine state-changing functions and their input parameters.

Resetting Contract State

• The contract state is reset after a sequence of function calls except for what was constructed initially in the constructor.

Using Echidna with Python

• Homebrew can be used on Macs instead of running the Docker image. More information can be found on the Echidna readme or by opening an issue on the Echidna issue tracker.

Exercise 2: Checking Access Controls

In this section, the speaker discusses exercise 2 where access controls are checked.

Setting up Exercise 2

• Same token setup as before but checking for access controls.

• The goal is to pause the contract and revoke ownership in setup.

• Pausing sets pause to true while resuming sets it to false.

• Ownership sends owner to mesh.center.

• Since Echidna deploys this system, it is also its owner allowing pausing in setup.

Adding Property to Check Unpausing Contract

• The property believed true is that once paused and no one owns it, no one can resume it because taking ownership would be impossible.

Introduction to Echidna and Property-Based Testing

In this section, the speaker introduces Echidna, a property-based testing tool for smart contracts. They explain how it works and its benefits over traditional testing methods.

What is Echidna?

• Echidna is a property-based testing tool for smart contracts.

• It generates random inputs to test the contract's properties.

• It can find bugs that traditional testing methods might miss.

How does Echidna work?

• Echidna generates random inputs to test the contract's properties.

• It uses symbolic execution to explore all possible paths through the code.

• It can find bugs by violating the contract's properties.

What are the benefits of using Echidna?

• Echidna can find bugs that traditional testing methods might miss.

• It can test complex properties that are difficult to test manually.

• It can save time and effort in testing by automating the process.

Property-Based Testing with Echidna

In this section, the speaker demonstrates how to use Echidna for property-based testing on a sample smart contract. They explain how to write properties and run tests using Echidna.

How do you write properties for property-based testing?

• Properties are statements about what should be true of a program under certain conditions.

• They are written as functions that take inputs and return a Boolean value indicating whether or not the property holds true.

How do you run tests with Echidna?

• To run tests with Echidna, you need to define a function that calls the property you want to test.

• Echidna will generate random inputs and test the property with those inputs.

• If the property fails for any input, Echidna will report a bug.

How do you interpret the results of Echidna tests?

• If Echidna reports a bug, it means that there is a violation of the property being tested.

• The bug report includes information about the input that caused the violation.

• You can use this information to debug and fix the issue in your code.

Assertion Testing with Echidna

In this section, the speaker introduces assertion testing with Echidna. They explain how it differs from property-based testing and when to use it.

What is assertion testing?

• Assertion testing is a form of testing where you check specific assertions about your program's behavior.

• It differs from property-based testing in that you are not generating random inputs.

When should you use assertion testing?

• Assertion testing is useful when you want to test specific behaviors or edge cases in your code.

• It can be used in conjunction with property-based testing to provide more comprehensive coverage of your code.

Conclusion

In this section, the speaker concludes by summarizing what was covered in the workshop and highlighting its relevance for real-world smart contract development.

What was covered in this workshop?

• The workshop covered an introduction to Echidna and its benefits over traditional testing methods.

• It demonstrated how to write properties and run tests using Echidna for both property-based and assertion testing.

Why is this relevant for real-world smart contract development?

• Property-based and assertion testing are important tools for ensuring the correctness and security of smart contracts.

• They can help identify bugs and vulnerabilities that might otherwise go unnoticed.

• Using these tools can save time and effort in testing, as well as improve the overall quality of your code.

Assertion Testing

This section covers the main difference between asserting a property and returning the property. Assertion mode has additional benefits as it can take input arguments, providing more flexibility to the user.

Asserting a Property vs Returning a Property

• Asserting a property is similar to returning a property, but with additional benefits.

• Assertion mode allows for input arguments, which can be fuzzed by Echidna to make them anywhere between zero and 256 sub Max.

• To run in assertion mode, specify test mode as assertion when calling test possible.

Exercise Two Summary

This section summarizes exercise two and how it teaches users to apply principles learned from simple examples into real-world code.

Applying Principles Learned in Exercise Two

• Exercise two teaches users how to write properties, understand what a setup is, and abstract simple examples into real-world code.

• These principles can be applied to more realistic scenarios such as loss of funds or access control.

Comparison of Echidna and Foundry

This section compares Echidna and Foundry in terms of speed, functionality, and smartness in choosing inputs.

Comparison of Echidna and Foundry

• Echidna is more feature-rich than Foundry at the moment.

• However, Foundry has some capabilities that Echidna does not have, such as vm.prank or cheat codes.

• Echidna uses a Corpus to determine its next sequence of calls, which is unique and can provide more coverage into the code base.

• The developing team is working on making Echidna more developer-friendly while still providing powerful capabilities.

There were no timestamps for the pause for questions and water break section.

Introduction

In this section, the speaker introduces Echidna and its features.

Features of Echidna

• Echidna can fuzz block timestamp and block number.

• It is possible to configure Echidna to jump up to a week in time or a day and time in 24 hours.

• Echidna has dap mode optimization mode and other features.

Defining Good Invariance

This section discusses how to define good invariance for testing with Echidna.

Defining Invariance

• Start by defining the invariant in English.

• Convert the invariant into solidity by creating a Boolean statement that can be defined as a truthy value.

• Run Echidna, investigate if the invariant breaks, fix it, then check if any other controls fail.

Types of Invariants

• Two types of invariants are functional level and system level invariants.

• Functional level invariants test a single function while system level invariants test the entire system.

• Testing each function individually helps understand the system better before testing system-level invariants.

I'm sorry, but I cannot provide a summary of the transcript without having access to it. Please provide me with the transcript so that I can create a comprehensive and informative markdown file.

Introduction to Echidna

In this section, the speaker introduces Echidna and explains how it works.

What is Echidna?

• Echidna is a property-based fuzzer for Ethereum smart contracts.

• It generates random inputs to test the contract's properties.

How does Echidna work?

• When Echidna finds new coverage, it stores that transaction sequence in a different data structure called the Corpus.

• The Corpus is the interesting stuff that Echidna found to be cool.

• To find something that's cool, you check whether coverage increases.

• If coverage increases, it means there's something interesting happening in the code.

Mutating and Splicing

• When Echidna wants to reuse a sequence from the Corpus, it deserializes it into an object that it can work with and then mutates stuff along the way.

• The mutation part depends on what type of data structure is being used (e.g., uint, string, address).

• There's also something called splicing where you can add stuff in the middle of a sequence or after the sequence using educated randomness based on information from previous runs.

Testing Smart Contracts with Echidna

In this section, the speaker explains how to use Echidna to test smart contracts.

Revisiting an Example

• The example contract has a buy function that takes in tokens value and buys some tokens based on the value.

• The valid buy function is called to make sure that you sent at least a tenth of the amount of way given how many other tokens you want to buy.

• If the required statement passes, which means the transaction doesn't revert, you'll mint.

Testing with Valid Buy

• The valid buy function is completely stateless and can be tested in an isolated fashion by copying it into a different contract.

• One important invariant for this function is that if way sent is zero, desired tokens should also be zero.

• A precondition for testing this invariant is that desired amount must be greater than zero.

Finding Bugs with Property-Based Testing

In this section, the speaker discusses how property-based testing can help identify logical flaws in code bases. They use Echidna to test a smart contract and find a bug that allows users to mint tokens for free.

Property-Based Testing

• Property-based testing is an important technique for finding difficult logical flaws in code bases.

• Echidna is a tool used for property-based testing of smart contracts.

• Properties are Boolean statements that are either true or false.

• You can test properties in property mode or assertion mode.

Finding a Bug with Echidna

• The speaker uses Echidna to test a smart contract and finds a bug that allows users to mint tokens for free.

• The bug occurs due to rounding errors when dividing by 10 in Solidity.

• This bug indirectly impacts other functions in the smart contract as well.

Next Steps

• In the next workshop, they will focus on fuzzing aptk math, which is a fixed-point math library.

• They will also discuss function-level testing and debugging and optimizing fuzz tests.

• Participants are encouraged to complete exercises 3 to 6 in building secure contracts if they feel comfortable with the material.

Conclusion and Future Workshops

In this section, the speaker concludes the workshop and invites participants to attend future workshops.

Workshop Conclusion

• The speaker thanks the participants for joining the workshop.

• The speaker invites participants to attend future workshops.

• The next stream will be on Tuesday, November 22nd at 12 p.m. with the same speaker.

• The date for the third stream will be announced next week.

Final Thoughts

• No further questions were asked by participants.

• The speaker hopes that everyone enjoyed the workshop.