Formal Verification of FlowSync

Abstract

Complex network layouts, currently used by internet service providers and large corporate networks, have lead to a phenomenon known as asymmetric routing. That is, the two directions of a traffic flow take different paths through the network. This poses a challenge for network management systems, which typically require knowledge of both directions of traffic to perform classification and statistics collection. In this thesis, we apply formal methods to identify and suggest solutions to issues in such a system. The system is called FlowSync, and has been developed at Sandvine for use in its internet traffic management product. The latter is an international company providing systems for classifying and managing internet traffic. We model three distinct components of FlowSync; classifier sharing, statistics synchronization and link redundancy, and identify potential issues and limitations in all three. Two of these limitations are consequences of known problems in distributed system design, and the relation to these problems is discussed, as well as known techniques for working around them.