Search

We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed.

A recent advance in networking is the deployment of path-aware multipath network architectures, where network endpoints are given multiple network paths to send their data on. In this work, we tackle the challenge of selecting paths for latency-sensitive applications. Even today's path-aware networks, which are much smaller than the current Internet, already offer dozens and in several cases over a hundred paths to a given destination, making it impractical to measure all path latencies to find the lowest latency path. Furthermore, for short flows, performing latency measurements may not provide benefits as the flow may finish before completing the measurements. To overcome these issues, we argue that endpoints should be provided with a latency estimate before sending any packets, enabling latency-aware path choice for the first packet sent. As we cannot predict the end-to-end latency due to dynamically changing queuing delays, we measure and disseminate the propagation latency, enabling novel use cases and solving concrete problems in current network protocols. We present the Global Latency Information Dissemination System (GLIDS), which is a step toward global latency transparency through the dissemination of propagation latency information., Comment: Extended version of the 7-page conference paper "Toward Global Latency Transparency" published at the IFIP Networking 2024 Conference

Internet censorship and global Internet reachability are prevalent topics of today's Internet. Nonetheless, the impact of network topology and Internet architecture to these aspects of the Internet is under-explored. With the goal of informing policy discussions with an objective basis, we present an approach for evaluating both censorship resilience and global Internet reachability using quantitative network metrics, which are applicable to current BGP/IP networks and also to alternative Internet network architectures. We devise and instantiate the metric on the network topology of multiple countries, comparing the BGP/IP network, an overlay network using a waypoint mechanism for circumventing undesired nodes, and the path-aware Internet architecture SCION. The novelty of the approach resides in providing a metric enabling the analysis of these aspects of the Internet at the routing level, taking into account the innate properties of the routing protocol and architecture. We demonstrate that the Internet topology matters, and strongly influences both censorship resilience and reachability to the global Internet. Finally, we argue that access to multiple paths accompanied with path-awareness could enable a higher level of censorship resilience compared to the current Internet, and reduce the centralization of Internet routing., Comment: Proceedings of the 23rd IFIP Networking Conference

With the rapid evolution and diversification of Internet applications, their communication-quality criteria are continuously evolving. To globally optimize communication quality, the Internet's control plane thus needs to optimize inter-domain paths on diverse criteria, and should provide flexibility for adding new criteria or modifying existing ones. However, existing inter-domain routing protocols and proposals satisfy these requirements at best to a limited degree. We propose IREC, an inter-domain routing architecture that enables multi-criteria path optimization with extensible criteria through parallel execution and real-time addition of independent routing algorithms, together with the possibility for end domains to express their desired criteria to the control plane. We show IREC's viability by implementing it on a global testbed, and use simulations on a realistic Internet topology to demonstrate IREC's potential for path optimization in real-world deployments.

The current Internet lacks quality-of-service guarantees for real-time applications like video calls and gaming, cloud-based systems, financial transactions, telesurgery, and other remote applications that benefit from reliable communication. To address this problem, this paper introduces Hummingbird: a novel, lightweight bandwidth-reservation system that provides fine-grained inter-domain reservations for end hosts and introduces several improvements over previous designs. Hummingbird enables flexible and composable reservations with end-to-end guarantees, and addresses an often overlooked, but crucial, aspect of bandwidth reservation systems: incentivization of network providers. Hummingbird represents bandwidth reservations as tradeable assets which allows markets to emerge that ensure fair and efficient resource allocation and encourage deployment by remunerating providers. This incentivization is facilitated by decoupling reservations from network identities, which enables novel control-plane mechanisms and allows us to design a control plane based on smart contracts. Hummingbird also provides an efficient reservation data plane which streamlines the processing on routers and thus simplifies the implementation, deployment, and traffic policing while maintaining robust security properties., Comment: 20 pages, 15 figures

