Smart Contract Synthesis Modulo Hyperproperties

TL;DR

This paper introduces HyperTSL, an extension of temporal logic, enabling the synthesis of smart contracts that satisfy complex hyperproperties like symmetry and information flow policies, enhancing security guarantees.

Contribution

It presents HyperTSL, a novel logic for specifying hyperproperties, and a synthesis method ensuring smart contracts meet these advanced security requirements.

Findings

HyperTSL can specify complex hyperproperties of smart contracts.

A preprocessing step detects when hyperproperties reduce to simpler trace properties.

The synthesis approach refines contracts to satisfy HyperTSL specifications.

Abstract

Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transactions on the blockchain. A broad range of methods has been developed to ensure that a smart contract is functionally correct. However, smart contracts often additionally need to satisfy certain hyperproperties, such as symmetry, determinism, or an information flow policy. In this paper, we show how a synthesis method for smart contracts can ensure that the contract satisfies its desired hyperproperties. We build on top of a recently developed synthesis approach from specifications in the temporal logic TSL. We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software. As a preprocessing step, we show how to detect if a hyperproperty has an equivalent formulation as a (simpler) trace property. Finally, we describe how to refine a synthesized contract to adhere to its HyperTSL specification.