|
" Formal Techniques for Automated Design of Adaptive Networked Systems Based on Security and Resiliency Requirements "
Jakaria, A. H. M.
Siraj, Ambareen
| Document Type
|
:
|
Latin Dissertation
|
| Language of Document
|
:
|
English
|
| Record Number
|
:
|
1053618
|
| Doc. No
|
:
|
TL52735
|
| Main Entry
|
:
|
Jakaria, A. H. M.
|
| Title & Author
|
:
|
Formal Techniques for Automated Design of Adaptive Networked Systems Based on Security and Resiliency Requirements\ Jakaria, A. H. M.Siraj, Ambareen
|
| College
|
:
|
Tennessee Technological University
|
| Date
|
:
|
2020
|
| Degree
|
:
|
Ph.D.
|
| student score
|
:
|
2020
|
| Note
|
:
|
177 p.
|
| Abstract
|
:
|
With the ever-growing need for connectivity in this era of smart and autonomous systems, we are observing an extensive use of network services. The increasing use of cyber technology, however, leads to the proliferation of security threats. Therefore, it is essential to design a secure and resilient architecture for networked systems. Moreover, due to the diversified cyber usages as well as security requirements, adaptive and ad-hoc networking solutions are increasingly being adopted. While adaptive networking provides many flexibilities, it requires to be properly (re)configured considering the changed context and dependability aspects. Organizations are seeking more reliable and automated design strategies that can meet the operational goals and security requirements within the budget and capability constraints, which is a multi-objective and combinatorially hard constraint satisfaction problem. This dissertation addresses this problem by proposing a suite of network synthesis techniques using formal methods that can automatically synthesize network configurations satisfying the given requirements. This research considers three configuration synthesis problems that cover different security and resiliency perspectives of the automated design of adaptive networked systems. The first problem addresses the configuration synthesis for a network functions virtualization (NFV)-based network concerning a security objective that requires the appropriate deployment of virtual network functions (VNFs) on physical servers. The second problem studies the automated synthesis of incremental deployment plans for software-defined networking (SDN) compatible switches. Here, we choose the context of enabling security and resiliency for a communication network in a smart grid. The objective of the third problem is to ensure resilient communication for a collaborative network of unmanned aerial vehicles (UAVs), maintaining in-flight constraints and mission requirements. To solve the problems mentioned above, this research designs and implements three frameworks that involve the formal modeling of the system specifications, operator requirements, and budget and network constraints. The formal models are encoded and solved using efficient logic formulas based on satisfiability modulo theories (SMT). The solutions to the models synthesize necessary network configuration parameters. Finally, simulated experiments are performed on synthetic data to evaluate the efficacy as well as the scalability of the developed solutions.
|
| Descriptor
|
:
|
Computer science
|
| Added Entry
|
:
|
Siraj, Ambareen
|
| Added Entry
|
:
|
Tennessee Technological University
|
| |