Automated Synthesis Framework for Network Security and Resilience - October 2019

PI: Matthew Caesar

Co-PI: Dong (Kevin) Jin

Researchers: Bingzhe Liu, Santhosh Prabhu, and Xiaoliang Wu

HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.

This project is developing 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 in a real-time and automated fashion. This project is building both theoretical underpinnings and a practical realization of Science of Security. 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.

PUBLICATIONS
Papers written as a result of your research from the current quarter only.

[1] Shangyu Xie, Han Wang, Shengbin Wang, Haibing Lu, Yuan Hong, Dong Jin and Qi Liu, Discovering Communities for Microgrids with Spatial-Temporal Net Energy, Journal of Modern Power Systems and Clean Energy (MPCE), July 2019

Abstract: Smart grid has integrated an increasing number of distributed energy resources to improve the efficiency and flexibility of power generation and consumption as well as the resilience of the power grid. The energy consumers on the power grid, e.g., households, equipped with distributed energy resources can be considered as "microgrids" that both generate and consume electricity. In this paper, we study the energy community discovery problems which identify energy communities for the microgrids to facilitate energy management, e.g., load balancing, energy sharing and trading on the grid. Specifically, we present efficient algorithms to discover such communities of microgrids considering both their geo-locations and net energy (NE) over any period. Finally, we experimentally validate the performance of the algorithms using both synthetic and real datasets.

Hard problem(s) addressed: resilient architectures

[2] Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, Matthew Caesar, Plankton: Scalable Network Configuration Verification Through Model Checking, NSDI, February 2020

Abstract: Network configuration verification enables operators to ensure that the network will behave as intended, prior to deployment of their configurations. Although techniques ranging from graph algorithms to SMT solvers have been proposed, scalable configuration verification with sufficient protocol support continues to be a challenge. In this paper, we show that by combining equivalence partitioning with explicit-state model checking, network configuration verification can be scaled significantly better than the state of the art, while still supporting a rich set of protocol features. We propose Plankton, which uses symbolic partitioning to manage large header spaces and efficient model checking to exhaustively explore protocol behavior. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000x speedup compared to the state of the art.

Hard problem(s) addressed: resilient architectures

KEY HIGHLIGHTS
Each effort should submit one or two specific highlights. Each item should include a paragraph or two along with a citation if available. Write as if for the general reader of IEEE S&P.
The purpose of the highlights is to give our immediate sponsors a body of evidence that the funding they are providing (in the framework of the SoS lablet model) is delivering results that "more than justify" the investment they are making.

In the current quarter, our project progress is centered on addressing SoS lablet hard problems primarily in resilient architecture. Key highlights are listed as follows.

• We continued the transfer of our technology to industry through interactions with Veriflow. Veriflow is a startup company commercializing verification technology that came out of this project's SoS lablet funding. This startup company has now employed over thirty people in the United States and has conducted multiple pilots and deployments across several industry sectors including within the US Department of Defense. More information is available at www.veriflow.net. Current collaborations target deployment of our verification technology to distributed cloud environments. Based on our work, Veriflow has released a new product, called CloudPredict. This product leverages our technology to perform formal verification on cloud environments. Our platform provides a fundamental advance in industry's ability to construct and maintain highly-resilient cloud architectures with provable guarantees.
• We continue to investigate of automated synthesis of network control to preserve desired security policies and network invariants. Specific invariants include (i) reduction of reaction time to fix problems, (ii) avoidance if introduction of errors in the repair process, and (iii) prevention of vulnerabilities. We have thus far designed a list of approximately 30 important and useful invariants to showcase the functionality of our system as well as to test it in practical use. We are also exploring how to synthesize patches to automatically fix critical invariants that were violated by the network controller application. The candidate approach under consideration models both the forwarding behavior of data through the network, control operations conducted on the network, as well as operations between the two. Since our last report, we have completed development of our parsing infrastructure, and performed a large-scale evaluation of our approach on real network data. Our results indicate the approach scales to large operational environments while providing formal guarantees on correctness of the cyber domain.
• We continued the exploration of self-healing network management to address the resilient architecture hard problem and application of the methods to applications in cyber-physical energy systems. We continue to conduct system evaluation using IEEE 14, 30 and 118 bus systems with a focus on the recovery plan generation time at the controller and the rule installation time in the network devices. We are refining our evaluation methods based on feedback from power system engineers as well as the early experimental results. Currently, we are preparing a manuscript describing this work.
  
• We study the interdependence between the power system and the communication network with the goal of improving resilience in critical energy infrastructures. We submitted a review paper on power grid resilience enhancement with the consideration of the interdependencies between power systems and communication networks. We also are investigating the power system restoration problem by considering the interdependencies among the two systems.
  
