We present a game semantics framework for open-world safety analysis of Ethereum smart contracts. We model the interaction between a contract and its environment as a two-player game between the contract and the environment, and prove up to gas model approximations soundness: every assertion violation found corresponds to a real execution; and completeness: every open-world execution is captured. To our knowledge, this provides the first formal open-world interaction semantics for Ethereum smart contracts with mathematical guarantees of soundness and completeness. We implement this framework in YulTracer, an assertion reachability tool for real-world Solidity contracts, built on Yul, the intermediate language of the Solidity compiler. YulTracer uses concrete execution and exhaustively explores game traces within user-specified bounds. We evaluate it on reentrancy benchmarks, where YulTracer achieves 100% recall and precision -- the only tool to do so from those we examined -- and on two large real-world exploits (the DAO and PredyPool), where it detects the known vulnerabilities and produces no false positives on fixed versions. To our knowledge, YulTracer is the first tool to achieve this level of precision on real-world contracts without false positives. We additionally demonstrate generality of the approach via the examination of access control benchmarks.

翻译：我们提出了一种用于以太坊智能合约开放世界安全性分析的博弈语义框架。我们将合约与其环境之间的交互建模为合约与环境的双人博弈，并证明了在Gas模型近似下的可靠性：每个发现的断言违反均对应实际执行；以及完备性：所有开放世界执行均能被捕获。据我们所知，这为以太坊智能合约提供了首个具备可靠性与完备性数学保证的开放世界交互语义。我们通过YulTracer工具实现该框架——一个基于Solidity编译器中间语言Yul构建的真实世界Solidity合约断言可达性分析工具。YulTracer采用具体执行方法，在用户指定边界内穷举搜索博弈轨迹。我们在重入攻击基准测试中评估YulTracer（该工具实现了100%的召回率与精确度——在所测试工具中唯一达到此性能），并在两个大型真实世界漏洞利用案例（The DAO与PredyPool）中，成功检测已知漏洞且对修复版本产生零误报。据我们所知，YulTracer是首个在真实世界合约上达到此精确度水平且无误报的工具。我们同时通过访问控制基准测试验证了该方法的通用性。