devcon 7 / can we formally verify implementations of cryptographic libraries like the c kzg library
- YouTube
- Details
Can we formally verify implementations of cryptographic libraries like the c-kzg library?
Duration: 00:00:00
Speaker: Thanh-Hai Tran
Type: Lightning Talk
Expertise: Intermediate
Event: Devcon
Date: Nov 2024
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.
- Related
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
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
05:34
Merkle Proofs: When Leaves Leave You Vulnerable
A Merkle proof is a cryptographically authenticated data structure widely used to minimize on-chain data storage. The Merkle algorithm is neat yet non-trivial to implement correctly and securely; its leaves may leave you vulnerable if not handled properly.
Devcon
Lightning Talk
Proving liquidity of an AMM
Liquidity providers in an AMM expect that they can always withdraw their tokens, even in case of a bank run. Taking the concrete implementation of Uniswap v4, we formally proved that the funds owned by the contract always cover the provided liquidity. This talk describes the methodology for proving this critical property, which can be applied to other protocols holding the liquidity for their users.
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
Lightning Talk
09:27
How to steal $1.1M from lending market in 15 minutes
In may 2024 I found multiple bugs in lending market which allowed to steal $1.1 mln. The exploit itself was very complicated and required multiple steps, including exploitation of liquidation process of unhealthy loan which worked very similar to flash loan. I'll tell the story of how I decided to check this project source code to finding an issue, contacting with owners of platform and fixing it. I'll also share the best tips how to avoid and prevent such issues in other projects.
Devcon
Talk
Lazarus! How to stay safe from the biggest threat actor in crypto
Lazarus has stolen by far the most funds in the blockchain space. They use the same or very similar attack vectors every time yet we see the biggest crypto companies falling victim to them one after another. In this talk, i'll go over some of the attack vectors used by Lazarus and how people can keep themselves safe from Lazarus.
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.