Modern DDoS defense systems rely on probabilistic monitoring algorithms to identify flows that exceed a volume threshold and should thus be penalized. Commonly, classic sketch algorithms are considered sufficiently accurate for usage in DDoS defense. However, as we show in this paper, these algorithms achieve poor detection accuracy under burst-flood attacks, i.e., volumetric DDoS attacks composed of a swarm of medium-rate sub-second traffic bursts. Under this challenging attack pattern, traditional sketch algorithms can only detect a high share of the attack bursts by incurring a large number of false positives. In this paper, we present ALBUS, a probabilistic monitoring algorithm that overcomes the inherent limitations of previous schemes: ALBUS is highly effective at detecting large bursts while reporting no legitimate flows, and therefore improves on prior work regarding both recall and precision. Besides improving accuracy, ALBUS scales to high traffic rates, which we demonstrate with an FPGA implementation, and is suitable for programmable switches, which we showcase with a P4 implementation., Comment: Accepted at the 42nd International Symposium on Reliable Distributed Systems (SRDS 2023)

Internet service providers (ISPs) have a variety of quality attributes that determine their attractiveness for data transmission, ranging from quality-of-service metrics such as jitter to security properties such as the presence of DDoS defense systems. ISPs should optimize these attributes in line with their profit objective, i.e., maximize revenue from attracted traffic while minimizing attribute-related cost, all in the context of alternative offers by competing ISPs. However, this attribute optimization is difficult not least because many aspects of ISP competition are barely understood on a systematic level, e.g., the multi-dimensional and cost-driving nature of path quality, and the distributed decision making of ISPs on the same path. In this paper, we improve this understanding by analyzing how ISP competition affects path quality and ISP profits. To that end, we develop a game-theoretic model in which ISPs (i) affect path quality via multiple attributes that entail costs, (ii) are on paths together with other selfish ISPs, and (iii) are in competition with alternative paths when attracting traffic. The model enables an extensive theoretical analysis, surprisingly showing that competition can have both positive and negative effects on path quality and ISP profits, depending on the network topology and the cost structure of ISPs. However, a large-scale simulation, which draws on real-world data to instantiate the model, shows that the positive effects will likely prevail in practice: If the number of selectable paths towards any destination increases from 1 to 5, the prevalence of quality attributes increases by at least 50%, while 75% of ISPs improve their profit., Comment: Accepted at the International Symposium on Computer Performance, Modeling, Measurements and Evaluation (PERFORMANCE) 2023

In its current state, the Internet does not provide end users with transparency and control regarding on-path forwarding devices. In particular, the lack of network device information reduces the trustworthiness of the forwarding path and prevents end-user applications requiring specific router capabilities from reaching their full potential. Moreover, the inability to influence the traffic's forwarding path results in applications communicating over undesired routes, while alternative paths with more desirable properties remain unusable. In this work, we present FABRID, a system that enables applications to forward traffic flexibly, potentially on multiple paths selected to comply with user-defined preferences, where information about forwarding devices is exposed and transparently attested by autonomous systems (ASes). The granularity of this information is chosen by each AS individually, protecting them from leaking sensitive network details, while the secrecy and authenticity of preferences embedded within the users' packets are protected through efficient cryptographic operations. We show the viability of FABRID by deploying it on a global SCION network test bed, and we demonstrate high throughput on commodity hardware.

The growing energy consumption of Information and Communication Technology (ICT) has raised concerns about its environmental impact. However, the carbon efficiency of data transmission over the Internet has so far received little attention. This carbon efficiency can be enhanced effectively by sending traffic over carbon-efficient inter-domain paths. However, challenges in estimating and disseminating carbon intensity of inter-domain paths have prevented carbon-aware path selection from becoming a reality. In this paper, we take advantage of path-aware network architectures to overcome these challenges. In particular, we design CIRo, a system for forecasting the carbon intensity of inter-domain paths and disseminating them across the Internet. We implement a proof of concept for CIRo on the codebase of the SCION path-aware Internet architecture and test it on the SCIONLab global research testbed. Further, we demonstrate the potential of CIRo for reducing the carbon footprint of endpoints and end domains through large-scale simulations. We show that CIRo can reduce the carbon intensity of communications by at least 47% for half of the domain pairs and the carbon footprint of Internet usage by at least 50% for 87% of end domains.

