2023-09-16 –, Lincoln Stage ( Builder / Legal)
Smart contract developers face a bevy of potential pitfalls that traditional web2 methodologies and tools are unequipped to handle. For example, reentrancy and flash loan vulnerabilities have enabled many attacks on various exchanges, and even simple functional correctness bugs can lead to costly attacks. This talk will discuss how developers can avoid these vulnerabilities in their projects, both with manual reasoning and by using tools developed by Veridise.
This talk will cover a variety of common vulnerabilities in smart contracts, as well as two tools used to find these vulnerabilities: Vanguard and OrCa.
Vanguard is an open-source static analyzer for finding bugs in Smart Contracts. Vanguard detects common vulnerabilities in a blockchain-agnostic way by targeting any smart contract language (e.g., Solidity, Rust, etc.) that can be compiled to LLVM.
OrCa is a fuzzer built for smart contracts that currently supports both Solidity and Cairo contracts. OrCa takes both the source code and a specification of correctness as input, which may contain temporal properties like “the highest bidder of an auction eventually gets rewards.” OrCa then fuzzes many combinations of possible transactions, attempting to find a sequence of transactions that violates the specification — and thus corresponds to a bug.
Come to the talk to learn more details Vanguard and OrCa!
I am a Senior Research Scientist at Veridise, specializing in building formal methods tools to enable both automatic bug finding and verification. I received my PhD in programming languages at the University of Washington, studying with Emina Torlak. I completed my undergraduate degree at UT Austin, where I studied formal methods with Isil Dillig.