Toward Inline Verification of Client Behavior
Abstract
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 in the last two years for OpenSSL alone, including the high-profile Heartbleed vulnerability, which enabled a tampered SSL client to extract contents of server memory. To defend against such exploits, we propose a research program to design and implement a verifier for client behavior that precisely determines whether interactions with the client are consistent with the software it is believed to be executing. We propose numerous technical innovations over our prior work that will improve the verification performance for legitimate client behavior, as well as methods for transforming software to support rapid verification of its components. Through these innovations we seek to demonstrate precise verification in the context of various applications and protocols at a pace that permits it to be performed inline.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- May 05, 2017
- Source ID
- N000141712369
Entities
People
- Michael Reiter
Organizations
- Office of Naval Research
- United States Navy
- University of North Carolina