Visible to the public Biblio

Filters: Keyword is Validation and Verification  [Clear All Filters]
2019-03-26
[Anonymous].  2019.  Synthesizing Stealthy Reprogramming Attacks on Cardiac Devices. IEEE/ACM International Conference on Cyber-Physical Systems (ICCPS 2019).

An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmias and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICDreprogrammingattackseeks to alter the device’s parameters to induce unnecessary therapy or prevent required therapy. In this paper, we present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., are hard to detect. We focus on the discrimination algorithm underlying Boston Scientific devices (one of the principal ICD manufacturers) and formulate the synthesis problem as one of multi-objective optimization. Our solution technique is based on an Optimization Modulo Theories encoding of the problem and allows us to derive device parameters that are optimal with respect to the effectiveness-stealthiness tradeoff. Our method can be tailored to the patient’s current condition, and readily generalizes to new rhythms. To the best of our knowledge, our work is the first to derive systematic ICD reprogramming attacks designed to maximize therapy disruption while minimizing detection.

2016-11-14
2016-06-27
Donghoon Kim, Mladen A. Vouk.  2015.  Securing Software Application Chains in a Cloud. 2nd International Conference on Information Science and Security (ICISS), 2015 . :1-4.

This paper presents an approach for securing software application chains in cloud environments. We use the concept of workflow management systems to explain the model. Our prototype is based on the Kepler scientific workflow system enhanced with a security analytics package. This model can be applied to other cloud based systems. Depending on the information being received from the cloud, this approach can also offer information about internal states of the resources in
the cloud. The approach we use hinges on (1) an ability to limit attacks to Input, Remote, and Output channels (or flows), and (2) validate the flows using operational profile (OP) or certification based signals. OP based validation is a statistical approach and may miss some of the attacks. However, where enumeration is possible (e.g., static web sites), this approach can offer high assurances of validity of the flows. It is also assumed that workflow components are sound so long as the input flows are limited to operational profile. Other acceptance testing approaches could be used to validate the flows. Work in progress has two thrusts: (1) using cloud-based Kepler workflows to probe and assess security states and operation of cloud resources (specifically VMs) under different workloads leveraging DACSA sensors; and (2) analyzing effectiveness of the proposed approach in securing workflows.

2014-09-17
Subramani, Shweta, Vouk, Mladen, Williams, Laurie.  2014.  An Analysis of Fedora Security Profile. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :35:1–35:2.

This paper examines security faults/vulnerabilities reported for Fedora. Results indicate that, at least in some situations, fault roughly constant may be used to guide estimation of residual vulnerabilities in an already released product, as well as possibly guide testing of the next version of the product.

Venkatakrishnan, Roopak, Vouk, Mladen A..  2014.  Diversity-based Detection of Security Anomalies. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :29:1–29:2.

Detecting and preventing attacks before they compromise a system can be done using acceptance testing, redundancy based mechanisms, and using external consistency checking such external monitoring and watchdog processes. Diversity-based adjudication, is a step towards an oracle that uses knowable behavior of a healthy system. That approach, under best circumstances, is able to detect even zero-day attacks. In this approach we use functionally equivalent but in some way diverse components and we compare their output vectors and reactions for a given input vector. This paper discusses practical relevance of this approach in the context of recent web-service attacks.

Kästner, Christian, Pfeffer, Jürgen.  2014.  Limiting Recertification in Highly Configurable Systems: Analyzing Interactions and Isolation Among Configuration Options. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :23:1–23:2.

In highly configurable systems the configuration space is too big for (re-)certifying every configuration in isolation. In this project, we combine software analysis with network analysis to detect which configuration options interact and which have local effects. Instead of analyzing a system as Linux and SELinux for every combination of configuration settings one by one (>102000 even considering compile-time configurations only), we analyze the effect of each configuration option once for the entire configuration space. The analysis will guide us to designs separating interacting configuration options in a core system and isolating orthogonal and less trusted configuration options from this core.

Xu, Shouhuai.  2014.  Cybersecurity Dynamics. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :14:1–14:2.

We explore the emerging field of Cybersecurity Dynamics, a candidate foundation for the Science of Cybersecurity.

Mitra, Sayan.  2014.  Proving Abstractions of Dynamical Systems Through Numerical Simulations. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :12:1–12:9.

