Engineering Science and Technology, an International Journal (Dec 2024)
Belief game: Verifying smart contract functionality in player dynamic interactions
Abstract
Smart contracts, being security-critical code, facilitate consensus among players and ensure secure and accurate value transfer, and formal verification is necessary to guarantee functional correctness of contracts. Game theory serves as one of the tools in formal verification by assessing whether the outcomes of contract executions meet the expected goals. While most studies employing game theory to verify smart contract functionality assume rational players, in practice, players may invoke and deploy smart contracts involving irrational behavior, casting doubt on the correctness of verification results. The aim of this study is to propose an alternative game model to verify smart contract functionality in dynamic player interactions where irrational behavior is involved. Specifically, a belief-based smart contract execution game (BSC-game) model was introduced, utilizing belief – the probability that a player believes in the irrationality of others – to capture how the irrational behavior of others affects a player’s contract execution decisions. Reasonable economic incentives were introduced to encourage honest behavior of players. Moreover, a computationally feasible method was designed to update players’ beliefs in large-scale dynamic smart contract executions. Theoretical analysis discloses the existence of equilibrium in the BSC-game, as well as the conditions for the number of faulty players within the system’s fault tolerance. We conducted the simulation experiments, and verified the business-oriented smart contract written in G language by the BSC-game model. The results further indicate that although players’ beliefs impact their decisions to execute contracts, reasonable economic incentives can motivate players to execute contracts honestly. This ensures that smart contract functionality aligns with expected goals, showing that the BSC-game model can verify and guarantee the correctness of contract functions. This new approach significantly contributes to bolstering smart contract security and credibility, positively influencing blockchain stability.
