#	Pagina
attuale pagina	/open-h2020/projects/200732/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - ProFoundNet (Probabilistic Foundations for Networks)

Teaser

Summary

In an ever-connected world, increasingly complex network systems play a crucial role in many daily tasks. This results in an acute need for methods/tools that can enable easy control of the network and, at the same time, provide rigorous guarantees about its behavior, performance, and security. Recent years saw the growth of a new software ecosystem â€“ Software-defined networking (SDN) â€“ which advocates a clean and open interface between networking devices and the software that controls them. Yet, existing high-level SDN languages do not support reasoning about crucial quantitative aspects, such as: â€œHow much congestion is there?â€ or â€œIs the network resilient under failure?â€. Enabling compositional quantitative reasoning is the major breakthrough needed to fully realize the vision of SDN.

The central objective of this project is to develop new abstractions for programming of networks, with modular constructs. We will provide rigorous semantic probabilistic foundations, enabling quantitative reasoning. This will serve as a solid platform for program analysis tools where compositional reasoning about complex interac- tions will be a reality. Our goal will be achieved through an interdisciplinary research effort: using techniques from concurrency and formal methods, areas where akin challenges can be found in the quest to design correct software systems. We will leverage the wealth of recent advances in those areas (some of which from the PIâ€™s own research) to networks, and bring awareness and new challenges arising from applications in networking to the other two communities.

The project will significantly advance the foundations of network programming/verification in new and previ- ously unexplored directions. This line of research will not only result in fundamental theoretical contributions and insights in their own right but will also impact the practice of network programming and lead to new and more powerful techniques for the use of engineers and programmers.

Work performed

Large computer networks typically require detailed configuration, applied at each node individually. This makes it hard to ensure that the total configuration of network nodes amounts to the intended behaviour of the network as a whole. To remedy this, one can separate the configuration of the network from the hardware implementing it. This technique, called Software Defined Networking (SDN) entails that network policy is decided centrally, after which relevant parts of a configuration implementing this policy are distributed among network devices.

As an added benefit of centralising network policy, it becomes possible to treat this policy as a single object, and reason about or even verify its properties. As an example, NetKAT [Anderson et al., 2014] is a framework which allows the user to specify global network policy in a domain-specific language. These expressions can be compiled [Smolka et al., 2015] to OpenFlow instructions and can run on actual hardware. Moreover, NetKAT allows the user to reason about the policy they wrote using straightforward algebraic laws, which accurately (i.e., soundly and completely) describe its semantics; as a matter of fact, this process can be automated [Foster et al., 2015] quite efficiently using coinductive techniques.

We have focussed on two lines of research:

1) Design and semantics of a probabilistic programming language that can be used for programming and verifying networks.

We have developed ProbNetKAT, a probabilistic programming language built on top of NetKAT that enables programming and verification of probabilistic features in SDN.
We develop McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the history-free fragment of Probabilistic NetKAT in terms of nite state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes. We used McNetKAT to automatically reason about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluated McNetKATâ€™s scalability using real-world topologies, compared its performance against state-of-the art tools, and developed an extended case study on a recently proposed data centre network design.

2) Development of a verification framework for properties with concurrent behaviour.

One feature missing from NetKAT is the ability to express concurrency, for instance when processing a packet using multiple tables simultaneously, or perhaps even multiple devices, such as a firewall and an intrusion detection system. We have worked extensively on developing tools for Concurrent Kleene Algebra: free models, complete axiomatisation, and decision procedures. We will next build on this foundation to develop a concurrent version of NetKAT, which enjoys the same benefits as NetKAT proper, including completeness of the algebraic theory, the possibility of running on network hardware and an efficient decision procedure.

Final results

The main efforts in the coming year will be on developing the concurrent version of NetKAT. This will be challenging and extending all previous results will require a lot of work. We aim at building a tool in which the results can be tested in a practical case study. We will also explore the combination of both probabilistic and concurrent versions. Finally, we will incorporate learning algorithms into the verification toolset of NetKAT.