Support

--- ## Memory and mstore ### Initial Memory State: - **Starting Point**: Before executing any memory operations, the memory is blank. - **Memory Representation**: Each block represents a byte. The memory layout is as follows: - `0x20`: Marks the 32nd byte in memory. - `0x40`: Marks the 64th byte in memory. - `0x60`: Marks the 96th byte in memory. - **Visualization**: Initially, all memory slots are zero, indicating no data has been stored yet. ### Understanding mstore Operation: - **Direct Memory Manipulation**: The `mstore` function is crucial for directly placing data in memory. - **Example Case**: Upon invoking `mstore` at `0x40`, the expected behavior is to place a value exactly at this position. - **Actual Behavior**: Contrary to expectations, `mstore` pads the value, filling from `0x40` to `0x60` with the value, using zero-padding for the bytes leading up to the last four bytes. ### Practical Implications of mstore Padding: - **Test Function**: A function `testMoleRevert` is used to ensure the code reverts under certain conditions by testing overflows with `type uint256 max`. - **Debugging**: Debugging tools such as Forge are employed to step through the execution and examine the memory and opcodes directly. - **Memory Overwriting Concern**: It’s revealed that `mstore` might be overwriting the free memory pointer at `0x40`, which is a critical error in memory management within Solidity contracts. ### The Forge Debugger Experience: - **Usage**: By holding down the key 'J', you can progress through the memory operations until the exact opcode is reached. - **Observations**: - The memory is modified by `mstore` at `0x40`, but because of zero-padding, the actual value is pushed to the end of the 32-byte block. - To access the meaningful data (last four bytes), you need to skip the preceding 28 bytes of zeros. ### Revert Function Analysis: - **Memory Reference for Revert**: The revert function aims to grab the error message starting from a certain memory position, but due to incorrect placement by `mstore`, it might end up with incorrect or no data. - **Correctness and Misplacement**: While the placement of data by `mstore` at `0x40` seems to comply with the intended memory operations, the analysis shows that the error handling might not work as expected due to this misplacement. #### Auditing Insights: - **Audit Finding**: The misuse of the free memory pointer (`0x40`) by overriding it during an `mstore` operation is highlighted as a significant issue in the contract, likely to be flagged as a critical error in an audit. - **Recommendation**: Corrective actions and code review are recommended to avoid such critical mistakes, ensuring that memory operations do not interfere with system-reserved pointers and that error messages are correctly handled and retrievable during a revert.

Spotting The Bug

A detailed look at a Solidity memory demonstration - This lesson covers the differences between Solidity's mstore and revert opcodes and how they interact with memory. We also discuss how they work with the Free Memory Pointer.

Course Overview

About the course

What you'll learn

Assembly

Writing smart contracts using Huff and Yul

Ethereum Virtual Machine OPCodes

Formal verification testing

Smart contract invariant testing

Halmos, Certora, Kontrol

Course Description

Who is this course for?

Smart contract security researchers
Advanced Smart contract engineers
Chief Security Officiers
Security professionals

Potential Careers

Security researcher

$49,999 - $120,000 (avg. salary)

Smart Contract Auditor

$100,000 - $200,000 (avg. salary)

Meet your instructors

Patrick Collins

Founder at Cyfrin

Web3 engineer, educator, and Cyfrin co-founder. Patrick's smart contract development and security courses have helped hundreds of thousands of engineers kickstarting their careers into web3.

Guest lecturers:

Josselin Feist

Head of Blockchain at Trail of Bits

Last updated on January 17, 2025

Thanks for checking us out

Start learning for free

Start for free

Solidity Developer

Assembly and Formal Verification

Section 1: Introduction

Duration: 30min

Section 2: Horse Store

Duration: 4h 38min

Section 3: Math Masters

Duration: 3h 57min

1. Introduction

A practical introduction to formal verification and symbolic execution - This lesson is focused on introducing the concept of formal verification and symbolic execution as applied to smart contracts. Using a code base for a math library, we walk through an initial audit and then explore the use of the Certora tool to test for bugs. Duration: 7min

2. Scoping

A beginner’s guide to performing a security audit on a Solidity smart contract codebase. This lesson covers the basic elements of a solidity audit, including an explanation of the different tools and techniques used to perform the audit. It demonstrates how to use Slither, Adern, and Foundry to identify bugs and security vulnerabilities. Duration: 7min

