检索结果-内蒙古大学图书馆

IEEE TRANSACTIONS ON NETWORKING 2025年第3期33卷 1279-1294页

作者： Wang, Jingyu Zhao, Chenyang Zhuang, Zirui Qi, Qi Guo, Yuebin Sun, Haifeng Guo, Lingqi Liao, Jianxin Beijing Univ Posts & Telecommun State Key Lab Networking & Switching Technol Beijing 100876 Peoples R China Pengcheng Lab Shenzhen 518000 Peoples R China Ebyte com Beijing 100191 Peoples R China

There is an increasing interest in data plane verification, which is designed to automatically verify network correctness through directly analyzing the data plane. Recent data plane verifiers have been able to do real-time sub-millisecond per rule verification. However, we observe that in real-world networks, individual data plane updates rarely occur. On the contrary, there are always a certain number of updates generated in a short period of time, called as burst updates, due to high-level user intend or uncertain network events. When it comes to this real-life scenario, yet, the current equivalence class (EC) based methods are unable to solve the model-wide changes problem caused by the EC itself, which significantly slows down the verification speed of burst updates. To overcome this limitation, we present EPVerifier, a fast, scalable data plane verifier accelerating burst updates verification with edge-predicate (EP). Instead of classifying packets into ECs according to global forwarding behavior, the EPVerifier uses one EP per edge to represent all packets that can pass through. Furthermore, with EPs that clearly have localized properties, we introduce a rule type extension that does not require a change in the granularity of the network model to support ACLs and NATs that are prevalent in real devices, and obtain better-performing parallelism by dividing the verification task based on switches. Experiments on both dataset simulations and real-life deployments show that EPVerifier achieves 2-10x faster data plane verification than the state-of-the-art and such advantage expand with the data plane's complexity and update scale growth.

关键词： data models Telecommunications Switches Firewalls (computing) Sun Process control Optimization Directed graphs Telecommunication traffic Technological innovation Automated tools formal methods network management data plane verification burst updates

来源：评论

学校读者我要写书评

暂无评论

Scaling data plane verification via Parallelization 8

Scaling Data Plane Verification via Parallelization

引用

8th Asia-Pacific Workshop on Networking (APNET)

作者： Wen, Sisi Abhashkumar, Anubhavnidhi Zhao, Chenyang Jiang, Weirong ByteDance Beijing Peoples R China Beijing Univ Posts & Telecommun Beijing Peoples R China

ISBN: (纸本)9798400717581

The data plane verification of networks in hyperscale environments is challenging due to the complexity and size of modern networks. In this paper, we introduce Medusa, a novel verifier that efficiently analyzes large data plane models using parallel processing on multi-core CPUs. First, we propose a new data structure called RANGESET, which overcomes the parallelism limitations of existing popular data structures such as Binary Decision Diagrams (BDD) used in data plane verifiers. Next, we leverage multi-core processing by dividing the network into distinct groups and assigning each group to a separate thread for computation. The results are then integrated for comprehensive verification. By optimizing the use of multi-core systems, we enhance computational efficiency and accelerate the verification process. Experimental results demonstrate that Medusa outperforms existing tools in terms of speed and memory. For instance, in a network with O(10K) devices and O(1M) forwarding rules, Medusa can detect loops in approximately 5 seconds, outperforming other data plane Verifiers (DPVs) where some cannot model and analyze the network. Moreover, in networks that we could compare with other state-of-the-art DPVs, Medusa provides a substantial improvement, with speedups up to 600X, 4000X, and 800X compared to alternatives like Flash, APKeep, and Tulkun, respectively.

关键词： data plane verification Parallelization Hyperscale Network

来源：评论

学校读者我要写书评

暂无评论

Enhancing Network data plane Analysis with Native Graph database

Enhancing Network Data Plane Analysis with Native Graph Data...

引用

IEEE/IFIP Network Operations and Management Symposium (NOMS)

作者： Abane, Amar Battou, Abdella Merzouki, Mheni NIST Gaithersburg MD 20899 USA

ISBN: (纸本)9798350327939;9798350327946

As modern networks grow in complexity, ensuring their reliability and security becomes increasingly vital. data plane analysis is a key process for verifying network behavior, but traditional data plane analysis tools face challenges in extensibility, customization, and interoperability. This paper explores the potential of implementing a data plane analysis system on a general-purpose native graph database, to create a more uniform and insightful approach to network verification and analysis. Using the graph database query language and built-in graph algorithms, we simplify the network forwarding analysis while enhancing its features. Our study offers practical insights into managing complex networks, promising more efficient and intuitive tools on the horizon.

关键词： network management data plane verification knowledge graph SDN Neo4j graph database graph algorithms

来源：评论

学校读者我要写书评

暂无评论

Toward Highly Reliable Programmable data planes: verification of P4 Code Generation 9

Toward Highly Reliable Programmable Data Planes: Verificatio...

引用

9th IEEE International Conference on Network Softwarization (IEEE NetSoft) - Boosting Future Networks through Advanced Softwarization

