Tampering with the software running in distributed applications is an ingredient in numerous abuses. In a client-server scenario where the client is malicious, these abuses can involve exploits on a server directly, or manipulation of application state for which the client is authoritative. Examples of the former include at least ten vulnerabilities since 2014 for OpenSSL, including the high-profile Heartbleed vulnerability that enabled a tampered SSL client to extract contents of server memory, and the vulnerability in the Windows implementation of the Server Message Block (SMB) protocol exploited by Wannacry in 2017. Examples of the latter are "invalid command" game cheats that permit the client greater powers in the game.
Since it is generally infeasible to anticipate all such abuses, in our work we are exploring a holistic approach to validating client behavior as consistent with a sanctioned client program. In this approach, a behavioral verifier monitors each client message as it is delivered to the server, to determine whether the sequence of messages received from the client so far is consistent with the program the client is believed to be running and the messages that the server has sent to the client. Performing this verification is challenging primarily because inputs or nondeterministic events at the client may be unknown to the verifier, and so intuitively, the verifier must solve for whether there exist inputs that could have driven the client software to send the messages it did. In general, this problem is undecidable.
Our work has broken new ground in showing that behavioral verification can often be accomplished for valid message traces in protocols of interest, at a speed that coarsely keeps pace with the protocol interactions. While definitively concluding that messages are invalid can take considerably longer, we prioritize speed in cases of valid message traces because (i) in most systems, valid message traces will be the common case, and (ii) minimizing verification cost for valid messages is a crucial step toward deploying behavioral verification as an inline defense (vs. an offline detector), as is eventually our goal.
The basic strategy of our verifier is to use symbolic execution to trace the client execution based on the messages received so far from the client (and the messages the server has sent to it). When the verifier, in tracing client execution, operates on a value that it does not know (a "symbolic" value), it considers all possibilities for that value (e.g., branching in both directions if a branch statement involves a symbolic variable) and records constraints on those symbolic values implied by the execution path taken. Upon an execution path reaching a message send point in the client software, the verifier reconciles the accumulated constraints on that execution path with the next message received from the client. If the path does not contradict the message, then the message is confirmed as being consistent with some valid client execution. To date, our research toward performing fast behavioral verification has focused on methods for parallelizing the search for such an execution path in the client; deferring client functions that would be prohibitively expensive to execute symbolically until their inputs could be inferred concretely based on client-message contents; and executing the "concrete" parts of candidate execution paths at speeds as close to native as possible.
D. Bethea, R. A. Cochran, and M. K. Reiter. Server-side verification of client behavior in online games. ACM Transactions on Information and System Security 14(4), December 2011. http://dx.doi.org/10.1145/2043628.2043633
R. A. Cochran and M. K. Reiter. Toward online verification of client behavior in distributed applications. In 20th ISOC Network and Distributed System Security Symposium, February 2013.
A. Chi, R. A. Cochran, M. Nesfield, M. K. Reiter, and C. Sturton. A system to verify the behavior of known cryptographic clients. In 14th USENIX Symposium on Networked Systems Design and Implementation, pages 177–195, March 2017.
A. Humphries, K. Cating-Subramanian, and M. K. Reiter. TASE: Reducing latency of symbolic execution with transactional memory. In 28th ISOC Network and Distributed System Security Symposium, February 2021. https://doi.org/10.14722/ndss.2021.24327
Please contact Prof. Reiter for further information.