Smart Contract exploits, minimized for your learning pleasure.

• Getting Started
  • Requirements
  • Quickstart
  • Test
    • Running a single test
    • Running a FV test
• Remix, CTFs, & Challenge Examples
• Invariants
  • Formal Verification
    • Halmos cheat sheet
    • Fuzzers vs Formal Verificaion cheat sheet
• Thank you!

• git
  • You'll know you did it right if you can run git --version and you see a response like git version x.x.x
• foundry
  • You'll know you did it right if you can run forge --version and you see a response like forge 0.2.0 (816e00b 2023-03-16T00:05:26.396218Z)

git clone https://github.com/Cyfrin/sc-exploits-minimized
cd sc-exploits-minimized
make

forge test

forge test --mt test_reenter

To run halmos test, you'll need to have Halmos installed.

halmos --function check_hellFunc_doesntRevert

A set of examples where you can see the attack in remix or practice it in a gameified way.

• The Remix links will bring you to a minimal example of the exploit.
• The Ethernaut links will bring you to a challenge where that exploit exists in a "capture the flag".
• The Damn Vulnerable DeFi links will bring you to a challenge where that exploit exists in a difficult DeFi/OnChain Finance related "capture the flag".

Now, "Invariant Breaks" isn't exactly a class of bug, however it's important to know about and use when it comes to hacks. We look at 3 different methods for attempting to break invariants.

1. Stateless Fuzzing (Easiest)
2. Stateful Fuzzing - Open / Unguided (A little harder)
3. Stateful Fuzzing - Handler method / Guided (Harder)
4. Formal Verification w/ Halmos (Hardest)

See more in ./src/invariant-break/README.md

We are using the following tools to do Formal Verification (FV) / Symbolic execution (SE). :

• halmos
• certora
• kontrol

Not used, with rationale:

• hevm: I had a very hard time setting it up. It's likely I didn't spend enough time.
• EthBMC: Unclear if it's still maintained.
• manticore: No longer maintained.
• mythril: It's unclear to me if it performs better than the Solidity SMT Checker.

• Use assert, don't revert or require
• vm.assume() works better than bound() or clamp()
• halmos looks for check_ by default so it's easier to have separate fuzz and symbolic tests. You can name it test_ if you want to run both halmos and foundry (halmos --function test_)

• Fuzzers try a bunch of pseudo-random data to try to break an invariant
• FV/Symbolic Execution convert
• Fuzzers are best at finding "simple" bugs (issues well spread out over a domain space that is not crazy large)
• Formal Verification/Halmos is currently best at showing the absence of bugs. You can have assurance you don't have a bug rather than wondering how long to run a fuzzer.
• FV is perfect for 100% equivalence tests 👌

Follow us!

• Cyfrin
• Cyfrin Updraft
• The Red Guild
• CodeHawks
• Solodit
• Cyfrin Twitter
• Patrick Collins YouTube