Title: Foundations for the security analysis of distributed blockchain applications
Language: English
Authors: Schneidewind, Clara 
Qualification level: Doctoral
Advisor: Maffei, Matteo 
Issue Date: 2021
Number of Pages: 281
Qualification level: Doctoral
Cryptocurrencies do not only allow for money transfers in the absence of a trusted third party but also enable the execution of distributed applications. Due to the rapid pace of development of cryptocurrencies, the foundations of such applications have not been rigorously studied. This is particularly problematic since in these applications, real money is at stake, and security breaches regularly cause severe financial losses.In this thesis, we present two systematic approaches to reliably verify the security of distributed blockchain applications based on formal foundations. To this end, we focus on the cryptocurrencies with the highest market capitalization, Bitcoin and Ethereum. In Ethereum, distributed applications are realized as smart contracts, reactive programs written in Ethereum’s expressive scripting language. In contrast, Bitcoin supports only a basic scripting language, and advanced applications are realized as peer-to-peer cryptographic protocols that resort to the execution of simple smart contracts in case of disputes among peers. As a result, the challenge in verifying distributed applications on the Ethereum blockchain lies in the study and abstraction of the semantics of Ethereum’s evolved scripting language, whereas Bitcoin, the study of distributed applications, requires a systematic analysis of the cryptographic protocols.In the thesis, we first formalize the formerly under-specified semantics of Ethereum’s native smart contract language EVM bytecode and implement the semantics in the proof assistant F*. In this context, we formally characterize relevant generic properties for smart contract security, which capture real-world attack scenarios.We then survey existing automated static analyzers for Ethereum smart contracts unveiling the weaknesses in the semantic foundations of these tools and the practical impact of these weaknesses on the analysis results. Based on these findings, we propose our own automatic static analysis tool for Ethereum smart contracts, which comes with a rigorous soundness proof while still showing competitive performance. In this course, we also propose a general framework for the modular and semantic-driven development of automatic static analyzers. Finally, we study the security of payment channel networks for Bitcoin. Payment channel networks are distributed protocols that allow for efficient and cheap payments between Bitcoin users and offer a promising solution to Bitcoin’s scalability problems. We unveil a security issue in Bitcoin’s existing payment channel network implementation and formally characterize the relevant security and privacy notions in this context. We further develop a cryptographic primitive for the construction of payment channel networks with formal security guarantees
Keywords: blockchain; static analysis; cryptocurrencies; verification; provable security; cryptographic protocols; privacy
URI: https://doi.org/10.34726/hss.2021.91204
DOI: 10.34726/hss.2021.91204
Library ID: AC16212134
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Jun 20, 2021


checked on Jun 20, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.