Verification of Smart Contracts
Time and Location
Potential Papers
Papers are available online and can be found by searching their names.
If you have trouble locating a paper, please contact me.
Smart Contracts Languages and Vulnerabilities
- A survey of attacks on Ethereum smart contracts. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli
- Move: A Language With Programmable Resources. Blackshear et al.
Verification of Software
- Chapters 1.1 -- 1.3, 2.1 -- 2.3, 3.1 -- 3.3 in the book "The Calculus of Computation". Aaron Bradley and Zohar Manna
- Chapters 12.1 -- 12.3 in the book "Decision Procedures: An Algorithmic Point of View". Daniel Kroening and Ofer Strichman
- A Polymorphic Intermediate Verification Language: Design and Logical Encodings. Leino and Rummer
Verification of Smart Contracts
- Making Smart Contracts Smarter. Luu, Chu, Olickel et al.
- Demystifying Loops in Smart Contracts. Mariano et al.
- ZEUS: Analyzing Safety of Smart Contracts. Sukrit Kalra, Seep Goel, Mohan Dhawan, Subodh Sharma
- KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. Hildenbrandt, Saxena, Rodrigues et al.
- Securify: Practical Security Analysis of Smart Contracts. Tsankov et al.
- Proof-Carrying Smart Contracts. Dickerson, Gazzillo, Herlihy, Saraph, Koskinen
- Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. Wang, Lahiri, Chen et al.
- SMT-Friendly Formalization of the Solidity Memory Model. Hajdu and Jovanovic
- The Move Prover. Zhong et al.
- SMT-Based Verification of Solidity Smart Contracts. Alt and Reitwiessner
More Resources
Tentative Schedule
- October 10, 2021:
- Yoni Zohar -- Introduction 1 slides
- October 17, 2021:
- Yoni Zohar -- Introduction 2 slides
- October 24, 2021:
- David Krongauz -- A survey of attacks on Ethereum smart contracts. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli slides
- Ehud Waserman -- Making Smart Contracts Smarter. Luu, Chu, Olickel et al. slides
- October 31, 2021:
- Zvika Berger -- Chapters 1.1 -- 1.3, 2.1 -- 2.3, 3.1 -- 3.3 in the book "The Calculus of Computation". Aaron Bradley and Zohar Manna slides
- November 7, 2021:
- Yuval Tal -- Chapters 12.1 -- 12.3 in the book "Decision Procedures: An Algorithmic Point of View". Daniel Kroening and Ofer Strichman slides
- November 14, 2021:
- Ido Faran -- A Polymorphic Intermediate Verification Language: Design and Logical Encodings. Leino and Rummer slides
- Nir Bagizada -- KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. Hildenbrandt, Saxena, Rodrigues et al. slides
- November 21, 2021:
- David Emmanuel -- SMT-Based Verification of Solidity Smart Contracts. Alt and Reitwiessner slides
- November 28, 2021:
- Saar Cohen -- Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. Wang, Lahiri, Chen et al. slides
- Ohad Azran -- SMT-Friendly Formalization of the Solidity Memory Model. Hajdu and Jovanovic slides
- December 5, 2021: No class
- December 12, 2021:
- Daniel Kaganovich -- ZEUS: Analyzing Safety of Smart Contracts. Sukrit Kalra, Seep Goel, Mohan Dhawan, Subodh Sharma slides
- December 19, 2021:
- Hezi Yafe -- Securify: Practical Security Analysis of Smart Contracts. Tsankov et al.
- Shani Cattan -- Move: A Language With Programmable Resources. Blackshear et al. slides
- December 26, 2021:
- Rafi Yzgeav -- Proof-Carrying Smart Contracts. Dickerson, Gazzillo, Herlihy, Saraph, Koskinen slides
- January 2, 2021:
- Ori Roza -- The Move Prover. Zhong et al. slides
- January 9, 2021:
- Certora -- Lecture about Certora.
- Yoni Zohar -- Summary of the seminar