Formal Foundations of Software Defined Networks

Rajeev Alur

Network Traffic Classification by Program Synthesis

Abstract

Writing classification rules to identify interesting network traffic is a time-consuming and error-prone task. Learning-based classification systems automatically extract such rules from positive and negative traffic examples. However, due to limitations in the representation of network traffic and the learning strategy, these systems lack both expressiveness to cover a range of applications and interpretability in fully describing the traffic’s structure at the session layer. We describe Sharingan system, which uses program synthesis techniques to generate network classification programs at the session layer. Sharingan accepts raw network traces as inputs and reports potential patterns of the target traffic in NetQRE, a domain specific language designed for specifying session-layer quantitative properties. We develop a range of novel optimizations that reduce the synthesis time for large and complex tasks to a matter of minutes. Our experiments show that Sharingan is able to correctly identify patterns from a diverse set of network traces and generates explainable outputs, while achieving accuracy comparable to state-of-the-art learning-based systems.

Joint work with Boon Thau Loo and Lei Shi

Bio

Rajeev Alur is Zisman Family Professor of Computer and Information Science at University of Pennsylvania. He obtained his bachelor's degree in computer science from IIT Kanpur in 1987 and PhD in computer science from Stanford University in 1991. Before joining Penn in 1997, he was with Computing Science Research Center at Bell Labs. His research is focused on formal methods for system design. He is a Fellow of the AAAS, a Fellow of the ACM, a Fellow of the IEEE, an Alfred P. Sloan Faculty Fellow, and a Simons Investigator. He was awarded the inaugural CAV (Computer-Aided Verification) award in 2008, ACM/IEEE Logic in Computer Science (LICS) Test-of-Time award in 2010, the inaugural Alonzo Church award by ACM SIGLOG / EATCS / EACSL / Kurt Goedel Society in 2016, Distinguished Alumnus Award by IIT Kanpur in 2017 for his work on timed automata. Prof. Alur has served as the chair of ACM SIGBED (Special Interest Group on Embedded Systems), the general chair of LICS, and the lead PI of the NSF Expeditions in Computing center ExCAPE (Expeditions in Computer Augmented Program Engineering). He is the author of the textbook Principles of Cyber-Physical Systems (MIT Press, 2015).

Katerina Argyraki

Network-function Verification without Verification Expertise

Abstract

Software middleboxes promise shorter development cycles and the flexibility to deploy network functionality on demand; but — like any piece of frequently updated software — they can suffer from bugs, unpredictable behavior, and security vulnerabilities. I will talk about Vigor, a software stack and toolchain for building software middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity. Vigor has three key features: network-function developers need no verification expertise, and the verification process does not require their assistance (push-button verification); the entire software stack is verified, down to the hardware (full-stack verification); and verification can be done in a pay-as-you-go manner, i.e., instead of investing upfront a lot of time in writing and verifying a complete specification, one can specify one-off properties in a few lines of Python and verify them without concern for the rest. I will also discuss how we are evolving this approach to enable performance—not only semantic—verification.

Bio

Katerina is an associate professor of computer science at EPFL, where she does research on network architecture and systems, with a particular interest in network transparency and neutrality. She received an IRTF applied networking research prize (2020) and Best Paper awards at SOSP (2009) and NSDI (2014), all shared with her students and co-authors. She has been honored with the EuroSys Jochen Liedtke Young Researcher Award (2016) and three teaching awards at EPFL. Prior to EPFL, she was an early employee at Arista Networks, and received her PhD from Stanford (2007).

Ryan Beckett

Engineering Network Verification at Scale in Azure

Abstract

This talk will describe our experiences from deploying services that leverage formal methods to assure the availability and safety of the Azure network. The first part of the talk will showcase the Network Change Verification Service (NCVS), which protects changes to Azure's physical datacenter networks. NCVS combines scalable and proactive simulation, emulation, and verification together with a rich specification language for describing network intent. The second part of the talk will elaborate on ongoing efforts to verify the correctness of Azure's virtual networks. This part of the talk will present ZenGuru, a tool and intermediate language for modeling and verifying connectivity between virtual network resources.

Bio

