SC Exploits Minimized

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!

Getting Started

Requirements

• 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)

Quickstart

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

Test

forge test

Running a single test

forge test --mt test_reenter

Running a FV test

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

halmos --function check_hellFunc_doesntRevert

Remix, CTFs, & Challenge Examples

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".

Exploit	Remix 🎧	Ethernaut 👩🏻‍🚀	Damn Vulnerable DeFi 💰	Case Studies 🔎
Reentrancy	Remix	Re-entrancy	Side Entrance	The Ultimate List
Arithmetic	Remix	Token	None	Coming Soon...
Denial Of Service (DoS)	Remix	Denial	Unstoppable	Coming Soon...
Mishandling Of Eth	Remix (Not using push over pull) Remix (Vulnerable to selfdestruct)	King	None	Sushi Swap
Weak Randomness	Remix	Coin Flip	None	Meebits
Missing Access Controls	Remix	Fallout	None	Coming Soon...
Centralization	Remix	None	Compromised	Oasis And every rug pull ever.
Failure to initialize	Remix	Motorbike	Wallet Mining	Parity Wallet
Storage Collision	Remix	Preservation	None	Coming Soon...
Oracle/Price Manipulation	(Click all of these) OracleManipulation.sol BadExchange.sol FlashLoaner.sol IFlashLoanReceiver.sol	Dex 2	Puppet Puppet V2 Puppet V3 The Rewarder Selfie	Cream Finance
Signature Replay	Remix	N/A	Coming soon...	Coming soon...
Opcode Support/EVM Compatibility	Coming Soon...	None	None	zkSync/GEM
Governance Attack	Coming Soon...	None	None	Tornado Cash
Stolen Private Keys	Coming Soon...	None	None	Vulcan Forged Mixin
MEV	Remix	None	None	Vyper Attack
Invariant Break (Other exploits can cause this)	Doesn't work great in remix	N/A	N/A	Euler

Invariants

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

Formal Verification

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.

Halmos cheat sheet

• 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 vs Formal Verificaion cheat sheet

• 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 👌

Thank you!

Follow us!

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