Dagstuhl Seminar 15071
Formal Foundations for Networking
( Feb 08 – Feb 13, 2015 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/15071
Organizers
- Nikolaj S. Bjørner (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)
Contact
- Andreas Dolzmann (for scientific matters)
- Dagmar Glaser (for administrative matters)
Schedule
The complexity of networks has increased dramatically in recent years, driven by rapidly expanding computing infrastructures, increased concerns about security, and generally more widespread and diverse uses of the Internet. As a result, there is an acute need for methods and tools that can provide rigorous guarantees about the behavior, performance, reliability, and security of networked systems. In many areas of computing, techniques ranging from automated test generation to modeling to full-blown verification have been used to help developers design and construct systems whose behavior satisfies formal correctness properties. But with a few notable exceptions, formal methods are not widely used in networked systems today. We believe that the time is ripe for the networking community to leverage the wealth of recent advances in formal methods, and for the formal methods community to become more aware of potential applications in networking.
This seminar will bring together researchers and practitioners from the fields of networking, formal methods, programming languages, and security, to investigate key questions the following areas:
- Abstractions. What is the best way to represent high-level knowledge about a network? What abstractions best manage complexity by enabling modular design, separation of concerns, generalization, and delayed optimization? How can programmers leverage abstraction to develop and analyze network software in a compositional manner?
- Logic. What are appropriate frameworks for expressing network properties? Can we engineer efficient decision procedures for checking certain properties automatically? How should we model quantitative resources and performance, which are needed for traffic engineering and service-level agreements? Can we encode existing logics and tools into a unified framework to facilitate precise comparisons and lay down a clear path for future improvements?
- Programming Languages. What are suitable linguistic abstractions for programming networks? What guarantees should a compiler for such a language provide—reachability, reliability, or even the correct use of cryptography? Can we effectively engineer verified compilers that are guaranteed to produce correct machine code?
- Systems. How can formal methods for constructing and reasoning about networks be deployed as production systems? What methods best address targeted pressing needs, or long-term systems challenges? What is the right division of labor between static and dynamic verification tools, to efficiently check global properties while scaling to large networks? Can we develop techniques for systematically monitoring system behavior, and for troubleshooting when errors occur?
The overall goal of the seminar is to focus the attention of the respective research communities on topics of common interest, and help participants fill in missing background knowledge. Possible outcomes include writing a survey article summarizing key problems and opportunities, identifying challenge problems to focus effort in the most promising directions, and organizing a workshop to be co-located with a major conference in the future.
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. Bjørner, Nate Foster, Philip Brighten Godfrey, and Pamela Zave
- Aditya Akella (University of Wisconsin - Madison, US) [dblp]
- Nikolaj S. Bjørner (Microsoft Corporation - Redmond, US) [dblp]
- Achim D. Brucker (SAP SE - Karlsruhe, DE) [dblp]
- Marco Canini (University of Louvain, BE) [dblp]
- Pavol Cerny (University of Colorado - Boulder, US) [dblp]
- Swarat Chaudhuri (Rice University - Houston, US) [dblp]
- Evgeny Chemeritskiy (ARCCN - Moscow Region, RU)
- Shiu-Kai Chin (Syracuse University, US) [dblp]
- Bryan Ford (Yale University, US) [dblp]
- Nate Foster (Cornell University, US) [dblp]
- Vijay Ganesh (University of Waterloo, CA) [dblp]
- Aaron Gember-Jacobson (University of Wisconsin - Madison, US) [dblp]
- Philip Brighten Godfrey (University of Illinois - Urbana-Champaign, US) [dblp]
- Arjun Guha (University of Massachusetts - Amherst, US) [dblp]
- Arie Gurfinkel (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Karthick Jayaraman (Microsoft Research - Redmond, US) [dblp]
- Limin Jia (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Ethan Katz-Bassett (University of Southern California - Los Angeles, US) [dblp]
- Shriram Krishnamurthi (Brown University - Providence, US) [dblp]
- Ori Lahav (MPI-SWS - Kaiserslautern, DE) [dblp]
- Nuno Lopes (Microsoft Research UK - Cambridge, GB) [dblp]
- Ratul Mahajan (Microsoft Corporation - Redmond, US) [dblp]
- Tim Nelson (Brown University - Providence, US) [dblp]
- Aurojit Panda (University of California - Berkeley, US) [dblp]
- Panagiotis Papadimitriou (Leibniz Universität Hannover, DE) [dblp]
- Mark Reitblatt (Cornell University, US) [dblp]
- Jennifer Rexford (Princeton University, US) [dblp]
- Timothy Roscoe (ETH Zürich, CH) [dblp]
- David Rosenblum (National University of Singapore, SG) [dblp]
- Kristin Yvonne Rozier (University of Cincinnati, US) [dblp]
- Andrey Rybalchenko (Microsoft Research UK - Cambridge, GB) [dblp]
- Mooly Sagiv (Tel Aviv University, IL) [dblp]
- Cole Schlesinger (Princeton University, US) [dblp]
- Stefan Schmid (TU Berlin, DE) [dblp]
- Sharon Shoham Buchbinder (Academic College of Tel Aviv, IL) [dblp]
- Robert Soulé (University of Lugano, CH) [dblp]
- David Walker (Princeton University, US) [dblp]
- Alexander L. Wolf (Imperial College London, GB) [dblp]
- Burkhart Wolff (University Paris-Sud, FR) [dblp]
- Yifei Yuan (University of Pennsylvania - Philadelphia, US) [dblp]
- Vladimir Zakharov (Moscow State University, RU) [dblp]
- Pamela Zave (AT&T Labs Research - Bedminster, US) [dblp]
Classification
- networks
- semantics / formal methods
- verification / logic
Keywords
- Networks
- Formal Methods
