February 8 – 13 , 2015, Dagstuhl Seminar 15071
Formal Foundations for Networking
Nikolaj S. Bjorner (Microsoft Corporation – Redmond, US)
Nate Foster (Cornell University, US)
Philip Brighten Godfrey (University of Illinois – Urbana-Champaign, US)
Pamela Zave (AT&T Labs Research – Bedminster, US)
1 / 2 >
For support, please contact
The scale and complexity of computer networks has increased dramatically in recent years, driven by the growth of mobile devices, data centers, and cloud computing; increased concerns about security; and generally more widespread and diverse uses of the Internet. Building and operating a network has become a difficult task, even for the most technologically sophisticated organizations.
To address these needs, the research community has started to develop tools for managing this complexity using programming language and formal methods techniques. These tools use domain-specific languages, temporal logics, satisfiability modulo theories solvers, model checkers, proof assistants, software synthesis, etc. to specify and verify network programs.
Yet despite their importance, tools for programming and reasoning about networks are still in a state of infancy. The programming models supported by major hardware vendors require configurations to be encoded in terms of low-level constructs - e.g., hardware forwarding rules and IP address prefixes. To express richer policies, network operators must incorporate "tribal knowledge" capturing requirements that cut across different customers, service-level agreements, and protocols and can easily lead to contradictions. In addition, networks are rarely static, so operators must deal with updates to configurations and the complications that arise during periods of transition or when unexpected failures occur.
The goal of this seminar was to bring together leading practitioners from the areas of formal methods, networking, programming languages, and security, to exchange ideas about problems and solutions, and begin the task of developing formal foundations for networks. The seminar program was grouped into broad categories addressing the following issues:
- Networking Applications (Akella, Gember-Jacobson, Jayaraman, Rexford). What are the key concerns in enterprise, data center, and wide-area networks today? What kinds of modeling, verification, and property-checking tools are operators deploying? What kinds of scalability challenges are they facing?
- Emerging Areas (Papadimitriou, Rozier). What are the key issues in emerging areas such as crowd-sourced networks and aerospace engineering? Can existing tools be easily adapted to these areas? How can new researchers get involved?
- Distributed Systems (Canini, Cerny). What are some techniques for handling the distributed systems issues that arise in modeling and reasoning about networks? How can we exploit these insights to build practical tools for verifying properties in the presence of replicated state, asynchronous communication, and unexpected failures?
- Domain-Specific Tools (Chemeritskiy, Mahajan, Panda, Rybalchenko, Sagiv). What are the best approaches for verifying properties of real-world networks? How can we incorporate features such as dynamic control programs and mutable state? How can we make these tools scale to networks of realistic size?
- General Tools (Brucker, Ganesh, Guha, Jia, Nelson, Rosenblum, Rybalchenko). There is a rich literature on temporal logics, satisfiability modulo theories checkers, model checkers, proof assistants, Datalog, etc. What are the key differences between these tools and how can they be applied to networks?
- Platforms and Models (Guha, Schlesinger, Reitblatt, Walker, Zave). What is the state-of-the-art in network programming? How can we build compilers and hypervisors that correctly translate from high-level models to low-level implementations?
- Program Synthesis (Buchbinder, Chaudhuri, Cerny, Yuan). Synthesis is a promising approach to building correct software, since programs are generated automatically using a verification tool. What are the best current techniques for using model checkers and satisfiability-modulo theories solvers to generate network configurations, update protocols, and policies?
The seminar comprised four and a half days of presentations, interspersed with discussions, tool demonstrations, and working groups. This report collects the abstracts of the presentations, gives summaries of discussions and working groups, and lists open questions.
Creative Commons BY 3.0 Unported license
Nikolaj S. Bjorner, Nate Foster, Philip Brighten Godfrey, and Pamela Zave
- Semantics / Formal Methods
- Verification / Logic
- Formal Methods