Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Seagull: Privacy preserving network verification system

Jaber Daneshamooz, Melody Yu, Sucheer Maddury

TL;DR

This paper addresses the challenge of privacy-preserving, scalable verification of BGP configurations across autonomous systems. It introduces Seagull, a framework based on secure multiparty computation (MPC) and additive secret sharing to verify loop-freedom, reachability, waypoint status, and policy conformance using only the boolean verification outcome. The approach combines an initial full verification with incremental updates, leveraging a 15-hop traversal bound and data-oblivious computation implemented on Scale-Mamba to protect routing data and access patterns. Evaluation on CAIDA AS-topology data shows practical performance for large networks (e.g., around 4,800 ASes) with incremental updates taking approximately 77 seconds, demonstrating the viability of private inter-domain verification for the Internet backbone. Seagull thus provides a secure foundation for verifying BGP-based routing while preserving confidentiality and enabling real-time policy checks.

Abstract

The Internet relies on routing protocols to direct traffic efficiently across interconnected networks, with the Border Gateway Protocol (BGP) serving as the core mechanism managing routing between autonomous systems. However, BGP configurations are largely manual, making them susceptible to human errors that can lead to outages or security vulnerabilities. Verifying the correctness and convergence of BGP configurations is therefore essential for maintaining a stable and secure Internet. Yet, this verification process faces two key challenges: preserving the privacy of proprietary routing information and ensuring scalability across large, distributed networks. This paper introduces a privacy-preserving verification framework that leverages multiparty computation (MPC) to validate BGP configurations without exposing sensitive routing data. Our approach overcomes both privacy and scalability challenges by ensuring that no information beyond the verification outcome is revealed. Through formal analysis, we show that the proposed method achieves strong privacy guarantees and practical scalability, providing a secure and efficient foundation for verifying BGP-based routing in the Internet backbone.

Seagull: Privacy preserving network verification system

TL;DR

This paper addresses the challenge of privacy-preserving, scalable verification of BGP configurations across autonomous systems. It introduces Seagull, a framework based on secure multiparty computation (MPC) and additive secret sharing to verify loop-freedom, reachability, waypoint status, and policy conformance using only the boolean verification outcome. The approach combines an initial full verification with incremental updates, leveraging a 15-hop traversal bound and data-oblivious computation implemented on Scale-Mamba to protect routing data and access patterns. Evaluation on CAIDA AS-topology data shows practical performance for large networks (e.g., around 4,800 ASes) with incremental updates taking approximately 77 seconds, demonstrating the viability of private inter-domain verification for the Internet backbone. Seagull thus provides a secure foundation for verifying BGP-based routing while preserving confidentiality and enabling real-time policy checks.

Abstract

The Internet relies on routing protocols to direct traffic efficiently across interconnected networks, with the Border Gateway Protocol (BGP) serving as the core mechanism managing routing between autonomous systems. However, BGP configurations are largely manual, making them susceptible to human errors that can lead to outages or security vulnerabilities. Verifying the correctness and convergence of BGP configurations is therefore essential for maintaining a stable and secure Internet. Yet, this verification process faces two key challenges: preserving the privacy of proprietary routing information and ensuring scalability across large, distributed networks. This paper introduces a privacy-preserving verification framework that leverages multiparty computation (MPC) to validate BGP configurations without exposing sensitive routing data. Our approach overcomes both privacy and scalability challenges by ensuring that no information beyond the verification outcome is revealed. Through formal analysis, we show that the proposed method achieves strong privacy guarantees and practical scalability, providing a secure and efficient foundation for verifying BGP-based routing in the Internet backbone.
Paper Structure (16 sections, 1 theorem, 8 figures, 7 tables, 1 algorithm)

This paper contains 16 sections, 1 theorem, 8 figures, 7 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Border Gateway Protocol
  4. FIB
  5. Existing Problems
  6. Contribution
  7. Methodology
  8. Input Representation and Sharing
  9. Basic Verification Tasks
  10. Loop Detection
  11. Algorithm Improvements
  12. Incremental Loop Detection (Query Phase)
  13. Threat Model and Privacy
  14. Evaluation
  15. Related works
  16. ...and 1 more sections

Key Result

Theorem 1

Let $G$ and $G'$ be trees with $m$ and $n$ nodes, respectively, and thus $m-1$ and $n-1$ edges. Adding an edge $E(u,v)$ where $u \in G$ and $v \in G'$ (or vice versa) results in a connected graph with $(m+n)$ nodes and $(m+n-1)$ edges, which is also a tree. This follows directly from Kruskal's minim

Figures (8)

  • Figure 1: BGP route computation process
  • Figure 2: BGP path selection algorithm networkslearning2020best
  • Figure 3: BGP customer-provider relation 10.5555/2584507
  • Figure 4: Policy change causing BGP loops at 2 and 3 when 4 withdraws a prefix from 2 and 3 but not 6 10.5555/1387589.1387614
  • Figure 5: Network topology and its corresponding forwarding graph of destination Dst(annotated in red)
  • ...and 3 more figures

Theorems & Definitions (3)

  • Theorem 1
  • Definition 1
  • Definition 2