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. 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.6 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. Demystifying Loops in Smart Contracts. Mariano et al.
  2. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. Hildenbrandt, Saxena, Rodrigues et al.
  3. Proof-Carrying Smart Contracts. Dickerson, Gazzillo, Herlihy, Saraph, Koskinen
  4. Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. Wang, Lahiri, Chen et al.
  5. SMT-Friendly Formalization of the Solidity Memory Model. Hajdu and Jovanovic
  6. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. Dill et al.
  7. Securing Aptos Framework with Formal Verification. Park et al.
  8. SolCMC: Solidity Compiler's Model Checker. Alt et al.
  9. Accurate Smart Contract Verification through Direct Modelling. Marescotti1, Otoni1, Alt et al.
  10. Overapproximation of Non-linear Integer Arithmetic for Smart Contract Verification. Petra Hozzová, Jaroslav Bendík, Alexander Nutz and Yoav Rodeh

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)
16.03.25 1 Yoni Introduction slides
23.03.25 2 Guy and Oz A survey of attacks on Ethereum smart contracts slides
30.03.25 3 Shira and Or L Proof-Carrying Smart Contracts slides
06.04.25 4 Avinoam and Khaled Demystifying Loops in Smart Contracts slides
13.04.25 -- Passover
20.04.25 -- Passover
27.04.25 5 Sharon and Nadav Chapters 1.1 -- 1.3, 2.1 -- 2.3, 3.1 -- 3.6 in the book "The Calculus of Computation"
04.05.25 6

7 		Sapir and Roy Mo

Dolev and Roy Ma 		Chapters 12.1 -- 12.3 in the book "Decision Procedures: An Algorithmic Point of View"

Securing Aptos Framework with Formal Verification
11.05.25 -- -- No class
18.05.25 9 Or H and Orel SolCMC: Solidity Compiler's Model Checker
25.05.25 8 Evyatar and Avichai SMT-Friendly Formalization of the Solidity Memory Model
01.06.25 -- SHAVUOT
08.06.25 10 Omri and Michael Move: A Language With Programmable Resources. Blackshear et al.
15.06.25 11 Sandos and Muhammad Overapproximation of Non-linear Integer Arithmetic for Smart Contract Verification
22.06.25 12 Elia and Or S Accurate Smart Contract Verification through Direct Modelling
29.06.25 13 Bar and Shaked Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain