08.02.15 - 13.02.15, Seminar 15071

Formal Foundations for Networking

The following text appeared on our web pages prior to the seminar, and was included as part of the invitation.

Motivation

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.