Checking Dynamic Policies in Stateful Next-Generation Networks

Project Overview

The security, performance, and availability of our critical network infrastructures relies on the correct implementation of different policy goals. Network operators realize these goals by composing and configuring diverse network appliances such as routers, firewalls, intrusion prevention systems, and web proxies. Unfortunately, this process of managing networks is extremely challenging, error-prone, and entails significant manual effort and operational costs. Configuration and implementation errors could have significant consequences as it can degrade network performance, induce downtime for critical infrastructures, and cause violations of key security postures. Systematically identifying and diagnosing potential violations has been, and continues to be, a fundamental challenge. This project will develop a principled framework to check if a network setup correctly implements a given suite of policies and to help operators proactively and automatically diagnose and localize the sources of policy violations. Checking policy violations is hard even for simple reachability properties (e.g., can A talk to B) in today's networks. Furthermore, next-generation technologies such as software-defined networking and network functions virtualization are poised to enable richer dynamic policies (e.g., if a host generates too many connections, subject it to deeper inspection) and also introduce new sources of complexity (e.g., elastic scaling, software bugs). Existing approaches in network testing and verification have fundamental expressiveness and scalability challenges in tackling dynamic policies and stateful elements. To address these challenges, the research will include developing a model-based testing framework that will lead to fundamental advances in network semantics, modeling, testing, and diagnosis.


  • PI: Vyas Sekar
  • PhD Students: Seyed Fayaz (graduated), Soo-jin Moon, Tianlong Yu
  • Postdoc: Yifei Yuan (graduated)
  • MS students: Tushar Sharma (graduated), Jeffrey Helt (graduated), Yves Bieri (visiting/graduated)
  • Collaborators: Sagar Chaki (SEI), Limin Jia (CMU), Sujata Banerjee (VMWare)
  • High school: Matthew Zhou
  • Papers

  • [NSDI] Alembic: Automated Model Inference for Stateful Network Functions
    Soo-Jin Moon, Jeffrey Helt, Yifei Yuan, Yves Bieri, Sujata Banerjee, Vyas Sekar, Wenfei Wu, Mihalis Yannakakis, Ying Zhang
    in NSDI 2019
  • [NSDI] Efficient and Correct Test Scheduling for Ensembles of Stateful Network Policies
    Yifei Yuan, Sanjay Chandrasekaran, Limin Jia, Vyas Sekar
    in NSDI 2018
  • [OSDI] Efficient Network Reachability Analysis using a Succinct Control Plane Representation
    Seyed K. Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, and George Varghese
    in USENIX OSDI, 2016
  • [NSDI] BUZZ: Testing Context-Dependent Policies in Stateful Networks
    Seyed K Fayaz, Tianlong Yu, Yoshiaki Tobioka, Sagar Chaki, Vyas Sekar
    in NSDI 2016
  • [HotSDN] Testing Stateful and Dynamic Dataplanes with FlowTest
    Seyed Kaveh Fayazbakhsh, Vyas Sekar
    in HotSDN 2014 slides
  • [NSDI] Enforcing Network-Wide Policies in the Presence of Dynamic Middlebox Actions using FlowTags
    Seyed Fayazbakhsh, Vyas Sekar, Minlan Yu, Jeff Mogul
    in NSDI 2014 slides


    Source code for Buzz
    Source code for Mikado (to be added soon)


  • Game for teaching network security and testing, by Matthew Zhou (Coming Up!)
  • CMU CIT article


    This work is supported by NSF CAREER Award 1552481