No Cover Image

Conference Paper/Proceeding/Abstract 474 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.

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!
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.
Keywords: Blockchain, Cryptocurrency, Bitcoin, Agda, Verification, Hoare logic, BitcoinScript, P2PKH, P2MS, Access control, Weakest precondition, Predicate transformer semantics,Provable correctness, Symbolic execution, Smart contracts
College: Faculty of Science and Engineering
Start Page: 1
End Page: 25