The question at which layer network functionality is presented or abstracted remains a research challenge. Traditionally, network functionality was either placed into the core network, middleboxes, or into the operating system -- but recent developments have expanded the design space to directly introduce functionality into the application (and in particular into the browser) as a way to expose it to the user. Given the context of emerging path-aware networking technology, an interesting question arises: which layer should handle the new features? We argue that the browser is becoming a powerful platform for network innovation, where even user-driven properties can be implemented in an OS-agnostic fashion. We demonstrate the feasibility of geo-fenced browsing using a prototype browser extension, realized by the SCION path-aware networking architecture, without introducing any significant performance overheads., Comment: 1 table, 6 figures

With the application of machine learning to security-critical and sensitive domains, there is a growing need for integrity and privacy in computation using accelerators, such as GPUs. Unfortunately, the support for trusted execution on GPUs is currently very limited - trusted execution on accelerators is particularly challenging since the attestation mechanism should not reduce performance. Although hardware support for trusted execution on GPUs is emerging, we study purely software-based approaches for trusted GPU execution. A software-only approach offers distinct advantages: (1) complement hardware-based approaches, enhancing security especially when vulnerabilities in the hardware implementation degrade security, (2) operate on GPUs without hardware support for trusted execution, and (3) achieve security without reliance on secrets embedded in the hardware, which can be extracted as history has shown. In this work, we present SAGE, a software-based attestation mechanism for GPU execution. SAGE enables secure code execution on NVIDIA GPUs of the Ampere architecture (A100), providing properties of code integrity and secrecy, computation integrity, as well as data integrity and secrecy - all in the presence of malicious code running on the GPU and CPU. Our evaluation demonstrates that SAGE is already practical today for executing code in a trustworthy way on GPUs without specific hardware support., Comment: 14 pages, 2 reference pages, 6 figures

To protect against naturally occurring or adversely induced congestion in the Internet, we propose the concept of flyover reservations, a fundamentally new approach for addressing the availability demands of critical low-volume applications. In contrast to path-based reservation systems, flyovers are fine-grained "hop-based" bandwidth reservations on the level of individual autonomous systems. We demonstrate the scalability of this approach experimentally through simulations on large graphs. Moreover, we introduce Helia, a protocol for secure flyover reservation setup and data transmission. We evaluate Helia's performance based on an implementation in DPDK, demonstrating authentication and forwarding of reservation traffic at 160 Gbps. Our security analysis shows that Helia can resist a large variety of powerful attacks against reservation admission and traffic forwarding. Despite its simplicity, Helia outperforms current state-of-the-art reservation systems in many key metrics.

Google's BBR is the most prominent result of the recently revived quest for efficient, fair, and flexible congestion-control algorithms (CCAs). While the performance of BBR has been investigated by numerous studies, previous work still leaves gaps in the understanding of BBR performance: Experiment-based studies generally only consider network settings that researchers can set up with manageable effort, and model-based studies neglect important issues like convergence. To complement previous BBR analyses, this paper presents a fluid model of BBRv1 and BBRv2, allowing both efficient simulation under a wide variety of network settings and analytical treatment such as stability analysis. By experimental validation, we show that our fluid model provides highly accurate predictions of BBR behavior. Through extensive simulations and theoretical analysis, we arrive at several insights into both BBR versions, including a previously unknown bufferbloat issue in BBRv2., Comment: Accepted at the ACM Internet Measurement Conference 2022 (IMC'22)

Many critical computing applications rely on secure and dependable time which is reliably synchronized across large distributed systems. Today's time synchronization architectures are commonly based on global navigation satellite systems at the considerable risk of being exposed to outages, malfunction, or attacks against availability and accuracy. This paper describes a practical instantiation of a new global, Byzantine fault-tolerant clock synchronization approach that does not place trust in any single entity and is able to tolerate a fraction of faulty entities while still maintaining synchronization on a global scale among otherwise sovereign network topologies. Leveraging strong resilience and security properties provided by the path-aware SCION networking architecture, the presented design can be implemented as a backward compatible active standby solution for existing time synchronization deployments. Through extensive evaluation, we demonstrate that over 94% of time servers reliably minimize the offset of their local clocks to real-time in the presence of up to 20% malicious nodes, and all time servers remain synchronized with a skew of only 2 ms even after one year of reference clock outage.

