From High-Level DeFi Properties to Concrete Security Bugs
summary
Certora verification language and unit-style properties map high-level DeFi rules to concrete checks and expose real bugs: a bitwise casting bug in Compound V3 causes half the collateral to be ignored, a Silo Finance miscompute loses accrued interest, and a SushiSwap Dutch-auction flaw lets a buyer claim twice; a single high-level rule finds two issues, a bug injection study of six faults shows about 20 distinct properties each catch at least one bug, and property-driven checks run across all contract functions.
AI-written summary · about
chapters (13)
- 0:00Start
- 4:29GOAL: COVERAGE
- 5:07SPECIFYING PROPERTIES
- 7:13OPENSEA: SEAPORT UNIT-TEST PROPERTIES
- 8:22OPENSEA Unit Test PROPERTIES REAL EXAMPLE
- 9:34VALID STATES PROPERTIES
- 10:17COMPOUND: COMET VALID STATE PROPERTY
- 13:42SILO FINANCE VARIABLE TRANSITION PROPERTY
- 14:40HIGH LEVEL PROPERITES
- 15:18RISK ANALYSIS
- 16:33DUTCH AUCTION - POSTMORTEM ON REAL BUGS
- 17:54SILO.FINANCE - BUG INJECTION STUDY
- 18:43TAKEAWAYS
related talks
23mThanks for all the bugs!
39mThe challenges of building, scaling and securing DeFi protocols
25mCommSec D2 - Smart Contract (In)Security
20mSolidity's most common security pitfalls and its best safeguards
51mA Deal with the Devil: Breaking Smart Contracts
22mHow Decompilation Uncovers Smart Contract Vulnerabilities
43mOutsmarting Smart Contracts
01h 33mWhite Hat Panel: DeFi Exploits