An Automated Synthesis Framework for Network Security and Resilience Analysis

Investigators: Matt Caesar and Dong (Kevin) Jin

Researchers: Bingzhe Liu, Santhosh Prabhu and Xiaoliang Wu

Today’s quality of life is highly dependent on the successful operation of many complex and largescale computer networks, supporting military applications, social communications, power grid facilities, cloud services, and other critical infrastructures. However, a chasm has grown between the complexity of these systems and the increasing need for resilience and security. This gap is now reaching a tipping point, and in the coming years, the way networks are architected, built, monitored, and protected may change dramatically, and the SoS research community has the opportunity to significantly influence these advances.

We propose to develop the analysis methodology needed to support scientific reasoning about the resilience and security of networks, with a particular focus on network control and information/data flow. The core of this vision is an automated synthesis framework (ASF), which will automatically derive network state and repairs from a set of specified correctness requirements and security policies. ASF consists of a set of techniques for performing and integrating security and resilience analyses applied at different layers (i.e., data forwarding, network control, programming language, and application software) in a real-time and automated fashion. The ASF approach is exciting because developing it adds to the theoretical underpinnings of SoS, while using it supports the practice of SoS.

With ASF, we could achieve a better understanding of network behaviors through formal synthesis, verification, and analysis from individual components to the entire network; we could compare a system before and after a change in configurations to quantify security breaches (e.g., unauthorized access); we could automate synthesis of the network’s data plane state and the control logic to enable powerful capabilities, such as immediate response to faults (rather than reaction at human timescales); and we could prevent errors and vulnerabilities before they happen by exploring abstractions and software frameworks that would allow programmers to easily write applications that are resilient to cyber-attacks and human errors.

However, accomplishing that vision will be challenging. First, an efficient synthesizer must consider how policies across the network stack interact, and how they are susceptible to subversion. One challenge is to compose these analyses while recognizing the limits of that composition and develop new inter-layer analyses. Another challenge is to integrate resilience and security evidence gathered in different ways at different layers (e.g., formal proofs at one layer, with empirical or simulationbased evaluation at another). Second, generating solutions to constrained problems is in general more difficult than verifying solutions. It is challenging to scale synthesis to moderate or large networks on real-world tasks.

The project will leverage the research team’s past work to accelerate progress. In our prior SoS seedling projects, we developed data plane verification (DPV), a technique that verifies properties of the network’s forwarding behavior. The DPV approach has proven to be extremely fruitful. We developed the first real-time DPV system (ACM HotSDN’12 best paper, USENIX NSDI’13 and NSDI’15), made possible by our custom real-time formal methods algorithms. We applied DPV to the University of Illinois campus network with 240+ backbone routers supporting 70,000+ machines, and have discovered a variety of vulnerabilities, including a globally exploitable DoS vulnerability and inconsistent security policies. We also applied DPV to secure cyber-physical energy systems, including the Illinois Institute of Technology’s campus microgrid. The developed technology has also spawned a startup company employing over 25 people, which has multiple active and upcoming pilot projects within DoD and the commercial sector.

Overall, ASF will develop algorithms and systems for automated synthesis of network behavior and control logic to significantly improve network security and resilience. The proposed project covers four hard problems: (1) resilient architectures (primary), (2) scalability and composability, (3) policy-governed secure collaboration, and (4) security-metrics-driven evaluation, design, development, and deployment.

Hard Problems Addressed


  1. Yanfeng Qu, Xin Liu, Dong Jin, Yuan Hong, and Chen Chen, “Enabling a Resilient and Self-healing PMU Infrastructure Using Centralized Network Control”, 2018 ACM International Workshop on Security in Software Defined Networks & Network Function Virtualization (SDN-NFV Security), Tempe, AZ, March 21, 2018. [full text]
  2. Jiaqi Yan, Dong Ji, and Cheol Won Lee, ” A Comparative Study of Off-Line Deep Learning Based Network Intrusion Detection”, 10th International Conference on Ubiquitous and Future Networks (ICUFN), Prague, Czech Republic, July 3-6, 2018. [full text]
  3. Santhosh Prabhu, Gohar Ifran Chaudhry, Brighten Godfrey and Matthew Caesar, “High Coverage Testing of Softwarized Networks”, ACM SIGCOMM 2018 Workshop on Security in Softwarized Networks: Prospects and Challenges (SecSoN), Budapest, Hungary, August 24, 2018. [full text]
  4. Christopher Hannon, Jiaqi Yan, Dong Jin, Chen Chen, and Jianhui Wang, “Combining Simulation and Emulation Systems for Smart Grid Planning and Evaluation”, ACM Transactions on Modeling and Computer Simulation (TOMACS) – Special Issue on PADS, Volume 28, Issue 4, Article 27, October 2018. [full text]
  5. Christopher Hannon, Nandakishore Santhi, Stephan Eidenbenz, Jason Liu, and Dong Jin, “Just-In-Time Parallel Simulation”, 2018 Winter Simulation Conference (WSC), Gothernburg, Sweden, December 9-12, 2018. [full text]
  6. Xiaoliang Wu, Jiaqi Yan, and Dong Jin, “Virtual-Time-Accelerated Emulation for Blockchain Networks and Application Evaluation”, 2019 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation (PADS), Chicago, IL, June 3-5, 2019.
  7. Christopher Hannon, Jiaqi Yan, Dong Jin, and Yuan-An Liu, “A Distributed Virtual Time System on Embedded Linux for Evaluating Cyber-Physical Systems”,
  8.  2019 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation (PADS), Chicago, IL, June 3-5, 2019. Best Paper Award
  9. Jiaqi Yan, Guanhau Yan, and Dong Jin, “Classifying Malware Represented as Control Flow Graphs using Deep Graph Convolutional Neural Network”, 2019 IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2019), Portland, OR, June 24-27, 2019.
  10. Mohammad Noureddine, Amanda Hsu, Matthew Caesar, Fadi A. Zaraket, William H. Sanders, “P4.AIG: Circuit-Level Verification of P4 Programs”,
  11. 2019 IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2019), Portland, OR, June 24-27, 2019.
  12. Christopher Hannon and Dong Jin, “Bitcoin Payment-Channels for Resource Limited IoT Devices”, 2019 International Conference on Omni-Layer Intelligent Systems (COINS), Barcelona, Spain, July 27-29, 2019.