Abstracts

Talk Abstracts

Stop Guessing - Start Knowing: An Overview on BENOCS Analytics and its Measurement Infrastructure by Ingmar Poese.

Doing near realtime network measurements and pushing the information back to the customer as quickly as possible is a difficult task that touches a wide range of expertise across many fields of research. On the one hand, the technical challenges range from CPU level thread optimization, memory optimization, algorithmic tricks to data correlation of multiple GBit/s in diverse network setups. On the other hand, the outcome of the analysis needs to be easy to handle and understandable by people without deep network knowledge, which forces a very easy to understand yet consistent view on highly complex data. Dealing with the demand of having technically diverse, but sophisticated analysis ready in near-real time while presenting an easy to understand and correct analysis is difficult terrain to navigate.

Using UPPAAL Stratego for Adaptive Control of Traffic by Kim G. Larsen.

UPPAAL Stratego is a tool in the UPPAAL family combining symbolic synthesis with reinforcement learning for obtaining safe and near-optimal control strategies for Timed Markov Decision Processes. The talk will be a tutorial on the formalism and capabilities of the tool. In particular I will demonstrate how the tool may be used highly efficient adaptive control of traffic lights in road intersections. The successful that it has lead to the spin-out company ATS.

Scalable, Reliable and Repeatable Mesh Network Simulation by Peter G. Jensen. [slides]

Estimating the performance and functional correctness of (implementations of) wireless mesh protocols is highly challenging, in particular as noise (i.e. clock sync and drift) and environmental factors (cross-talk from third party devices) impact performance heavily and are hard to control. We propose a simulation and data-analysis framework for simulating large scale deployments of wireless IoT networks. We utilize the expressive power of state-of-the-art tool Uppaal to build digital twins of the underlying hardware platform as well as for emulating radio signal propagation and collision. Combined with Uppaals ability to link with external C-libraries, we provide a fully virtualized testbench in which developers can measure the performance of their specific protocol implementation -- in a manner which is reliable and repeatable. The framework has been developed in collaboration with NeoCortec and has been used successfully to estimate the performance of several (prototype) protocols, leading to early design changes.

Automatic Verification of MPLS Networks by Jiri Srba. [slides]

I shall present an automated what-if analysis tool AalWiNes for MPLS networks which allows us to verify both logical properties (e.g., related to the policy compliance) as well as quantitative properties (e.g., concerning the latency) under multiple link failures. Our tool relies on the theory of weighted pushdown automata, a quantitative extension of classic automata theory, and takes into account the actual dataplane configuration, rendering it especially useful for debugging. In particular, our tool collects the different router forwarding tables and then builds a pushdown system, on which quantitative reachability is performed based on an expressive query language. Our experiments show that our tool outperforms state-of-the-art approaches (which until now have been restricted to logical properties) by several orders of magnitude; furthermore, our quantitative extension only entails a moderate overhead in terms of runtime. The tool comes with a platform-independent user interface and is publicly available as open-source.

R-MPLS: Recursive Protection for Highly Dependable MPLS Networks by Morten K. Schou. [slides]

To meet their high dependability requirements, most modern communication networks feature fast rerouting (FRR) mechanisms in the data plane. Upon local detection of a failure, FRR routes traffic onto a precomputed backup path to avoid packet loss until the network converges to a new set of paths. In order to increase the resilience, we propose R-MPLS, a link protection mechanism that uses recursive FRR protection to route around multiple simultaneously failed links. Naively protecting the backup paths can lead to forwarding loops, but R-MPLS includes a loop avoidance algorithm, which provably guarantees that no forwarding loops are introduced. We find that R-MPLS significantly increases network robustness against multiple failures, with only a moderate increase in the number of forwarding rules and communication overhead.

Type-Safe Data Plane Programming by Matthias Eichholz. [slides]

With the advent of software-defined networks, the way we can configure networks has changed significantly. There is a shift towards more flexible platforms that allow the behavior of networks to be specified in software. While early efforts focused on the control plane software, there is a recent interest in specifying the behavior of the data plane in software as well, opening a whole new range of applications, from new network protocols to relocating application-level functionality into the network. However, with increasingly powerful and complex applications running in the network, the risk of faults also increases. Hence, there is growing recognition of the need for methods and tools to statically verify the correctness of data plane programs, especially since languages such as P4—the de facto standard for programming data planes—lack basic safety guarantees. We argue that safety guarantees should be part of the language itself. In this talk, by using P4 as an example, I'll show that static type systems are well-suited to equip data plane programming languages with safety guarantees. By providing expressive types, these type systems not only allow data plane programmers to express rich network properties, but also to verify them in a modular fashion.

Time Sensitive Networking - A dive into IEEE802.1Q-2018 by Damien Saucez. [slides]

