Verification of Smart Contracts using the Interactive Theorem Prover Agda

Thumbnail Image

Date

2024-07-25

Journal Title

Journal ISSN

Volume Title

Publisher

Swansea University

Abstract

The goal of this thesis is to verify smart contracts in Blockchain. In particular, we focus on smart contracts in Bitcoin and Solidity. In order to specify the correctness of smart contracts, we use weakest preconditions. For this, we develop a model of smart contracts in the interactive theorem prover and dependent type programming language Agda and prove the correctness of smart contracts in it. In the context of Bitcoin, our verification of Bitcoin scripts consists of non-conditional and conditional scripts. For Solidity, we refer to programs using object- oriented features of Solidity, such as calling of other contracts, full recursion, and the use of gas in order to guarantee termination while having a Turing-complete language. We have developed a simulator for Solidity-style smart contracts. As a main example, we executed a reentrancy attack in our model. We have verified smart contracts in Bitcoin and Solidity using weakest precondition in Agda. Furthermore, Agda, combined with the fact that it is a theorem prover and programming language, allows the writing of verified programs, where the verification takes place in the same language in which the program is written, avoiding the problem of translation from one language to another (with possible translation mistakes).

Description

Keywords

Access control, Security, Verification, Provable correctness, Weakest precondition, Precondition, Postcondition, Symbolic execution, Agda proof assistant, Solidity, theorem prover, Model of Solidity-style, Blockchain, Reentrancy attacks, Bitcoin, Ethereum, Interface, Simulator, Blockchain control flow, Operational semantics, Hoare logic, Bitcoin script, P2PKH, P2MS, Predicate transformer semantics, Smart contracts

Citation

Endorsement

Review

Supplemented By

Referenced By

Copyright owned by the Saudi Digital Library (SDL) © 2024