Spotlight on Lablet Research #2 - Automated Synthesis Framework for Network Security and Resilience
Spotlight on Lablet Research #2 -
Project: Automated Synthesis Framework for Network Security and Resilience
Lablet: University of Illinois at Urbana-Champaign
Participating Sub-Lablet: Illinois Institute of Technology
This project proposes to develop 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 (i.e., data forwarding, network control, programming language, and application software) in a real-time and automated fashion. The ASF approach is exciting because developing it adds to the theoretical underpinnings of SoS, while using it supports the practice of SoS.
This project is led by Principal Investigator (PI) Matt Caesar and Co-PI Dong Jin. As has been the case since the start of the project, the technology developed as a result of the research is transferred to industry through interactions with Veriflow, a startup company commercializing verification technology that came out of the project's SoS Lablet funding. In September 2019, Veriflow was sold to VMWare, and the technology is slated to be incorporated into VMWare NSX, a very widely used virtualization platform in industry. Collaborations with VMWare continue by incorporating the project platform with NSX, targeting deployment of verification technology to distributed cloud environments, and integration of real-time traffic data into analysis.
In continuing the researchers' investigation of automated synthesis of network control to preserve desired security policies and network invariants, they have designed a list of approximately 30 important and useful invariants to showcase the functionality of the system, as well as to test it in practical use. They have completed the development of parsing infrastructure and performed a large-scale evaluation of the approach on real network data.
They are developing a simulation/emulation-based platform for Cyber-Physical System (CPS) resilience and security evaluation. The platform combines physical computing and networking hardware for the cyber presence while allowing for offline simulation and computation of the physical world. The platform consists of a distributed virtual time kernel module for efficient synchronization between simulation and network emulation/hardware. The kernel module enables processes and their clocks to be paused, resumed, and dilated across embedded Linux devices through the use of hardware interrupts.
Self-healing network management to address the resilient architecture hard problem and apply the methods to applications in cyber-physical energy systems, in particular, phasor measurement unit (PMU) networks in the electric grid, is being explored. The research team developed an efficient algorithm that considers both power system observability and communication network characteristics. The algorithm also assigns weights to the end-devices according to selected power system metrics before performing the optimization. There has been a system evaluation with the proof-of-concept system using IEEE 14, 30 and 118 bus systems.
Other efforts with industry include a collaboration with AT&T to customize and deploy the technology in their environments, and with Boeing on constructing a resilient IoT platform for the battlefield.
Project research has passed extensive peer review, and researchers have published over fifteen works at top conferences. In addition, they have regularly released software packages and data sets used in the publications, which have been used by a number of other researchers.
Additional details on this project can be found here.