Network Verification and Testing

New capabilities for stateful network verification

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.

  1. NSDI
    Don’t Yank My Chain: Auditable NF Service Chaining
    Liu, Grace, Sadok, Hugo, Kohlbrenner, Anne, Parno, Bryan, Sekar, Vyas, and Sherry, Justine
    In Proc. NSDI 2021
    PDF
  2. NSDI
    NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification
    Yuan, Yifei, Moon, Soo-Jin, Uppal, Sahil, Jia, Limin, and Sekar, Vyas
    In 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020, Santa Clara, CA, USA, February 25-27, 2020 2020
    PDF
  3. NSDI
    Alembic: Automated Model Inference for Stateful Network Functions
    Moon, Soo-Jin, Helt, Jeffrey, Yuan, Yifei, Bieri, Yves, Banerjee, Sujata, Sekar, Vyas, Wu, Wenfei, Yannakakis, Mihalis, and Zhang, Ying
    In 16th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2019, Boston, MA, February 26-28, 2019 2019
    PDF
  4. NSDI
    BUZZ: Testing Context-Dependent Policies in Stateful Networks
    Fayaz, Seyed Kaveh, Yu, Tianlong, Tobioka, Yoshiaki, Chaki, Sagar, and Sekar, Vyas
    In 13th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2016, Santa Clara, CA, USA, March 16-18, 2016 2016
    PDF
  5. OSDI
    Efficient Network Reachability Analysis Using a Succinct Control Plane Representation
    Fayaz, Seyed Kaveh, Sharma, Tushar, Fogel, Ari, Mahajan, Ratul, Millstein, Todd D., Sekar, Vyas, and Varghese, George
    In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016 2016
    PDF
  6. NSDI
    Efficient and Correct Test Scheduling for Ensembles of Network Policies
    Yuan, Yifei, Chandrasekaran, Sanjay, Jia, Limin, and Sekar, Vyas
    In 15th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2018, Renton, WA, USA, April 9-11, 2018 2018
    PDF