Analyzing Protocol Implementations for Interoperability
Luis Pedrosa, University of Southern California; Ari Fogel, University of California, Los Angeles; Nupur Kothari, Microsoft; Ramesh Govindan, University of Southern California; Ratul Mahajan, Microsoft; Todd Millstein, University of California, Los Angeles
We propose PIC, a tool that helps developers search for non-interoperabilities in protocol implementations. We formulate this problem using intersection of the sets of messages that one protocol participant can send but another will reject as non-compliant. PIC leverages symbolic execution to characterize these sets and uses two novel techniques to scale to real-world implementations. First, it uses joint symbolic execution, in which receiver-side program analysis is constrained based on sender-side constraints, dramatically reducing the number of execution paths to consider. Second, it incorporates a search strategy that steers symbolic execution toward likely non-interoperabilities. We show that PIC is able to find multiple previously unknown noninteroperabilities in large and mature implementations of the SIP and SPDY (v2 through v3.1) protocols, some of which have since been fixed by the respective developers.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
author = {Luis Pedrosa and Ari Fogel and Nupur Kothari and Ramesh Govindan and Ratul Mahajan and Todd Millstein},
title = {Analyzing Protocol Implementations for Interoperability},
booktitle = {12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15)},
year = {2015},
isbn = {978-1-931971-218},
address = {Oakland, CA},
pages = {485--498},
url = {https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/pedrosa},
publisher = {USENIX Association},
month = may
}