Category
Smart Contract Fairness
Abstract & Info
Smart contracts are computer programs allowing users to define and execute transactions automatically on top of the blockchain platform. Many of such smart contracts can be viewed as games. A game-like contract accepts inputs from multiple participants, and upon ending, automatically derives an outcome while distributing assets according to some predefined rules. Without clear under- standing of the game rules, participants may suffer from fraudulent advertisements and financial losses. In this paper, we present a framework to perform (semi-)automated verification of smart con- tract fairness, whose results can be used to refute false claims with concrete examples or certify contract implementations with respect to desired fairness properties. We implement FairCon, which is able to check fairness properties including truthfulness, efficiency, optimality, and collusion-freeness for Ethereum smart contracts. We evaluate FairCon on a set of real-world benchmarks and the experiment result indicates that FairCon is effective in detecting property violations and able to prove fairness for common types of contracts.
Link: https://dl.acm.org/doi/abs/10.1145/3368089.3409740
Arthur: Ye Liu, Yi Li, Shang-Wei Lin, Rong Zhao, Nanyang Technological University
Time: 2020
Publish: ESEC/FSE 2020: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Summary
- The paper proposes a framework called FairCon to verify fairness properties of smart contracts. Smart contracts are viewed as games/mechanisms involving multiple participants.
- Fairness properties checked include truthfulness, efficiency, optimality, and collusion-freeness. These are well-studied properties in game theory and mechanism design.
- The key challenge is translating arbitrary smart contract code into standard mechanism models to enable fairness checking. The paper introduces an intermediate representation specific for auction and voting contracts.
- Users provide annotations on the source code to help identify key components like bidders and bids. Symbolic execution is used to extract symbolic expressions for the allocation and pricing rules.
- Bounded model checking is done by encoding the mechanism model and properties in SMT. Unbounded proofs rely on user-provided loop invariants and program verification tools.
- The FairCon framework is implemented and evaluated on 17 real-world Ethereum contracts. It effectively detects fairness violations and is able to prove properties for common contract types.
Thoughts
- This technique and framework can be utilized to verify not only auction contracts, but more types of contracts. Many contracts actually focus on a few specific types, such as erc20, erc721, erc1155, etc. These types of contracts have relatively high degrees of standard paradigms, so the framework can be further expanded.
- In addition to fairness verification, more verifications can be performed, such as whether users care about whether it is a risky contract, whether there is arbitrary restriction on buying and selling rights, etc.
- Automated reasoning about fairness can inspire new techniques to analyze complex socio-technical systems with security implications, such as social media algorithms.