Ethereum mainnet is an evolving platform where tremendous effort is made to ensure most projects, including opaque smart contracts are unaffected by each chain upgrade. In particular, changes to the semantics of the EVM can entail serious security issues affecting multiple protocols on chain. An important practice that the ecosystem benefits from are impact studies that aim to find affected projects or smart contracts that may misbehave if the chain’s semantics are changed at an early stage of the development process.

In this talk I will share my experience leading several of these studies for the Ethereum execution layer team. Throughout most of these we’ve developed techniques to audit, at scale, all deployed contracts against a different semantics of Ethereum. Some of these techniques involve formal methods, adapted to work at scale, and include: reverse-compilation, static program analysis with theorem proving (symvalic), and resimulation of past executions,

Finally I will share insights and current and future upgrades (removal of selfdestruct, account abstraction, Verkle trees, gas cost changes) and their summary implications.

Why would this talk is important to this event The event is dedicated to smart contract developers or VM designers with a high level of expertise. The author of this talk has conducted high-level security assessments that impact the entire ecosystem and sharing the learnings is prime content for the audience.

Most of the audience don’t yet have the experience conducting these high level security assessments. The knowledge obtained from this talk may address this gap.