Adversaries can exploit inter-domain routing vulnerabilities to intercept communication and compromise the security of critical Internet applications. Meanwhile the deployment of secure routing solutions such as Border Gateway Protocol Security (BGPsec) and Scalability, Control and Isolation On Next-generation networks (SCION) are still limited. How can we leverage emerging secure routing backbones and extend their security properties to the broader Internet? We design and deploy an architecture to bootstrap secure routing. Our key insight is to abstract the secure routing backbone as a virtual Autonomous System (AS), called Secure Backbone AS (SBAS). While SBAS appears as one AS to the Internet, it is a federated network where routes are exchanged between participants using a secure backbone. SBAS makes BGP announcements for its customers' IP prefixes at multiple locations (referred to as Points of Presence or PoPs) allowing traffic from non-participating hosts to be routed to a nearby SBAS PoP (where it is then routed over the secure backbone to the true prefix owner). In this manner, we are the first to integrate a federated secure non-BGP routing backbone with the BGP-speaking Internet. We present a real-world deployment of our architecture that uses SCIONLab to emulate the secure backbone and the PEERING framework to make BGP announcements to the Internet. A combination of real-world attacks and Internet-scale simulations shows that SBAS substantially reduces the threat of routing attacks. Finally, we survey network operators to better understand optimal governance and incentive models., Comment: Usenix Security 2022

This paper presents a security analysis of the InfiniBand architecture, a prevalent RDMA standard, and NVMe-over-Fabrics (NVMe-oF), a prominent protocol for industrial disaggregated storage that exploits RDMA protocols to achieve low-latency and high-bandwidth access to remote solid-state devices. Our work, NeVerMore, discovers new vulnerabilities in RDMA protocols that unveils several attack vectors on RDMA-enabled applications and the NVMe-oF protocol, showing that the current security mechanisms of the NVMe-oF protocol do not address the security vulnerabilities posed by the use of RDMA. In particular, we show how an unprivileged user can inject packets into any RDMA connection created on a local network controller, bypassing security mechanisms of the operating system and its kernel, and how the injection can be used to acquire unauthorized block access to NVMe-oF devices. Overall, we implement four attacks on RDMA protocols and seven attacks on the NVMe-oF protocol and verify them on the two most popular implementations of NVMe-oF: SPDK and the Linux kernel. To mitigate the discovered attacks we propose multiple mechanisms that can be implemented by RDMA and NVMe-oF providers.

Many systems today rely heavily on virtual private network (VPN) technology to connect networks and protect their services on the Internet. While prior studies compare the performance of different implementations, they do not consider adversarial settings. To address this gap, we evaluate the resilience of VPN implementations to flooding-based denial-of-service (DoS) attacks. We focus on a class of stateless flooding attacks, which are particularly threatening to real connections, as they can be carried out by an off-path attacker using spoofed IP addresses. We have implemented various attacks to evaluate DoS resilience for three major open-source VPN solutions, with surprising results: On high-performance hardware with a $40\,\mathrm{Gb/s}$ interface, data transfer over established WireGuard connections can be fully denied with $700\,\mathrm{Mb/s}$ of attack traffic. For strongSwan (IPsec), an adversary can block any legitimate connections from being established using only $75\,\mathrm{Mb/s}$ of attack traffic. OpenVPN can be overwhelmed with $100\,\mathrm{Mb/s}$ of flood traffic denying data transfer through the VPN connection as well as connection establishment completely. Further analysis has revealed implementation bugs and major inefficiencies in the implementations related to concurrency aspects. These findings demonstrate a need for more adversarial testing of VPN implementations with respect to DoS resilience., Comment: Major update has been made and will be published at a later point in time

