Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1311.4303

Applying Formal Methods to Networking: Theory, Techniques and Applications

Junaid Qadir·Osman Hasan
View original source ↗Read source document ↗Export metadata ↓

Abstract

Despite its great importance, modern network infrastructure is remarkable for the lack of rigor in its engineering. The Internet which began as a research experiment was never designed to handle the users and applications it hosts today. The lack of formalization of the Internet architecture meant limited abstractions and modularity, especially for the control and management planes, thus requiring for every new need a new protocol built from scratch. This led to an unwieldy ossified Internet architecture resistant to any attempts at formal verification, and an Internet culture where expediency and pragmatism are favored over formal correctness. Fortunately, recent work in the space of clean slate Internet design---especially, the software defined networking (SDN) paradigm---offers the Internet community another chance to develop the right kind of architecture and abstractions. This has also led to a great resurgence in interest of applying formal methods to specification, verification, and synthesis of networking protocols and applications. In this paper, we present a self-contained tutorial of the formidable amount of work that has been done in formal methods, and present a survey of its applications to networking.

Explore related subjects

cs.NIcs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Junaid Qadir, Osman Hasan. 2013-11-18. Applying Formal Methods to Networking: Theory, Techniques and Applications. https://doi.org/10.1109/comst.2014.2345792

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Where Have All the Firewalls Gone? Security Consequences of Residential IPv6 Transition

IPv4 NAT has limited the spread of IoT botnets considerably by default-denying bots' incoming connection requests to in-home devices unless the owner has explicitly allowed them. As the Internet transitions to majority IPv6, however, residential connections no longer require the use of NAT. This paper therefore asks: has the transition from IPv4 to IPv6 ultimately made residential networks more vulnerable to attack, thereby empowering the next generation of IPv6-based IoT botnets? To answer this question, we introduce a large-scale IPv6 scanning methodology that, unlike those that rely on computationally intensive algorithms, can be run on low-resource devices common in IoT botnets. We use this methodology to perform the largest-scale measurement of IPv6 residential networks to date, and compare which devices are publicly accessible to comparable IPv4 networks. We received responses from 93,832,220 distinct IPv6 addresses, 14,901,892 of which are inside of residential networks (i.e., not the external-facing gateway IP). These residential network internal addresses span 4,412 ASes across 144 countries. These responses come from protocols commonly exploited by IoT botnets (including telnet and FTP), as well as protocols typically associated with end-user devices (including iPhone-Sync and IPP). Compared with IPv4, we reach 11x more HP printers over IPv6 than Shodan finds across the entire IPv4 Internet, and thousands of iPhones and smart lights whose services IPv4 NAT made unreachable by default. Collectively, our results show that NAT has indeed acted as the de facto firewall of the Internet, and the IPv4-to-IPv6 transition of residential networks is opening up new devices to attack. Finally, we discuss potential mitigations to prevent in-home network reachability as IPv6 adoption continues to grow.

cs.NI↗
arXiv2026

Burst-mode timing recovery based on fourth-power phase detector for passive optical networks

Driven by the ever-increasing capacity demands, 50G passive optical network (50G-PON) is ready for practical application. It is highly challenging to realize 50GHz burst-mode analog components; therefore, based on 25GHz burst-mode analog devices, burst-mode digital signal processing (DSP) is introduced to achieve the reception and processing of 50Gb/s on-off keying burst signals. To optimize the power consumption and area of the DSP chip, a one-sample-per-symbol (1-SPS) analog-to-digital converter has been applied in 50G-PON. One of the main challenges is implementing burst-mode timing recovery (BM-TR) for the 1-SPS burst signal in 50G-PON. In this paper, we first propose a BM-TR based on the fourth-power phase detector (4PPD) for 50G-PON. We mathematically verify that 4PPD can directly compute the timing phase offset (TPO) from the 1-SPS signal without using training sequences, allowing for immediate BM-TR initialization within 20 cycles to prevent long convergence times. After the initialization, the feedback loop structure tracks the TPO changes based on the sign of 4PPD, the loop filter, and the numerically controlled oscillator. In conclusion, training-sequence-free 4PPD-based BM-TR achieves low burst overhead via fast convergence and is particularly effective for handling burst signals in 50G-PON.

cs.NI↗
arXiv2026

AI-Native Open RAN: A Roadmap from xApps and rApps to Autonomous Network Agents

Open Radio Access Networks (O-RAN) have emerged as a transformative paradigm for future wireless systems by introducing openness, virtualization, disaggregation, and programmable intelligence through the RAN Intelligent Controller (RIC). The availability of standardized interfaces and near-real-time control loops has created unprecedented opportunities for integrating artificial intelligence (AI) into radio access network management and optimization. Over the past several years, a broad range of AI techniques have been proposed to address key O-RAN challenges such as radio resource management, network slicing, traffic prediction, mobility management, interference mitigation, and spectrum sharing. Despite significant progress, existing solutions often remain task-specific, require extensive retraining, and exhibit limited generalization across deployment environments and network conditions. This paper presents a comprehensive review of AI-enabled O-RAN systems and provides a unifying perspective on the evolution of intelligence in wireless networks. We first examine the O-RAN architecture and the role of intelligence within near-real-time and non-real-time RIC frameworks. We then develop a taxonomy of AI approaches for O-RAN, covering machine learning, deep reinforcement learning (DRL), digital-twin-assisted optimization, and emerging foundation-model-based architectures.

cs.NI↗