Exploiting and Securing DeFi Projects with Formal Methods

We present a systematic way of finding/proving the absence of vulnerabilities in DeFi projects based on automatically extracting financial models from smart contracts and reasoning about them symbolically using DeepSEA, an open-source language/verification system. Attendees will learn how to capture the exact concept of soundness in DeFi projects, how to use DeepSEA to formally find/prevent two classes of interesting hacks (flash-loan attacks & price oracle manipulation attacks) using model checking and interactive proofs, and how to extend this method to DeFi protocol design.