Formal Analysis of Smart Contracts: Applying the KeY System
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, w
- PDF / 528,289 Bytes
- 15 Pages / 439.37 x 666.142 pts Page_size
- 2 Downloads / 217 Views
3
Karlsruher Institut f¨ ur Technology, Karlsruhe, Germany {jonas.schiffl,beckert}@kit.edu 2 Chalmers Tekniska H¨ ogskola, Gothenburg, Sweden [email protected] Technische Universit¨ at Darmstadt, Darmstadt, Germany [email protected]
Abstract. 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.
1
Introduction
Smart contracts are programs that run on a blockchain infrastructure. They are a prime target for security attacks, because they usually manage resources representing valuable assets. Moreover, their source code is visible to potential attackers. Due to their distributed nature, bugs are hard to fix. Thus, they are susceptible to attacks exploiting programming errors. This makes rigorous formal analysis of smart contracts highly desirable. Even though the distributed applications that are implemented by smart contracts can be quite complex, individual contracts and their functions are small and simple enough to make formal analysis feasible. And – quite often – precise (informal) descriptions of their required properties are available. Smart contract are binding “contracts” (only) in the sense that they are immutable and are deterministically and automatically executed by the platform on which they run. They are (only) “smart” in the sense that they define and implement some non-trivial business logic or protocol for handling digital assets. But in the end, smart contracts are just computer programs representing a reactive system. They are amenable to formal analysis and program verification, and they are great use cases for the application of formal methods. c Springer Nature Switzerland AG 2020 W. Ahrendt et al. (Eds.): Deductive Software Verification, LNCS 12345, pp. 204–218, 2020. https://doi.org/10.1007/978-3-030-64354-6_8
Formal Analysis of Smart Contracts: Applying the KeY System
205
There are many different components at different levels in a smart contract platform which together produce a single, shared view of the state of a distributed system. That includes implementations of a blockchain data structure, network protocols, consensus protocols, cryptographic functionality, compilers and virtual machines supporting the smart contract programming language. In the following, we focus on formal verification of smart contracts themselves, as opposed to verifying the correctness of the underlying components. In this paper, we show that the arch
Data Loading...
