2015/05/13 by Seyed K. Fayaz, Yoshiaki Tobioka, Fayaz, Seyed K. +5
Computer Science · Engineering · #FOS: Computer and information sciences #Ferroelectric and Negative Capacitance Devices #Networking and Internet Architecture (cs.NI) #Software System Performance and Reliability #Software-Defined Networks and 5G #cs.NI
paper · pdf · doi:10.48550/arxiv.1505.03356
openalex publication_date 2015/05/13 · arxiv created 2015/06/09 · arxiv updated 2015/06/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Network operators today spend significant manual effort in ensuring and checking that the network meets their intended policies. While recent work in network verification has made giant strides to reduce this effort, they focus on simple reachability properties and cannot handle context-dependent policies (e.g., how many connections has a host spawned) that operators realize using stateful network functions (NFs). Together, these introduce new expressiveness and scalability challenges that fall outside the scope of existing network verification mechanisms. To address these challenges, we present Armstrong, a system that enables operators to test if network with stateful data plane elements correctly implements a given context-dependent policy. Our design makes three key contributions to address expressiveness and scalability: (1) An abstract I/O unit for modeling network I/O that encodes policy-relevant context information; (2) A practical representation of complex NFs via an ensemble of finite state machines abstraction; and (3) A scalable application of symbolic execution to tackle state space explosion. We demonstrate that Armstrong is several orders of magnitude faster than existing mechanisms.