Back
2023INF015
Doctoral thesis

Automated verification of blockchain technologies with correctness guarantees

  • 2023

PhD: Università della Svizzera italiana

Formal verification
Model checking
TLA+
Smart contracts
SMT
CHC
English 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.
Collections
Language
  • English
Classification
Computer science and technology
License
License undefined
Open access status
green
Identifiers
Persistent URL
https://n2t.net/ark:/12658/srd1326503
Statistics
Document views: 176 File downloads:
  • 2023INF015.pdf: 136