Verification of Smart Contracts in the Blockchain (89400)

Technical Details

Time and Location

• Semester: BIU 2023/2024 Semester B
• Time: Sundays 09:00 -- 10:30
• Location: Building 902, Room 210

Grading

• Presentation (80%)
• Participation (20%)
• IMPORTANT: The presentations and discussions will all be in English.

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

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

Verification of Smart Contracts

8. Making Smart Contracts Smarter. Luu, Chu, Olickel et al.
9. Demystifying Loops in Smart Contracts. Mariano et al.
10. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. Hildenbrandt, Saxena, Rodrigues et al.
11. Securify: Practical Security Analysis of Smart Contracts. Tsankov et al.
12. Proof-Carrying Smart Contracts. Dickerson, Gazzillo, Herlihy, Saraph, Koskinen
13. Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. Wang, Lahiri, Chen et al.
14. SMT-Friendly Formalization of the Solidity Memory Model. Hajdu and Jovanovic
15. The Move Prover. Zhong et al.
16. SolCMC: Solidity Compiler's Model Checker. Alt et al.
17. Accurate Smart Contract Verification through Direct Modelling. Marescotti1, Otoni1, Alt et al.
18. Overapproximation of Non-linear Integer Arithmetic for Smart Contract Verification. Petra Hozzová, Jaroslav Bendík, Alexander Nutz and Yoav Rodeh

Other Papers

Schedule