3. Wad Ray Rad

A brief overview of WAD, RAY and RAD in solidity. The lesson covers what these terms mean, and how they are used to define the number of decimal places for different tokens. Duration: 2min

4. Version Compatibility

A quick guide to checking for version compatibility in Solidity. The lesson covers checking for compiler compatibility using a library, which may be necessary when using inherited libraries. In this lesson, the compiler is incompatible with the library because the library requires a newer version of the compiler to support its features. Duration: 1min

5. Mulwad

A deep dive into the muWad function in Solidity - The lesson examines the code used in a muWad function within a Solidity contract. Specifically, it analyzes the assembly code in depth, breaking down each line and the various opcodes used, with the use of a helpful tool called Chisel. Duration: 12min

6. Reverting

A deep dive into memory and revert in Solidity - This lesson provides a deep dive into the memory and revert opcodes. It explores how the memory opcodes work in the context of the EVM, and how to use the revert opcode in Solidity to throw a custom error. Duration: 4min

7. Spotting The Bug

8. Incorrect Memory Access

A deep dive into Incorrect Memory Access Bug Recap - This lesson revisits the memory access bug and identifies the error in the code, then utilizes a memory diagram to demonstrate the correct way to handle memory allocation and reversion. Duration: 1min

9. Error Code Function Selector

A detailed explanation of the function selectors error code. The lesson covers examining the function signature and how it can lead to incorrect function selectors. The lesson also covers the function selector for revert in Solidity. Duration: 1min

10. Finishing Mulwad

A technical deep dive into the Solidity function `mulWadUp` and its assembly code - the video highlights an audit process for a Solidity function which reveals several instances of unusual assembly code being used, including a blank message revert and a `div` function, before going into a breakdown of how the assembly code for the `mulWadUp` function actually works. Duration: 1min

11. Mulwadup

A detailed explanation on Solidity's 'or' command - A closer look at Solidity's 'or' command. This lesson shows how the 'or' command works in Solidity, and walks through a quick debugging scenario. Duration: 1min

12. Where Fuzzing Fails

A comprehensive guide to finding a bug in Solidity code using fuzz testing. The lesson covers how to set up fuzz testing in Foundry and provides an example to show how fuzz testing can be used to find edge cases and errors that are difficult to find with traditional unit testing. Duration: 10min

13. Sqrt Function Intro

A comprehensive guide to auditing square root functions in Solidity - This lesson covers formal verification of the square root function and also highlights a potential edge case that might be missed by a fuzzer. The video will introduce the student to two different approaches to finding a square root: using the Babylonian method in assembly and using the Solmate library's approach. Duration: 6min

14. Formal Verification

A comprehensive guide to Formal Verification and Symbolic Execution - This video walks through a high-level overview of formal verification and symbolic execution, covering how they're used for security and testing in web3, and the path explosion problem. Duration: 15min

15. The 4 Stages Of Invariant Tests

A practical guide to formal verification for smart contracts - This lesson shows a repo that includes minimized examples of smart contract exploits as well as different testing techniques for them. It includes examples of stateless fuzzing, stateful fuzzing, stateful fuzzing with a handler, and formal verification. You'll also learn about the pros and cons of each. Duration: 10min

16. Where Fuzzing Fails 2

A deep dive into where fuzzing fails - This lesson looks at an example of a code base where a fuzzer would give the false impression that there are no bugs. It then goes on to explore some of the potential reasons why fuzzing might fail to find bugs, including the possibility that a fuzzer might not be run for long enough. The lesson also considers the idea that, while fuzzing might be a powerful tool, some codebases might be so complex that they require manual auditing instead of fuzzing. Duration: 3min

17. Formal Verification Speedrun

A comprehensive guide to formal verification in Solidity. The lesson shows how to use formal verification tools (Halmos, K, and Certora) to find bugs in your code and demonstrate the advantages that formal verification offers in comparison to traditional fuzz testing. Duration: 4min

18. Formal Verification Setup

A comprehensive guide to Formal Verification - This lesson covers how to write formal verification suites, using two tools: Halmos and Certora. The lesson also highlights the trade-offs between these two formal verification tools. Duration: 1min

19. Wsl Python Setup

A practical guide to creating a Python virtual environment. This lesson demonstrates how to install the virtualenv library, and create and activate a virtual environment to ensure that project dependencies are isolated and do not conflict with other projects on your system. Duration: 11min

20. Halmos Wsl

A quick guide to installing and running Halmos on your computer. This lesson covers installing and setting up Halmos, as well as writing a simple test using an ERC20 token and showing it in action. Duration: 2min

21. Halmos

A comprehensive guide to symbolic testing with Halmos. This lesson provides you with the basics of setting up your Halmos testing environment, writing a simple Halmos test, and using Halmos to help you prove or disprove your assertions. Duration: 12min

22. Certora

A practical guide to formal verification using Certora. This lesson covers the concept of formal verification, how Certora can be used to ensure the security of smart contracts, and how to use the Certora prover. Duration: 3min

23. Certora Wsl

A comprehensive guide to installing Certora on your WSL environment. This lesson will teach you how to set up a virtual environment, install the Certora package, and add your personal access key as an environment variable. Duration: 2min

24. Setting Up Our Spec And Conf Folders

A beginner’s guide to running Certora formal verification tools using a simple example. This lesson covers the basic setup for Certora formal verification, including creating a ‘specs’ and ‘conf’ folder, writing a rule and an invariant, and explaining the different parameters that you need to provide Certora. Duration: 8min

25. Installing Certora

A comprehensive guide to installing Certora and solc-select - This lesson covers how to install the Certora prover package and solc-select in a Linux-like environment to set up your Solidity development environment. The guide covers setting up your personal access key as an environment variable, and explains the different ways to install and switch between Solidity compiler versions with solc-select. Duration: 5min

26. First Certora Run

A simple guide to running the Certora prover - This video lesson covers how to run a Certora prover using a terminal command line. The lesson covers the details of how to write the command line and how to understand the output that is generated once the prover has completed. Duration: 4min

27. The Methods Block

A technical guide to writing methods in the Certora prover using the “methods” block. This lesson covers the basics of the “methods” block and explains how to specify different methods and their returns. It also discusses the concepts of “envfree” tags and how they affect the proving process. Duration: 2min

28. lastReverted

A simple guide to using invariants in Certora. The lesson covers the key elements of an invariant as it relates to Solidity smart contracts. It walks through how to use Certora to ensure a smart contract never reverts when being run. Duration: 1min

29. Analyzing A Failed Certora Run

A practical guide to analyzing a failed Certora run - In this lesson, you will learn how to analyze a failed Certora run, including how to understand the different parts of the call trace, how to identify the counter-example that caused the failure, and how to interpret the results of the run. Duration: 5min

30. Require Statements

A detailed explanation of require statements in Solidity for Formal Verification. This lesson discusses the need to specify pre-conditions for Certora to run correctly, and walks through using 'require' statements to declare the initial state of storage variables. Duration: 2min

31. Failed Certora Run 2

A comprehensive guide to identifying and debugging a failed Certora Run 2 - The lesson covers the process of identifying and resolving an issue with a formal verification check. This involves looking at the Certora output, tracing the call stack and then looking at the code in order to identify the bug. Duration: 3min

32. Envfree

A detailed guide to understanding the 'envfree' function, and how the environment can be used as a first parameter in function calls in Certora. This lesson covers what the 'envfree' keyword does, how to pass an environment into a function, and how to use the environment to find edge cases that can break your invariants or rules in Certora. Duration: 6min

33. Leveling Up Our Conf File

A practical guide to leveling up your configuration file - The video explores several key parameters within your Certora configuration file such as 'wait for results' and 'rule sanity'. You will learn how to use these parameters to optimize your formal verification process. Duration: 2min

34. Formal Verification Introduction Recap

A quick introduction to formal verification in Solidity. The lesson goes over how to use the Halmos and Certora tools to verify a simple rule or invariant for a solidity contract. This example will show how to write a rule that proves that a function will never revert. Duration: 2min

35. Using Formal Verification On Math Masters

A fun challenge in formal verification to Math Masters - This lesson will use Halmos and Certora to do formal verification of two Solidity functions: mulWadUp and sqrt. The lesson will also reveal the clue that should've tipped you off that there was an issue with the sqrt function and that it was not actually passing. Duration: 1min

