Server-side verification of client behavior in cryptographic protocols

TL;DR

This paper presents a practical, non-intrusive method for verifying that a cryptographic client’s messaging behavior aligns with its expected program, using symbolic execution and multi-path exploration to detect malicious activity like Heartbleed exploits.

Contribution

It introduces a novel client verification toolchain that explores multiple execution paths concurrently without modifying the client or knowing all inputs, applicable to cryptographic and other client applications.

Findings

Can detect Heartbleed exploits within seconds of malicious packets

Verifies legitimate clients at scale, matching Gmail workloads

Operates without client modifications or prior knowledge of inputs

Abstract

Numerous exploits of client-server protocols and applications involve modifying clients to behave in ways that untampered clients would not, such as crafting malicious packets. In this paper, we demonstrate practical verification of a cryptographic protocol client's messaging behavior as being consistent with the client program it is believed to be running. Moreover, we accomplish this without modifying the client in any way, and without knowing all of the client-side inputs driving its behavior. Our toolchain for verifying a client's messages explores multiple candidate execution paths in the client concurrently, an innovation that we show is both specifically useful for cryptographic protocol clients and more generally useful for client applications of other types, as well. In addition, our toolchain includes a novel approach to symbolically executing the client software in multiple passes that defers expensive functions until their inputs can be inferred and concretized. We demonstrate client verification on OpenSSL to show that, e.g., Heartbleed exploits can be detected without Heartbleed-specific filtering and within seconds of the first malicious packet, and that verification of legitimate clients can keep pace with, e.g., Gmail workloads.