Formal Analysis of Smart Contracts: Applying the KeY System

Autor:	Jonas Schiffl, Richard Bubel, Bernhard Beckert, Wolfgang Ahrendt
Rok vydání:	2020
Předmět:	Correctness business.industry Computer science Computation Distributed ledger Key (cryptography) Software engineering business Formal methods Prime (order theory)
Zdroj:	Lecture Notes in Computer Science ISBN: 9783030643539 20 Years of KeY
Popis:	Smart contracts are programs running on decentralized, distributed ledger platforms. Rigorous formal analysis of these programs is highly desirable because they manage valuable assets and therefore are a prime target for security attacks. In this paper, we show that the computation model of smart contracts allows the application of formal methods designed for analysing single-threaded imperative programs. We discuss different classes of correctness properties and the formal methods that may be applied. Furthermore, we show how deductive program verification in particular can be used to prove correctness of smart contracts, and we discuss two approaches where we have applied the program verification tool KeY.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::7c4a749050f51242f5ac1c7d64cf26ca https://doi.org/10.1007/978-3-030-64354-6_8 Zobrazit plný text záznamu