Seminar Homepage : Druckversion


http://www.dagstuhl.de/15071

February 8 – 13 , 2015, Dagstuhl Seminar 15071

Formal Foundations for Networking

Organizers

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

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 5, Issue 2 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Schedule [pdf]

Summary

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.

License
  Creative Commons BY 3.0 Unported license
  Nikolaj S. Bjorner, Nate Foster, Philip Brighten Godfrey, and Pamela Zave

Classification

Keywords



Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Seminar Homepage : Last Update 23.06.2017, 22:47 o'clock