Hunting for Bugs in Source Code of Video and Computer Games

我们研究的目的是开发工具来检测视频和电脑游戏中的漏洞。我们并没有将众所周知的技术应用到游戏中，而是专注于寻找游戏漏洞时所遇到的基本问题。我们预期的解决方案不仅会影响游戏行业，还会影响其他应用领域和学术界。测试是检测bug最常用的方法。它对确定性代码特别有效，即对于固定输入只执行一次的代码。然而，在存在不确定性的情况下，也就是说，当存在不同的潜在执行时，测试就不那么有效了。多次运行测试不能保证检查了不同的执行。此外，如果发现了bug，可能很难再复制。因此，要检测不确定代码中的bug，就需要补充测试的方法。模型检查是测试的另一种选择。与在测试中检查单个执行不同，模型检查试图系统地检查所有可能的执行。然而，潜在的执行次数可能与代码中不确定选择的数量呈指数关系。处理如此庞大数量的执行的基本问题被称为状态空间爆炸问题。随机性和并发性是当今游戏的关键元素，它们都会产生不确定性。因此，模型检查似乎是寻找游戏漏洞的可行选择。虽然已经开发了许多模型检查器，但我们还没有发现任何可以验证游戏源代码属性的模型检查器。我们的总体目标是开发第一个这样的模型检查器。我们的主要目标是对抗由随机化和并发性组合引起的臭名昭著的状态空间爆炸。我们关注的是直接处理源代码的模型检查器。我们最初只关注Java，它是目前最流行的编程语言。尽管c++在游戏中应用最为广泛，但许多游戏，特别是在线游戏，都是用Java编写的。例如，根据吉尼斯世界纪录，用Java实现的RuneScape是世界上最受欢迎的免费大型多人在线角色扮演游戏，拥有超过2亿的注册账户。游戏的Java代码包含原生调用，即调用用不同于Java的语言编写的代码。例如，与图形、网络和声音相关的呼叫通常是本地的。使用本机调用对Java代码进行模型检查通常需要对Java中的本机代码进行建模，这既耗时又容易出错。为了让我们的工具能够为游戏开发者所用，我们应该自动处理本地调用。这是我们的第二个主要目标。玩家通过电子游戏控制器、鼠标、键盘等与游戏互动。为了对游戏进行模型检查，我们需要结合玩家的模型。理想情况下，模型应该从游戏的源代码中自动构建，这样我们的工具就很容易被游戏开发者使用。我们的第三个目标是尽可能地自动化球员模型的生成。加拿大的视频和电脑游戏产业是世界上最大的产业之一。它每年为加拿大经济贡献近20亿美元。因为我们的工具能够让游戏开发者自动发现漏洞，所以它们能够提高游戏质量并提高游戏开发者的生产力。我们希望我们的研究结果也能影响其他应用领域和学术界。例如，在包含大量本机调用的Java工具包中实现的通信协议中查找错误的工具应该受益于我们处理本机调用的技术。

The aim of our research is to develop tools to detect bugs in video and computer games. Rather than applying well-known techniques to games, we focus on fundamental problems that are encountered when hunting for bugs in games. Our anticipated solutions will not only impact the game industry but also other application areas and academia. Testing is the most commonly used method to detect bugs. It is particularly effective for deterministic code, i.e., code that for a fixed input gives rise to a single execution. However, in the presence of nondeterminism, i.e., when there are different potential executions, testing is less effective. Running a test multiple times provides no guarantee that different executions have been checked. Also, if a bug has been found, it may be difficult to reproduce. Therefore, to detect bugs in nondeterministic code, methods that complement testing are needed. Model checking is an alternative to testing. Rather than checking a single execution, as is done in testing, model checking attempts to systematically check all potential executions. However, the number of potential executions can be exponential in the number of nondeterministic choices in the code. The fundamental problem of dealing with such a huge number of executions is known as the state space explosion problem. Randomization and concurrency, which are key ingredients of today’s games, both give rise to nondeterminism. Therefore, model checking seems a viable alternative to testing for finding bugs in games. Although numerous model checkers have been developed, we are not aware of any that can verify properties of the source code of games. Our overall aim is to develop the first such model checker. Our main objective is to combat the notorious state space explosion caused by a combination of randomization and concurrency. We focus on model checkers that work directly with the source code. We initially restrict our attention to Java, currently the most popular programming language. Although C++ is most widely used for games, many, in particular online games, are written in Java. For example, according to Guinness World Records, RuneScape, implemented in Java, is the world's most popular free massively multiplayer online role-playing game with more than 200 million registered accounts. The Java code of games contains native calls, i.e., calls which invoke code that is written in a language different from Java. For example, calls related to graphics, networking and sound are usually native. Model checking Java code with native calls usually involves modelling the native code in Java, which is time consuming and error-prone. To make our tools of use to game developers, native calls should be handled automatically. This is our second major objective. Players interact with a game by means of the video game controller, the mouse, the keyboard, etc. In order to model check a game, we need to incorporate a model of the players. Ideally, the models should be built automatically from the source code of the game, so that our tools are easy to use by game developers. Our third objective is to automate the generation of models of the players as much as possible. The Canadian video and computer game industry is among the largest in the world. It contributes almost two billion dollars per year to the Canadian economy. Since our tools will allow game developers to find bugs automatically, they will improve the quality of the games and increase the productivity of game developers. We expect our results to also impact other application areas and academia. For example, tools to find bugs in communication protocols implemented in Java toolkits, which contain numerous native calls, should benefit from our techniques to handle native calls.