Ryan Beckett is a researcher at Microsoft working in the area of network reliability. He graduated with his PhD from Princeton in 2018 after working with his advisor David Walker. While a graduate student, Ryan was a recipient of the Google Fellowship and his PhD thesis won the ACM dissertation honorable mention award as well as the SIGCOMM 2018 dissertation award in networking and the John C. Reynolds dissertation award in Programming Languages. His research interests lie primarily at the intersection of programming languages and networks, and he is broadly interested in topics spanning compilers, verification, static analysis, distributed systems, and networks. He has recently focused on improving network reliability by both designing higher-level language abstractions for network automation as well as by applying ideas from formal methods to statically verify the correctness of network configurations.

Vyas Sekar

Checking Dynamic Policies in Stateful Networks

Abstract

The security, performance, and availability of our critical network infrastructures relies on the correct implementation of different policy goals. Network operators realize these goals by composing and configuring diverse stateful middleboxes such as firewalls, intrusion prevention systems, and web proxies. Checking policy violations is hard even for simple reachability properties (e.g., can A talk to B) in today's networks. The stateful nature of processing in middleboxes and the dynamic context-dependent policies implemented using them introduces new concerns with respect to correctness. This talk will provide a brief overview of recent advances in the space of stateful network testing and verification, including: (1) application of program analysis techniques to automatically generate test cases; (2) principled approach to enable scalable parallel testing for stateful networks; (3) more systematic verification capabilities beyond testing; and (4) techniques to automatically synthesize such models from blackbox observations to aid these aforementioned tools.

Bio

Vyas Sekar is the Tan Family Chair Professor of Electrical and Computer Engineering at Carnegie Mellon University. His research is in the area of networking, security, and systems. He is a member of CyLab, where he co-directs the IoT@Cylab initiative. His research spans the areas of data-driven networking, software-defined network security, IoT security, network telemetry, and network verification. Vyas received a B.Tech from the Indian Institute of Technology, Madras where he was awarded the President of India Gold Medal, and a Ph.D from Carnegie Mellon University. He is the recipient of the NSF CAREER award, the ACM SIGCOMM Rising Star Award, and the Angel Jordan Early Career Chair Professorship. His work has received best paper awards at ACM Sigcomm, ACM CoNext, and ACM Multimedia, the NSA Science of Security prize, the CSAW Applied Security Research Prize, and the Applied Networking Research Prize.

Alexandra Silva

Prognosis: Closed-Box Analysis of Network Protocol Implementations

Abstract

We present Prognosis, a framework offering automated closed-box learning and analysis of models of network protocol implementations. Prognosis can learn models that vary in abstraction level from simple deterministic automata to models containing data operations, such as register updates, and can be used to unlock a variety of analysis techniques -- model checking temporal properties, computing differences between models of two implementations of the same protocol, or improving testing via model-based test generation. Prognosis is modular and easily adaptable to different protocols (e.g. TCP and QUIC) and their implementations. We use Prognosis to learn models of (parts of) three QUIC implementations -- Quiche (Cloudflare), Google QUIC, and Facebook mvfst -- and use these models to analyse the differences between the various implementations. Our analysis provides insights into different design choices and uncovers potential bugs. Concretely, we have found critical bugs in multiple QUIC implementations, which have been acknowledged by the developers.

Joint work with Tiago Ferreira (UCL), Harrison Brewton and Loris D'Antoni (University of Wisconsin-Madison).

Bio

Alexandra Silva is a theoretical computer scientist whose main research focuses on semantics of programming languages and modular development of algorithms for computational models. A lot of her work uses the unifying perspective offered by coalgebra, a mathematical framework established in the last decades. Alexandra is currently a Professor at Cornell University, and she was up to recently a Professor of Algebra, Semantics, and Computation at University College London, where part of her research group is still based. She was the recipient of an ERC consolidator grant in 2021, a Royal Society Wolfson Award 2019, Needham Award 2018, the Presburger Award 2017, the Leverhulme prize 2016, and an ERC starting Grant in 2015.

Qiao Xiang

Scaling Network Verification to Large Networks: Progress and Opportunities

Abstract

A fundamental issue of network verification is scalability. This talk will present some of our recent results toward scaling network verification to large networks. For control plane, we made a new finding on the classic stable path problem, the foundation of many control plane verification tools. We also designed a privacy-preserving tool to verify control planes on an interdomain level. For data plane, we proposed a distributed design, which allows us to verify a wide range of properties at the scale of data center networks. Other than showcasing our progress, we also summarize some interesting research opportunities.

Bio

Qiao Xiang is a professor of computer science at Xiamen University, China. Before that, he worked at Yale University as a postdoc and later a research assistant professor. He received his PhD from Wayne State University in 2014. His research interests include interdomain routing, network verification, SDN, and IoT.