No Cover Image

Conference Paper/Proceeding/Abstract 401 views 43 downloads

A model of Solidity-style smart contracts in the theorem prover Agda

Fahad Alhabardi, Anton Setzer Orcid Logo

2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings), Pages: 1 - 10

Swansea University Author: Anton Setzer Orcid Logo

  • 64153.pdf

    PDF | Accepted Manuscript

    Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).

    Download (251.04KB)

DOI (Published version): 10.1109/aibthings58340.2023.10292478

Abstract

The use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some ch...

Full description

Published in: 2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings)
ISBN: 979-8-3503-2235-4 979-8-3503-2234-7
Published: IEEE 2023
URI: https://cronfa.swan.ac.uk/Record/cronfa64153
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2023-09-01T10:51:48Z
last_indexed 2023-09-01T10:51:48Z
id cronfa64153
recordtype SURis
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>64153</id><entry>2023-08-29</entry><title>A model of Solidity-style smart contracts in the theorem prover Agda</title><swanseaauthors><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2023-08-29</date><deptcode>MACS</deptcode><abstract>The use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some challenges, such as security vulnerabilities, still need to be addressed before smart contracts can be widely adopted.This paper introduces two models of smart contracts – one simple and one more complex – using the interactive theorem prover Agda. This is a step towards converting the previous work of verifying Bitcoin smart contracts using weakest preconditions [1], [2] to Ethereum’s Solidity-style [3] smart contracts. Since Ethereum’s contracts are object-oriented, this model is substantially more complex than Bitcoin’s. We provide models supporting simple and complex executions, the calling of other contracts, and functions referring to addresses and messages. Furthermore, these models also support transferring money to other contracts and updating specific contracts, and the more complex model includes gas cost and pure functions.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings)</journal><volume>0</volume><journalNumber/><paginationStart>1</paginationStart><paginationEnd>10</paginationEnd><publisher>IEEE</publisher><placeOfPublication/><isbnPrint>979-8-3503-2235-4</isbnPrint><isbnElectronic>979-8-3503-2234-7</isbnElectronic><issnPrint/><issnElectronic/><keywords>Ethereum, smart contracts, Agda proof assistant, cryptocurrency, theorem prover, Solidity, Model of soliditystyle, transaction, blockchain</keywords><publishedDay>30</publishedDay><publishedMonth>10</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-10-30</publishedDate><doi>10.1109/aibthings58340.2023.10292478</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2024-10-07T13:35:26.5775101</lastEdited><Created>2023-08-29T09:14:55.6505631</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><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>2</order></author></authors><documents><document><filename>64153__28390__1ecab0655c514c598979edc99af2f362.pdf</filename><originalFilename>64153.pdf</originalFilename><uploaded>2023-08-29T09:26:57.2068087</uploaded><type>Output</type><contentLength>257061</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><documentNotes>Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/deed.en</licence></document></documents><OutputDurs/></rfc1807>
spelling v2 64153 2023-08-29 A model of Solidity-style smart contracts in the theorem prover Agda 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2023-08-29 MACS The use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some challenges, such as security vulnerabilities, still need to be addressed before smart contracts can be widely adopted.This paper introduces two models of smart contracts – one simple and one more complex – using the interactive theorem prover Agda. This is a step towards converting the previous work of verifying Bitcoin smart contracts using weakest preconditions [1], [2] to Ethereum’s Solidity-style [3] smart contracts. Since Ethereum’s contracts are object-oriented, this model is substantially more complex than Bitcoin’s. We provide models supporting simple and complex executions, the calling of other contracts, and functions referring to addresses and messages. Furthermore, these models also support transferring money to other contracts and updating specific contracts, and the more complex model includes gas cost and pure functions. Conference Paper/Proceeding/Abstract 2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings) 0 1 10 IEEE 979-8-3503-2235-4 979-8-3503-2234-7 Ethereum, smart contracts, Agda proof assistant, cryptocurrency, theorem prover, Solidity, Model of soliditystyle, transaction, blockchain 30 10 2023 2023-10-30 10.1109/aibthings58340.2023.10292478 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2024-10-07T13:35:26.5775101 2023-08-29T09:14:55.6505631 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Fahad Alhabardi 1 Anton Setzer 0000-0001-5322-6060 2 64153__28390__1ecab0655c514c598979edc99af2f362.pdf 64153.pdf 2023-08-29T09:26:57.2068087 Output 257061 application/pdf Accepted Manuscript true Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention). true eng https://creativecommons.org/licenses/by/4.0/deed.en
title A model of Solidity-style smart contracts in the theorem prover Agda
spellingShingle A model of Solidity-style smart contracts in the theorem prover Agda
Anton Setzer
title_short A model of Solidity-style smart contracts in the theorem prover Agda
title_full A model of Solidity-style smart contracts in the theorem prover Agda
title_fullStr A model of Solidity-style smart contracts in the theorem prover Agda
title_full_unstemmed A model of Solidity-style smart contracts in the theorem prover Agda
title_sort A model of Solidity-style smart contracts in the theorem prover Agda
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Fahad Alhabardi
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title 2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings)
container_volume 0
container_start_page 1
publishDate 2023
institution Swansea University
isbn 979-8-3503-2235-4
979-8-3503-2234-7
doi_str_mv 10.1109/aibthings58340.2023.10292478
publisher IEEE
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 use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some challenges, such as security vulnerabilities, still need to be addressed before smart contracts can be widely adopted.This paper introduces two models of smart contracts – one simple and one more complex – using the interactive theorem prover Agda. This is a step towards converting the previous work of verifying Bitcoin smart contracts using weakest preconditions [1], [2] to Ethereum’s Solidity-style [3] smart contracts. Since Ethereum’s contracts are object-oriented, this model is substantially more complex than Bitcoin’s. We provide models supporting simple and complex executions, the calling of other contracts, and functions referring to addresses and messages. Furthermore, these models also support transferring money to other contracts and updating specific contracts, and the more complex model includes gas cost and pure functions.
published_date 2023-10-30T13:35:24Z
_version_ 1812258645570748416
score 11.036706

Similar Items