Verifying Correctness of Smart Contracts with Conditionals

Fahad Alhabardi, Bogdan Lazar, Anton Setzer

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

2 Citations (SciVal)

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

Original languageEnglish
Title of host publication2022 IEEE 1st Global Emerging Technology Blockchain Forum
Subtitle of host publicationBlockchain and Beyond, iGETblockchain 2022
PublisherIEEE
ISBN (Electronic)9781665451987
ISBN (Print)9781665452601
DOIs
Publication statusPublished - 11 Nov 2022
Externally publishedYes
Event1st IEEE Global Emerging Technology Blockchain Forum: Blockchain and Beyond, iGETblockchain 2022 - Irvine, USA United States
Duration: 7 Nov 202211 Nov 2022

Publication series

Name2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain and Beyond, iGETblockchain 2022

Conference

Conference1st IEEE Global Emerging Technology Blockchain Forum: Blockchain and Beyond, iGETblockchain 2022
Country/TerritoryUSA United States
CityIrvine
Period7/11/2211/11/22

Keywords

  • access control
  • Agda
  • Bitcoin
  • Bitcoin script
  • blockchain control flow
  • cryptocurrency
  • Hoare logic
  • operational semantics
  • security
  • smart contracts
  • weakest precondition

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Information Systems
  • Information Systems and Management
  • Health Informatics

Fingerprint

Dive into the research topics of 'Verifying Correctness of Smart Contracts with Conditionals'. Together they form a unique fingerprint.

Cite this