Automated Verification of Blockchain Technologies with Correctness Guarantees

You are cordially invited to attend the PhD Dissertation Defence of Rodrigo Benedito Otoni on Monday 9 October 2023 at 17:00 in room D0.02 (USI East Campus) and online.

Abstract:
Blockchain technologies have drawn significant attention from both academia and industry over the last decade, with increasing adoption by the general public and potential to drastically change the way in which individuals and institutions interact with each other. Due to their extensive use as a means to hold and manipulate financial assets, they are likely targets of attacks, with assets estimated in the order of millions of US Dollars having already been lost in the past. In light of this, the ability to ensure the absence of vulnerabilities is of crucial importance. This work addresses the need for automated verification of blockchain technologies with correctness guarantees. The blockchain space is approached both at the platform and the application level, with the use of verification techniques based on first-order logic being investigated as a means to tackle the growing need of assurances in this domain. To strengthen the guarantees provided, the use of correctness witnesses to validate the results of logic solvers dedicated to logic fragments of interest is also investigated. This dissertation draws on recent advances in the field of symbolic model checking, specifically on techniques based on satisfiability modulo theories (SMT) and constrained Horn clauses (CHC), and extend the state of the art in a fourfold manner. It (i) proposes a novel scalable SMT-based model checking approach for distributed algorithms, which are the cornerstone of blockchain platforms, specified in TLA+. It (ii) evaluates and enhances a direct modelling CHC-based model checking approach for smart contracts, which are programs executing on top of blockchain platforms, written in Solidity. It (iii) proposes a novel format for witnesses of SMT unsatisfiability results, which leads to witnesses that are compact and lightweight to produce and validate. It (iv) proposes a novel proof-backed approach for the validation of CHC satisfiability results. The first two contributions are directly applicable in the blockchain domain and they interface with the last two via their use of SMT and CHC. Despite the focus on one specific domain, the insights presented in this dissertation can in principle be applied in the general case and serve as a basis for further research.

Dissertation Committee:
- Prof. Patrick Thomas Eugster, Università della Svizzera italiana, Switzerland (Research Advisor)
- Prof. Natasha Sharygina, Università della Svizzera italiana, Switzerland (Research co-Advisor)
- Prof. Gabriele Bavota, Università della Svizzera italiana, Switzerland (Internal Member)
- Prof. Fernando Pedone, Università della Svizzera italiana, Switzerland (Internal Member)
- Prof. Arie Gurfinkel, University of Waterloo, Canada (External Member)
- Prof. Shuvendu Lahiri, Microsoft Research Redmond, USA (External Member)