Hunting for Bugs in Source Code of Video and Computer Games

我们研究的目的是开发工具来检测视频和电脑游戏中的漏洞。我们不是将众所周知的技术应用到游戏中，而是专注于在游戏中寻找错误时遇到的基本问题。我们预期的解决方案不仅将影响游戏行业，还将影响其他应用领域和学术界。 测试是检测错误的最常用方法。它对于确定性代码特别有效，即，对于固定输入导致单次执行的代码。然而，在存在不确定性的情况下，即当有不同的潜在处决时，测试就不那么有效了。多次运行测试并不能保证检查过不同的执行。此外，如果发现了错误，可能很难重现。因此，要检测不确定代码中的错误，需要补充测试的方法。 模型检查是测试的替代方案。模型检查尝试系统地检查所有可能的执行，而不是像在测试中所做的那样检查单个执行。但是，潜在执行的数量可能与代码中的不确定性选择数量成指数关系。处理如此巨大数量的死刑的根本问题被称为状态空间爆炸问题。 随机化和并发性是当今游戏的关键因素，两者都导致了非决定论。因此，模型检查似乎是寻找游戏中错误的测试的一个可行的替代方案。虽然已经开发了许多模型检查器，但我们还不知道有什么可以验证游戏源代码的属性。我们的总体目标是开发第一个这样的模型检查器。我们的主要目标是打击由随机性和并发性相结合而引起的臭名昭著的状态空间爆炸。 我们关注的是直接与源代码一起工作的模型检查器。我们最初只关注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.