Watch / Bad Proofs in Formal Verification
Speaker: Uri Kirstein
Event: Devcon 6
Date: Oct 2022
Uri is a Developer Advocate and Software Developer at Certora. Uri fell in love with blockchain in 2018 after doing a research project as an undergraduate student at the Technion. He joined Certora right after graduation.
Keeping the Public Record Safe and Accessible
Dr. Daniel Nagy presents on permanent public records, security and accessibility.
Multi Protocol Peer Network Framework: Vision and Roadmap
Alex Leverington presents on the vision and roadmap of Ethereum's multi protocol peer network framework.
Whisper: the Multi DHT Messaging System with Routing Privacy. Vision & Roadmap.
Gavin Wood presents Whisper, the low-level, low-bandwidth, dark p2p messaging protocol. Whisper (codename) is a multi DHT messaging system with routing privacy that acts as a companion protocol to the Ethereum next-generation blockchain.
Ethereum's Dr. Jutta Steiner and Gustav Simonsson present on the work undertaken to secure Ethereum.
Jutta Steiner, Gustav Simonsson
DigixGlobal’s security robustness and the Stablecoin, DGX
Talk on Contract Patterns and Security.
Anthony Eufemio, Chris Hitchcott
Ethereum Security Overview
Martin Swende gives an overview of Ethereum Security.
Smart Contract Security
After a quick overview of smart contract failures in the past, a list of important takeaways will be covered. Some coding techniques to prevent unexpected behaviour in smart contracts will be covered as well as some remarks about governance in decentralized systems.
Smart Contract Security in Ethereum
Martin Swende, Vitalik Buterin, Christian Reitwiessner, Raine Revere, Philip Daian discuss Smart Contract Security.
Martin Swende, Vitalik Buterin, Christian Reitwiessner, Raine Revere, Philip Daian
Smart Contract Security Tips
Through the use of examples, Joseph Chow walks us through some common things to avoid when developing and deploying smart contracts.
State Channels Systemic Security Considerations and Solutions
The principal author of the Lightning Network describes how to improve state channels on Ethereum to maximize the chance of transactions being processed despite protocol constraints.
Enter the Hydra – An Experimental Approach to Smart Contract Security
In this talk, we will demonstrate a new approach to secure smart contract development that we believe has the potential to remove a large class of implementation bugs that has plagued the ecosystem. We will discuss connections to other topics in secure smart contract development and announce an effort to build the most secure Ethereum contract ever launched on the mainnet! Philip Daian is a Computer Science graduate student pursuing a PhD at Cornell University. He specializes in smart contracts and smart contract security, as well as the confidentiality properties of distributed ledger technology. He brings experience in the formal verification and automotive domains. Before coming to Cornell, he worked with runtime verification and formal methods, first collaborating with the FSL on several projects as an undergraduate at the University of Illinois at Urbana-Champaign and later moving to the private sector. He looks forward to building the next generation of efficient and open financial cryptosystems.
Martin Swende gives their talk on Ethereum Security.
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.
Hardening Smart Contracts with Hardware Security
Trusted hardware is not your enemy – as threats against cryptocurrencies are evolving (from dumb malware sweeping private keys to smart attackers attacking the presentation layers of smart contracts), we’ll review during this presentation a short history of trusted hardware, how Open Source code can be designed today on modern trusted execution environments to provide a flexible and auditable environment to delegate the security critical parts of smart contracts, and the security compromises made when dealing with the opaque features of trusted hardware.
Mist: towards a decentralized, secure architecture
Everton Fraga will be talking about challenges and latest updates on Mist development and Victor Maia will be talking about Mist Lite, a moonshot project for a more decentralized app engine for Ethereum DApps.
Everton Fraga, Victor Maia
Random numbers on the blockchain
Random numbers on the blockchain: How to guarantee randomness between multiple parties not trusting each other I will discuss the different techniques used to get random number on the blockchain. The talk will cover the security of the methods from technical and game-theoretical point of views. The first 4 techniques will be literature review. While the “Sequential proof of work” will also cover my own research.
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.
Applying Trusted Compute to Ethereum
Explore the role of trusted computation in blockchain and decentralized computing for improving scalability, privacy and security. The breakout will begin with a number of short perspectives on how trusted computation can and should integrate with Ethereum, before shifting to a conversation of what is needed from trusted computation going forward from perspective of decentralization. Participants are members of Enterprise Ethereum Alliance that are working on applying trusted computation to Ethereum broadly. A common implementation of trusted computation is a Trusted Execution Environment (TEE) which is a secure area of a main processor. Code and data loaded inside the secure area, commonly known as secure enclave, is protected with respect to integrity and confidentiality. Intel SGX, TrustZone, Keystone etc. are examples of such TEEs. 10 companies are committed to support this breakout session.
Sanjay Bakshi, Marley Gray, Guy Zyskind, Nicolas Bacca, Lei Zhang, Sebastian Gajek, Andreas Freund, Noah Johnson, John Whelan, Joanna Rutkowska
Blockchain Autopsies - Analyzing selfdestructs
On the blockchain, contracts may be lost but are never forgotten. Of the over 1,800,000 Ethereum smart contracts ever created, more than 54,000 are empty. When a contract’s purpose is fulfilled, the owner typically triggers a self-destruct switch that removes code and state. These steps are similar to what an attacker would do after hijacking a contract. Is it likely the selfdestruct was intentional or performed by a trusted third party? Or was it a hack or fraud? Old contracts have been purged from the world computer’s working memory but they can be reconstructed and analyzed. By investigating the transactions leading up to the selfdestruct, the circumstances of contract deaths can be determined.
Browser 3.0 - How to Build Secure Web3 Clients
The Internet and Ethereum share many parallels. We can learn from the history of the Web and its "browser wars" and will see that "time to market" plays an important role for the positioning and adoption of network clients. The Chrome browser defines for most people how they use services and experience the Internet and a new generation of clients will eventually do the same for the Ethereum network. Applications such as Mist or Brave use popular frameworks like Electron to accelerate the development of browser(-like) applications without giving up platform ownership as it is the case for plugins such as Metamask. However, Electron has some serious security issues that should be considered and which are discussed together with their alternatives.
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.
Current State of Security
Matthew Di Ferrante, Martin Swende, J. Maurelian, Dan Guido, Phil Daian, and Kevin Seagraves have a conversation on the Current State of Security in Ethereum.
Matthew Di Ferrante, Martin Swende, J. Maurelian, Dan Guido, Phil Daian, Kevin Seagraves
Dark Crystal Secure Scuttlebutt
Peg talks about the Dark Crystal project.
Decentralized Oracles: Reliably Triggering Smart Contracts using Decentralized Computation and TEEs
We’ll define and examine what makes a secure oracle mechanism reliable enough to be used by smart contracts for external data delivery, off-chain payment execution, and provable off-chain computation. We’ll go over the security risks and failure scenarios to be avoided based on various smart contract’s reliance on an oracle mechanism as their trigger and/or payment mechanism; closely examining the methods that developers should keep in mind for minimizing the most common failure scenarios. We’ll look in depth at how decentralization can help make oracle mechanisms more secure through the use of a decentralized oracle network, while also presenting a defense in-depth approach that applies additional layers of security through the use of Trusted Execution Environments, and cutting edge approaches like TownCrier.
Defeating front-runners with Submarine Sends
Front-running is a fundamental problem in blockchain-based markets in which miners reorder, censor, and/or insert their own (or the highest gas bidder's) transactions to directly profit from markets running on blockchain economic mechanisms. Submarine Sends (first introduced here: http://hackingdistributed.com/2017/08/28/submarine-sends/) are a powerful general-purpose mechanism to prevent front-running on Ethereum by hiding the very existence of a transaction until it is no longer front-runnable. Unfortunately, so far no practical (in terms of gas) Submarine Send constructions were known. In this talk, I will introduce: a freshly discovered, practical Submarine Send construction that works on the Ethereum mainnet today.LibSubmarine, an open source project implementing it.
Lorenz Breidenbach, Tyler Kell
devp2p development update
This talk presents 2018's developments in devp2p, the communication system underpinning the Ethereum main network. I will speak about the state of the network and implementation progress on the ideas presented in last year's devp2p talk.
Efficient and cryptoeconomically driven DKG as a smart contract
In the absence of a trusted party, Distributed Key Generation (DKG) protocols are essential for the initial setup of any type of threshold cryptosystem. The protocol results with each of the participants holding a valid key share. We use Ethereum as a decentralized trusted platform to run a DKG protocol for BLS signatures. We use precompiled contracts that were initially designed for fast (within the block gas limit) zkSNARKs verification to overcome the computational complexity of the protocol. We rely on a previously proven DKG protocol, but our version is specifically designed to be implemented as a smart contract over Ethereum. We prove the security of our DKG protocol in the random oracle model and other common cryptographic assumptions. To conclude the system, we give an efficient smart contract for signature verification. Our smart contract consumes reasonable gas and scales nicely (in terms of the number of participants). Only a dispute between two of the participants will invoke elliptic curve arithmetics or paring computations. Ethereum is used for three reasons: As a medium for (synchronous) communication, as a mediating authority in case of conflicts, and as a cryptoeconomic incentivization layer over the plain DKG protocol.
David Yakira, Ido Grayevsky, Avi Asayag, Ido Zilberberg
In 2017, I presented the ideas behind the Moon Project, which aims to create a blazingly fast and secure decentralized browser for DApps. In this talk, I'll highlight advancements towards this goal, highlighting Formality, a massively parallel programming language featuring formal proofs and smart contracts, and the FVM, a decentralized virtual machine dedicated to running functional programs with much lower gas costs using the so-called Abstract Algorithm.
Victor Maia, Leonardo Souza
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.
Live Smart Contract Hacking
In this break-out session, a panel of well-renowned hackers and builders will perform security assessments of contracts that the audience submits - and anyone in the room is highly encouraged to help out and take part in the audit. There will not be time to perform full-scale reviews, but the panel will discuss the contracts both from a high-level perspective and also dive into the nitty gritty details, to see if we can find faults in the implementation. This is a panel session, where we want to interact with the community and bash as many bugs as possible, and hopefully demonstrate how tricky it can be to program for the EVM. Mistakes are what makes us learn: There shall be no shaming of anyone who submits a contract for review.
Martin Holst Swende, Nick Johnson, Richard Moore, Matthew Di Ferrante
Managing upgradeability and EVM packages
At Zeppelin, we have been working on a toolset for deploying and managing upgradeable smart contracts and on-chain libraries, we have had the opportunity to collaborate with other teams to gather better understanding on their needs. We have also onboarded several projects to share their code on-chain via a common package registry. We are building an open source tool that offers the best possible developer experience for securely managing smart contract applications. In this talk we will revisit the importance of upgradeability in smart contracts security, present the lessons learned from this semester of usage, and share the work we have been doing as a result.
Reversing Ethereum Smart Contracts to find out what's behind EVM bytecode
Reverse engineering is a common technique used by security researcher to understand and analyze the behavior of closed-source binaries. If you apply this to Ethereum smart contract (and more specifically on the EVM bytecode), thats allow you to analyze and verify the result of your Solidity source code compilation. From a developer point of view, it can save you a lot of time and money if you succeed to detect flaws and missing bytecode optimization. Also, providing the Solidity source code it's not mandatory during the smart contract creation, that’s why being able to directly reverse the EVM bytecode make even more sense if you want to understand the behavior of external smart contracts.
Smart Contract Security - Incentives Beyond the Launch
To mitigate security issues that were quickly present in the deployment of smart contracts, the community has turned to a wide variety of security techniques. Standard when deploying new contracts is manual review by an externally contracted company/individual. In many ways this has been a success, reducing the number of observed security incidents. In this talk, we take a look at how unique incentives in smart contracts affect the process of securing them. For example, smart contracts are often non-upgradeable: enshrinement at release time encourages security processes that end after the deployment of the contract, leaving blind spots in long-term security guarantees against evolving threats. Pressure to ship often leaves critical security guarantees out-of-scope of external reviews, and auditor incentives tend away from detailed or fundamental criticisms of contracts' protocols. In this talk, we review the reviews and take a look at several top contracts in the ecosystem: what are the provided guarantees, who were they reviewed by, and what is missing? How do these guarantees compare to guarantees provided users in systems outside the smart contract ecosystem? And how can we most effectively deploy the immense talent coming into the community towards more secure, more usable systems for end-users?
Smart contracts: Approach with caution
Some of Ethereum’s most critical use cases come from it’s ability to create smart contracts, but this feature has a downside. Transactions no longer either succeed or fail, there are partial failure states that affect what occurred and all variations need to be accounted for when people get paid from it. Jake will discuss how Coinbase mitigates these risks and ensures smart contract transactions are handled safely.
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.
Using Solidity's SMTChecker
Solidity's SMTChecker is a formal verification module that automatically tries to prove safety properties in Solidity smart contracts. These properties include checks for underflow, overflow, trivial conditions, unreachable code and user defined assertions. The checks are performed statically during compilation time, and the properties are either proved correct or a counterexample representing a bug is given to the user. Formal specifications for user defined properties are written using constructs already available in the language, therefore not requiring learning a new verification language/framework. If the formal specification is inaccurate or wrong, proofs are useless to the developer. Therefore, it is important to write specifications in a way that the target properties do represent the program logic. For the advanced user, some understanding about the SMTChecker may lead to specifications that also increase the module's efficiency and proving power. This talk gives an overview of the available features in Solidity's SMTChecker, and presents some insights on writing better formal specifications.
Writing Robust Code
What the elements of a robust and secure development process looks like: 1) V Model of development 2) Writing requirements 3) Requirements traceability 4) Test-driven development in practice 5) Obtaining an audit 6) Operational security during launch
Bryant Eisenbach, Kirill Pimenov
Analyzing The Security Of Casper
From the beginning of this year, we have been working on the security analysis of Casper FFG/CBC, resulting in findings of attacks and formal proofs of properties. In this talk, I'll share a few tips towards the secure development of cryptoeconomic protocols, as well as our research on Casper.
Batched Bonding Curves: Grieving DEX Frontrunners
It's been widely publicized that front-running is rampant across decentralized exchanges. Billy Rennekamp describes the technique developed to stop the parasitic behavior by using batched orders in tandem with bonding curves and how it's being used in a new fundraising app by Aragon Black.
Breaking Smart Contracts
Some of the most financially devastating hacks in recent years have happened on the blockchain. In this workshop, we will walk through a series of simple Solidity coding challenges and common mistakes, where participants are asked read code, understand and try to break them. Regarding each challenge, we will talk about the history of the hacks involving that family of bug. We will talk about the attacks and possible solutions.
Shayan Eskandari, Sergii Kravchenko, John Mardlin, Bernhard Mueller
Build a constraint system, prover and verifier using OpenZKP Stark
There are great tools and tutorials for R1CS proof systems (aka Snarks) but not much is known about programming Starks. Starks have a much more complex constraint language, but in return you can achieve a much better performance. In this workshop we will * learn about the mathematical underpinnings of Stark proofs, * use 0x's OpenZKP library to generate and verify proofs, and * implement a Stark constraint system.
Complementing DApps with Trusted Computing: The Challenge of Designing Rock Solid Oracles
Decentralized Applications aim to change the way verticals across multiple industries work. An important element for this to happen is for smart contracts to access real-world data. Problem is, blockchain is a walled-garden and smart contracts cannot natively fetch data from the outside world. Blockchain oracles enable DApps to overcome this limitation. Designing such a tool is quite a challenge - elements such as security, decentralization and feasibility must be kept into consideration. Is blockchain a self-standing technology? Security-focused techniques such as Trusted Computing or ZKSnarks are being explored as a complementary technology enhancing the power of decentralized tools. How do those technologies complement each other? What’s the benefit for blockchain oracles to rely on both? And what’s the benefit for users?
(Defense Against) The Dark Arts - Contract Runtime Mutability
Smart contracts are no longer guaranteed to have immutable runtime code, and can be redeployed with new code using a variety of methods involving the CREATE2 and SELFDESTRUCT opcodes. In this presentation, we will investigate how this is done and how to protect against malicious mutable contracts. We will also explore ways these new techniques can be applied in order to enable new use-cases and to improve the user experience.
Designing Smart Contracts With Free Will
A range of bribery attacks, collusion possibilities, and other economic vulnerabilities plague our smart contract design. Unlike with simple anti-patterns like recursion, these security vulnerabilities have no obvious fix. Join us for a deep dive into the state of the art bribery attacks that are technically feasible on cryptocurrency today, and their countermeasures. We will introduce and explain new signature schemes that resist the ability for users to be bribed on Ethereum-based smart contracts. We will teach developers of smart contracts how to build contracts that are maximally resistant to bribery, and provide practical tips for the protection of your users.Lastly, we will show and launch a toolkit that provides signatures with protection from an advanced form of bribery known as the Dark DAO, in which users are bribed undetectably. Our toolkit provides a simple API for any Ethereum contract to ensure the free will of their users through an easy to use library.Building bribery resistant smart contracts is of critical importance for voting schemes, oracles, prediction markets, proof of stake and other consensus protocols, randomness generation, and more. Join us in ensuring the protection
ERC725 - The future of on chain interaction
One of the biggest problems for blockchain its is difficulty to store and secure assets and manage interacting with a blockchain. The main cause is the use of private keys for the source of interactions on-chain. ERC725 is a standard proposed to make abstract accounts from keys to a smart contract account. This not only makes security upgradable, but lets accounts become information holders. Fabian Vogelsteller the author of ERC20 and ERC725, the Mist browser and web3.js will talk about how on-chain interaction should look like.
ERC 20 Test Suite: Towards Decentralized Security
Nowadays, a lot of Dapps and exchanges interact with ERC20 tokens and they expect certain behavior from those contracts. It is crucial to make sure that the token fully complies with ERC20 standard to avoid loss of funds and reputation. The problem is that one cannot easily verify this compliance. This can be done only by ordering an audit or writing and running a bunch of tests. However, these options are expensive and not scalable. In my speech, I will tell about a decentralized tool that we created to help developers solve such problems. ERC20 Test Suite is a service that runs a series of tests for ERC20 standard compliance in the form of on-chain transactions. The final test results are recorded in a smart contract. Test Suite cannot fake the test results as each test is a transaction recorded in the blockchain. SmartDec ERC20 Test Suite is open source: https://github.com/smartdec/testsuite Also, we have deployed our centralized instance of the tool here: http://testsuite.net/ropsten/
Ethereum 2.0 Security Considerations
Ethereum 2.0 is fast approaching with multiple implementations underway. We examine the attack surface of Eth2, specifically: -Networking (eclipse attacks, transport encryption, discovery protocol, anonymity) -Software vulnerabilities (DoS, code integrity, inconsistent state transitions) -Consensus assumptions (honest majority, liveness) -Efforts underway (fuzzing, code review, external assessments)
Adrian Manning, Paul Hauner
Formal verification of smart contracts made easy
In this hands-on workshop, we will go through the process of formally verifying smart contracts. The attendees will learn (1) how to formally specify relevant functional requirements of Ethereum contracts, such as "the sum of deposits never exceeds the contract’s balance", and (2) how to verify these using existing analysis tools for Ethereum. First, we will show how to formally specify the intended behavior of smart contracts. We will look closer at safety temporal properties, an expressive class of properties for capturing which sequences of contract states are considered correct. We will present common requirement idioms, including access control, state-based properties, multi-contract invariants, and others. Next, we will provide an overview of existing testing tools, such as tools based on symbolic execution and fuzzers. The goal is to understand how they can be used to identify violations of the formalized properties as well as their limitations in providing unbounded formal guarantees. Finally, we will learn how formal verifiers go beyond testing and can provide unbounded formal guarantees (for any sequence of transactions). We will take a closer look at the specification language used by VerX and its automated verification method, which is easy to use and does not require in-depth knowledge in formal verification.
Dimitar Dimitrov, Anton Permenev, Hubert Ritzdorf, Petar Tsankov
Fully automated inductive invariants inference for Solidity smart contracts
One of the hardest challenges in formal verification is handling loops in a fully automated way. A common approach is to compute inductive loop invariants, properties that formally capture the essence of the loop independent of the rest of the program. These sound loop summaries are then used to check further desired properties from a specification. In the context of Solidity smart contracts, properties over state variables can also be seen as loop invariants where one loop iteration is one transaction. We developed a technique using systems of Horn clauses to infer state and loop inductive invariants at compile-time in a fully automated way, while proving safety properties. The algorithms are released as part of the SMTChecker module inside the Solidity compiler. Thus, the process is seamless to the developer and requires nothing more than the source code. The generated inductive invariants can be used by the compiler and other tools to check properties more easily, to confirm/correct external specifications, and to provide potentially hidden program logic insights to the developer. The goal of the talk is to present the technicalities and use cases of our approach, and to continue discussions around formal verification and inductive invariants.
Leo Alt, Matteo Marescotti
Fuzzing the Solidity Compiler
Since the Solidity programming language does not have a formal specification, testing the compiler implementation is an important way to obtain assurance about the correctness of code generated by the compiler. Fuzz testing is well-suited for this setting. However, applying fuzzing in the traditional manner (random input generation that is coverage-guided) is inefficient for testing compilers because a significant fraction of randomly generated code is syntactically invalid. If the fuzzer does not generate syntactically correct Solidity programs, the compiler will simply reject it. As a consequence, code optimization and generation subsystems of the compiler will not be tested. The approach adopted by us is to define a grammar for the Solidity programming language and automatically generate inputs based on this grammar. Grammar based fuzzing ensures that generated programs are successfully parsed by the front-end parser. We make use of libProtobuf and libProtobufMutator for defining the grammar and performing grammar-based mutations, and libFuzzer as the underlying fuzzing engine.
Grantee Exposé Lightning Talk 1 - Formality: An efficient proof language
Formality is a dependently-typed functional programming language similar to Agda that compiles to a non-garbage-collected, parallel runtime based on interaction combinators and Lamping's optimal reduction algorithm. The language is suitable both as a formal proof language as well as a fast low-level systems language, which allows it to be used to write verifiably secure software at every level of the stack, from hardware drivers to smart contracts and everything in between. Formal proofs are of particular interest for smart contracts applications, given that they often have large amounts of capital depending on the safety of relatively small code bases.
How do we make dapps as secure as the underlying Ethereum?
How to make ethereum really trustless?
Every month, more than 1.5 million smart contracts are published to the blockchain.Every day, more than 1.2 million calls are being made to smart contracts.There are more than 10 million smart contracts on the blockchain already.At the same time, there are less than 1000 publicly verified source codes.Without verified source codes, users who interact with smart contracts directly or through the use of DAPPs, have to trust that the contracts actually do what they promise to do and don't contain any malicious parts.We would like to host a session to discuss how to motivate smart contract creators to publish/verify their source code. Furthermore, we would like to discuss to store verified source code in a decentralized way.
Nina Breznik, Alexander Praetorius
Keymanagement: Multisig based Custody as Enabler for Mass Adoption
Key management is a fundamental challenge in the widespread use of blockchain technology. Especially when it comes to managing large tokenized values, a suitable custody service is essential. While many existing custody services are primarily based on technologies such as Shamir's Secret Sharing, it makes sense to use a Smart Contract based Multisig to manage the rules such as access, what signatures are required, time delay, recovery of lost accesses, etc.
LavaMoat: MetaMask's approach to secure apps
Cryptocurrency is a juicy target for attackers: just grab the coins and run! As app developers, how can we protect our users? Especially given the new trend of "supplychain attacks" where the attackers get into your own app code! LavaMoat is a set of tools to help keep invaders at bay.
Least Authority’s ProgPoW Audit
Least Authority will present the results of the ProgPow security audit, including the auditing process used, the findings of the review and outstanding areas for further discussion. The goal of the presentation or panel would be to increase the transparency of the ProgPow audit that was performed on behalf of the Ethereum Cat Herders for the larger Ethereum community. The discussion could also extend into lessons learned by the community and how to most effectively incorporate security reviews into the development and governance processes in the Ethereum community.
Tanya Karsou, Ramakrishnan Muthukrishnan, Liz Steininger
Pentesting Ethereum Contracts: Exploring a honeypot contract using Ganache
In this workshop we will demonstrate some of Ganache's advanced features to instantly fork Ethereum Mainnet, granting developers a safe, secure, and risk-free environment. We'll explore what a re-entrancy attack is, review historical re-entrancy attacks (like the DAO hack), as well as the narrowly avoided re-entrancy attack vector that would have been introduced by the original Constantinople hardfork proposal. Attendees will attempt to perform a re-entrancy attack against an actual Mainnet-deployed contract that has been cleverly crafted to trick aspiring exploiters into becoming victims. We will utilize Ganache's forking feature to safely discover how it works, and how to write better — and more secure — contracts.At the end of the workshop we'll play a game of Capture the Flag, where you'll have a chance to exploit a real contract, earning actual Mainnet Ether if you are the the first to execute the exploit! But you'll have to be careful as things aren't always as they seem! Ganache is a fast, lightweight development blockchain, and is part of the Truffle tool suite. Ganache forking is a feature that enables developers to read from Mainnet, while transacting against a local development chain, enabling fast, sync-free development and penetration testing.
David Murdoch, Nick Paterno
Preventing Disaster: Advances in Smart Contract Vulnerability Detection
What do the DAO, Parity MultiSig wallet and Beautychain have in common? 1. All three were hacked with disastrous consequences, 2. in each case, the bugs could have easily been spotted in advance using automated analysis techniques. In this talk, we'll investigate the above exploits in depth and show how to use a combination of multi-transactional symbolic execution, taint analysis and greybox fuzzing to detect similar bugs with high accuracy and a low false positive rate. Well' also introduce optimization tricks that enable fast detection of "deep" vulnerabilities - exploit conditions that are triggered over a longer sequence of highly specific transactions. Finally, we'll show how developers can apply these security analysis methods to their own contracts using MythX and Mythril.
Daniel Luca, Bernhard Mueller
PoS Security and Ethylene
Emin Gün Sirer gives his talk on PoS Security & Ethylene.
Emin Gün Sirer
Protecting The Baselayer - from Shanghai to Osaka
Most people know that Ethereum runs smart contracts and move ether around. However, "Ethereum Security" involves a lot more than only smart contracts, mining difficulty and managing private keys. This is a talk about the base layer security. There is a peer-to-peer stack, with it's own separate discovery protocol and p2p protocol, which can be used for eclipse-, DoS- and amplification attacks. There's a consensus engine which encompasses a lot more than only the EVM. In this talk, Martin Holst Swende will talk about vulnerabilities, attacks and hotpatching the mainnet -- lesser known incidents, hiccups and close-calls that have occurred on the road from Shanghai (Devcon2) to Osaka (Devcon5).
Martin Holst Swende
Scaling Ethereum with security and usability in mind
In this talk, I will go through scaling mechanisms and their disadvantages at a user and developer perspective. With our approach at Matic https://matic.network, plasma-fied sidechain, I will explain how we are tackling security using plasma, predicates, and normal state computation on the sidechain. Having specialized DApp specific fraud-proof using predicates, partial confirmations, different fee models allow us better usability for end users. Then will talk about how we are addressing the issue for users when they interact with multiple chains - Ethereum and Plasma sidechain using walletconnect protocol. Overall, it explains how connecting some important dots on Ethereum landscape can help us achieve scalability and usability, and clears our path to mass adoption which we all are aiming for.
Securely storing wallet private keys for application use
Private key management is a complex problem in cryptography. In the last few years, we have seen attacks against cryptocurrency companies that seek to retrieve the private keys of user wallets. Within cryptocurrency, private key management has an additional complexity: the value of stored user funds related to that private key. Truly, key management is a challenge that has plagued secure computing for years.While storing keys is essential, it is equally important to securely use those keys in an application. Without secure use of private keys, applications are vulnerable to attacks to exfiltrate those private keys.In this talk, we will discuss the approach the AirSwap team uses to securely store and use private keys for high value wallets. We will show real world permissions, policies, and code used by our team. We will discuss common attacks against private key management systems and the ways that our implementation thwarts those attacks.This talk is beneficial to any team or company that interacts with the Ethereum blockchain via signed transactions and off-chain custom code. It is essential for any team that wishes to use a private key in their application code securely.
Securely Connecting Smart Contracts to Off-Chain Data and Events
For smart contracts to achieve mass adoption, they need the ability to securely connect to external off-chain data and existing non-blockchain systems. The reliability with which smart contracts connect to key external systems determines their overall security. This critical security factor determines whether smart contracts will be used to secure the many forms of value beyond tokenization, such as prediction market outcomes, insurance payouts, trade finance, and more. In this talk, we’ll examine what makes a secure oracle mechanism reliable enough to be trusted by smart contracts for external data delivery, access web APIs, and off-chain payments. We’ll review the security risks and failure scenarios to avoid when using oracles and share how developers should set up methods to maximize success. We’ll examine how a decentralized network makes oracle mechanisms more secure, and how decentralization, combined with approaches like Trusted Execution Environments, can enable the highest level of security when connecting with external systems. Finally, we will show the design patterns which leading smart contracts use to remain reliable and provide high levels of overall security while connecting to external systems.
Sharing Security between 1st Layer Blockchains
Nowadays one of the evolving fields in the blockchain technology is a protocol which shares security between a main blockchain and a child blockchain. A protocol which shares it between main blockchains, however, is not developed yet. To do that, we would like to introduce a new Sybil control mechanism, Proof of Unit. In this protocol, a new concept, “unit” appears. The unit has three features. First, a unit is generated with any works such as mining, staking, computing prime numbers, and so on. Second, the amount of minted unit is in proportion to the consumed cost. Third, a unit is used as vote power in the consensus algorithm. Proof of Unit would make it possible for 1st layer blockchains to share their security.
Sidechains Are Not Layer 2
In this talk we argue that sidechains are strictly an interoperability protocol, and any attempt at describing them as scalability solutions is misleading. Proof of Work sidechains require each chain to be individually secure, and thus make a double honest majority assumption. Proof of Stake sidechains rely on DMMS-like mechanisms, but even with proper short-long range attack protection they have a different security model to a Proof of Work chain. On the other hand, Layer 2 is a set of mechanisms which allow state to be manipulated more efficiently than the base layer, while inheriting the base layer's security. This is achieved through fraud proofs and client side validation or validity proofs which enforce valid state transitions.
Smart contract interaction out of the coldest of storage
At Coinbase Custody, we provide top of the line security for our client's assets. This security comes at a cost though. Through its very nature, our cold storage process creates friction when broadcasting transactions to the network. For HODLers, this friction is a welcome and blessed thing, as it keeps their funds safe. When our clients want to use their funds to participate in decentralized applications however, we have had to get creative. This talk will focus on the patterns we have developed to facilitate rich and convenient network participation between our clients and the decentralized networks they patronize.
Store your keys safely offline - never get online to sign transactions
The best way to keep your private key safe, is to keep it disconnected from the internet. This is usually done in hardware wallet, however most of those wallets are directly connected to a computer, either via usb or bluetooth. What if the wallet was never online and never ever connected to an online device. This is achievable using QR code. We did it with Parity Signer. I will present why we built it, how, do a short live demo, and what we will do in the future.
The Gas Siphon Attack: How it Happened and How to Protect Yourself
The Gas Siphon Attack allows anyone to siphon value from many exchanges in the form of gas refunds, a mechanism built directly into the Ethereum protocol. Users can write a simple script that continuously drains unprotected exchange hot wallets of all of their ETH. Until this was responsibly disclosed, many exchanges were affected with varying degrees of severity. How it happened, who was affected, and the technical details behind the attack are discussed during the presentation. The talk dives into the details of the refund mechanism built into the Ethereum network, and how it can be maliciously abused. The presentation explains who is vulnerable and what they can do about it. Finally, the talk covers different ways to protect yourself and your dapp from both known and unknown exploits. Preventative measures are presented that will allow for protection from these types of attacks.
The Gas Siphon Attack: The Technical and Economic Realities Behind Hacking Exchanges
The Gas Siphon Attack allows anyone to siphon value from many exchanges in the form of gas refunds, a mechanism built directly into the Ethereum protocol. Users can write a simple script that continuously drains unprotected exchange hot wallets of all of their ETH. Until this was responsibly disclosed, many exchanges were affected with varying degrees of severity. How it happened, who was affected, and the technical details behind the attack are discussed during the presentation. The talk dives into the details of the refund mechanism built into the Ethereum network, and how it can be maliciously abused. The presentation explains who is vulnerable and what they can do about it. A number of these types of technical exploits exist on both centralized and decentralized exchanges, and one may find that responsibly disclosing these attacks are harder than the actual exploit itself. Getting in touch with exchanges, continuous communication with services, and helping fix different systems may be a month-long journey that yields very little in return. Hacks, front-running, misaligned miner incentives, and economic disparities are all issues for exchanges and services that are discussed in this presentation. Finally, the talk covers different ways to protect yourself and your dapp from both known and unknown exploits. Preventative measures are presented that will allow for protection from these types of attacks.
The inner workings of a smart contract decompiler
The workshop will teach some of the most useful algorithms and tricks needed to analyse and decompile an EVM smart contract: symbolic execution, memory modelling, loop handling and so on.Techniques shown during the workshop are useful in anything related to contract analysis - from writing your own decompiler, through using existing tools like Eveem, Mythril or Manticore, to working with formal verification K Lab style. Based on the experience from building Eveem.org decompiler and analysing all the bytecodes on the Ethereum blockchain.
The magic of ethereum addresses
More often than not, people get messed up when writing or copying ethereum addresses. The ENS is supposed to solve that but is not adopted by everyone yet. These errors can have spectacular consequences. Some end up with a happy end.- https://medium.com/bitclave/how-we-sent-eth-to-the-wrong-address-and-successfully-recovered-them-2fc18e09d8f6- https://twitter.com/drew___stone/status/1135703041997516801With the adoption of wallet smart contracts, this issue is only going to grow. This talk will describe where ethereum address comes from, how you could exploit knowledge of these mechanisms, and how you could protect yourself and your users using create2 based factory like the one deployed at 0xfac100450af66d838250ea25a389d8cd09062629.
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.
Being a Responsible Multisig Signer (Verify, Don't Trust!)
So you have been trusted with safeguarding a project along with other members of your community, congratulations! But, alas, the first transaction from a developer on the team comes in. How do you proceed? Can you blindly trust the developer? Should you? It's tempting to just see what other multisig members do and roll along, right? In this talk we'll go over what you can do to verify what a transaction will actually do, and what tools you have at your disposal for this. No coding required!
Battle of the Bridges: Untangling the Tradeoffs of Various Bridge Designs
This panel invites 3 of the leading bridge protocols to debate the various tradeoffs that have emerged between different cross chain bridge designs, including pros and cons, and security considerations. Panelists include the founders of Across (Hart Lambur), Hop (Chris Whinfrey), Succinct (Uma Roy), and will be moderated by Tarun Chitra (Gauntlet).
Tarun Chitra, Hart Lambur, Chris Whinfrey, Uma Roy
Building Secure Contracts: Use Echidna Like a Pro
In this workshop, attendees will gain hands-on experience with Echidna - an open-source smart contract fuzzer - to build secure smart contracts. Echidna has been used in many professional audits, and fuzzing is a key component to increasing the contracts’ security. Attendees will learn how to define and write invariants and how to use Echidna efficiently. By the end of the session, they will know how to integrate property testing into their development process and write more secure code.
Josselin Feist, Gustavo Grieco
Crosschain Security Considerations for the Degen in All of Us
Crosschain applications (xApps) are often considered too risky, but this viewpoint is divorced from reality. People **will** use these applications and it is our responsibility to understand the security implications. xApp developers must be able to reason about concurrency and asynchrony across two different networks, as well as understand the trust assumptions introduced by the data transport layer. By understanding this, we can allow users to engage in risky behavior in the safest way.
Decentralized Threat Detection Bots
Decentralized threat detection bots are a recent area of research and development for protecting the ecosystem. This talk will cover concepts and recent research on detection bots and implementation patterns including heuristic-based, time-series based, multi-block, and TX simulation. Examples involving prior exploits will be included, as well as tools, limitations, the potential for automated threat prevention, and areas for further research.
Ethereum Foundation's Bug Bounty Program
The Ethereum Foundation's Bug Bounty program is one of the longest running bounty programs for blockchains. This talk focus on its history, reported vulnerabilities, where it's heading and why having a bug bounty program is important.
Formal Methods for the Working DeFi Dev
Lecture notes: https://bit.ly/3RFwvBx Runtime Verification is known for formal methods, but you don't need a PhD to make your code better by thinking like a prover. Here we want to show you how you as a developer or auditor can apply fairly simple mathematical thinking to make your code more robust and your security work simpler. By thinking “invariants first” you can get stronger tests, better docs, and reduce the risk of introducing bugs in your future coding.
Future of Smart Contract Security Audits: REKT or WAGMI?
Smart contract security audits have become a de facto requirement for Ethereum applications. However, there continue to be multi-million dollar hacks every week highlighting significant challenges with audits such as questionable quality, arguable effectiveness, unreasonable expectations, high cost, low availability and dearth of talent. This panel proposes to debate on these contentious aspects with some leaders in this space and peek into their crystal ball to see if we are REKT or WAGMI.
Jonathan Alexander, Gonçalo Sá, Nick Selby, Mehdi Zerouali, Chandrakana Nandi, Maurelian
Future-block MEV in Proof of Stake
In PoS Ethereum, block proposers are known ahead of time. This allows for new types of MEV, which leverage the ownership of future block space. Using this, some attacks that were expensive due to arbitrage competition, such as oracle manipulations, become very cheap. There could also be opportunities for incentivizing high-MEV transactions in a future block that you know you will control.
How to Not Be Worth Kidnapping
Personal physical security, specifically violent kidnapping and compulsion to disclose keys, is often brought up as a concern by cryptocurrency participants. We will quickly present a way of thinking about these threats and a model for not merely protecting from loss of cryptocurrency, but prevention of victimization through violence entirely.
Hunting and Monitoring for On-Chain Attacks
Web3 security requires a comprehensive security approach from reuse of secure, audited libraries, audits, threat modeling and security assessments to bug bounties, monitoring, and incident response. In this workshop, we will dissect a real world on-chain attack, categorize each step the attacker took into four distinct stages (funding, preparation, exploitation, and money laundering) and walk through the development of a heuristic/ ML approach to identify these attacks using the Forta Network.
Christian Seifert, Dmitry Gusakov
Nosy Neighbor - Automated Fuzz Harness Generation for Golang Projects
Nosy Neighbor was developed as a breadth-first fuzzing tool for the critical golang clients in the ethereum network - Prysm, Go-Ethereum, and Mev-Boost. Nosy is a very annoying (to the devs) tool that aims to find bugs the moment they are introduced. Leveraging the go/types and go/parser libraries used by the Go compiler, Nosy analyzes the AST of a repo and generates fuzz harnesses for continuous fuzzing Come learn about Nosy's novel approach to go-fuzzing and the issues it has uncovered!
Notable security incidents since Devcon V
October 2019 seems like an eternity ago, and there have been a variety of interesting, sometimes novel, and sometimes repetitive security incidents across the ecosystem since then. We will discuss those incidents, what went wrong, how they've been resolved, and what lessons have been learned, or new mechanisms put in place, in the service of preventing a repeat.
Lane Rettig, Ryan Lackey, Tom Howard, Arun Devabhaktuni
Crypto wallet is an entry point to onboard users to Web3, but the complexity of key management prevents the real decentralization to be realized and widely adopted. After the Merge, Ethereum is pivoting to a rollup-centric roadmap. What does the future wallet look like? In this talk, I would like to talk about what is the missing part for current wallet design centered around L2, DeFi applications, abstract account and social recovery from our past experience.
Read-only Reentrancy - a Novel Vulnerability class responsible for 100m+ funds at risk
Reentrancy is one of the first lessons learned when getting started with smart contract development and security. In this lightning talk we will present a novel form of reentrency, the "read-only reentrency" which is mostly unknown, although devastating in today's DeFi world and which has been single-handedly responsible for $100m+ in funds at risk.
Rug Life: Using Blockchain Analytics to Detect Illicit Activity, Track Stolen Funds, and Stay Safe
Learn how to use blockchain analytics to identify and protect yourself from the latest rugs, hacks, and scams. The purpose of this talk is to discuss: - How to (automatically) identify illicit activity on the blockchain - Typologies of the latest rugs, hacks, and scams - Tracing where funds from a latest rug/hack/scam have gone - How to protect yourself as a dev
Securing Cross-chain Communication
The last year witnessed several cross-chain bridges being hacked and millions of dollars stolen by hackers. Despite the bridges having gone through several audits, we still see them getting exploited because hackers were able to get access to authorized private keys, signature replay attacks, etc. Let us see what a secure cross-chain bridge architecture should look like and what are the possible attack vectors and mitigation techniques.
Shamir Secret Sharing with No ID Numbers!
Recall that, when splitting a seedphrase via Shamir Secret Sharing into n shares, each share is numbered (from 1 to n). These ID numbers are necessary for reconstruction—if they are lost, reconstruction may be impossible or require brute force. We will quickly review Shamir Secret Sharing and show a trick that can be used to encode the ID numbers into each share for BIP-39 compliant seeds, so that users only need to store the share mnemonic.
Tackling Rounding Errors with Precision Analysis
Rounding errors in smart contracts can lead to severe security vulnerabilities. In this talk, we'll motivate the importance of rigorous numerical analysis through real-world exploits, and review existing precision analysis techniques. We'll then argue for the development of automated error propagation analysis tools to overcome the tediousness of manual efforts.
The $10B Problem - web3 Security Against Coordinated Adversaries
Bored Ape Yacht Club Discord hacked, Ronin Bridge compromised, the news articles are fraught with Ethereum exploits. Chainalysis has identified that these attacks are often executed by a small circle of well-funded, well-coordinated adversaries. In this session, Chainalysis examines how these actors operate, how we investigate the flow of funds to try to disrupt attacks, and how the web3 community can work together to raise costs for attackers using the transparency of public blockchains.
Julia Hardy, Adam Hart
Thinking Like an Auditor to Develop Safer Smart Contracts
Since 2017, ChainSecurity has audited countless smart contracts. Based on this experience, our experts will present a methodology for secure smart contract development. During the workshop, we will coach attendees to think about their project like an auditor would, to help them develop safer smart contracts using foundry and forked mainnet tests.
Time-locked Recovery Factors for Secret Sharing
Verifiable delay encryption allows us to construct time-locked secret shares which reveal themselves after some time. Paired with share refreshing, this allows users to automatically recover their account after a set amount of time even if they have lost secret shares, without compromising key security. Setup requires no user input which allows for a streamlined UX, and we show a demo of this functionality by generating and recovering a private key using this technique.
A brief description of the exploit behind the winning submission to the Underhanded Solidity Contest 2022.
Usable Security in Web3
Self-custodial wallets are the most powerful expression of autonomy we can aspire to in web3, but can people actually keep their EOA accounts safe? Balancing security and usability is critical for onboarding the next billion to web3. During this talk, we will explore how both can converge to give users a usable, secure experience.
Web3 vs Web2 Security: Same or Different?
Web3 security is typically associated with smart contract security. The biggest Web3 hacks have however involved traditional Web2 vulnerabilities and attack vectors. This panel proposes to debate on the similarities and differences between Web3 vs Web2 security with some leaders in this space towards the goal of highlighting the current status, historical lessons from Web2 security and future challenges for a safer Ethereum ecosystem.
Mudit Gupta, Spencer Macdonald, samczsun, Cory Hardman, Nassim Eddequiouaq, Taylor Monahan