Conference Paper/Proceeding/Abstract 744 views
Verifying Correctness of Smart Contracts with Conditionals
2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain & Beyond (iGETblockchain), Pages: 1 - 25
Swansea University Author:
Anton Setzer
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...
| 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 |