NSF WATCH TALK - Server-Side Verification of Client Behavior
The next WATCH talk, called Server-Side Verification of Client Behavior, from Michael Reiterat the University of North Carolina at Chapel Hill is Thursday, February 15th, from 12PM -1PM.
The talk will be held in the new National Science Foundation building (Room 3430) at 2415 Eisenhower Ave. in Alexandria, VA 22314. The new security requirements require that everyone who enters the building have an entry badge, so please send an email to Cassandra Queen at cqueen@nsf.gov if you plan to attend.
Michael Reiter is the Lawrence M. Slifkin Distinguished Professor in the Department of Computer Science at UNC Chapel Hill. His research interests include all areas of computer and communications security, distributed computing, and networking. His professional responsibilities during his career so far have included Director of Secure Systems Research at Bell Labs; founding Technical Director of CyLab at Carnegie Mellon University; program chair for the flagship computer security conferences of the IEEE, the ACM, and the Internet Society; and Editor-in-Chief of ACM Transactions on Information and System Security, among others. Dr. Reiter was named an ACM Fellow in 2008 and an IEEE Fellow in 2014, and he received the ACM SIGSAC Outstanding Contributions Award in 2016.
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 talk, we summarize our research on a method for verifying the consistency of a client's messaging behavior with the program it is believed to be running, without knowing all of the client-side inputs driving its behavior. We then turn our attention specifically to cryptographic protocols, which present unique challenges to our method of behavioral verification. The toolchain we have constructed 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.
