Automated Synthesis Framework for Network Security and Resilience - April 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] Santhosh Prabhu, Ali Kheradmand, Brighten Godfrey and Matthew Caesar, "Plankton: Scalable Network Configuration Verification through Model Checking", one-shot revision decision ,17^th USENIX Symposium on Networked Systems Design and Implementation, Santa Clara, CA, February 25-27, 2020.

Abstract: A variety of network verification tools have been proposed in the recent years, using different network abstractions and analysis techniques. For configuration verification, techniques ranging from graph algorithms to SMT solvers have been proposed. In spite of this, 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: scalability

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. Veriflow continues to make inroads on deploying our technology at multiple large companies this quarter. We have also begun discussions with Veriflow on incorporating our synthesis work into their product.

• 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 the first cut of the network configuration parsing infrastructure for our platform. Our parser is developed in C++ and takes as input Cisco IOS configuration files. We have also discussed with UIUC's Engineering IT group to acquire real configuration files for our platform, they have agreed and provided the traces. We have conducted an extensive evaluation study using their traces. This has provided very valuable data on the performance of our approach, which we are now leveraging to tune and improve our design.

• We continued 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 are developing an algorithm for identifying power system critical assets, which is an important new power system constraint to consider in the self-healing optimization algorithm. We continue to conduct system evaluation using IEEE 14, 30 and 118 bus systems with the focus on the recovery time and the number of updated rules in the network devices. Currently, we are preparing a manuscript describing this work.
  
• We continue to explore deep learning techniques for malware classification. We build a system that extend a special type of graph kernel-based deep neural network, Deep Graph Convolutional Neural Network (DGCNN) for classifying CFG-represented malware programs. DGCNN enables embedding high-dimensional structural information into vectors that are amenable to efficient classification. We use two large independent datasets that contain more than 20K malware samples to evaluate our system and the experimental results are comparable to those of the state-of-the-art methods applied with handcrafted malware features. A paper describing this work has been accepted to DSN'19. We will also present this work in the coming SoS research seminar at UIUC in April 30^th, 2019.

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 Caesar has begun an engagement with the University of Illinois Center for Digital Agriculture towards securing our nation's food supply.
• Kevin Jin served as a technical program committee member of HotSoS, Feb 2019.
• Kevin Jin is serving 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
• Jiaqi Yan will give a talk at the Science of Security Seminar at UIUC in April 2019

EDUCATIONAL ADVANCES:

• Kevin Jin and Gady Agam are leading the effort of creating a new CS Master of Cyber Security program in at IIT. The program has been approved by the university, which 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) submitted a tutorial titled "Electric Power System Resilience" to the 2019 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm)
  
• We received an NSF student travel grant award to support 5 US-based students ($1000 per student) to attend the ACM SIGSIM-PADS conference held in Chicago, June 2019.
  
• Matthew Caesar is in the process of creating a new class on Internet of Things. The class will contain 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.
  
• 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.