In the recent years time sensitiveness has become a subject of discussion in networking and some may even dream of providing real-time guarantees and deterministic behaviour in 5G networks. Naturally, when it comes to such properties, the next step is to prove that the network is going to respects these guarantees and behave in a deterministic manner. In this talk, we will list and explain the main features offered by Ethernet that can help in building real time/deterministic networks with COTS. To that aim, we will follow a functional approach where a reference Ethernet switch will be decomposed into elementary functions and see how the combinations of them contribute to offering real-time and deterministic networking. This talk is a tutorial to show how real time support is implemented at the switch level. This presentation is accessible to any attendees with standard computer science knowledge.

Correct-by-Construction Network Programming for Stateful Data-Planes by Jedidiah McClurg.

As switch hardware becomes faster, more stateful, and more programmable, functionality that was once confined to end hosts or the control plane is being pushed into the data plane. For example, recent work on adaptive congestion control and heavy hitter detection uses stateful switches to implement sophisticated functionality with only minor controller involvement. In applications where correctness depends on individual switches making coherent decisions, it is important that the switches have a consistent view of global state. However, such a consistency requirement makes it difficult to maintain efficiency (high throughput), due to the CAP theorem. Moreover, previous work on data-plane programming provides little to no built-in support for addressing this difficulty. We propose Callback State Machines (CSMs), a new high-level declarative network programming abstraction which allows operators to write correct data-plane programs against global state. CSMs offer programmers useful consistency guarantees without the need to manage how global state is replicated/updated at the individual switch level. To aid in the implementation of this high-level programming framework, we present a flexible new intermediate representation (IR) called TAPIR that natively supports stateful data plane functionality, as well as a compiler to generate device-specific code such as P4 from TAPIR code. Additionally, we demonstrate the power of TAPIR itself by using it to build a working implementation of the CONGA congestion control system.

Temporal Logics for the Specification of Hyperproperties by Martin Zimmermann. [slides]

Hyperproperties, as introduced by Clarkson and Schneider, generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. HyperLTL, the extension of LTL with trace quantifiers, has recently been introduced to specify hyperproperties. In this talk, we give a light introduction to HyperLTL and related logics. We hope this will stimulate discussion on the applicability of HyperLTL to networks.

Network Performance Verification by Costin Raiciu.

Network correctness is more than checking for reachability and isolation. Lossy links, ECMP collisions, incast and other anomalous traffic patterns result in unpredictable performance that affects the functioning of applicaitons to the point where they are not usable. In this talk I will outline a research agenda and some preliminary results towards verifying network performance.

AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences by Kim G. Larsen.

We present AllSynth, a symbolic synthesis tool for updating communication networks in a provably correct and efficient manner. AllSynth automatically synthesizes network update schedules which transiently ensure a wide range of policy properties (expressed in the LTL logic), also during the reconfiguration process. In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible solutions. At its heart, AllSynth relies on a novel, two-level and parameterized use of BDDs which greatly improves performance. Indeed, AllSynth not only provides formal correctness guarantees and outperforms existing state-of-the-art tools in terms of generality, but often also in terms of runtime as documented by experiments on a benchmark of real-world network topologies.

Self-Adjusting Networks by Stefan Schmid.

The bandwidth and latency requirements of modern datacenter applications have led researchers to propose various datacenter topology designs using static, dynamic demand-oblivious (rotor), and/or dynamic demand-aware switches. However, given the diverse nature of datacenter traffic, there is little consensus about how these designs would fare against each other. In this talk, I will present the vision of self-adjusting networks, networks which are optimized towards the nature of the traffic workload they serve. We will discuss metrics to quantify the structure in traffic demands as well as the achievable performance in datacenter networks matching their demands, present network design algorithms accordingly, and identify open research challenges.

Optimizing Packet Classification by Pavel Chuprikov. [slides]

While secure efficient operation of computer networks requires cost-effective line-rate packet classification, network programmability strengthens this need. A promising approach is to transform a packet classifier to a semantically equivalent representation. We will consider one such representation that supports more effective classification and will briefly touch on another spanning multiple devices.

Matching Ingress Flows to Egress Flows on BENOCS' Data Set by Noah Witte-Winnett

BENOCS gathers an immense amount of flow data from its clients' edge routers for the purpose of helping clients understand what is happening on their network. Collecting these data involves sampling traffic at two distinct points in a network: once when it enters (ingress) and once when it exits (egress) the network. These separated measurements are useful for the average user of BENOCS' Analytics tool, but some advanced users want to have information that can only be synthesized by bringing these ingress and egress flows together. This talk will describe how it is possible to join these bifurcated flows to predict which egress interface a given flow will use to exit the network. Moreover, by bringing these two flows together data analysts and engineers at BENOCS can verify how well a network is configured, for example by determining what proportion of traffic forwarded to a specific router actually arrives there.

DyNetKAT: An Algebra of Dynamic Networks by Georgiana Caltais

In this talk I will introduce DyNetKAT -a formal language for specifying dynamic updates for Software Defined Networks-. The language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data plane in dynamic updates. A sound and ground-complete axiomatisation of DyNetKAT will be discussed, together with an efficient method for reasoning about safety properties, and associated case studies. This is joint work with Hossein Hojjat at TeIAS, Mohammad Mousavi at King’s College London, and Hünkar Can Tunç at Aarhus University.