Automated Synthesis Framework for Network Security and Resilience - July 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] Jiaqi Yan, Guanhua Yan, 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), June 2019.

Abstract: Malware have been one of the biggest cyber threats in the digital world for a long time. Existing machine learning-based malware classification methods rely on handcrafted features extracted from raw binary files or disassembled code. The diversity of such features created has made it hard to build generic malware classification systems that work effectively across different operational environments. To strike a balance between generality and performance, we explore new machine learning techniques to classify malware programs represented as their control flow graphs (CFGs). To overcome the drawbacks of existing malware analysis methods using inefficient and non-adaptive graph matching techniques, in this work, we build a new 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 proposed system and the experimental results show that it can classify CFG-represented malware programs with performance comparable to those of the state-of-the-art methods applied on handcrafted malware features.

Hard problem(s) addressed: security-metrics-driven evaluation, design, development, and deployment

[2] Xiaoliang Wu, Jiaqi Yan and Dong Jin. "Virtual-Time-Accelerated Emulation for Blockchain Network and Application Evaluation." 2019 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation (PADS), June 2019

Abstract: Blockchain technologies are in the ascendant of transforming the ways we manage contracts, make transactions, and manifest ownership of property. The trend calls for a realistic testing and evaluation platform for blockchain applications and systems. We present Minichain, a container-based emulator that allows testing proof-of-work-based blockchains on a commodity computer. Minichain contains a realistic and configurable network environment, which is missing in today's blockchain testbeds. This unique feature enables us to evaluate the impact of network events (e.g., cyber-attacks) and conditions (e.g., congested or failed links) on blockchain applications. Meanwhile, Minichain allows the direct execution of unmodified application code in the containers for fidelity, and utilizes the virtual time technique to speed up experiments and improve the system scale that one can accurately emulate. In particular, we mathematically analyze the convergence of the proof-of-work-based consensus algorithm to show the effectiveness of virtual time. We evaluate the performance of Minichain across both network layer and application layer, and demonstrate its usability by emulating a selfish mining attack initiated from the network layer.

Hard problem(s) addressed: scalability

[3] Christopher Hannon, Jiaqi Yan, Dong Jin and Yuan-An Liu. "A Distributed Virtual Time System on Embedded Linux for Evaluating Cyber-Physical Systems." 2019 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation (PADS), June 2019, Best Paper Award

Abstract: Cyber-physical systems have a cyber presence, collecting and transmitting data, while also collecting information and modifying the physical surrounding world. In order to evaluate the cyber-security of cyber-physical systems, simulation and modeling is a tool often used. In this work, we develop a distributed virtual time system that enables the synchronization of virtual clocks between physical machines enabling a high-fidelity simulation-based testing platform. The platform combines physical computing and networking hardware for the cyber presence, while allowing for offline simulation and computation of the physical world. By incorporating virtual clocks into distributed embedded Linux devices, the testbed creates the opportunity to interrupt real and emulated cyber-physical applications to inject offline simulated data values. The ability to run real applications and being able to inject simulated data temporally transparent to the running process allows for high fidelity experimentation. Distributed virtual time enables processes and their clocks to be paused, resumed, and dilated across embedded Linux devices through the use of hardware interrupts and a common kernel module. By interconnecting the embedded devices' general-purpose IO pins, they can coordinate and synchronize through a distributed virtual time kernel module with low overhead, under 50 microseconds for 8 processes across 4 embedded Linux devices. We demonstrate the usability of our testbed in a power grid control application.

Hard problem(s) addressed: scalability

[4] Christopher Hannon and Dong Jin. Bitcoin Payment-Channels for Resource Limited IoT Devices. 2019 International Conference on Omni-Layer Intelligent Systems (COINS), May 2019

Abstract: Resource-constrained devices are unable to maintain a full copy of the Bitcoin Blockchain in memory. This paper proposes a bidirectional payment channel framework for IoT devices. This framework utilizes Bitcoin Lightning-Network-like payment channels with low processing and storage requirements. This protocol enables IoT devices to open and maintain payment channels with traditional Bitcoin nodes without a view of the blockchain. Unlike existing solutions, it does not require a trusted third party to interact with the blockchain nor does it burden the peer-to-peer network in the way SPV clients do. The contribution of this paper includes a secure and crypto-economically fair protocol for bidirectional Bitcoin payment channels. In addition, we demonstrate the security and fairness of the protocol by formulating it as a game in which the equilibrium is reached when all players follow the protocol.

Hard problem(s) addressed: resilient architectures

[5] Mohammad Noureddine, Amanda Hsu, Matthew Caesar, Fadi A. Zaraket, William H. Sanders. P4 AIG: Circuit-Level Verification of P4 Programs, Dependable Systems and Networks (DSN), June 2019.

Abstract: In this work, we set out to develop P4AIG, a tool for the static verification of programmable data planes using sequential circuit analysis. P4AIG targets P4 programs by treating them as hardware pipelines rather than software programs. P4AIG allows for the circuit-level treatment of P4 programs, a feature not available for traditional software verification techniques. We believe that P4AIG will exploit the nature of P4 programs to achieve higher scalability in verification.

Hard problem(s) addressed: resilient architectures

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

Abstract: A variety of network verification tools have been proposed in the recent years to verify networks, using different network abstractions and analysis techniques. For configuration verification, techniques ranging from graph algorithms to SMT solvers have been proposed. 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, without compromising correctness or expressibility. We propose Plankton, which uses symbolic partition 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.

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. 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 formulated a new algorithm to self-heal the PMU network upon detection of compromised PDCs. 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 and compare the results to the LLP model. 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 published at DSN'19. Jiaqi Yan presented this work in the SoS research seminar at UIUC in April as well as the DSN conference in June, 2019.

• We develop a distributed virtual time system that enables the synchronization of virtual clocks between physical machines enabling a high-fidelity simulation-based testing platform with the goal of evaluating cyber-security of cyber-physical systems. A key component is a distributed virtual time kernel module that enables processes and their clocks to be paused, resumed, and dilated across embedded Linux devices through the use of hardware interrupts and a common kernel module. A paper describing this work has won the Best Paper Award at ACM SIGSIM-PADS'19, and Christopher Hannon presented the work in the conference in June 2019.

• We have begun a 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. We plan to incorporate these extensions into our design, and work with AT&T to implement and deploy the resulting system into their network.

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 begun an engagement with the University of Illinois Center for Digital Agriculture towards securing our nation's food supply.
• 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.

EDUCATIONAL ADVANCES

• 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) submitted a tutorial titled "Electric Power System Resilience" to the 2019 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm) and the tutorial is accepted by the conference.
  
• We organized a Ph.D. colloquium as part of the ACM SIGSIM-PADS conference. 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 35% filmed.
  
• 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.