eprintid: 10137858
rev_number: 20
eprint_status: archive
userid: 608
dir: disk0/10/13/78/58
datestamp: 2021-12-16 14:10:48
lastmod: 2021-12-16 14:10:48
status_changed: 2021-12-16 14:10:48
type: thesis
metadata_visibility: show
creators_name: Schett, Maria A
title: Cost Reduction With Guarantees: Formal Reasoning Applied To Blockchain Technologies
ispublished: unpub
divisions: UCL
divisions: B04
divisions: C05
divisions: F48
note: Copyright © The Author 2021.  Original content in this thesis is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0) Licence (https://creativecommons.org/licenses/by-nc/4.0/).  Any third-party copyright material present remains the property of its respective owner(s) and is licensed under its existing terms.  Access may initially be restricted at the author’s request.
abstract: Blockchain technologies are moving fast and their distributed nature as well as their high-stake (financial) applications make it crucial to “get things right”. Moreover, blockchain technologies often come with a high cost for maintaining blockchain infrastructure and for running applications. In this thesis formal reasoning is used for guaranteeing correctness while reducing the cost of (i) maintaining the infrastructure by optimising blockchain protocols, and (ii) running applications by optimising blockchain programs—so called smart contracts. Both have a clear cost measure: for protocols the amount of exchanged messages, and for smart contracts the monetary cost of execution. In the first result for blockchain protocols starting from a proof of correctness for an abstract blockchain consensus protocol using infinitely many messages and infinite state, a refinement proof transfers correctness to a concrete implementation of the protocol reducing the cost to finite resources. In the second result I move from a blockchain to a block graph. This block graph embeds the run of a deterministic byzantine fault tolerant protocol, thereby getting parallelism “for free” and reducing the exchanged messages to the point of omission. For blockchain programs, I optimise programs executed on the Ethereum blockchain. As a first result, I use superoptimisation and encode the search for cheaper, but observationally equivalent, program as a search problem for an automated theorem prover. Since solving this search problem is in itself expensive, my second result is an efficient encoding of the search problem. Finally for reusing found optimisations, my third results gives a framework to generate peephole optimisation rules for a smart contract compiler.
date: 2021-11-28
date_type: published
oa_status: green
full_text_type: other
thesis_class: doctoral_open
thesis_award: Ph.D
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_id: 1897749
lyricists_name: Schett, Maria
lyricists_id: MSCHE30
actors_name: Schett, Maria
actors_id: MSCHE30
actors_role: owner
full_text_status: public
pagerange: 1-185
pages: 186
event_title: UCL (University College London)
institution: UCL (University College London)
department: Computer Science
thesis_type: Doctoral
citation:        Schett, Maria A;      (2021)    Cost Reduction With Guarantees: Formal Reasoning Applied To Blockchain Technologies.                   Doctoral thesis  (Ph.D), UCL (University College London).     Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/10137858/1/schett_thesis_final.pdf