Analyzing Protocol Implementations for Interoperability
12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2015), Oakland, CA, May 4-6, 2015.
Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, Todd Millstein
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
non-interoperabilities 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.
[PDF]