E-Thesis 241 views 72 downloads
Verification of Smart Contracts using the Interactive Theorem Prover Agda / FAHAD ALHABARDI
Swansea University Author: FAHAD ALHABARDI
-
PDF | E-Thesis – open access
Copyright: The Author, Fahad Faleh Alhabardi, 2024 Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0)
Download (3.45MB)
DOI (Published version): 10.23889/SUThesis.67283
Abstract
The goal of this thesis is to verify smart contracts in Blockchain. In particular, we focus on smart contracts in Bitcoin and Solidity. In order to specify the correctness of smart contracts, we use weakest preconditions. For this, we develop a model of smart contracts in the interactive theorem pro...
| Published: |
Swansea University, Wales, UK
2024
|
|---|---|
| Institution: | Swansea University |
| Degree level: | Doctoral |
| Degree name: | Ph.D |
| Supervisor: | Setzer, A., and Beckmann, A. |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa67283 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
The goal of this thesis is to verify smart contracts in Blockchain. In particular, we focus on smart contracts in Bitcoin and Solidity. In order to specify the correctness of smart contracts, we use weakest preconditions. For this, we develop a model of smart contracts in the interactive theorem prover and dependent type programming language Agda and prove the correctness of smart contracts in it. In the context of Bitcoin, our verification of Bitcoin scripts consists of non-conditional and conditional scripts. For Solidity, we refer to programs using object-oriented features of Solidity, such as calling of other contracts, full recursion, and the use of gas in order to guarantee termination while having a Turing-complete language. We have developed a simulator for Solidity-style smart contracts. As a main example, we executed a reentrancy attack in our model. We have verified smart contracts in Bitcoin and Solidity using weakest precondition in Agda. Furthermore, Agda, combined with the fact that it is a theorem prover and programming language, allows the writing of verified programs, where the verification takes place in the same language in which the program is written, avoiding the problem of translation from one language to another (with possible translation mistakes). |
|---|---|
| Item Description: |
A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information. |
| Keywords: |
Access control, Security, Verification, Provable correctness, Weakest precondition,Precondition, Postcondition, Symbolic execution, Agda proof assistant, Solidity,theorem prover, Model of Solidity-style, transaction, Blockchain, Bitcoin, Ethereum,Local instructions, non-local instructions, Reentrancy attacks, Cryptocurrency, Interface,Simulator, Blockchain control flow, Operational semantics, Hoare logic, Bitcoin script,P2PKH, P2MS, Predicate transformer semantics, Smart contracts, Script. |
| College: |
Faculty of Science and Engineering |
| Funders: |
Royal Embassy of Saudi Arabia/Cultural Bureau in London |