• We have continued our collaboration with AT&T, which operates one of the largest networks in the world, to customize and deploy our technology in their environments. AT&T faces some unique challenges which will require custom solutions for their environment. In particular, AT&T runs application-centric networks, composed of both traditional networking elements and application services. To perform verification and synthesis in these networks, we are developing extensions to verify application-level semantics across the network. The operator can specify end-to-end requirements on application behavior, which are analyzed across the entire network. For this to work, our system requires extensions to analyze application-level properties, as well as information about how each device or application component in the network manipulates data flow. Since our last report we have had weekly meetings with AT&T to build understanding of their challenges. We have formulated a set of invariants that characterize their operational challenges. Moving forward, we are developing a platform to translate invariants and network data into the Planning Domain Definition Language (PDDL). We believe these efforts will allow us to solve their challenges efficiency in a manner that leverages the capabilities of planning algorithms. When this is complete, we plan to work with AT&T to evaluate performance on their network. Based on their interest in our work, AT&T has agreed to share operational data and access to their network engineers.

• We have begun collaborations with Boeing on constructing a resilient IoT platform for the battlefield. IoT is crucially important to modern battlefield environments, making it a ripe target for adversaries. We are exploring an approach that leverages deep learning to dynamically relocate drone-mounted access points to evade the adversary. As part of this work we have formulated a placement algorithm that leverages Model-Agnostic Machine Learning (MAML) to construct a machine learning algorithm resilient to an adversary attempting to disrupt the learning process. We are in process of constructing simulations of our approach, and leveraging those results to tune and refine our designs. We hope to proceed to a completed approach and construction of a drone-mounted testbed within the next three quarters.

COMMUNITY ENGAGEMENTS

• Matthew Caesar continues to serve as Chief Science Officer of Veriflow, a company commercializing technology spun out of our Science of Security lablet work. Matthew has worked with Veriflow to undertake multiple new deployments of our earlier technology at top commercial-sector firms this quarter. The most recent news about Veriflow is available on the Veriflow web site (http://www.veriflow.net).
• Matthew Caesar has continued an engagement with the University of Illinois Center for Digital Agriculture towards securing our nation's food supply. His work leverages machine learning to detect anomalies in supply-chain operations.
• Kevin Jin served as the general chair of the 2019 ACM SIGSIM-PADS Conference.
• Kevin Jin is serving as a track coordinator of the "Simulation and Cyber Security" track in the Winter Simulation Conference 2019. The track now consists two paper sessions and one panel with the topic "Simulation for Cyber Security Risk Management."

EDUCATIONAL ADVANCES

• Kevin Jin and Kyle Hale are developing a new graduate-level cyber security laboratory class "System and Network Security" targeting release for Spring 2020 at Illinois Institute of Technology.
  
• Kevin Jin has been appointed as the Director of the new Master of Cybersecurity Program in the College of Science at Illinois Institute of Technology (https://science.iit.edu/programs/graduate/master-cybersecurity-mcybcode). The program will serve as one more platform to disseminate the educational and research outcomes of our Science of Security projects.
  
• Kevin Jin and Chen Chen (Argonne National Lab) are preparing a tutorial titled "Electric Power System Resilience" at the 2019 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm) in October 2019.
  
• We organized a Ph.D. colloquium as part of the ACM SIGSIM-PADS conference in June 2019. The Ph.D. colloquium include a career panel, poster session, student presentations, and a meeting with editors. We received 20+ submissions and 15 students were selected to present their work, among which 5 US-based Ph.D. students received the NSF student travel grant. The event has provided mentoring and educational opportunities to the young researchers, thus contributing to equipping them with tools that support their career success.
  
• Kevin Jin gave a full-day tutorial on "Cyber Security and Resilience of Cyber-Physical Systems" in the Internet of Things (IoT) Systems Research Center at the University of Wisconsin Madison, June 2019
  
• Matthew Caesar has created a new class on Internet of Things at UIUC. The class contains extensive coverage of security in this important domain. The class is slated for public release this fall on Coursera's Massive Online Open Course (MOOC) platform. The course will be open for enrollment by anyone, even people not attending the University of Illinois. Most lecture content and labs have been created and the course is approximately 85% filmed. We are currently working on an autograding infrastructure - when completed the class will be fully automated, allowing large numbers of students to enroll and learn advanced concepts in IoT security.
  
• Matthew Caesar also continues to refine his Networking Laboratory class, targeting release for Spring 2020. He has developed a new set of Cybersecurity lectures for his class, covering important topics, and educating students how to improve security of common networking deployments.
  
• Matthew Caesar is currently constructing an online platform for working with IoT devices in the cloud. The platform virtualizes IoT devices, internally leveraging a new technology that extends virtual machines into the IoT domain. This work will probably take another year to develop, but when it is released, we hope to grow from small pilots to a platform that can allow students across the world to learn about and work with IoT security in a manner that greatly accelerates their ability to experiment and learn.