Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a smart contract is difficult, which complicates development, auditing, and the post-mortem analysis of attacks.
A new paper presents the first specification mining technique for smart contracts. Our technique extracts the possible behaviors of smart contracts from contract executions recorded on a blockchain and expresses them as finite automata. A novel dependency analysis
allows us to separate independent interactions with a contract. The technique tunes the abstractions for the automata construction automatically based on configurable metrics, for instance, to maximize readability or precision. They implemented their technique for the Ethereum blockchain and evaluated its usability on several real-world contracts.
Smart contracts are programs that store and automatically move digital assets according to specified rules. While this idea was proposed over 20 years ago, it only gained traction when it was combined with blockchain technology to store an immutable record of all contract executions. Smart contracts have a wide range of applications, including fundraising, securities trading and settlement, supply-chain management, and electricity sourcing.
Despite their conceptual simplicity, understanding how to correctly interact with a smart contract is often challenging, not only for developers but also auditors. Specifically, legal invocations of contract operations typically need to satisfy implicit temporal ordering constraints, such as bidding only before an auction has ended. As an additional complication, contract executions may have subtle interactions (similar to data races) with each other when accessing the same state, especially since the smart-contract execution model provides no scheduling guarantees.
Specification mining has been shown to help software engineers understand behaviors of complex systems. This is the first application of specification mining to smart contracts. Our technique can be used to understand a contract of interest and its interactions with users and other smart contracts.
They mine these specifications from contract executions recorded on a blockchain and express them as finite automata, describing the observed sequences of interactions with the contract.
The automata produced by our technique not only characterize the protocol (API) for using a contract, but also shed light on temporal dependencies between different contract invocations that access the same state. This is useful for understanding the functionality of a smart contract, for debugging it, or even for a post-mortem analysis of an attack.
A bug in the Parity wallet allowed a function for setting the wallet owner to be called by anyone, even after the wallet was constructed. As a result, attackers managed to claim existing wallets by setting themselves as owners. In an automaton generated by our technique, the contract invocation for updating the wallet owner would appear as a transition that may be taken even after the wallet construction, which would help developers understand the attack.
The new approach goes beyond existing specification mining techniques for classical execution environments in two major ways.
1. most techniques target interactions of sequential clients with a data structure. In contrast, on a blockchain it is common that multiple clients interleave their interactions with a contract. To obtain precise specifications, our approach uses a novel dependency analysis to separate independent interactions with a contract and extract self-contained sequential traces from the blockchain.
2. existing mining techniques use fixed, built-in abstractions to extract automata from sets of traces, e.g., by only considering method signatures. To support a wide range of use cases, our approach automatically adjusts its abstractions to maximize configurable metrics. These metrics can, for instance, favor coarse abstractions to obtain simple automata that are easy to grasp by a contract client, or precise abstractions to facilitate accurate understanding by a human auditor.
They presented the first specification mining technique for smart contracts. Our precise specifications provide important insights into the functionality and interactions between smart contracts, and are useful to develop, understand, and audit smart contracts. The new technique gives users the flexibility to adjust the generated automata based on their needs during specific usage scenarios. They achieve this by phrasing the problem of finding useful abstractions for automaton construction as an optimization problem with user-adjustable costs.
As future work, they plan to to identify common design patterns and evolve the language design of smart contracts. They also plan to apply the idea of cost-guided abstraction tuning to other forms of program analysis, such as heap analyses, invariant inference, and process mining.