36. Halmos Mulwadup

A practical guide to path explosions and timeouts in formal verification - This lesson covers the importance of using fuzzing first in formal verification, as well as how to increase Halmos’ run time by modifying its parameters. Duration: 7min

37. Certora Mulwadup

A comprehensive guide to verifying internal functions and libraries in Solidity - This lesson focuses on understanding the use of code harnesses to verify the functionality of internal functions and libraries, and introduces Certora, a formal verification tool. Duration: 6min

38. Formal Verification Soundness

A technical guide to formal verification soundness - This lesson discusses the concept of soundness in formal verification, particularly as it relates to the Certora prover. We see an example of an unsound approximation, and learn how to address this problem. Duration: 2min

39. Definitions

A detailed breakdown of definitions in the Certora Verification Language - This lesson explains how to use definitions to encapsulate commonly used expressions. You will learn how to declare a definition, how to use a definition, and what kind of expressions you can encapsulate within a definition. Duration: 1min

40. Refactoring

A detailed guide to refactoring for CVL - This lesson covers how to refactor code for the Certora Verification Language (CVL) including using the `require` keyword, the concept of `max_uint`, and the difference between `mathint` and `uint256` types. Duration: 5min

41. Your First Certora Invariant

A detailed guide to writing and understanding invariants in Certora - The lesson covers the definition of an invariant and how to write one using the invariant keyword, and explains the difference between an invariant and a rule. Duration: 6min

42. Invariant Preserved Blocks

A comprehensive guide to using invariants and preserved blocks in Certora. This lesson covers the process of rewriting a rule to be an invariant in Certora, as well as the differences between a rule and an invariant. The lesson also shows how to use preserved blocks in conjunction with invariants to establish conditions necessary for the invariant to hold. Duration: 3min

43. Certora Recap

A comprehensive recap of Certora invariants, harness, rules, and types - This lesson covers the basics of formally verifying internal functions using Certora. It explains how to use harness to wrap and verify the functionality of a function, and how to use definitions to define different types of variables. The lesson also demonstrates how to define rules, including pre-conditions and post-conditions, and how to use invariants to ensure the properties of the system hold. Finally, the lesson shows how to perform correct conversions between different types using the assert keyword. Duration: 2min

44. Tackling The Sqrt Function

A comprehensive guide to tackling the SQRT function - This lesson walks through the process of auditing a square root function by comparing different codebases and testing cases to find the most accurate and secure solution. We also learn how to utilize fuzz testing to identify any potential errors within the SQRT function. Duration: 2min

45. Naive Formal Verification With Halmos

A naive approach to formal verification with Halmos - The video goes over how to use Halmos and how naive formal verification can be. Halmos is a tool that is used to formally verify solidity code. Duration: 2min

46. Naive Optimistic Loop

A detailed guide to using the Certora prover for verifying the SQRT function. This lesson covers how to use Certora to verify that the SQRT functions in different libraries are equivalent to each other and will also walk you through how to debug timeout errors when using Certora. Duration: 8min

47. Modular Verification

A practical guide to modular verification for Solidity. The lesson discusses how to break a complex problem into simpler subproblems and how to verify each part separately. The video then walks through a real-world example of finding a bug in a square root function by utilizing modular verification and a fuzz test. Duration: 11min

48. Sqrt Function Hint

A practical guide to finding a bug in a square root function using modular verification - In this lesson, we explore the concept of modular verification and use it to locate a bug in a square root function. We will leverage the Certora tool to execute verification checks, ensuring that our code matches the intended behavior of the square root function. Duration: 3min

49. Modular Verification Recap

A comprehensive guide to formal verification in Web3 – Learn how to use Certora to test your Solidity code. The lesson covers modular verification, how to use Certora's different functionalities, and how to write a detailed formal verification audit report. Duration: 9min

50. Recap

A comprehensive guide to Formal Verification - Let's dive deep into the world of Formal Verification with a detailed overview of the process. We'll learn how to identify potential vulnerabilities and bugs in Solidity code and verify that the code is functioning as intended. Duration: 6min

Section 4: Gas Bad NFT Marketplace

Duration: 1h 56min