• Verification of smart contract...

Treffer: Verification of smart contract business logic : exploiting a Java source code verifier

Title:
Verification of smart contract business logic : exploiting a Java source code verifier
Authors:
Ahrendt, Wolfgang, Bubel, Richard, Ellul, Joshua, Pace, Gordon J., Pardo, Raul, Rebiscoul, Vincent, Schneider, Gerardo, 8th International Conference, FSEN 2019
Publisher Information:
Springer International Publishing
Publication Year:
2019
Collection:
University of Malta: OAR@UM / L-Università ta' Malta
Subject Terms:
Blockchains (Databases), Smart contracts -- Technological innovations, Application software, Computer software -- Development, Java (Computer program language)
Document Type:
Konferenz conference object
Language:
English
Relation:
https://www.um.edu.mt/library/oar/handle/123456789/136289
Availability:
https://www.um.edu.mt/library/oar/handle/123456789/136289
Rights:
info:eu-repo/semantics/restrictedAccess ; The copyright of this work belongs to the author(s)/publisher. The rights of this work are as defined by the appropriate Copyright Legislation or as modified by any successive legislation. Users may access this work and can make use of the information contained in accordance with the Copyright Legislation provided that the author must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the prior permission of the copyright holder.
Accession Number:
edsbas.E9E9899E
Database:
BASE

Weitere Informationen

Smart contracts have been argued to be a means of building trust between parties by providing a self-executing equivalent of legal contracts. And yet, code does not always perform what it was originally intended to do, which resulted in losses of millions of dollars. Static verification of smart contracts is thus a pressing need. This paper presents an approach to verifying smart contracts written in Solidity by automatically translating Solidity into Java and using KeY, a deductive Java verification tool. In particular, we solve the problem of rolling back the effects of aborted transactions by exploiting KeY’s native support of JavaCard transactions. We apply our approach to a smart contract which automates a casino system, and discuss how the approach addresses a number of known shortcomings of smart contract development in Solidity. ; peer-reviewed