Halmos vs Damn Vulnerable DeFi is the series of articles about solving the Damn Vulnerable DeFi CTF using the Halmos symbolic analyzer.
Since theredguild have released Damn Vulnerable Defi v4, that is fully migrated to foundry-based testing, it is very comfortable to use Halmos to solve these challenges.
This material should be considered as a tutorial about possibilities of using Halmos against CTFs or building attacks on smart contracts.
A comparison with fuzzing techniques using Foundry fuzzing and Echidna in the context of Damn Vulnerable DeFi solutions was also described.
WARNING: This repository is still in progress, so there may not be solutions for all problems.
- The reader should be familiar with the Halmos basics: https://github.com/a16z/halmos
- It is expected that the reader is familiar with Damn Vulnerable DeFi and knows how to solve these challenges. Here is a great material with solutions: https://www.youtube.com/playlist?list=PLwHGiYB583YuDoAjKPDfYMKOmuFIGJCnW
For reasons of ease of presentation of new material, new techniques, etc., the order of the articles differs from the original order of the challenges. Actually, the order:
- Unstoppable
- Truster
- TBD
- ...
Don't be afraid to make pull requests if you have any improvement ideas.
Also, you can reach me in Telegram: https://t.me/super_uzer
Special thanks to Halmos development team for their support :)