Automated Synthesis Framework for Network Security and Resilience - October 2018

PI(s), Co-PI(s), Researchers: Matthew Casear, Dong (Kevin) Jin, 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] 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), August 2018

Abstract: Software-defined networking enables efficient network management. As the technology matures, utilities are looking to integrate those benefits to their operations technology (OT) networks. To help the community to better understand and evaluate the effects of such integration, we develop DSSnet, a testing platform that combines a power distribution system simulator and an SDN-based network emulator for smart grid planning and evaluation. DSSnet relies on a container-based virtual time system to achieve efficient synchronization between the simulation and emulation systems. To enhance the system scalability and usability, we extend DSSnet to support a distributed controller environment. To enhance system fidelity, we extend the virtual time system to support kernel-based switches. We also evaluate the system performance of DSSnet and demonstrate the usability of DSSnet with a resilient demand response application case study.

Hard problem(s) addressed: resilient architectures; scalability; design, development and deployment

[2] Santhosh Prabhu, Gohar Irfan Chaudhry, Brighten Godfrey and Matthew Caesar, "High Coverage Testing of Softwarized Networks", ACM SIGCOMM 2018 Workshop on Security in Softwarized Networks: Prospects and Challenges, Budapest, Hungary, August 24, 2018.

Abstract: Network operators face a challenge of ensuring correctness as networks grow more complex, in terms of scale and increasingly in terms of diversity of software components. Network-wide verification approaches can spot errors, but assume a simplified abstraction of the functionality of individual network devices, which may deviate from the real implementation. In this paper, we propose a technique for high-coverage testing of end-to-end network correctness using the real software that is deployed in these networks. Our design is effectively a hybrid, using an explicit-state model checker to explore all network-wide execution paths and event orderings, but executing real software as subroutines for each device. We show that this approach can detect correctness issues that would be missed both by existing verification and testing approaches, and a prototype implementation suggests the technique can scale to larger networks with reasonable performance.

Hard problem(s) addressed: resilient architectures, design, development and deployment

[3] Jiaqi Yan, Dong Jin, 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.

Abstract: Network intrusion detection systems (NIDS) are essential security building-blocks for today's organizations to ensure safe and trusted communication of information. In this paper, we study the feasibility of off-line deep learning based NIDSes by constructing the detection engine with multiple advanced deep learning models and conducting a quantitative and comparative evaluation of those models. We first introduce the general deep learning methodology and its potential implication on the network intrusion detection problem. We then review multiple machine learning solutions to two network intrusion detection tasks (NSL-KDD and UNSW-NB15 datasets). We develop a TensorFlow-based deep learning library, called NetLearner, and implement a handful of cutting-edge deep learning models for NIDS. Finally, we conduct a quantitative and comparative performance evaluation of those models using NetLearner.

: resilient architectures; security-metrics-driven evaluation, design, development and deployment

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 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 are also exploring of 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. We have formulated a simplified solution for OSPF based network using SMT constraints and executed it using a Z3 solver. The project team at UIUC and IIT have regular bi-weekly meetings to discuss the research collaboration progress.
• 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 developed an enhanced version of the self-healing algorithm that considers both power system observability and communication network characteristics. The current version also assigns weights to the end-devices (i.e., PMU) according to certain selected power system metrics before performing the optimization. We implement a proof-of-concept system in Mininet and are conducting system performance evaluation using the IEEE 30-bus system.
• We studied the network intrusion detection system with various deep learning models with the goal of enhancing network security and resilience. We designed and implemented a TensorFlow-based deep learning library, called NetLearner. We made the software code of NetLearner publicly available at https://github.com/littlepretty/NetLearner
• We continued 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 employs 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.

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.
• Kevin Jin will serve as a technical program committee member of HotSoS 2019.
• Kevin Jin was invited to the NSF Visioning Workshop on Programmable Security in a Software Defined World, August 2018.
• Kevin Jin served as a technical program committee member of the 2018 International Conference on Information and Communications Security (ICICS)
• Kevin Jin gave a technical talk at the CODES summer workshop at Argonne National Lab in July 2018. The topic of the talk is about "Scalable Simulation and Modeling Framework for Evaluation of Software-Defined Networking Design and Applications."

EDUCATIONAL ADVANCES:

• Kevin Jin supervised one undergraduate student research project in Summer 2018 and the project is ongoing in Fall 2018. Matthew Caesar supervised five undergraduate student research projects during this same timeframe. Matthew also participated in the 2018 University of Illinois Undergraduate Research Symposium.
• Matthew Caesar is teaching a Networking Laboratory class this semester. This semester, he has developed a new Cybersecurity module for his class. This module gives students the opportunity to set up and configure security features of routers and switches in a virtualized environment. Students configure ACLs and VLANs to ensure desirable security properties such as segmentation and access control The lab is structured to give students direct hands-on experience with these techniques, making them confident to use these techniques in the field.