Verification of Smart Contracts in the Blockchain (89400)

Yoni Zohar
Department of Computer Science
Bar-Ilan University

Technical Details

Time and Location

Grading

Potential Papers

Smart Contracts Languages and Vulnerabilities

  1. Ethereum: A secure decentralised generalised transaction ledger (Yellow Paper). Garvin Wood.
  2. A survey of attacks on Ethereum smart contracts. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli
  3. Bitcoin: A Peer-to-Peer Electronic Cash System. Satoshi Nakamoto
  4. Move: A Language With Programmable Resources. Blackshear et al.

Verification of Software

  1. 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
  2. Chapters 12.1 -- 12.3 in the book "Decision Procedures: An Algorithmic Point of View". Daniel Kroening and Ofer Strichman
  3. A Polymorphic Intermediate Verification Language: Design and Logical Encodings. Leino and Rummer

Verification of Smart Contracts

  1. Making Smart Contracts Smarter. Luu, Chu, Olickel et al.
  2. Demystifying Loops in Smart Contracts. Mariano et al.
  3. ZEUS: Analyzing Safety of Smart Contracts. Sukrit Kalra, Seep Goel, Mohan Dhawan, Subodh Sharma
  4. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. Hildenbrandt, Saxena, Rodrigues et al.
  5. Securify: Practical Security Analysis of Smart Contracts. Tsankov et al.
  6. Proof-Carrying Smart Contracts. Dickerson, Gazzillo, Herlihy, Saraph, Koskinen
  7. Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. Wang, Lahiri, Chen et al.
  8. SMT-Friendly Formalization of the Solidity Memory Model. Hajdu and Jovanovic
  9. The Move Prover. Zhong et al.
  10. SolCMC: Solidity Compiler's Model Checker. Alt et al.

Other Papers

If you would like to present a paper that is not in the above list but is related to the seminar, that is probably fine. Feel free to suggest it to me via email.

Schedule

Date Lesson # Lecturer(s) Paper(s)
19.03.23 1 Yoni Introduction slides
26.03.23 2 Itay Atlis and Dor Huri A survey of attacks on Ethereum smart contracts. Atzei et al.
slides
code
02.04.23 -- Passover
09.04.23 -- Passover
16.04.23 3 Ben and Gal 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
23.04.23 4 Itay and Reuven Chapters 12.1 -- 12.3 in the book "Decision Procedures: An Algorithmic Point of View". Daniel Kroening and Ofer Strichman
slides
30.04.23 5 Neria and Moria Bitcoin: A Peer-to-Peer Electronic Cash System. Satoshi Nakamoto
slides
07.05.23 6 Eliran and Ben A Polymorphic Intermediate Verification Language: Design and Logical Encodings. Leino and Rummer
slides
14.05.23 7 Uriel and Noa Making Smart Contracts Smarter. Luu, Chu, Olickel et al.
slides
code
Oyente run log
21.05.23 -- Strike
28.05.23 -- Strike
04.06.23 -- Strike
11.06.23 8


9		 Niv and Or


Tom and Daniel 		Move: A Language With Programmable Resources. Blackshear et al.
slides

The Move Prover. Zhong et al.
slides
18.06.23 10

-- 		Tommy and Idan

Yoni 		ZEUS: Analyzing Safety of Smart Contracts. Sukrit Kalra, Seep Goel, Mohan Dhawan, Subodh Sharma
slides

Summary
slides
25.06.23 11

12 		Yossef and Yossef

Yoav and Omer 		Demystifying Loops in Smart Contracts. Mariano et al.
slides

SMT-Friendly Formalization of the Solidity Memory Model. Hajdu and Jovanovic
slides