A key question that arises in rigorous analysis of cyberphysical systems under attack involves establishing whether or not the attacked system deviates significantly from the ideal allowed behavior. This is the problem of deciding whether or not the ideal system is an abstraction of the attacked system. A quantitative variation of this question can capture how much the attacked system deviates from the ideal. Thus, algorithms for deciding abstraction relations can help measure the effect of attacks on cyberphysical systems and to develop attack detection strategies. In this paper, we present a decision procedure for proving that one nonlinear dynamical system is a quantitative abstraction of another. Directly computing the reach sets of these nonlinear systems are undecidable in general and reach set over-approximations do not give a direct way for proving abstraction. Our procedure uses (possibly inaccurate) numerical simulations and a model annotation to compute tight approximations of the observable behaviors of the system and then uses these approximations to decide on abstraction. We show that the procedure is sound and that it is guaranteed to terminate under reasonable robustness assumptions.

Han, Yujuan, Lu, Wenlian, Xu, Shouhuai.  2014.  Characterizing the Power of Moving Target Defense via Cyber Epidemic Dynamics. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :10:1–10:12.

Moving Target Defense (MTD) can enhance the resilience of cyber systems against attacks. Although there have been many MTD techniques, there is no systematic understanding and quantitative characterization of the power of MTD. In this paper, we propose to use a cyber epidemic dynamics approach to characterize the power of MTD. We define and investigate two complementary measures that are applicable when the defender aims to deploy MTD to achieve a certain security goal. One measure emphasizes the maximum portion of time during which the system can afford to stay in an undesired configuration (or posture), without considering the cost of deploying MTD. The other measure emphasizes the minimum cost of deploying MTD, while accommodating that the system has to stay in an undesired configuration (or posture) for a given portion of time. Our analytic studies lead to algorithms for optimally deploying MTD.

Layman, Lucas, Diffo, Sylvain David, Zazworka, Nico.  2014.  Human Factors in Webserver Log File Analysis: A Controlled Experiment on Investigating Malicious Activity. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :9:1–9:11.

While automated methods are the first line of defense for detecting attacks on webservers, a human agent is required to understand the attacker's intent and the attack process. The goal of this research is to understand the value of various log fields and the cognitive processes by which log information is grouped, searched, and correlated. Such knowledge will enable the development of human-focused log file investigation technologies. We performed controlled experiments with 65 subjects (IT professionals and novices) who investigated excerpts from six webserver log files. Quantitative and qualitative data were gathered to: 1) analyze subject accuracy in identifying malicious activity; 2) identify the most useful pieces of log file information; and 3) understand the techniques and strategies used by subjects to process the information. Statistically significant effects were observed in the accuracy of identifying attacks and time taken depending on the type of attack. Systematic differences were also observed in the log fields used by high-performing and low-performing groups. The findings include: 1) new insights into how specific log data fields are used to effectively assess potentially malicious activity; 2) obfuscating factors in log data from a human cognitive perspective; and 3) practical implications for tools to support log file investigations.

Schmerl, Bradley, Cámara, Javier, Gennari, Jeffrey, Garlan, David, Casanova, Paulo, Moreno, Gabriel A., Glazier, Thomas J., Barnes, Jeffrey M..  2014.  Architecture-based Self-protection: Composing and Reasoning About Denial-of-service Mitigations. Proceedings of the 2014 Symposium and Bootcamp on the Science of Security. :2:1–2:12.

Security features are often hardwired into software applications, making it difficult to adapt security responses to reflect changes in runtime context and new attacks. In prior work, we proposed the idea of architecture-based self-protection as a way of separating adaptation logic from application logic and providing a global perspective for reasoning about security adaptations in the context of other business goals. In this paper, we present an approach, based on this idea, for combating denial-of-service (DoS) attacks. Our approach allows DoS-related tactics to be composed into more sophisticated mitigation strategies that encapsulate possible responses to a security problem. Then, utility-based reasoning can be used to consider different business contexts and qualities. We describe how this approach forms the underpinnings of a scientific approach to self-protection, allowing us to reason about how to make the best choice of mitigation at runtime. Moreover, we also show how formal analysis can be used to determine whether the mitigations cover the range of conditions the system is likely to encounter, and the effect of mitigations on other quality attributes of the system. We evaluate the approach using the Rainbow self-adaptive framework and show how Rainbow chooses DoS mitigation tactics that are sensitive to different business contexts.