Analysis and Automated Discovery of Attacks in Transport Protocols

Transport protocols like TCP and QUIC are a crucial component of today’s Internet, underlying services as diverse as email, file transfer, web browsing, video conferencing, and instant messaging as well as infrastructure protocols like BGP and secure network protocols like TLS. Transport protocols provide a variety of important guarantees like reliability, in-order delivery, and congestion control to applications. As a result, the design and implementation of transport protocols is complex, with many components, special cases, interacting features, and efficiency considerations, leading to a high probability of bugs. Unfortunately, today the testing of transport protocols is mainly a manual, ad-hoc process. This lack of systematic testing has resulted in a steady stream of attacks compromising the availability, performance, or security of transport protocols, as seen in the literature. Given the importance of these protocols, we believe that there is a need for the development of automated systems to identify complex attacks in implementations of these protocols and for a better understanding of the types of attacks that will be faced by next generation transport protocols. In this dissertation, we focus on improving this situation, and the security of transport protocols, in three ways. First, we develop a system to automatically search for attacks that target the availability or performance of protocol connections on real transport protocol implementations. Second, we implement a model-based system to search for attacks against implementations of TCP congestion control. Finally, we examine QUIC, Google’s next generation encrypted transport protocol, and identify attacks on availability and performance