Capturing the Ethereum virtual machine in the UC framework

Ethereum’s smart contract system has become a powerful platform for developing decentralized applications. Its introduction of programmability to blockchain systems has significantly expanded the use cases of blockchains. The technology that had been mostly used as a distributed ledger has now evolved into a distributed state machine, allowing developers to upload their programs to the blockchain and users to request execution of arbitrary computations by the platform. However, this exciting new advancement is not without risks. Attackers have been able to exploit various design flaws of Ethereum smart contracts and caused loss of highly valuable assets. On the other hand, security analyses of smart contract designs are often empirical and lack adoption of formal methods. Developers sometimes are only able to identify security breaches after attacks have been carried out. This is understandable, as the Ethereum smart contract system is difficult to capture, even by some of the most expressive frameworks that security analysts use to study distributed protocols. This work aims to provide a solution to this problem, by modeling the Ethereum Virtual Machine (EVM) as a global functionality in the Universal Composability (UC) framework and formulating proofs of smart contract security. It is our hope that formal proof techniques can receive wider adoption among developers of decentralized applications in the near future.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Electrical & Computer Engr

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2023

Author dc:creator

• Han, Fangqi

Contributors dc:contributor

• Miller, Andrew

• Security
• Blockchain
• Smart Contracts

Statement dc:rights

• Copyright 2023 Fangqi Han

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/121552

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F121552