Verification of Smart Contracts using the Interactive Theorem Prover Agda

ALHABARDI, FAHAD

doi:10.23889/SUThesis.67283

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...

Full description

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 veriﬁcation 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 veriﬁed 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 veriﬁed programs, where the veriﬁcation 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 veriﬁcation 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 veriﬁed 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 veriﬁed programs, where the veriﬁcation 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 veriﬁcation 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 veriﬁed 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 veriﬁed programs, where the veriﬁcation 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.037056

Verification of Smart Contracts using the Interactive Theorem Prover Agda / FAHAD ALHABARDI

Similar Items