In various contexts of networking research, end-host path selection has recently regained momentum as a design principle. While such path selection has the potential to increase performance and security of networks, there is a prominent concern that it could also lead to network instability (i.e., flow-volume oscillation) if paths are selected in a greedy, load-adaptive fashion. However, the extent and the impact vectors of instability caused by path selection are rarely concretized or quantified, which is essential to discuss the merits and drawbacks of end-host path selection. In this work, we investigate the effect of end-host path selection on various metrics of networks both qualitatively and quantitatively. To achieve general and fundamental insights, we leverage the recently introduced axiomatic perspective on congestion control and adapt it to accommodate joint algorithms for path selection and congestion control, i.e., multi-path congestion-control protocols. Using this approach, we identify equilibria of the multi-path congestion-control dynamics and analytically characterize these equilibria with respect to important metrics of interest in networks (the 'axioms') such as efficiency, fairness, and loss avoidance. Moreover, we analyze how these axiomatic ratings for a general network change compared to a scenario without path selection, thereby obtaining an interpretable and quantititative formalization of the performance impact of end-host path-selection. Finally, we show that there is a fundamental trade-off in multi-path congestion-control protocol design between efficiency, stability, and loss avoidance on one side and fairness and responsiveness on the other side., Comment: 39th International Symposium on Computer Performance, Modeling, Measurements and Evaluation (PERFORMANCE) 2021

We present F-PKI, an enhancement to the HTTPS public-key infrastructure (or web PKI) that gives trust flexibility to both clients and domain owners, and enables certification authorities (CAs) to enforce stronger security measures. In today's web PKI, all CAs are equally trusted, and security is defined by the weakest link. We address this problem by introducing trust flexibility in two dimensions: with F-PKI, each domain owner can define a domain policy (specifying, for example, which CAs are authorized to issue certificates for their domain name) and each client can set or choose a validation policy based on trust levels. F-PKI thus supports a property that is sorely needed in today's Internet: trust heterogeneity. Different parties can express different trust preferences while still being able to verify all certificates. In contrast, today's web PKI only allows clients to fully distrust suspicious/misbehaving CAs, which is likely to cause collateral damage in the form of legitimate certificates being rejected. Our contribution is to present a system that is backward compatible, provides sensible security properties to both clients and domain owners, ensures the verifiability of all certificates, and prevents downgrade attacks. Furthermore, F-PKI provides a ground for innovation, as it gives CAs an incentive to deploy new security measures to attract more customers, without having these measures undercut by vulnerable CAs., Comment: Network and Distributed System Security Symposium (NDSS) 2022

Path-aware networks (PANs) are emerging as an intriguing new paradigm with the potential to significantly improve the dependability and efficiency of networks. However, the benefits of PANs can only be realized if the adoption of such architectures is economically viable. This paper shows that PANs enable novel interconnection agreements among autonomous systems, which allow to considerably improve both economic profits and path diversity compared to today's Internet. Specifically, by supporting packet forwarding along a path selected by the packet source, PANs do not require the Gao-Rexford conditions to ensure stability. Hence, autonomous systems can establish novel agreements, creating new paths which demonstrably improve latency and bandwidth metrics in many cases. This paper also expounds two methods to set up agreements which are Pareto-optimal, fair, and thus attractive to both parties. We further present a bargaining mechanism that allows two parties to efficiently automate agreement negotiations., Comment: 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)

To address the rising demand for strong packet delivery guarantees in networking, we study a novel way to perform graph resource allocation. We first introduce allocation graphs, in which nodes can independently set local resource limits based on physical constraints or policy decisions. In this scenario we formalize the distributed path-allocation (PAdist) problem, which consists in allocating resources to paths considering only local on-path information -- importantly, not knowing which other paths could have an allocation -- while at the same time achieving the global property of never exceeding available resources. Our core contribution, the global myopic allocation (GMA) algorithm, is a solution to this problem. We prove that GMA can compute unconditional allocations for all paths on a graph, while never over-allocating resources. Further, we prove that GMA is Pareto optimal with respect to the allocation size, and it has linear complexity in the input size. Finally, we show with simulations that this theoretical result could be indeed applied to practical scenarios, as the resulting path allocations are large enough to fit the requirements of practically relevant applications.

