Systematic analysis of network protocol implementations

2018-11-02As networked systems become more complex, and as interactions between distributed entities become more subtle, our ability to analyze such systems has fallen behind. Failing to keep up with the ever increasing amount of software interactions that these systems can potentially be subject to can lead to software glitches which, if unmitigated, can lead to costly and embarrassing outages and even data loss. It is clear the community needs better tools to analyze these systems and to better understand their behavior under varying circumstances. ❧ Towards this end we start by presenting one such analysis specifically tailored towards the problem of protocol interoperability: the Protocol Interoperability Checker or PIC. PIC uses symbolic execution to explore the space of messages used by a protocol sender and receiver to communicate. By finding messages the sender can generate but that the receiver subsequently determines to be invalid, PIC can find scenarios where interoperability breaks down. To scale such an analysis to real-world implementations we make several key novel contributions, including joint symbolic execution that constrains the receiver-side analysis based on results from the sender, and a custom form of directed symbolic execution, that guides the analysis towards meaningful results. On mature implementations of two protocols, PIC found thousands of instances of non-interoperabilities, across multiple message types and fault causes. Many of the issues have been acknowledged as undesirable by developers and some have already been fixed. ❧ We then move on to generalize our work on PIC to address two new challenges, handling arbitrary networked systems and checking more general correctness properties. By extending joint symbolic execution with concepts borrowed from model checking, we build a more general conversational analysis. Conversational analysis implements a detailed symbolic network model that supports communication with multiple messages between multiple parties, while also considering the effects of concurrency and message loss. In effect, we create a novel approach to exploring the outcomes of a distributed system while varying both its inputs and the underlying network dynamics. We show that conversational analysis is able to analyze Redis, a popular key-value store, and perform a bounded static verification of its master-slave handshake while also reproducing a complex known bug, as well as a nuanced injected fault. ❧ Finally, we address the challenge of checking more general correctness properties. By exporting our analysis capabilities as a set of operations in a toolkit we call the Systematic Protocol Analysis Framework or SPA, we allow users to ""script"" new analyses more flexibly. These scripts then produce direct value to developers, enabling, as we show, novel systematic analyses for interoperability, security, correctness, and reliability