TC: Small: Server-side Verification of Client Behavior in Distributed Applications

这项研究将开发一些技术，使服务器能够验证与其通信的客户端的行为是否与受制裁的客户端软件一致。由于具有客户端计算机物理访问权限的对手或已感染客户端的恶意软件对客户端软件或其数据结构的操纵，客户端的行为可能偏离受制裁的客户端软件。这种操作可能在客户端产生不正确的状态；示例可能包括对协作应用中的共享状态的修改，该修改不应该是可能的，或者对即将到来的服务器端调用的输入，该服务器端调用包含被批准的客户端软件不允许的内容。如果该状态在较大的分布式应用程序中是权威的，或者对服务器或其他客户端是危险的，则这种不正确的状态可能会危及应用程序的完整性。在这项拟议的工作中开发的技术将检测由此类修改引起的客户端行为，更具体地说，任何与受制裁的客户端软件不一致的客户端到服务器消息。验证客户端行为的一个主要挑战是，此行为是客户端处理输入可能对服务器未知的结果。这些未知输入可以包括在客户端的环境输入(例如，在客户端位置感测到的值)、用户输入(例如，用户的击键)，甚至包括客户端在其发送被验证的消息的点处处理了哪些服务器消息。为了能够不顾这一障碍进行验证，该项目将调查批准的客户端软件的符号执行和约束求解的使用情况，以使服务器能够确定是否有任何可能引起该客户端消息的输入。如果它发现没有任何输入可能导致此消息，则它会检测到客户端行为与受制裁的客户端软件不一致。该项目将产生新的研究成果和工具，以使这种分析能够有效地进行。此外，使用电脑游戏作为一种工具来演示这项研究，使该项目成为推广到高中生和本科生的理想选择，因为电脑游戏在他们中非常受欢迎。

This research will develop techniques that enable a server to verify the behavior of a client with which it is communicating as being consistent with the sanctioned client software. A client's behavior might deviate from the sanctioned client software due to manipulation of the client software or its data structures by an adversary with physical access to the client computer or by malware that has infected the client. This manipulation may yield incorrect state at the client; examples might include modifications to shared state in a collaborative application that should not have been possible, or an input to an imminent server-side invocation containing content that the sanctioned client software would not have allowed. If this state is authoritative within a larger distributed application or otherwise dangerous to the server or other clients, then this incorrect state may compromise the integrity of the application. The techniques developed in this proposed work will detect client behaviors arising from such modifications or, more specifically, any client-to-server messages that are inconsistent with the sanctioned client software.A central challenge in validating client behavior is that this behavior is the result of client processing with inputs that are potentially unknown to the server. These unknown inputs can include environmental inputs at the client (e.g., values sensed at the client location), user inputs (e.g., the user's keystrokes), and even which server messages were processed by the client at the point at which it sent the message being verified. To permit verification despite this obstacle, this project will investigate the use of symbolic execution of the sanctioned client software and constraint solving to enable the server to determine whether there are any inputs that could have given rise to this client message. If it finds that no inputs could have given rise to this message, then it detects the client behavior as being inconsistent with the sanctioned client software. The project will produce new research results and tools to enable this analysis to be performed efficiently. Moreover, the use of computer games as one vehicle to demonstrate this research makes this project ideal for outreach to high-school students and undergraduates, with whom computer games are immensely popular.