devcon 7 / clear a formal verification framework for smart contracts in lean
- YouTube
- Details
Clear: a Formal Verification framework for smart contracts in Lean
Duration: 00:00:00
Speaker: Julian Sutherland
Type: Workshop
Expertise: Expert
Event: Devcon
Date: Nov 2024
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.
- Related
Devcon
Panel
Formal Verification in the Ethereum Protocol: Current Status and Future Directions
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.
Devcon
Talk
23:35
Solutions towards trusted and private computations - built by Golem for the wider ecosystem
Intel SGX is a technology first developed by Intel for the protection of code and data. This an extremely promising technology that will contribute to the development of the blockchain space and is focusing efforts on solutions and further development.Our hard work has allowed us to be positioned as the most advanced team in this field. We are building this solution and open-sourcing it because we believe that our user-friendly product will enable many projects facing challenges like the ones we have faced apply this solution and push other development aspects of their projects. This talk will cover what we have accomplished so far and what are the next steps related to Intel SGX technology development. We will explain how we have achieved total security and privacy for requestors (people requesting computing power via the Golem p2p marketplace). They can be certain that the data they share is not accessible for the providers and they can be certain that the results are not manipulated. We'll also show how that integrates with our Concent service.Most importantly we will talk about other new possibilities that this technology enables for decentralized computations, explaining how to run arbitrary binaries inside SGX.
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
Workshop
1:28:22
How I Audit
Dom, a former security researcher at Trail of Bits, is going to give a peek of what it's like to be an auditor in 2024. Some of the techniques and tools discussed: * How to prepare for an audit? * How to hand over the resources? * What is the first thing auditors do? * How to communicate with auditors? * How I use the following tools, and their evaluation: * Codebase visualization with Wake and Neovim * Static analysis tools * Fuzzing (and debugging) * Manual review
Devcon
Talk
30:18
CBC Casper Design Philosophy
Consensus protocols are used by nodes to make consistent decisions in a distributed network. However, consensus protocols for public blockchains should satisfy other requirements, by virtue of the protocol being open. For example, they need to be incentivized, in that people will be incentivized to run consensus forming nodes in the first place, and in that following the protocol should be an equilibrium for consensus forming nodes.The CBC Casper family of consensus protocols has been designed to fit design criteria necessary for secure public blockchains. In this talk, we will explore the design goals and methodology used in CBC Casper research: economically motivated properties of the consensus protocol, the correct-by-construction approach to protocol specification, and the resulting rapid iteration.
Devcon
Talk
18:31
Ledger SGX enclave - (un)popularity assessment and the way forward
An overview of the new developer features available for Ledger Nano S Ethereum application, including the validation of an arbitrary smart contract call on screen and how to design a Dapplet on a Nano S to assist the security of Dapps.
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
From Web2 Security With Love
Web3 organizations often rely on Web2 for infrastructure, communications, and development, yet their Web2 security posture is often neglected. This leaves them vulnerable to a wide range of adversaries, from well-funded sophisticated attackers to opportunistic script kiddies. In this talk,Joe Dobson will share hard-earned lessons from the Web2 trenches that can help secure Web3.Don’t make it easy for the adversary. Learn from the past: strengthen your Web2 security to safeguard your Web3 future.
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