A lightweight approach to smart contracts supporting safety, security, and privacy

The concept of smart contract represents one of the most attractive uses of blockchain technology and has the advantage of being transparent, immutable, and corruption-free. However, blockchain is a highly resource demanding technology. The ambition of this paper is to propose a new approach for defining lightweight smart contracts, offering a high level of trust even without blockchain, when the underlying operating system can be trusted. Blockchain can be used for a higher degree of trust, for instance when the runtime system cannot be trusted. The approach gives transparency and immutability, and gives protection against corrupted or incorrect smart contract implementations. This is achieved by letting smart contract requirement specifications be separated from the smart contract implementations, provided by special objects, so-called history objects, recording all transactions of the associated contract. The history objects are generated by the runtime system as specially protected objects. Contract partners may interact with the history objects through predefined interfaces. We present a framework which includes an executable, imperative language for writing smart contracts, a functional language for contract specifications by means of invariants over the transaction history of a contract, as well as a verification system. The framework allows compositional and class-wise verification. A history object can provide runtime checking of specified behavioral properties of the contract, and can provide safety, security, and privacy control, as well as trusted transfer of assets. We demonstrate the approach on an auction system. (c) 2022 Elsevier Inc. All rights reserved.