devcon 5 / fully automated inductive invariants inference for solidity smart contracts
- YouTube
- IPFS
- Details
Fully automated inductive invariants inference for Solidity smart contracts
Duration: 00:24:41
Speaker: Leo Alt, Matteo Marescotti
Type: Breakout
Expertise: Advanced
Event: Devcon
Date: Invalid Date
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.
- Related
Devcon
Talk
21:04
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.
Devcon
Talk
22:32
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.
Devcon
Talk
15:46
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.
Devcon
Breakout
23:05
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.
Devcon
Breakout
30:18
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.
Devcon
Breakout
27:10
(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.
Devcon
Breakout
28:57
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.
Devcon
Breakout
18:25
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.
Devcon
Breakout
20:22
How do we make dapps as secure as the underlying Ethereum?
Web3.js is a Javascript API for web applications (dapps) to access Ethereum blockchain. However, its security assumption inherited the security assumption of an Ethereum node, which is entirely open to the node's owner. The privacy and security consequences of that assumption are two-fold. First, a web application can learn sensitive information about the user. Second, the web application can feign a representation of blockchain data to be another or even tricking users to signing obfuscate transactions. A website which simply draws a crypto kitty would look no different than another which reads the user’s kitty from Ethereum smart contracts. Much makeshift work has been down for this underdesigned infrastructure. For example, MetaMask resorted to hardcoding CryptoKitty and requesting permission to read the user's address. However, only so much patches could do. Furthermore, such patches weren’t designed with abstraction to accommodate next-generation blockchains with privacy and efficiency improvements. For example, failing to find truth quickly using the low-level interfaces provided by web3.js, many dapp browsers resorted to relying on a centralised token status database. The speaker presents a design which abstracts token interface away from low-level Eth-node interface, remodels the basic web code trust inheritance for practicality and security. It involves high-level API for web applications and a secure, WebAssembly based sandbox running signed code designed to embed in the Web itself.
Devcon
Breakout
05:40
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.