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

TC：小型：分布式应用程序中客户端行为的服务器端验证

• 批准号: 1115948
• 负责人: Michael Reiter
• 金额: $ 47.25万
• 依托单位: University of North Carolina at Chapel Hill
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1115948&HistoricalAwards=false
• 关键词: TC; Small; Server; side; Verification

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.

这项研究将开发技术，使服务器能够验证客户与批准的客户软件一致的客户的行为。 客户的行为可能会偏离被认可的客户端软件，这是由于客户软件或其数据结构的对手，可以通过物理访问对客户端计算机或感染客户端的恶意软件。 这种操作可能会在客户处产生不正确的状态；示例可能包括对不可能的协作应用程序中共享状态的修改，或者对迫在眉睫的服务器端调用的输入，其中包含批准的客户端软件不允许使用的内容。 如果此状态在较大的分布式应用程序中具有权威性或对服务器或其他客户端的危险，则此不正确状态可能会损害应用程序的完整性。 在这项拟议的工作中开发的技术将检测由这种修改引起的客户行为，或者更具体地说，更具体地说，与批准的客户端软件不一致的任何客户对服务器消息。验证客户端行为的核心挑战是，此行为是客户处理与服务器潜在未知的输入的结果。 这些未知的输入可以包括客户端的环境输入（例如，在客户端位置感知的值），用户输入（例如，用户的键击），甚至在发送验证的消息时，客户端也处理了哪些服务器消息。 为了允许验证，尽管有这一障碍，该项目将调查使用批准的客户端软件和约束求解的符号执行，以使服务器能够确定是否有任何输入可以引起此客户端消息。 如果发现没有输入可以引起此消息，那么它将检测到客户行为与批准的客户端软件不一致。 该项目将产生新的研究结果和工具，以使该分析有效地执行。 此外，将计算机游戏用作展示这项研究的一种工具，这使该项目非常适合向高中生和本科生推广，这些项目非常受欢迎。