Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

Smart Contracts: Application Scenarios for Deductive Program Verification

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Jonas Schiffl, and Mattias Ulbrich
In:1st Workshop on Formal Methods for Blockchains (FMBC 2019) hosted by the 3rd Formal Methods World Congress (FM’19)
Year:2019
Links:

Abstract

Smart contracts are programs that run on a distributed ledger platform. They usually manage resources representing valuable assets. Moreover, their source code is visible to potential attackers, they are distributed, and bugs are hard to fix. Thus, they are susceptible to attacks exploiting programming errors. Their vulnerability makes a rigorous formal analysis of the functional correctness of smart contracts highly desirable. In this short paper, we show that the architecture of smart contract platforms offers a computation model for smart contracts that yields itself naturally to deductive program verification. We discuss different classes of correctness properties of distributed ledger applications, and show that design-by-contract verification tools are suitable to prove these properties. We present experiments where we apply the KeY verification tool to smart contracts in the Hyperledger Fabric framework which are implemented in Java and specified using the Java Modeling Language.

BibTeX

@inproceedings{schiffl_smart_2019,
    title     = {Smart Contracts: Application Scenarios for Deductive Program Verification},
    author    = {Bernhard Beckert and Jonas Schiffl and Mattias Ulbrich},
    editor    = {Bruno Bernardo and N\'{e}stor Cata\~{n}o and Diego Marmsoler},
    booktitle = {1st Workshop on Formal Methods for Blockchains ({FMBC} 2019)
                 hosted by the 3rd Formal Methods World Congress ({FM}’19)},
    month     = oct,
    year      = {2019},
    abstract  = {Smart contracts are programs that run on a distributed ledger platform.		
                 They usually manage resources representing valuable
                 assets. Moreover, their source code is visible to potential
                 attackers, they are distributed, and bugs are hard to
                 fix. Thus, they are susceptible to attacks exploiting programming errors.
                 Their vulnerability makes a rigorous formal analysis of the functional
                 correctness of smart contracts highly desirable.

                 In this short paper, we show that the architecture of smart
                 contract platforms offers a computation model for smart
                 contracts that yields itself naturally to deductive program
                 verification. We discuss different classes of correctness
                 properties of distributed ledger applications, and show that
                 design-by-contract verification tools are suitable to prove
                 these properties. We present experiments where we apply the
                 \KeY verification tool to smart contracts in the Hyperledger
                 Fabric framework which are implemented in Java and 
                 specified using the Java Modeling Language.},
    place     = {Porto, Portugal},
    date      = {October 11}
}