Proactive Network Verification with 5STARS
|
ABSTRACT Modern military and enterprise systems increasingly depend on traditional enterprise networks combined with (or managed by) complex, software-defined networking (SDN) infrastructures spanning tactical, enterprise, and coalition environments. While technologies such as SDN and 5G offer unprecedented flexibility and adaptability, they also introduce significant operational complexity and expanded attack surfaces—which is of particular concern in contested and rapidly changing environments. Existing network monitoring approaches are largely reactive, detecting failures or security violations only after traffic has already been impacted. This lag undermines resilience, survivability, and operator confidence in mission-critical networks. This talk presents 5STARS, a vendor-agnostic, formally grounded network verification and monitoring system that enables dynamic and proactive assurance of network reliability and security. 5STARS continuously analyzes network forwarding configurations using automated reasoning to exhaustively model every path that every packet can take through a deployed network. Built on NetKAT [1, 2], a foundational mathematical theory of network behavior, 5STARS proves key properties such as reachability, isolation, confidentiality, and integrity across enterprise, tactical, software-defined and 5G network stacks—without sending or sampling live traffic. Unlike traditional monitoring tools, 5STARS detects misconfigurations, policy violations, and security flaws at configuration time, including those caused by operator error, software bugs, or malicious manipulation. When violations are found, the system produces actionable diagnostic artifacts, including counterexample traces that explain root causes and support rapid remediation. We present performance and scalability results demonstrating analysis of mid-sized operational networks in seconds, along with recent advances in counterexample generation and root cause analysis that improve operator usability. The talk also reports on real-world transition experience across multiple high-consequence application domains. We describe the application of this technology within the ARPA-H UPGRADE program to analyze the security and resilience of hospital and healthcare networks, where misconfigurations can directly impact patient safety, privacy, and continuity of care. In this setting, proactive verification enables continuous assurance of segmentation, reachability, and policy compliance across heterogeneous clinical and IT infrastructures. We also briefly touch on work under the DARPA PWND² program, applying formal network modeling and verification to hidden and overlay communication systems spanning traditional and nontraditional network substrates. These case studies highlight how mathematically grounded analysis can improve confidence in emergent communication pathways, support detection of unintended information flows, and strengthen assurance of privacy and survivability properties in complex, evolving network architectures. This work exemplifies the Beyond AI theme of HCSS by showing how classical formal methods can be transitioned into practical, high-impact operational tools that materially improve the reliability, resilience, and security of critical networked systems. The results demonstrate that proactive, mathematically based assurance is not only feasible at operational scale, but essential for building high-confidence software-intensive systems in contested environments. 1. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole 2. Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, |
|
BIO Dr. Cole Schlesinger is a Principal Scientist at Galois, Inc. with over fifteen years of experience leading research and transition efforts in programming languages, formal methods, network systems, and security. He has led multi-agency government programs for DARPA, ONR, and ARPA-H, directing technical vision, systems architecture, customer engagement, and transition strategy from concept development through deployable, mission-focused deliverables. His expertise spans type systems, operational semantics, program logics, compiler construction, and network verification, with experience translating foundational research into operational capabilities at companies ranging from small startups (Akita Software, Barefoot Networks) to large, publicly-traded companies (Amazon Web Services, Samsung Research). Cole has a publication record in top-tier venues including PLDI, POPL, SIGCOMM, NSDI, and OOPSLA, and has served on major program committees across the programming languages and systems communities. He holds a Ph.D. from Princeton University and a B.S. from Ithaca College. |