E-Thesis 108 views 26 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!
|
first_indexed |
2024-08-01T12:16:39Z |
---|---|
last_indexed |
2024-08-01T12:16:39Z |
id |
cronfa67283 |
recordtype |
RisThesis |
fullrecord |
<?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>67283</id><entry>2024-08-01</entry><title>Verification of Smart Contracts using the Interactive Theorem Prover Agda</title><swanseaauthors><author><sid>d4af80b64a1f646a7e061016901fb3b0</sid><firstname>FAHAD</firstname><surname>ALHABARDI</surname><name>FAHAD ALHABARDI</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2024-08-01</date><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).</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea University, Wales, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><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.</keywords><publishedDay>24</publishedDay><publishedMonth>7</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-07-24</publishedDate><doi>10.23889/SUThesis.67283</doi><url/><notes>A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information.</notes><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Setzer, A., and Beckmann, A.</supervisor><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><degreesponsorsfunders>Royal Embassy of Saudi Arabia/Cultural Bureau in London</degreesponsorsfunders><apcterm/><funders>Royal Embassy of Saudi Arabia/Cultural Bureau in London</funders><projectreference/><lastEdited>2024-08-01T13:36:49.9907978</lastEdited><Created>2024-08-01T13:08:49.4434848</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>FAHAD</firstname><surname>ALHABARDI</surname><order>1</order></author></authors><documents><document><filename>67283__31024__387fadf897e3425ea39a001cf20e5698.pdf</filename><originalFilename>2024_Alhabardi_F.final.67283.pdf</originalFilename><uploaded>2024-08-01T13:15:16.7673887</uploaded><type>Output</type><contentLength>3620399</contentLength><contentType>application/pdf</contentType><version>E-Thesis – open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The Author, Fahad Faleh Alhabardi, 2024
Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0)</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807> |
spelling |
v2 67283 2024-08-01 Verification of Smart Contracts using the Interactive Theorem Prover Agda d4af80b64a1f646a7e061016901fb3b0 FAHAD ALHABARDI FAHAD ALHABARDI true false 2024-08-01 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). E-Thesis Swansea University, Wales, UK 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. 24 7 2024 2024-07-24 10.23889/SUThesis.67283 A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information. COLLEGE NANME COLLEGE CODE Swansea University Setzer, A., and Beckmann, A. Doctoral Ph.D Royal Embassy of Saudi Arabia/Cultural Bureau in London Royal Embassy of Saudi Arabia/Cultural Bureau in London 2024-08-01T13:36:49.9907978 2024-08-01T13:08:49.4434848 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science FAHAD ALHABARDI 1 67283__31024__387fadf897e3425ea39a001cf20e5698.pdf 2024_Alhabardi_F.final.67283.pdf 2024-08-01T13:15:16.7673887 Output 3620399 application/pdf E-Thesis – open access true Copyright: The Author, Fahad Faleh Alhabardi, 2024 Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0) true eng |
title |
Verification of Smart Contracts using the Interactive Theorem Prover Agda |
spellingShingle |
Verification of Smart Contracts using the Interactive Theorem Prover Agda FAHAD ALHABARDI |
title_short |
Verification of Smart Contracts using the Interactive Theorem Prover Agda |
title_full |
Verification of Smart Contracts using the Interactive Theorem Prover Agda |
title_fullStr |
Verification of Smart Contracts using the Interactive Theorem Prover Agda |
title_full_unstemmed |
Verification of Smart Contracts using the Interactive Theorem Prover Agda |
title_sort |
Verification of Smart Contracts using the Interactive Theorem Prover Agda |
author_id_str_mv |
d4af80b64a1f646a7e061016901fb3b0 |
author_id_fullname_str_mv |
d4af80b64a1f646a7e061016901fb3b0_***_FAHAD ALHABARDI |
author |
FAHAD ALHABARDI |
author2 |
FAHAD ALHABARDI |
format |
E-Thesis |
publishDate |
2024 |
institution |
Swansea University |
doi_str_mv |
10.23889/SUThesis.67283 |
college_str |
Faculty of Science and Engineering |
hierarchytype |
|
hierarchy_top_id |
facultyofscienceandengineering |
hierarchy_top_title |
Faculty of Science and Engineering |
hierarchy_parent_id |
facultyofscienceandengineering |
hierarchy_parent_title |
Faculty of Science and Engineering |
department_str |
School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science |
document_store_str |
1 |
active_str |
0 |
description |
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). |
published_date |
2024-07-24T13:36:50Z |
_version_ |
1806188738090369024 |
score |
11.021648 |