Research Directions in Formal Verification of Network Configurations Toward Verification of Mobile Networks

被引：0
作者：
Sakurada, Hideki [1 ,2 ]
Sakurai, Kouichi [2 ,3 ]
机构：
[1] NTT Corp, Tokyo, Japan
[2] Kyushu Univ, Fukuoka, Japan
[3] Adv Telecommun Res Inst Int, Kyoto, Japan
来源：
MOBILE INTERNET SECURITY, MOBISEC 2023 | 2024年 / 2095卷
关键词：
formal verification; network configuration; software-defined networking;
D O I：
10.1007/978-981-97-4465-7_18
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper reviews current research trends in the formal verification of computer network configurations, specifically focusing on formal verification for software-defined networking (SDN). We explore the challenges encountered when applying formal verification, comparing its application to pre-SDN network verification efforts. Additionally, we discuss the potential application of formal verification in mobile networks. We first provide an overview of research on the formal verification of virtual LAN (VLAN) configurations, which predates the emergence of SDN. We next illustrate SDN and existing research applying formal verification to SDN. Finally, we briefly examine potential scenarios for applying formal verification to mobile networks.
引用
收藏
页码：248 / 259
页数：12
相关论文
共 50 条
[41]   Formal Verification of Developer Tests: A Research Agenda Inspired by Mutation Testing [J].
Demeyer, Serge ;
Parsai, Ali ;
Vercammen, Sten ;
van Bladel, Brent ;
Abdi, Mehrdad .
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: ENGINEERING PRINCIPLES, ISOLA 2020, PT II, 2020, 12477 :9-24
[42]   QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks [J].
Zhang, Yedi ;
Zhao, Zhe ;
Chen, Guangke ;
Song, Fu ;
Zhang, Min ;
Chen, Taolue ;
Sun, Jun .
PROCEEDINGS OF THE 37TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, ASE 2022, 2022,
[43]   Verifying and Improving Neural Networks Using Testing-Based Formal Verification [J].
Liu, Haiyi ;
Liu, Shaoying ;
Liu, Ai ;
Fang, Dingbang ;
Xu, Guangquan .
STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2022, 2023, 13854 :126-141
[44]   Formal verification of synchronous data-flow program transformations toward certified compilers [J].
Van Chan Ngo ;
Jean-Pierre Talpin ;
Thierry Gautier ;
Paul Le Guernic ;
Loïc Besnard .
Frontiers of Computer Science, 2013, 7 :598-616
[45]   Formal verification of synchronous data-flow program transformations toward certified compilers [J].
Van Chan Ngo ;
Talpin, Jean-Pierre ;
Gautier, Thierry ;
Le Guernic, Paul ;
Besnard, Loic .
FRONTIERS OF COMPUTER SCIENCE, 2013, 7 (05) :598-616
[46]   Toward AI-Augmented Formal Verification: A Preliminary Investigation of ENGRU and Its Challenges [J].
Dechsupa, Chanon ;
Panboonyuen, Teerapong ;
Vatanawood, Wiwat ;
Padungweang, Praisan ;
So-In, Chakchai .
IEEE ACCESS, 2025, 13 :84357-84379
[47]   Formal Verification of Virtual Network Function Graphs in an SP-DevOps Context [J].
Spinoso, Serena ;
Virgilio, Matteo ;
John, Wolfgang ;
Manzalini, Antonio ;
Marchetto, Guido ;
Sisto, Riccardo .
SERVICE ORIENTED AND CLOUD COMPUTING, ESOCC 2015, 2015, 9306 :253-262
[48]   Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method [J].
Ouranos, Iakovos ;
Stefaneas, Petros ;
Ogata, Kazuhiro .
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT I, 2010, 6415 :75-+
[49]   Research on method of formal design and verification of memory management based on microkernel architecture [J].
Qian Z.-J. ;
Liu Y.-J. ;
Yao Y.-F. ;
Tang L. ;
Huang H. ;
Song F.-M. .
Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2017, 45 (01) :251-256
[50]   Formal Verification of Authorization Policies for Enterprise Social Networks Using PlusCal-2 [J].
Akhtar, Sabina ;
Zahoor, Ehtesham ;
Perrin, Olivier .
COLLABORATIVE COMPUTING: NETWORKING, APPLICATIONS AND WORKSHARING, COLLABORATECOM 2017, 2018, 252 :530-540
12345