作者： Gyoergyi, Csaba Laki, Sandor Schmid, Stefan Univ Vienna Vienna Austria Eotvos Lorand Univ Budapest Hungary TU Berlin Berlin Germany Fraunhofer SIT Darmstadt Germany

ISBN: (纸本)9798350399806

data plane programming gained much attention in the past years, having a fast-growing community both in academia and industry. Many tools have emerged to simplify and/or help the development of reliable data plane programs, including fuzzing, formal verification, and different code generators. However, even the tools themselves must be verified to meet the most stringent dependability requirements. In this paper, we investigate various tools and methods to verify code generators leveraging P4 through the example of P4RROT (an open source code generator focusing on the application layer). We show that our approach is efficient and can indeed successfully find bugs. We identify two bugs and propose reusable ideas, such as the use of ghost code.

关键词： code generation in-network computing data plane verification P4

来源：评论

学校读者我要写书评

暂无评论

Improving the Formal verification of Reachability Policies in Virtualized Networks

引用

IEEE TRANSACTIONS ON NETWORK AND SERVICE MANAGEMENT 2021年第1期18卷 713-728页

作者： Bringhenti, Daniele Marchetto, Guido Sisto, Riccardo Spinoso, Serena Valenza, Fulvio Yusupov, Jalolliddin Politecn Torino Dipartimento Automat & Informat I-10129 Turin Italy Turin Polytech Univ Dept Automat Control & Comp Engn Tashkent 100095 Uzbekistan

Network Function Virtualization (NFV) and Software Defined Networking (SDN) are new emerging paradigms that changed the rules of networking, shifting the focus on dynamicity and programmability. In this new scenario, a very important and challenging task is to detect anomalies in the data plane, especially with the aid of suitable automated software tools. In particular, this operation must be performed within quite strict times, due to the high dynamism introduced by virtualization. In this article, we propose a new network modeling approach that enhances the performance of formal verification of reachability policies, checked by solving a Satisfiability Modulo Theories (SMT) problem. This performance improvement is motivated by the definition of function models that do not work on single packets, but on packet classes. Nonetheless, the modeling approach is comprehensive not only of stateless functions, but also stateful functions such as NATs and firewalls. The implementation of the proposed approach achieves high scalability in complex networked systems consisting of several heterogeneous functions.

关键词： Task analysis Virtualization Tools Scalability Network function virtualization Middleboxes Testing Network reachability data plane verification service function chains network security policies

来源：评论

学校读者我要写书评

暂无评论

Adversarial Exploitation of P4 data planes 17

Adversarial Exploitation of P4 Data Planes

引用

IFIP/IEEE International Symposium on Integrated Network Management (IM)

作者： Black, Conor Scott-Hayward, Sandra Queens Univ Ctr Secure Informat Technol Belfast Antrim North Ireland

ISBN: (纸本)9783903176324

Programmable data planes can support flexible and feature-rich networks. However, the network operator must have confidence that the network data plane correctly implements the specified policies. To address this, data plane testing and verification mechanisms have been proposed, which, in general, trust the data plane devices to behave faithfully. A few current solutions recognise that one or more of the network devices may be under the control of a malicious adversary but do not address either the enhanced capabilities or motivations of an attacker in a modern P4-programmable data plane. Furthermore, the ability of an attacker to utilise these enhanced capabilities in an exploit has not been investigated. In this paper, we address this knowledge gap by means of a case study in which we assume the role of an attacker in an open-source implementation of a P4-programmable software switch and attempt a range of methods to exploit the program running on that switch. We find that attacks that exploit both the programmability and statefulness of the P4 switch are indeed possible, and discuss the impact of our findings with proposals for future adversarial data plane verification mechanisms to address this new threat model.

关键词： P4 Programmable data planes data plane verification Software-Defined Networks

来源：评论

学校读者我要写书评

暂无评论

SymNet: scalable symbolic execution for modern networks 16

SymNet: scalable symbolic execution for modern networks

引用

ACM Conference on Special Interest Group on data Communication (SIGCOMM)

作者： Stoenescu, Radu Popovici, Matei Negreanu, Lorina Raiciu, Costin Univ Politehn Bucuresti Splaiul Independentei 313 Bucharest Romania

ISBN: (纸本)9781450341936

We present SymNet, a network static analysis tool based on symbolic execution. SymNet injects symbolic packets and tracks their evolution through the network. Our key novelty is SEFL, a language we designed for expressing data plane processing in a symbolic-execution friendly manner. SymNet statically analyzes an abstract data plane model that consists of the SEFL code for every node and the links between nodes. SymNet can check networks containing routers with hundreds of thousands of prefixes and NATs in seconds, while verifying packet header memory-safety and covering network functionality such as dynamic tunneling, stateful processing and encryption. We used SymNet to debug middle-box interactions from the literature, to check properties of our department's network and the Stanford backbone. Modeling network functionality is not easy. To aid users we have developed parsers that automatically generate SEFL models from router and switch tables, firewall configurations and arbitrary Click modular router configurations. The parsers rely on prebuilt models that are exact and fast to analyze. Finally, we have built an automated testing tool that combines symbolic execution and testing to check whether the model is an accurate representation of the real code.

关键词： data plane verification symbolic execution SymNet

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：