No Cover Image

Conference Paper/Proceeding/Abstract 610 views

Verifying Correctness of Smart Contracts with Conditionals

Fahad Alhabardi, Bogdan Lazar, Anton Setzer Orcid Logo

2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain & Beyond (iGETblockchain), Pages: 1 - 25

Swansea University Author: Anton Setzer Orcid Logo

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1109/igetblockchain56591.2022.10087054

Abstract

In this paper, we specify and verify the correctness of programs written in Bitcoin's smart contract Script in the interactive theorem prover Agda. As in the previous article [1] we use weakest preconditions of Hoare Logic to specify the security property of access control, and show how to deve...

Full description

Published in: 2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain & Beyond (iGETblockchain)
ISBN: 978-1-6654-5260-1 978-1-6654-5198-7
Published: IEEE 2022
Online Access: http://dx.doi.org/10.1109/igetblockchain56591.2022.10087054
URI: https://cronfa.swan.ac.uk/Record/cronfa61633
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2022-10-23T19:32:18Z
last_indexed 2023-04-13T03:21:19Z
id cronfa61633
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>61633</id><entry>2022-10-23</entry><title>Verifying Correctness of Smart Contracts with Conditionals</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>2022-10-23</date><deptcode>SCS</deptcode><abstract>In this paper, we specify and verify the correctness of programs written in Bitcoin's smart contract Script in the interactive theorem prover Agda. As in the previous article [1] we use weakest preconditions of Hoare Logic to specify the security property of access control, and show how to develop human-readable specifications.In this article, we include conditionals into the language. For the operational semantics we use an additional stack, the ifstack, to deal with nested conditionals. This avoids the addition of extra jump instructions, which are usually used for the operational semantics of with conditionals in Forth-style stack languages. The ifstack preserves the original nesting of conditionals, and we determine an ifthenselse-theorem which allows to derive verification conditions of conditionals by referring to conditions for the if- and else-case.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain &amp;amp; Beyond (iGETblockchain)</journal><volume/><journalNumber/><paginationStart>1</paginationStart><paginationEnd>25</paginationEnd><publisher>IEEE</publisher><placeOfPublication/><isbnPrint>978-1-6654-5260-1</isbnPrint><isbnElectronic>978-1-6654-5198-7</isbnElectronic><issnPrint/><issnElectronic/><keywords>Blockchain, Cryptocurrency, Bitcoin, Agda, Verification, Hoare logic, BitcoinScript, P2PKH, P2MS, Access control, Weakest precondition, Predicate transformer semantics,Provable correctness, Symbolic execution, Smart contracts</keywords><publishedDay>7</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2022</publishedYear><publishedDate>2022-11-07</publishedDate><doi>10.1109/igetblockchain56591.2022.10087054</doi><url>http://dx.doi.org/10.1109/igetblockchain56591.2022.10087054</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2023-09-01T12:16:36.0264663</lastEdited><Created>2022-10-23T20:07:25.9955320</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>Bogdan</firstname><surname>Lazar</surname><order>2</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>3</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling v2 61633 2022-10-23 Verifying Correctness of Smart Contracts with Conditionals 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2022-10-23 SCS In this paper, we specify and verify the correctness of programs written in Bitcoin's smart contract Script in the interactive theorem prover Agda. As in the previous article [1] we use weakest preconditions of Hoare Logic to specify the security property of access control, and show how to develop human-readable specifications.In this article, we include conditionals into the language. For the operational semantics we use an additional stack, the ifstack, to deal with nested conditionals. This avoids the addition of extra jump instructions, which are usually used for the operational semantics of with conditionals in Forth-style stack languages. The ifstack preserves the original nesting of conditionals, and we determine an ifthenselse-theorem which allows to derive verification conditions of conditionals by referring to conditions for the if- and else-case. Conference Paper/Proceeding/Abstract 2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain &amp; Beyond (iGETblockchain) 1 25 IEEE 978-1-6654-5260-1 978-1-6654-5198-7 Blockchain, Cryptocurrency, Bitcoin, Agda, Verification, Hoare logic, BitcoinScript, P2PKH, P2MS, Access control, Weakest precondition, Predicate transformer semantics,Provable correctness, Symbolic execution, Smart contracts 7 11 2022 2022-11-07 10.1109/igetblockchain56591.2022.10087054 http://dx.doi.org/10.1109/igetblockchain56591.2022.10087054 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2023-09-01T12:16:36.0264663 2022-10-23T20:07:25.9955320 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Fahad Alhabardi 1 Bogdan Lazar 2 Anton Setzer 0000-0001-5322-6060 3
title Verifying Correctness of Smart Contracts with Conditionals
spellingShingle Verifying Correctness of Smart Contracts with Conditionals
Anton Setzer
title_short Verifying Correctness of Smart Contracts with Conditionals
title_full Verifying Correctness of Smart Contracts with Conditionals
title_fullStr Verifying Correctness of Smart Contracts with Conditionals
title_full_unstemmed Verifying Correctness of Smart Contracts with Conditionals
title_sort Verifying Correctness of Smart Contracts with Conditionals
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Fahad Alhabardi
Bogdan Lazar
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title 2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain &amp; Beyond (iGETblockchain)
container_start_page 1
publishDate 2022
institution Swansea University
isbn 978-1-6654-5260-1
978-1-6654-5198-7
doi_str_mv 10.1109/igetblockchain56591.2022.10087054
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
url http://dx.doi.org/10.1109/igetblockchain56591.2022.10087054
document_store_str 0
active_str 0
description In this paper, we specify and verify the correctness of programs written in Bitcoin's smart contract Script in the interactive theorem prover Agda. As in the previous article [1] we use weakest preconditions of Hoare Logic to specify the security property of access control, and show how to develop human-readable specifications.In this article, we include conditionals into the language. For the operational semantics we use an additional stack, the ifstack, to deal with nested conditionals. This avoids the addition of extra jump instructions, which are usually used for the operational semantics of with conditionals in Forth-style stack languages. The ifstack preserves the original nesting of conditionals, and we determine an ifthenselse-theorem which allows to derive verification conditions of conditionals by referring to conditions for the if- and else-case.
published_date 2022-11-07T12:18:08Z
_version_ 1775833803142463488
score 11.013731

Similar Items