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.
 

To help establish a more scientific basis for security science, which will enable the development of fundamental theories and move the field from being primarily reactive to primarily proactive, it is important for research results to be reported in a scientifically rigorous manner. Such reporting will allow for the standard pillars of science, namely replication, meta-analysis, and theory building. In this paper we aim to establish a baseline of the state of scientific work in security through the analysis of indicators of scientific research as reported in the papers from the 2015 IEEE Symposium on Security and Privacy. To conduct this analysis, we developed a series of rubrics to determine the completeness of the papers relative to the type of evaluation used (e.g. case study, experiment, proof). Our findings showed that while papers are generally easy to read, they often do not explicitly document some key information like the research objectives, the process for choosing the cases to include in the studies, and the threats to validity. We hope that this initial analysis will serve as a baseline against which we can measure the advancement of the science of security.

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.
 

State estimation plays a critically important role in ensuring the secure and reliable operation of the electric grid. Recent works have shown that the state estimation process is vulnerable to stealthy attacks where an adversary can alter certain measurements to corrupt the solution of the process, but evade the existing bad data detection algorithms and remain invisible to the system operator. Since the state estimation result is used to compute optimal power flow and perform contingency analysis, incorrect estimation can undermine economic and secure system operation. However, an adversary needs sufficient resources as well as necessary knowledge to achieve a desired attack outcome. The knowledge that is required to launch an attack mainly includes the measurements considered in state estimation, the connectivity among the buses, and the power line admittances. Uncertainty in information limits the potential attack space for an attacker. This advantage of uncertainty enables us to apply moving target defense (MTD) strategies for developing a proactive defense mechanism for state estimation.

In this paper, we propose an MTD mechanism for securing state estimation, which has several characteristics: (i) increase the knowledge uncertainty for attackers, (ii) reduce the window of attack opportunity, and (iii) increase the attack cost. In this mechanism, we apply controlled randomization on the power grid system properties, mainly on the set of measurements that are considered in state estimation, and the topology, especially the line admittances. We thoroughly analyze the performance of the proposed mechanism on the standard IEEE 14- and 30-bus test systems.