Solidity Summit 2020
-
Solidity Summit Day 1
2-day, interactive online event with talks & workshops feat. all things Solidity - live from https://interspace.solidity-summit.ethereum.org -
Solidity Summit Day 2
2-day, interactive online event with talks & workshops feat. all things Solidity - live from https://interspace.solidity-summit.ethereum.org -
Solidity Summit Opening & Welcome by Franziska Heintel
Franziska Heintel welcomes us to The Solidity Summit for April 2020 and gives us a quick overview of how to use the technology. -
Solidity 2020 Roadmap by Chris Reitwiessner
Chris gives us a quick tour of the roadmap for Solidity Summit for 2020. -
Solc-verify, a source-level formal verification tool for Solidity smart contracts by Akos Hajdu
Solc-verify is a source-level formal verification tool for Soldity smart contracts, developed in collaboration with SRI International. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code. This enables solc-verify to effectively reason about high-level functional properties while modeling low-level language semantics (e.g., the memory model) precisely. The contract properties, such as contract invariants, loop invariants, function pre- and post-conditions and fine grained access control can be provided as in-code annotations by the developer. This enables automated, yet user-friendly formal verification for smart contracts. -
Introduction to the K Framework and KSolidity by Rikard Hjort and Shang Wei Lin
Learn about the K's background and the Solidity semantics in the K framework. -
Certora: Keeping your code secure forever: Move Fast and Break Nothing by Mooly Sagiv
We will describe a platform for formally verifying smart contract correctness that can be integrated in CI/CD. Smart contracts and their invariants are converted into SMT formulas and the SMT solvers automatically identify vulnerabilities or generate mathematical proofs of correctness. We describe our experience applying this technology in the development phase and present bugs found and smart contracts verified. Our hope is that this SaaS technology can speed up the development process. The secret sauce for integrating in the CI/CD is that the invariants are reusable across different versions of the code, and targeting the low level EVM bytecode. This raises various technical challenges both at the conceptual level of the specification and at the technical level. -
dType and ChainLens by Loredana Cirstea
"dType is a decentralized & distributed type system for interoperable protocols.
ChainLens: Lens implementation for Ethereum as a browser and fine-grained search for smart contracts with a distributed database cache of types, functions, ABIs, code sources, and other metadata information. Available as a Remix IDE plugin, interoperable with other plugins. -
Thoughts on Language Design and Fragmentation by Alex Beregszaszi
Solidity is a relatively young language in a rapidly evolving space. The challenges it faces changed over time, greatly influencing the language design. In this brief talk, we examine the current language design processes in place and compare it against other models (i.e. language design committees). -
Introduction to Yul+ by Nick Dodson
"Yul+ is an extension to Yul, an intermediate language for the Ethereum Virtual Machine. It adds several quality of language features such as enums, constants, memory structures and injected methods. Our talk will go over the motivations, objectives and the features that Yul+ brings to the Ethereum ecosystem.
1) Yul overview, what we liked and what we needed
2) Motivations for an extension language
3) Objectives for a new language
4) Yul+ feature overview
5) Roadmap and future language exploration" -
SOLL Compiler (for YUL and Solidity) by Michael Yuan
Learn more about the evolution and current state of the SOLL compiler project, which builds compiler front ends for YUL and Solidity, and backends for Ewasm and EVM. This talk includes a report on the technical progress made so far as well as future roadmaps and collaborations. It also discussed the web-based IDE developed for Solidity that allows fast dapp development and deployment on Ethereum compatible blockchains. -
Tracking mapping keys with the Truffle Debugger by Harry Altman
The Solidity language does not keep track of what keys are set in a given mapping. However, the Truffle Debugger can, when debugging a transaction, keep track of what keys have been accessed during that transaction, and it can do this even if the mappings are nested inside arrays, structs, or other mappings. In this talk, we will dissect Truffle Debugger's mapping key tracking system and learn how it works.