A Hypothesis Testing Framework for Network Security - July 2017
Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.
PI(s): P. Brighten Godfrey
Co-PI(s): : Matthew Caesar, David Nicol, William Sanders, and Kevin Jin (Illinois Institute of Technology)
HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.
This project covers four hard problems:
- Scalability and composability
- Policy-governed secure collaboration
- Predictive security metrics
- Resilient architectures
PUBLICATIONS
Papers published in this quarter as a result of this research. Include title, author(s), venue published/presented, and a short description or abstract. Identify which hard problem(s) the publication addressed. Papers that have not yet been published should be reported in region 2 below.
Current quarter:
- Santhosh Prabhu, Mo Dong, Tong Meng, P. Brighten Godfrey, and Matthew Caesar, "Let me rephrase that: Transparent optimization in SDNs", ACM SIGCOMM Symposium on SDN Research (SOSR 2017), Santa Clara, CA, April 3-4, 2017.
- Soudeh Ghorbani and P. Brighten Godfrey, "COCONUT: Seamless Scale-out of Network Elements", European Conference on Computer Systems (EuroSys 2017), Belgrade, Serbia, April 23-26, 2017.
- Jiaqi Yan, Xin Liu and Dong Jin, "Simulation of a Software-Defined Network as One Big Switch", 2017 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation (PADS 2017), Singapore, May 24-26, 2017.
- Santhosh Prabhu, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar, "Predicting Network Futures with Plankton", 1st Asia-Pacific Workshop on Networking (APNet'17), Hong Kong, China, August 3-4, 2017, to appear. DOI: 10.1145/3106989.3106991.
- Dong Jin, Zhiyi Li, Christopher Hannon, Chen Chen, Jianhui Wang, Mohammad Shahidehpour, Cheol Won Lee and Jong Cheol Moon, "Towards a Resilient and Secure Microgrid Using Software-Defined Networking", IEEE Transactions on Smart Grid, Special section on Smart Grid Cyber-Physical Security, to appear.
- Ning Liu, Adnan Haider, Dong Jin and Xian-He Sun. "A Modeling and Simulation of Extreme-Scale Fat-Tree Networks for HPC Systems and Data Centers", ACM Transactions on Modeling and Computer Simulation (TOMACS), to appear.
ACCOMPLISHMENT HIGHLIGHTS
In the current quarter, our project progress is centered on addressing three SoS Lablet hard problems: scalability, resilient architecture, and predictive security metrics. Specifically:
- Developing effective evaluation methodologies for large-scale and complex networked systems using emulation and simulation
- Utilized our DSSNet platform (https://github.com/annonch/DSSnet) to evaluate the self-healing ability of SDN to microgrid application; the results show that it is easier to deploy replacement of traditional network recovery protocols with faster recovery time in SDN-enabled microgrids.
- Enhanced the fidelity and scalability of our simulation/emulation testing and evaluation platform, including a new network model abstraction technique that effectively transforms network devices in an SDN-based network to one virtualized switch model.
- One paper published in ACM SIGSIM-PADS'17 in May 2017, and currently waiting decision of a submitted ACM TOMACS journal paper
- Investigating infrastructure-level and application-level approach to apply SDN technologies to make industrial control systems more cyber secure and resilient
- Designed an SDN-based communication network architecture for microgrid operations for a resilient and secure microgrid in the face of growing cyber-attacks and cyber-mistakes,
- Investigating multiple microgrid security applications, such as self-healing PMU, network verification, by leveraging the global visibility, direct networking controllability and programmability offered by SDN
- Developed hardware-in-the-loop SDN simulation testbed, performing validation test, and preparing a manuscript
- Working on the extended version of ConVenus to address timing uncertainty (https://bitbucket.org/ksj0609/convenus)
- Our IEEE Transaction of Smart Grid journal paper has been accepted in May 2017
- Initiated work on predicting and verifying future behavior of networks including temporal properties. Recent years have seen significant advancement in the field of formal network verification. Tools have been proposed for offline data plane verification, real-time data plane verification and configuration verification under arbitrary, but static sets of failures. However, due to the fundamental limitation of not treating the network as an evolving system, current verification platforms have significant constraints in terms of scope. In real-world networks, correctness policies may be violated only through a particular combination of environment events and protocol actions, possibly in a non-deterministic sequence. Moreover, correctness specifications themselves may often correlate multiple data plane states, particularly when dynamic data plane elements are present. Tools in existence today are not capable of reasoning about all the possible network events, and all the subsequent execution paths that are enabled by those events. We propose Plankton, a verification platform for identifying undesirable evolutions of networks. By combining symbolic modeling of data plane and control plane with explicit state exploration, Plankton performs a goal-directed search on a finite-state transition system that captures the behavior of the network as well as the various events that can influence it. In this way, Plankton can automatically find policy violations that can occur due to a sequence of network events, starting from the current state. An example use of the system would be verifying whether there exists a failure that could cause routes to change and circumvent a security control point or monitoring point, thus evading forensics. The system can prove whether such a dynamic event could occur, and if so, give an example.
- We have been actively working on dissemination of knowledge through tutorials on network verification. Brighten Godfrey developed and presented a half-day tutorial at a workshop at Hebrew University. Santhosh Prabhu and Brighten Godfrey submitted a proposal to present an expanded tutorial at the IEEE/ACM International Conference on Software Engineering (ASE) in October 2017; this proposal was accepted.