by Thomas Osterland and Thomas Rose (Fraunhofer FIT)
Smart contracts are a proposed mechanism to help maintain consistency among data and transactions. They are automatically triggered by the conduct of a transaction and they also function to safeguard transaction histories. A cascade of automatically initiated smart contracts could result in data errors and smart contracts interfering with one another, but correctness can be assured by means of model checking.
Blockchain technology was initially introduced as a transaction management technology that transfers centralised control to a distributed environment with new means of consistency enforcement [1]. Platforms with smart contracts extend the original blockchain protocol by a process automation to proactively maintain consistency among data, and in particular transactions, by enabling a full automation of agreements and the autonomous adherence of these agreements [2].
An appealing use-case of smart contracts is the documentation and clearing of micro-payments between parties in smart grid environments - for example, among members of a community that share a renewable energy network and e-mobility-oriented consumers. A variety of different small plants homogeneously distributed over the grid produces, controls and invoices the energy flow, in contrast to traditional electrical plants in large-scale grids that operate in a centralised fashion. All activities by entities in the grid can be managed as well as safeguarded by a smart contract.
Figure 1: Chances and challenges of smart contracts.
The major benefit of using blockchain-enabled smart contracts for such grids is that participation on the network is permissionless and self-regulating. Someone who erects a wind turbine in their garden can directly participate in the global energy supply, independent from central trusted intermediaries. Blockchain technology allows the coequal participation of different parties on the smart grid without the requirement that they trust each other. Small contributions from individuals will be negotiated in the same way as large contributions by industrial companies. Smart contracts thus allow the elimination of intermediaries both in topological regard - for instance, large suppliers of electricity are replaced by individual smart contracts, and in regard to function - for instance, tasks like bookkeeping and payment are handled by smart contracts. In addition, a blockchain provides 100% up-time and its decentralised nature protects against catastrophes and acts of terrorism.
While the protected execution of smart contracts is ensured by the blockchain protocol, there is no approach that ensures the correctness of the rules encoded in the smart contract.
As a consequence, the correctness of a smart contract must be ensured in advance, before formal instantiation in a blockchain. This is certainly important for developers, as well as suppliers and consumers that rely on the soundness of a smart contract. Moreover, it furnishes a source of trust for users because trust is maintained by algorithmic concepts. When proving the correctness of smart contracts, a model of the actual correct behaviour of a contract is necessary in first place. Determining whether a contract reacts correctly is not always as trivial as it seems, and proving it (automatically) means that the behaviour must be defined as conditions in a formal notation, for instance (temporal) first order logics.
The process of testing whether a given system satisfies these formally introduced conditions is called formal verification. In the example of the limited selling price a corresponding condition ensures that the selling price depends on the movements of the energy market and that it is not limited to a certain range.
One approach with a high degree of industry acceptance is model checking [3]. The idea is to analyse the state space of a program. A program state is the valuation of every variable of a program for a given execution step. Running a program means executing the program instructions consecutively and every instruction changes the storage and thus alters the program state. Certain (forbidden) states in the graph represent situations that contradict the desired behaviour of the contract. For instance, in the smart grid example, every state from which we cannot reach a state in which the selling price exceeds a specified limit. Model checking can then confirm whether forbidden states are reachable. Besides the checking of forbidden behavior, model checking can also test liveness properties, that describe desired behavior that must eventually occur.
To-reiterate, smart contracts certainly provide a powerful functional surplus for maintaining the consistency of transactions in applications governed by blockchain technology. However, the intended level of automation might cause cascading effects that have to be checked by formal methods of algorithmic proof. Model checking appears as a favourite candidate because of its balance among expressiveness of conditions to be verified and computational complexity for verification. In case of erroneous contracts, it provides counterexamples that support debugging and its application does not require expert knowledge.
References:
[1] J. McKeogh, R. Cheong. “Consensus: Immutable agreement for the internet of value,” in KPMG, 2016
[2] S. Underwood. “Blockchain beyond bitcoin,” in Commun. ACM 59, 2016, pp 15-17.
[3] K. Havelund , T. Pressburger. “Model Checking Java Programs Using Java PathFinder,” in T.STTT (2000) 2:366, 2000, pp 366-381.
Please contact:
Thomas Rose, Thomas Osterland
Fraunhofer FIT, Germany
+49 2241 14 2798, +49 2241 14 3618,
