Automated Synthesis Framework for Network Security and Resilience - January 2019

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, Nandakishore Santhi, Stephan Eldenbenz, Jason Liu, and Dong Jin, "Just-In-Time Parallel Simulation", 2018 Winter Simulation Conference (WSC), Gothernburg, Sweden, December 9-12, 2018.

Abstract: : Due to the evolution of programming languages, interpreted languages have gained widespread use in scientific and research computing. Interpreted languages excel at being portable, easy to use, and fast in prototyping than their ahead-of-time (AOT) counterparts, including C, C++, and Fortran. While traditionally considered as slow to execute, advancements in Just-in-Time (JIT) compilation techniques have significantly improved the execution speed of interpreted languages and in some cases outperformed AOT languages. In this paper, we explore some challenges and design strategies in developing a high performance parallel discrete event simulation engine, called Simian, written with interpreted languages with JIT capabilities, including Python, Lua, and Javascript. Our results show that Simian with JIT performs similarly to AOT simulators, such as MiniSSF and ROSS. We expect that with features like good performance, user-friendliness, and portability, the just-in-time parallel simulation will become a common choice for modeling and simulation in the near future.

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.

• 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 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. Since our last report, we have made substantial progress on developing a 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 pending approval of UIUC's Security team. We hope to acquire this approval and use these real, large-scale network traces to evaluate our platform.

• 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 a mapping algorithm to generate a realistic PMU network topology from the standard IEEE N-bus system with sufficient redundancy to ensure complete power system observability. We also documented the system model and self-healing algorithm. We are conducting system evaluation with our proof-of-concept system using IEEE 14, 30 and 118 bus systems.
  
• We explore deep learning techniques to classify malware programs represented as their control flow graphs (CFGs). We build a system that uses deep graph convolutional neural network to embed structural information inherent in CFGs for effective yet efficient malware 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. We have submitted a paper to DSN'19.

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.
• Our paper on smart traffic light secuirty was tweeted by NSA: https://twitter.com/NSAGov/status/1055519365104390147
• Kevin Jin will serve as a technical program committee member of HotSoS 2019.
• Kevin Jin will serve as a technical program committee memeber of ACM SDN-NFV Security 2019.

EDUCATIONAL ADVANCES:

• Kevin Jin submitted an NSF conference proposal requesting funds to support 5 U.S. students to attend the 2019 ACM SIGSIM-PADS conference.
  
• Matthew Caesar supervised five undergraduate student research projects in Fall 2018. Kevin Jin supervised one undergraduate student research project during this same timeframe, and two more undergraduate students will join in Spring 2019. Matthew also participated in the 2018 University of Illinois Undergraduate Research Symposium.
  
• Matthew Caesar taught a Networking Laboratory class in Fall 2018. 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.