Specifying Framing Conditions for Smart Contracts

摘要

Smart contracts are programs which run in conjunction with distributed ledgers. They often manage valuable assets, but, like all programs, they contain errors which can be exploited by an attacker. This makes them are a prime target for formal methods. Many formal analysis methods require the contracts' program code to be annotated with formal specifications. In this paper, we propose an approach and a formalism to enrich specifications with frame conditions, i.e., a specification of what a smart contract function cannot resp. will not do. We discuss the storage models of two smart contract platforms, Ethereum and Hyperledger Fabric, and propose languages for specifying frame conditions for both of them, based on the theory of dynamic frames.