devcon 7 / formal verification in the ethereum protocol current status and future directions
- YouTube
- Details
Formal Verification in the Ethereum Protocol: Current Status and Future Directions
Duration: 00:00:00
Speaker: David Pearce, Igor Konnov, Julian Sutherland, Zoe P
Type: Panel
Expertise: Intermediate
Event: Devcon
Date: Nov 2024
Vitalik believes "ethereum's biggest technical risk probably is bugs in code, and anything that could significantly change the game on that would be amazing". Formal verification is a key technology which many believe could significantly help. However, it has yet to see wide adoption for a variety of reasons. This panel will bring together formal verification experts working in blockchain to discuss the challenges faced in increasing the use of formal verification within the community.
- Related
Devcon
Workshop
Clear: a Formal Verification framework for smart contracts in Lean
Join us for an in-depth workshop on the Clear framework, a cutting-edge tool designed for the formal verification of smart contracts by extracting Yul code into Lean. This workshop will explore Clear’s remarkable expressivity, enabling any pen-and-paper proof of correctness to be mechanized in Lean. Participants will learn about Clear's compositionality and abstraction, allowing scalable verification of complex smart-contracts, and its automation capabilities to streamline proof generation.
Devcon
Talk
25:40
What don't we know? Understanding Security Vulnerabilities in SNARKs
Zero-knowledge proofs (ZKPs) have evolved from being a theoretical concept providing privacy and verifiability to having practical, real-world implementations, with SNARKs (Succinct Non-Interactive Argument of Knowledge) emerging as one of the most significant innovations. Prior work has mainly focused on designing more efficient SNARK systems and providing security proofs for them. Many think of SNARKs as "just math," implying that what is proven to be correct and secure is correct in practice.
Devcon
Lightning Talk
Can we formally verify implementations of cryptographic libraries like the c-kzg library?
In this talk, we present our work on formally verifying the implementation of a cryptographic library key to the security of the Ethereum Data Availability layer: the c-kzg library. We will explore what we have been able to prove so far and what is ahead of us.
Devcon
Talk
26:28
hevm or: How I Learned to Stop Worrying and Love the Symbolic Execution
hevm is a symbolic execution engine for the EVM that can prove safety properties for EVM bytecode or verify semantic equivalence between two bytecode objects. It exposes a user-friendly API in Solidity that allows you to define symbolic tests using almost exactly the same syntax as usual unit tests. In this talk, we'll present hevm, what it's useful for, and when and how to use it to help secure your digital contracts.
Devcon
Lightning Talk
07:38
Transaction simulation, the good, the bad & the ugly
Transaction simulation allows users to preview the outcomes of signing a transaction, enabling them to make informed decisions rather than fully trusting the dApp. However, several caveats and risks are associated with relying on simulated transaction outcomes. State changes, differing contract behavior between simulation and on-chain execution, and randomness can all affect the outcome. In this talk, I'll share my experiences and learnings from simulating user transactions over the past 2 years
Devcon
Talk
Web3 Security is Embarrasing
The explosive growth of Web3 has brought about innovation, decentralization, and financial opportunity. But let’s be honest—Web3 security is a disaster. In this talk, we’ll confront embarrassing truths: drainer attacks, weak wallet protections, and overlooked vulnerabilities. But we won’t stop there; I’ll share practical fixes to protect users and show how Web3 developers can raise the bar. If we want Web3 to thrive, we have to stop attackers beating us with low-effort attacks. We can do better!
Devcon
Talk
17:48
Ethereum Security
Martin Swende gives their talk on Ethereum Security.
Devcon
Talk
19:41
Evolution of Smart Contract Security in the Ethereum Ecosystem
A lot has changed in the smart contract development ecosystem in the year since DEVCON2. Our perspective as leaders of the smart contract security community OpenZeppelin shows us that the industry is maturing. We give a brief overview of how security patterns and practices have evolved in the past months, dive into some details of recent developments, and talk about promising projects and their plans for the future.
Devcon
Talk
21:00
The Melon security approach
Melonport is striving to build a vibrant and successful developer ecosystem of Melon module builders. An important part of that ecosystem is the security and behaviour of smart contracts that make up Melon modules as well as how they interact with the Melon core and each other. In this presentation, we’ll demonstrate our ongoing technical efforts to assist Melon module developers in creating safe, secure smart contracts and touch on the importance of getting the auditing process right and how others can learn from our experience.
Devcon
Breakout
24:32
Vulnerability Coordination and Incident Response in a Decentralized World
There’s one question that every team of core blockchain developers has discussed at least once: what are we going to do when a critical vulnerability in our software is surfaced? By definition, everything we create is likely to include a vulnerability or code flaw and the difficult legal, ethical, and business issues arise when bugs show up in code. While decentralization does not require us to reinvent the first principles security, it does force us to challenge ourselves to manage significant complexity to reduce harm to those who depend on our code. This talk will discuss the CosmosCERT as a model for how teams can successfully coordinate vulnerabilities and respond to incidents in decentralized environments using on-chain governance mechanisms in a way that ensures stakeholders have a dedicated emergency response capabilities ready to go when the worst happens.