Current probabilistic flow-size monitoring can only detect heavy hitters (e.g., flows utilizing 10 times their permitted bandwidth), but cannot detect smaller overuse (e.g., flows utilizing 50-100% more than their permitted bandwidth). Thus, these systems lack accuracy in the challenging environment of high-throughput packet processing, where fast-memory resources are scarce. Nevertheless, many applications rely on accurate flow-size estimation, e.g. for network monitoring, anomaly detection and Quality of Service. We design, analyze, implement, and evaluate LOFT, a new approach for efficiently detecting overuse flows that achieves dramatically better properties than prior work. LOFT can detect 1.5x overuse flows in one second, whereas prior approaches fail to detect 2x overuse flows within a timeout of 300 seconds. We demonstrate LOFT's suitability for high-speed packet processing with implementations in the DPDK framework and on an FPGA.

By delegating path control to end-hosts, future Internet architectures offer flexibility for path selection. However, there is a concern that the distributed routing decisions by end-hosts, in particular load-adaptive routing, can lead to oscillations if path selection is performed without coordination or accurate load information. Prior research has addressed this problem by devising path-selection policies that lead to stability. However, little is known about the viability of these policies in the Internet context, where selfish end-hosts can deviate from a prescribed policy if such a deviation is beneficial fromtheir individual perspective. In order to achieve network stability in future Internet architectures, it is essential that end-hosts have an incentive to adopt a stability-oriented path-selection policy. In this work, we perform the first incentive analysis of the stability-inducing path-selection policies proposed in the literature. Building on a game-theoretic model of end-host path selection, we show that these policies are in fact incompatible with the self-interest of end-hosts, as these strategies make it worthwhile to pursue an oscillatory path-selection strategy. Therefore, stability in networks with selfish end-hosts must be enforced by incentive-compatible mechanisms. We present two such mechanisms and formally prove their incentive compatibility., Comment: 38th International Symposium on Computer Performance, Modeling, Measurements and Evaluation (PERFORMANCE 2020)

Byzantine fault tolerant protocols enable state replication in the presence of crashed, malfunctioning, or actively malicious processes. Designing such protocols without the assistance of verification tools, however, is remarkably error-prone. In an adversarial environment, performance and flexibility come at the cost of complexity, making the verification of existing protocols extremely difficult. We take a different approach and propose a formally verified consensus protocol designed for a specific use case: secure logging. Our protocol allows each node to propose entries in a parallel subroutine, and guarantees that correct nodes agree on the set of all proposed entries, without leader election. It is simple yet practical, as it can accommodate the workload of a logging system such as Certificate Transparency. We show that it is optimal in terms of both required rounds and tolerable faults. Using Isabelle/HOL, we provide a fully machine-checked security proof based upon the Heard-Of model, which we extend to support signatures. We also present and evaluate a prototype implementation., Comment: International Symposium on Reliable Distributed Systems (SRDS) 2020

Path selection by selfish agents has traditionally been studied by comparing social optima and equilibria in the Wardrop model, i.e., by investigating the Price of Anarchy in selfish routing. In this work, we refine and extend the traditional selfish-routing model in order to answer questions that arise in emerging path-aware Internet architectures. The model enables us to characterize the impact of different degrees of congestion information that users possess. Furthermore, it allows us to analytically quantify the impact of selfish routing, not only on users, but also on network operators. Based on our model, we show that the cost of selfish routing depends on the network topology, the perspective (users versus network operators), and the information that users have. Surprisingly, we show analytically and empirically that less information tends to lower the Price of Anarchy, almost to the optimum. Our results hence suggest that selfish routing has modest social cost even without the dissemination of path-load information., Comment: 27th International Colloquium on Structural Information and Communication Complexity (SIROCCO 2020)