Biblio

Due to the extensive use of network services and emerging security threats, enterprise networks deploy varieties of security devices for controlling resource access based on organizational security requirements. These requirements need fine-grained access control rules based on heterogeneous isolation patterns like access denial, trusted communication, and payload inspection. Organizations are also seeking for usable and optimal security configurations that can harden the network security within enterprise budget constraints. In order to design a security architecture, i.e., the distribution of security devices along with their security policies, that satisfies the organizational security requirements as well as the business constraints, it is required to analyze various alternative security architectures considering placements of network security devices in the network and the corresponding access controls. In this paper, we present an automated formal framework for synthesizing network security configurations. The main design alternatives include different kinds of isolation patterns for network traffic flows. The framework takes security requirements and business constraints along with the network topology as inputs. Then, it synthesizes cost-effective security configurations satisfying the constraints and provides placements of different security devices, optimally distributed in the network, according to the given network topology. In addition, we provide a hypothesis testing-based security architecture refinement mechanism that explores various security design alternatives using ConfigSynth and improves the security architecture by systematically increasing the security requirements. We demonstrate the execution of ConfigSynth and the refinement mechanism using case studies. Finally, we evaluate their scalability using simulated experiments.
 

Smart grids provide innovative and efficient energy management services that offer operational reliability. The Supervisory Control and Data Acquisition (SCADA) system is a core component of a smart grid. Unlike the traditional cyber networks, these components consist of heterogeneous devices, such as intelligent electronic devices, programmable logic controllers, remote terminal units, control servers, routing and security devices, etc. SCADA devices communicate with one another under various communication protocols, physical media, and security properties. Failures or attacks on such networks have the potential of data unavailability and false data injection causing incorrect system estimations and control decisions leading to critical damages including power outages and destruction of equipment. In this work, we develop an automated security and resiliency analysis framework for SCADA in smart grids. This framework takes smart grid configurations and organizational security and resiliency requirements as inputs, formally models configurations and various security constraints, and verifies the dependability of the system under potential contingencies. We demonstrate the execution of this framework on an example problem. We also evaluate the scalability of the framework on synthetic SCADA systems.

Smart grids provide innovative and efficient energy management services that offer operational reliability. The Supervisory Control and Data Acquisition (SCADA) system is a core component of a smart grid. Unlike the traditional cyber networks, these components consist of heterogeneous devices, such as intelligent electronic devices, programmable logic controllers, remote terminal units, control servers, routing and security devices, etc. SCADA devices communicate with one another under various communication protocols, physical media, and security properties. Failures or attacks on such networks have the potential of data unavailability and false data injection causing incorrect system estimations and control decisions leading to critical damages including power outages and destruction of equipment. In this work, we develop an automated security and resiliency analysis framework for SCADA in smart grids. This framework takes smart grid configurations and organizational security and resiliency requirements as inputs, formally models configurations and various security constraints, and verifies the dependability of the system under potential contingencies. We demonstrate the execution of this framework on an example problem. We also evaluate the scalability of the framework on synthetic SCADA systems.
 

Enterprise networks deploy security devices to control access and limit potential threats. Due to the emergence of zero-day attacks, security device based isolation measures like access denial, trusted communication, and payload inspection are often not adequate for the resilient execution of an organization's mission. Diversity between two hosts in terms of operating systems and services running on these hosts is crucial for limiting the attack propagation. Since different software systems have different vulnerabilities, it is important to have the hosts diversified considering the isolation among the hosts as well as the mission requirements. In this paper, we present a formal model for synthesizing network resiliency configurations. The resiliency design integrates isolation and diversity measures. We take the network topology, resiliency requirements, and business constraints as inputs. Then, our proposed model synthesizes cost-effective resiliency configurations satisfying the constraints. The output of the model provides necessary placements of different security devices in the topology and necessary installments of operating systems and services on the hosts. We demonstrate the execution of the proposed model as well as their scalability using simulated experiments.
 

Network reconnaissance of IP addresses and ports is prerequisite to many host and network attacks. Meanwhile, static configurations of networks and hosts simplify this adversarial reconnaissance. In this paper, we present a novel proactive-adaptive defense technique that turns end-hosts into untraceable moving targets, and establishes dynamics into static systems by monitoring the adversarial behavior and reconfiguring the addresses of network hosts adaptively. This adaptability is achieved by discovering hazardous network ranges and addresses and evacuating network hosts from them quickly. Our approach maximizes adaptability by (1) using fast and accurate hypothesis testing for characterization of adversarial behavior, and (2) achieving a very fast IP randomization (i.e., update) rate through separating randomization from end-hosts and managing it via network appliances. The architecture and protocols of our approach can be transparently deployed on legacy networks, as well as software-defined networks. Our extensive analysis and evaluation show that by adaptive distortion of adversarial reconnaissance, our approach slows down the attack and increases its detectability, thus significantly raising the bar against stealthy scanning, major classes of evasive scanning and worm propagation, as well as targeted (hacking) attacks.
 

A fundamental drawback of current anomaly detection systems (ADSs) is the ability of a skilled attacker to evade detection. This is due to the flawed assumption that an attacker does not have any information about an ADS. Advanced persistent threats that are capable of monitoring network behavior can always estimate some information about ADSs which makes these ADSs susceptible to evasion attacks. Hence in this paper, we first assume the role of an attacker to launch evasion attacks on anomaly detection systems. We show that the ADSs can be completely paralyzed by parameter estimation attacks. We then present a mathematical model to measure evasion margin with the aim to understand the science of evasion due to ADS design. Finally, to minimize the evasion margin, we propose a key-based randomization scheme for existing ADSs and discuss its robustness against evasion attacks. Case studies are presented to illustrate the design methodology and extensive experimentation is performed to corroborate the results.
 

The need of cyber security is increasing as cyber attacks are escalating day by day. Cyber attacks are now so many and sophisticated that many will unavoidably get through. Therefore, there is an immense need to employ resilient architectures to defend known or unknown threats. Engineer- ing resilient system/infrastructure is a challenging task, that implies how to measure the resilience and how to obtain sufficient resilience necessary to maintain its service delivery under diverse situations. This paper has two fold objective, the first is to propose a formal approach to measure cyber resilience from different aspects (i.e., attacks, failures) and at different levels (i.e., pro-active, resistive and reactive). To achieve the first objective, we propose a formal frame- work named as: Cyber Resilience Engineering Framework (CREF). The second objective is to build a resilient system by construction. The idea is to build a formal model of a cyber system, which is initially not resilient with respect to attacks. Then by systematic refinements of the formal model and by its model checking, we attain resiliency. We exemplify our technique through the case study of simple cyber security device (i.e., network firewall).

he Advanced Metering Infrastructure (AMI) in a smart grid comprises of a large number of smart meters along with heterogeneous cyber-physical components. These components communicate with each other through different communication media, protocols, and delivery modes for transmitting usage reports and control commands to and from the utility. There is potential for dependability threats especially due to misconfigurations, which can easily disrupt the operations in AMI. Therefore, an AMI must be configured correctly. In this paper, we present an automated configuration synthesis framework that mitigates potential threats by eliminating mis-configurations. We have manifold contributions in this research: (i) formal modeling of AMI configurations including AMI device configurations, topology and communication properties, and data flows among the devices; (ii) formal modeling of AMI operational integrity properties considering the interdependencies among AMI devices' configurations; and (iii) implementing the model using Satisfiability Modulo Theories (SMT), execution of which synthesizes necessary AMI configurations. We demonstrate the proposed framework on an example case study and evaluate the scalability of the framework on various synthetic AMI networks.