The 3rd ACM SIGCOMM Workshop on Formal Methods Aided Network Operation (FMANO)

Title: Can We Verify 5G Networks?

Abstract: 5G networks are at the cutting edge of network technology today. Their high-value services make them a focus for investment, development, and innovation. And as their complexity and usage for safety-critical applications expand, their reliability and accountability will become a growing concern. This talk considers how they might be made verifiable, by beginning with a top-down model of 5G based on Compositional Network Architecture.

Speaker: Pamela Zave (Princeton University)

Pamela Zave is a researcher with the Computer Science Department of Princeton University, having held previous positions at the University of Maryland, Bell Labs, and AT&T Labs. She is an ACM Fellow, an IFIP Fellow, an AT&T Fellow, and the 2017 recipient of the IEEE Harlan D. Mills Award for sustained contributions to the theory and practice of software engineering. At AT&T, she led a group that implemented the enhanced features for AT&T's first public voice-over-IP offering. Her book, "The Real Internet Architecture: Past, Present, and Future Evolution," was recently published by Princeton University Press.

9:30am-9:40am

An Automatic HCPN Modeling Method for Microservice-Orchestrated Network Operation Workflows

Guoshuai Li, Tao Sun, Wenjie Zhong (Inner Mongolia University)

9:40am-9:50am

SemDNS: A Declarative Semantics for DNS Resolution

Kaiqiang Hu, Haizhou Du (Shanghai University of Electric Power); Kexin Yu (Xiamen University); Xiaoliang Wang (Nanjing University)

9:50am-10:00am

LST-Sim: An Efficient Simulation Platform for Large-Scale Model Training

Siwei Ji, Yihao Sun, Bo Lei, Jing Tang, Yongchen Pan, Ziheng Xu, Xiaoting Ma, Yue Zhang (China Telecom Research Institute)

10:00am-10:10am

Explaining Network Configurations Under Failures via Localized Subspecifications

Yaxuan Lin, Yongzheng Zhang (ShanghaiTech University); Haoxian Chen (Shanghai Tech University)

10:10am-10:20am

IntentP4: Bridging P4 Temporal Specifications and Executable Network Tests

Ruonan Feng, Mingming Zhang, Yu Jiang, Shijie Gao, Yaping Liu, Shuo Zhang (School of Cybersecurity, Guangzhou University)

10:20am-10:25am

Chameleon: Toward Runtime-Pluggable Verification of Programmable Networks

Ying Yao, Le Tian, Yuxiang Hu (Information Engineering University)

Title: Network Verification at Hyperscale: Lessons Learned and Open Challenges

Abstract: Formal verification has become one of the most effective tools for keeping large-scale networks correct and available, catching misconfigurations before they can cause outages that ripple across millions of users. In this talk I will recount our experience deploying verification in Microsoft's Azure cloud network, detailing how it has grown into a production system that today gates live configuration changes across both the physical datacenter network and the virtual networks that run on top of it. I will describe the suite of new techniques that made verification work at this scale, including digital twins to faithfully replicate network behavior, modular verification to scale beyond monolithic analysis, and new ways to specify correctness itself. Along the way I will share some practical lessons this experience has taught us, as well as the open challenges that remain.

Speaker: Ryan Beckett (Microsoft Research)

Ryan Beckett is a Principal Researcher at Microsoft working in the area of network reliability. He graduated with his PhD from Princeton in 2018 after working with his advisor David Walker, and has been at Microsoft since. While a graduate student, Ryan was a recipient of the Google Fellowship. In addition, his PhD thesis on network verification and synthesis went on to win awards spanning both the networking and programming languages communities, including the SIGCOMM 2018 dissertation award in networking and the John C. Reynolds dissertation award in Programming Languages, as well as the ACM dissertation honorable mention award, recognizing the best PhD theses across all of computer science. His research interests lie primarily at the intersection of programming languages and networks, and he is broadly interested in topics spanning compilers, verification, static analysis, and distributed systems.

11:20am-11:30am

Lynx: Queueing-theoretic Congestion Control Robust to Large Number of Flows

Satoshi Utsumi, Salahuddin Muhammad Salim Zabir (Fukushima University); Go Hasegawa (Tohoku University)

11:30am-11:40am

A Unifying Framework for Streaming Query Languages

Anthony Dario, Chris Misa, Zena M. Ariola (University of Oregon)

11:40am-11:50pm

Characterization of destination-based routing via an algebraic property of cycles

Rulin Zhang, Hui Dong, Ju Zhang, Hua Li (College of Computer Science, Inner Mongolia University)

11:50pm-12:00pm

Tree-based Publish-Subscribe Model and Load Partition for Distributed Object System

Lujia Yin, Zhongxiang Dai (National University of Defense Technology); Hailiang Chen, Xiufen Fu, Menglong Lu, Chuan Ai (National University of Defence Technology)

12:00pm-12:10pm

Investigating Neuro-Symbolic AI for Context-Aware Process Classification with MITRE ATT&CK

Omar Anser, Léo Lavaur, Jerome Francois (University of Luxembourg)