Verifying Correctness of Smart Contracts with Conditionals

【Author】 Alhabardi, Fahad; Lazar, Bogdan; Setzer, Anton

【Source】2022 IEEE 1ST GLOBAL EMERGING TECHNOLOGY BLOCKCHAIN FORUM: BLOCKCHAIN & BEYOND, IGETBLOCKCHAIN

【影响因子】

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

【Keywords】Bitcoin; Bitcoin script; smart contracts; security; cryptocurrency; blockchain control flow; Agda; operational semantics; Hoare logic; weakest precondition; access control

【发表时间】2022

【收录时间】2023-06-25

【文献类型】实证数据

【主题类别】

区块链技术-核心技术-智能合约