SoS Lablet Publications
This page highlights publications by SoS University Lablets. Universities featured are part of the ongoing effort to quantify and establish security properties and behaviours. Please feel free to click on a university to see current publications and highlights.
(ID#:14-2622)
Note:
Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to SoS.Project (at) SecureDataBank.net for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.
CMU – Carnegie Mellon University
These publications were done for the Lablet activities at this school, and were listed in the Quarterly Reports back to the government. Please direct any comments to research (at) securedatabank.net if there are any questions or concerns regarding these publications.
CMU - Carnegie Mellon University
Topic: Recertification
Title: Analyzing Interactions and Isolation among Configuration Options
Author(s): Kaestner, Christian & Pfeffer, Juergen
Hard Problem: Scalability and Composability, Metrics
Abstract: PDF not found, the following abstract listed on CPS-VO SoS site: 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 (>10^2000 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. (ID#:14-2495)
URL: http://cps-vo.org/node/11855
Publication Location: HotSoS 2014
CMU - Carnegie Mellon University
Topic: Recertification
Title: Limiting Recertification in Highly Configurable Systems. Analyzing Interactions and Isolation among Configuration Options
Author(s): Kaestner, Christian & Pfeffer, Juergen
Hard Problem: Scalability and Composability, Metrics
Abstract: Christian Kastner and Jurgen Pfeffer. 2014. Limiting recertification in highly configurable systems: analyzing interactions and isolation among configuration options. In Proceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 23 , 2 pages. DOI=10.1145/2600176.2600199 http://doi.acm.org/10.1145/2600176.2600199
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. (ID#:14-2496)
URL: http://dl.acm.org/citation.cfm?id=2600199&dl=ACM&coll=DL&CFID=552978724&CFTOKEN=96539078
Publication Location: HotSoS 2014
CMU - Carnegie Mellon University
Topic: Geo-Temporal Characterization of Security Threats
Title: Longitudinal Analysis of a Large Corpus of Cyber Threat Descriptions
Author(s): Ghita Mezzour, L. Richard Carley and Kathleen M. Carley
Hard Problem: Policy-Governed Secure Collaboration
Abstract: Available from Springer via link listed below. (ID#:14-2497)
URL: http://link.springer.com/article/10.1007%2Fs11416-014-0217-8
Publication Location: Journal of Computer Virology and Hacking Techniques
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: Less is More? Investigating the Role of Examples in Security Studies using Analogical Transfer
Author(s): Ashwini Rao, Hanan Hibshi, Travis Breaux, Jean-Michel Lehker, Jianwei Niu
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: Ashwini Rao, Hanan Hibshi, Travis Breaux, Jean-Michel Lehker, and Jianwei Niu. 2014. Less is more?: investigating the role of examples in security studies using analogical transfer. InProceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 7 , 12 pages. DOI=10.1145/2600176.2600182 http://doi.acm.org/10.1145/2600176.2600182
Information system developers and administrators often overlook critical security requirements and best practices. This may be due to lack of tools and techniques that allow practitioners to tailor security knowledge to their particular context. In order to explore the impact of new security methods, we must improve our ability to study the impact of security tools and methods on software and system development. In this paper, we present early findings of an experiment to assess the extent to which the number and type of examples used in security training stimuli can impact security problem solving. To motivate this research, we formulate hypotheses from analogical transfer theory in psychology. The independent variables include number of problem surfaces and schemas, and the dependent variable is the answer accuracy. Our study results do not show a statistically significant difference in performance when the number and types of examples are varied. We discuss the limitations, threats to validity and opportunities for future studies in this area. (ID#:14-2498)
URL: http://dl.acm.org/citation.cfm?id=2600182
Publication Location: HotSoS 2014
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: Less is More? Investigating the Role of Examples in Security Studies using Analogical Transfer
Author(s): Ashwini Rao, Hanan Hibshi, Travis Breaux, Jean-Michel Lehker, Jianwei Niu
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: Ashwini Rao, Hanan Hibshi, Travis Breaux, Jean-Michel Lehker, and Jianwei Niu. 2014. Less is more?: investigating the role of examples in security studies using analogical transfer. InProceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 7 , 12 pages. DOI=10.1145/2600176.2600182 http://doi.acm.org/10.1145/2600176.2600182
Information system developers and administrators often overlook critical security requirements and best practices. This may be due to lack of tools and techniques that allow practitioners to tailor security knowledge to their particular context. In order to explore the impact of new security methods, we must improve our ability to study the impact of security tools and methods on software and system development. In this paper, we present early findings of an experiment to assess the extent to which the number and type of examples used in security training stimuli can impact security problem solving. To motivate this research, we formulate hypotheses from analogical transfer theory in psychology. The independent variables include number of problem surfaces and schemas, and the dependent variable is the answer accuracy. Our study results do not show a statistically significant difference in performance when the number and types of examples are varied. We discuss the limitations, threats to validity and opportunities for future studies in this area. (ID#:14-2499)
URL: http://dl.acm.org/citation.cfm?id=2600182
Publication Location: HotSoS 2014
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: Managing Security Requirement Patterns Using Feature Diagram Hierarchies
Author(s): R. Slavin, J.-M. Lehker, J. Niu, T. Breaux
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: Hosted on UTSA site: Security requirements patterns represent reusable security practices that software engineers can apply to improve security in their system. Reusing best practices that others have employed could have a number of benefits, such as decreasing the time spent in the requirements elicitation process or improving the quality of the product by reducing product failure risk. Pattern selection can be difficult due to the diversity of applicable patterns from which an analyst has to choose. The challenge is that identifying the most appropriate pattern for a situation can be cumbersome and time-consuming. We propose a new method that combines an inquiry-cycle based approach with the feature diagram notation to review only relevant patterns and quickly select the most appropriate patterns for the situation. Similar to patterns themselves, our approach captures expert knowledge to relate patterns based on decisions made by the pattern user. The resulting pattern hierarchies allow users to be guided through these decisions by questions, which elicit and refine requirements as well as introduce related patterns. Furthermore, our approach is unique in the way that pattern forces are interpreted as quality attributes to balance trade-offs in the resulting requirements. We evaluate our approach using access control patterns in a pattern user study. (ID#:14-2500)
URL: http://venom.cs.utsa.edu/dmz/techrep/2014/CS-TR-2014-002.pdf
Publication Location: IEEE International Requirements Engineering Conference, 2014
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: Discovering Security Requirements from Natural Language
Author(s): Slankas, J., Riaz, M. King, J., Williams, L.
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: Hosted on NCSU.edu: Natural language artifacts, such as requirements specifications, often explicitly state the security requirements for software systems. However, these artifacts may also imply additional security requirements that developers may overlook but should consider to strengthen the overall security of the system. The goal of this research is to aid requirements engineers in producing a more comprehensive and classified set of security requirements by (1) automatically identifying security-relevantsentences in natural language requirements artifacts, and (2) providing context-specific security requirements templates to help translate the security-relevant sentences into functional security requirements. Using machine learning techniques, we have developed a tool-assisted process that takes as input a set of natural language artifacts. Our process automatically identifies security-relevant sentences in the artifacts and classifies them according to the security objectives, either explicitly stated or implied by the sentences. We classified 10,963 sentences in six different documents from healthcare domain and extracted corresponding security objectives. Our manual analysis showed that 46% of the sentences were security-relevant. Of these, 28% explicitly mention security while 72% of the sentences are functional requirements with security implications. Using our tool, we correctly predict and classify 82% of the security objectives for all the sentences (precision). We identify 79% of all security objectives implied by the sentences within the documents (recall). Based on our analysis, we develop context-specific templates that can be instantiated into a set of functional security requirements by filling in key information from security-relevant sentences. (ID#:14-2501)
URL: http://www4.ncsu.edu/~mriaz/docs/re14main-hidden-in-plain-sight-preprint.pdf
Publication Location: IEEE International Requirements Engineering Conference, 2014
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: Rethinking Security Requirements in RE Research
Author(s): H. Hibshi, R. Slavin, J. Niu, T. Breaux
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: From UTSA.edu: As information security became an increasing concern for software developers and users, requirements engineering (RE) researchers brought new insight to security requirements. Security requirements aim to address security at the early stages of system design while accommodating the complex needs of different stakeholders. Meanwhile, other research communities, such as usable privacy and security, have also examined these requirements with specialized goal to make security more usable for stakeholders from product owners, to system users and administrators. In this paper we report results from conducting a literature survey to compare security requirements research from RE Conferences with the Symposium on Usable Privacy and Security (SOUPS). We report similarities between two research areas, such as common goals, technical definitions, research problems, and directions. Further, we clarify the differences between these two communities to understand how they can leverage each other's insights from out analysis, we recommend new directions in security requirements research mainly to expand the meaning of security requirements in RE to reflect the technological advancements that the broader field of security is experiencing. These recommendations to encourage cross-collaboration with other communities are not limited to the security requirements area; in fact, we believe they can be generalized to other areas of RE. (ID#:14-2502)
URL: http://venom.cs.utsa.edu/dmz/techrep/2014/CS-TR-2014-001.pdf
Publication Location: University of Texas at San Antonio, Technical Report #CS-TR-2014-001, January, 2014
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: On the Design of Empirical Studies to Evaluate Software Patterns: A Survey
Author(s): Riaz, M., Breaux, T., Williams, L.
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: From NCSU.edu: Software patterns are created with the goal of capturing expert knowledge so it can be efficiently and effectively shared with the software development community. However, patterns in practice may or may not achieve these goals. Empirical studies of the use of software patterns can help in providing deeper insight into whether these goals have been met. The objective of this paper is to aid researchers in designing empirical studies of software patterns by summarizing the study designs of software patterns available in the literature. The important components of these study designs include the evaluation criteria and how the patterns are presented to study the participants. We select and analyze 19 distinct empirical studies and identify 17 independent variables in three different categories (participants demographics; pattern presentation; problem presentation). We also extract 10 evaluation criteria with 23 associated observable measures. Additionally, by synthesizing the reported observations, we identify challenges faced during study execution. Provision of multiple domain-specific examples of pattern application and tool support to assist in pattern selection are helpful for the study participants in understanding and completing the study task. Capturing data regarding the cognitive processes of participants can provide insights into the findings of the study. (ID#:14-2503)
URL: http://repository.lib.ncsu.edu/dr/bitstream/1840.4/8269/1/tr-2012-9.pdf
Publication Location: ACM SIGSOFT'12
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: Towards a Framework for Pattern Experimentation: Understanding empirical validity in requirements engineering patterns
Author(s): Breaux, T., Hibshi, H., Rao, A., Lehker, J.-M.
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: Breaux, T.D.; Hibshi, H.; Rao, A; Lehker, J., "Towards a framework for pattern experimentation: Understanding empirical validity in requirements engineering patterns," Requirements Patterns (RePa), 2012 IEEE Second International Workshop on , vol., no., pp.41,47, 24-24 Sept. 2012 doi: 10.1109/RePa.2012.6359975
Despite the abundance of information security guidelines, system developers have difficulties implementing technical solutions that are reasonably secure. Security patterns are one possible solution to help developers reuse security knowledge. The challenge is that it takes experts to develop security patterns. To address this challenge, we need a framework to identify and assess patterns and pattern application practices that are accessible to non-experts. In this paper, we narrowly define what we mean by patterns by focusing on requirements patterns and the considerations that may inform how we identify and validate patterns for knowledge reuse. We motivate this discussion using examples from the requirements pattern literature and theory in cognitive psychology.(ID#:14-2504)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6359975&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F6338383%2F6359964%2F06359975.pdf%3Farnumber%3D6359975
Publication Location: 2nd IEEE Workshop on Requirements Engineering Patterns (RePa'12), Chicago, Illinois, Sep. 2012
CMU - Carnegie Mellon University
Topic: Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal)
Title: Characterizations and Boundaries of Security Requirements Patterns
Author(s): Slavin, R., Shen, H., Niu, J.
Hard Problem: Metrics, Human Behavior
Collaborating Institution(s): UTSA
Abstract: Slavin, R.; Hui Shen; Jianwei Niu, "Characterizations and boundaries of security requirements patterns," Requirements Patterns (RePa), 2012 IEEE Second International Workshop on , vol., no., pp.48,53, 24-24 Sept. 2012 doi: 10.1109/RePa.2012.6359974
Very often in the software development life cycle, security is applied too late or important security aspects are overlooked. Although the use of security patterns is gaining popularity, the current state of security requirements patterns is such that there is not much in terms of a defining structure. To address this issue, we are working towards defining the important characteristics as well as the boundaries for security requirements patterns in order to make them more effective. By examining an existing general pattern format that describes how security patterns should be structured and comparing it to existing security requirements patterns, we are deriving characterizations and boundaries for security requirements patterns. From these attributes, we propose a defining format. We hope that these can reduce user effort in elicitation and specification of security requirements patterns. (ID#:14-2505)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=6359974
Publication Location: 2nd IEEE Workshop on Requirements Engineering Patterns (RePa'12)
CMU - Carnegie Mellon University
Topic: Science of Secure Frameworks (CMU/Wayne State University/George Mason University Collaborative Proposal)
Title: Language-Based Architectural Control
Author(s): Jonathan Aldrich, Cyrus Omar, Alex Potanin, and Du Li
Hard Problem: Scalability and Composability
Collaborating Institution(s): Victoria University of Wellington
Abstract: From CMU.edu: Software architects design systems to achieve quality attributes like security, reliability, and performance. Key to achieving these quality attributes are design constraints governing how components of the system are configured, communicate, and access resources. Unfortunately, identifying, specifying, communication and enforcing important design constraints - achieving architectural control - can be difficult, particularly in large software systems.
We argue for the development of architectural frameworks, built to leverage language mechanisms that provide for domain-specific syntax, editor services and explicit control over capabilities, that help increase architectural control. In particular, we argue for concise, centralized architectural descriptions which are responsible for specifying constraints and passing a minimal set of ca pabilities to downstream system components, or explicitly entrusting them to individuals playing defined roles within a team. BY integrating these architectural descriptions directly into the language, the type system can help enforce technical constraints and editor services can help enforce social constraints. We sketch our approach in the context of distributed systems. (ID#:14-2506)
URL: http://www.cs.cmu.edu/~aldrich/papers/iwaco2014-arch-control.pdf
Publication Location: Submitted to 6th International Workshop on Aliasing, Capabilities, and Ownership (IWACO '14)
CMU - Carnegie Mellon University
Topic: Secure Frameworks
Title: A Systematic Survey of Self-Protecting Software Systems
Author(s): Eric Yuan, Naeem Esfahani, and Sam Malek
Hard Problem: Scalable and Composable
Abstract: Eric Yuan, Naeem Esfahani, and Sam Malek. 2014. A Systematic Survey of Self-Protecting Software Systems. ACM Trans. Auton. Adapt. Syst. 8, 4, Article 17 (January 2014), 41 pages. DOI=10.1145/2555611 http://doi.acm.org/10.1145/2555611
Self-protecting software systems are a class of autonomic systems capable of detecting and mitigating security threats at runtime. They are growing in importance, as the stovepipe static methods of securing software systems have been shown to be inadequate for the challenges posed by modern software systems. Self-protection, like other self-* properties, allows the system to adapt to the changing environment through autonomic means without much human intervention, and can thereby be responsive, agile, and cost effective. While existing research has made significant progress towards autonomic and adaptive security, gaps and challenges remain. This article presents a significant extension of our preliminary study in this area. In particular, unlike our preliminary study, here we have followed a systematic literature review process, which has broadened the scope of our study and strengthened the validity of our conclusions. By proposing and applying a comprehensive taxonomy to classify and characterize the state-of-the-art research in this area, we have identified key patterns, trends and challenges in the existing approaches, which reveals a number of opportunities that will shape the focus of future research efforts. (ID#:14-2507)
URL: http://dl.acm.org/citation.cfm?id=2555611
Publication Location: ACM Transactions on Autonomous and Adaptive Systems (TAAS)
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: Safely Composable Type-Specific Languages
Author(s): Cyrus Omar, Darya Kurilova, Ligia Nistor, Benjamin Chung, Alex Potanin, and Jonathan Aldrich
Hard Problem: Scalability and Composability, Human Behavior
Collaborating Institution(s): Victoria University of Wellington
Abstract: Available from Springer via link listed below.. (ID#:14-2508)
URL: http://link.springer.com/chapter/10.1007%2F978-3-662-44202-9_5
Publication Location: To appear in proceedings of the European Conference on Object-Oriented Programming, 2014
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming
Author(s): Joshua Sunshine, James D. Herbsleb, and Jonathan Aldrich
Hard Problem: Scalability and Composability, Human Behavior
Abstract: From Springer: Application Programming Interfaces (APIs) often define object protocols. Objects with protocols have a finite number of states and in each state a different set of method calls is valid. Many researchers have developed protocol verification tools because protocols are notoriously difficult to follow correctly. However, recent research suggests that a major challenge for API protocol programmers is effectively searching the state space. Verification is an ineffective guide for this kind of search. In this paper we instead propose Plaiddoc, which is like Javadoc except it organizes methods by state instead of by class and it includes explicit state transitions, state-based type specifications, and rich state relationships. We compare Plaiddoc to a Javadoc control in a between-subjects laboratory experiment. We find that Plaiddoc participants complete state search tasks in significantly less time and with significantly fewer errors than Javadoc participants. (ID#:14-2509)
URL: http://link.springer.com/chapter/10.1007%2F978-3-662-44202-9_7
Publication Location: To appear in proceedings of the European Conference on Object-Oriented Programming, 2014
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: In-Nimbo Sandboxing
Author(s): Michael Maass, Bill Scherlis, and Jonathan Aldrich
Hard Problem: Scalability and Composability, Human Behavior
Abstract: Michael Maass, William L. Scherlis, and Jonathan Aldrich. 2014. In-nimbo sandboxing. InProceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 1 , 12 pages. DOI=10.1145/2600176.2600177 http://doi.acm.org/10.1145/2600176.2600177
Sandboxes impose a security policy, isolating applications and their components from the rest of a system. While many sandboxing techniques exist, state of the art sandboxes generally perform their functions within the system that is being defended. As a result, when the sandbox fails or is bypassed, the security of the surrounding system can no longer be assured. We experiment with the idea of in-nimbo sandboxing, encapsulating untrusted computations away from the system we are trying to protect. The idea is to delegate computations that may be vulnerable or malicious to virtual machine instances in a cloud computing environment.
This may not reduce the possibility of an in-situ sandbox compromise, but it could significantly reduce the consequences should that possibility be realized. To achieve this advantage, there are additional requirements, including: (1) A regulated channel between the local and cloud environments that supports interaction with the encapsulated application, (2) Performance design that acceptably minimizes latencies in excess of the in-situ baseline.
To test the feasibility of the idea, we built an in-nimbo sandbox for Adobe Reader, an application that historically has been subject to significant attacks. We undertook a prototype deployment with PDF users in a large aerospace firm. In addition to thwarting several examples of existing PDF-based malware, we found that the added increment of latency, perhaps surprisingly, does not overly impair the user experience with respect to performance or usability. (ID#:14-2510)
URL: http://dl.acm.org/citation.cfm?id=2600177
Publication Location: To appear in proceedings of HotSOS, 2014.
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: The Power of Interoperability: Why Objects Are Inevitable
Author(s): Jonathan Aldrich
Hard Problem: Scalability and Composability, Human Behavior
Abstract: Jonathan Aldrich. 2013. The power of interoperability: why objects are inevitable. In Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software (Onward! '13). ACM, New York, NY, USA, 101-116. DOI=10.1145/2509578.2514738 http://doi.acm.org/10.1145/2509578.2514738
Three years ago in this venue, Cook argued that in their essence, objects are what Reynolds called procedural data structures. His observation raises a natural question: if procedural data structures are the essence of objects, has this contributed to the empirical success of objects, and if so, how?
This essay attempts to answer that question. After reviewing Cook's definition, I propose the term service abstractions to capture the essential nature of objects. This terminology emphasizes, following Kay, that objects are not primarily about representing and manipulating data, but are more about providing services in support of higher-level goals. Using examples taken from object-oriented frameworks, I illustrate the unique design leverage that service abstractions provide: the ability to define abstractions that can be extended, and whose extensions are interoperable in a first-class way. The essay argues that the form of interoperable extension supported by service abstractions is essential to modern software: many modern frameworks and ecosystems could not have been built without service abstractions. In this sense, the success of objects was not a coincidence: it was an inevitable consequence of their service abstraction nature. (ID#:14-2511)
URL: http://dl.acm.org/citation.cfm?id=2514738
Publication Location: In Onward! Essays, 2013.
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: Type-Directed, Whitespace-Delimited Parsing for Embedded DSLs
Author(s): Cyrus Omar, Benjamin Chung, Darya Kurilova, Alex Potanin, and Jonathan Aldrich
Hard Problem: Scalability and Composability, Human Behavior
Abstract: From CMU.edu: Domain-specific languages improve ease-of-use, expressiveness and verifiability, but defining and using different DSLs within a single application remains difficult. We introduce an approach for embedded DSLs where 1) whitespace delimits DSL-governed blocks, and 2) the parsing and type checking phases occur in tandem so that the expected type of the block determines which domain-specific parser governs that block. We argue that this approach occupies a sweet spot, providing high expressiveness as ease-of-use while maintaining safe composability. We introduce the design, provide examples and describe an ongoing implementation of this strategy in the Wyvern programming language. We also discuss how a more conventional keyword-directed strategy for parsing of DSLs can arise as a special case of this type-directed strategy. (ID#:14-2512)
URL: http://www.cs.cmu.edu/~aldrich/papers/globaldsl13.pdf
Publication Location: Proceedings of the International Workshop on the Globalization of Domain Specific Languages (GlobalDSL), 2013
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: Wyvern: A Simple, Typed, and Pure Object-Oriented Language
Author(s): Ligia Nistor, Darya Kurilova, Stephanie Balzer, Benjamin Chung, Alex Potanin, and Jonathan Aldrich
Hard Problem: Scalability and Composability, Human Behavior
Abstract: Ligia Nistor, Darya Kurilova, Stephanie Balzer, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. 2013. Wyvern: a simple, typed, and pure object-oriented language. In Proceedings of the 5th Workshop on MechAnisms for SPEcialization, Generalization and inHerItance (MASPEGHI '13), Markku Sakkinen (Ed.). ACM, New York, NY, USA, 9-16. DOI=10.1145/2489828.2489830 http://doi.acm.org/10.1145/2489828.2489830
The simplest and purest practical object-oriented language designs today are seen in dynamically-typed languages, such as Smalltalk and Self. Static types, however, have potential benefits for productivity, security, and reasoning about programs. In this paper, we describe the design of Wyvern, a statically typed, pure object-oriented language that attempts to retain much of the simplicity and expressiveness of these iconic designs.
Our goals lead us to combine pure object-oriented and functional abstractions in a simple, typed setting. We present a foundational object-based language that we believe to be as close as one can get to simple typed lambda calculus while keeping object-orientation. We show how this foundational language can be translated to the typed lambda calculus via standard encodings. We then define a simple extension to this language that introduces classes and show that classes are no more than sugar for the foundational object-based language. Our future intention is to demonstrate that modules and other object-oriented features can be added to our language as not more than such syntactical extensions while keeping the object-oriented core as pure as possible.
The design of Wyvern closely follows both historical and modern ideas about the essence of object-orientation, suggesting a new way to think about a minimal, practical, typed core language for objects. (ID#:14-2513)
URL: http://dl.acm.org/citation.cfm?id=2489830
Publication Location: Proceedings of the Workshop on Mechanisms for Specialization, Generalization, and Inheritance (MASPEGHI), 2013
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: How Does Your Password Measure Up? The Effect of Strength Meters on Password Creation
Author(s): vBlase Ur, Patrick Gage Kelley, Saranga Komanduri, Joel Lee, Michael Maass, Michelle Mazurek, Timothy Passaro, Richard Shay, Timothy Vidas, Lujo Bauer, Nicolas Christin, and Lorrie Faith Cranor
Hard Problem: Scalability and Composability, Human Behavior
Abstract: Blase Ur, Patrick Gage Kelley, Saranga Komanduri, Joel Lee, Michael Maass, Michelle L. Mazurek, Timothy Passaro, Richard Shay, Timothy Vidas, Lujo Bauer, Nicolas Christin, and Lorrie Faith Cranor. 2012. How does your password measure up? the effect of strength meters on password creation. In Proceedings of the 21st USENIX conference on Security symposium (Security'12). USENIX Association, Berkeley, CA, USA, 5-5.
To help users create stronger text-based passwords, many web sites have deployed password meters that provide visual feedback on password strength. Although these meters are in wide use, their effects on the security and usability of passwords have not been well studied.
We present a 2,931-subject study of password creation in the presence of 14 password meters. We found that meters with a variety of visual appearances led users to create longer passwords. However, significant increases in resistance to a password-cracking algorithm were only achieved using meters that scored passwords stringently. These stringent meters also led participants to include more digits, symbols, and uppercase letters.
Password meters also affected the act of password creation. Participants who saw stringent meters spent longer creating their password and were more likely to change their password while entering it, yet they were also more likely to find the password meter annoying. However, the most stringent meter and those without visual bars caused participants to place less importance on satisfying the meter. Participants who saw more lenient meters tried to fill the meter and were averse to choosing passwords a meter deemed "bad" or "poor." Our findings can serve as guidelines for administrators seeking to nudge users towards stronger passwords. (ID#:14-2514)
URL: http://dl.acm.org/citation.cfm?id=2362793.2362798
Publication Location: Proceedings of the 21st USENIX Security Symposium.
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: Declarative Access Policies based on Objects, Relationships, and States
Author(s): Simin Chen
Hard Problem: Scalability and Composability, Human Behavior
Abstract: Simin Chen. 2012. Declarative access policies based on objects, relationships, and states. InProceedings of the 3rd annual conference on Systems, programming, and applications: software for humanity (SPLASH '12). ACM, New York, NY, USA, 99-100. DOI=10.1145/2384716.2384757 http://doi.acm.org/10.1145/2384716.2384757
Access policies are hard to express in existing programming languages. However, their accurate expression is a prerequisite for many of today's applications. We propose a new language that uses classes, first-class relationships, and first-class states to express access policies in a more declarative and fine-grained way than existing solutions allow. (ID#:14-2515)
URL: http://dl.acm.org/citation.cfm?id=2384757
Publication Location: Proceedings of the SPLASH 2012 Student Research Competition
CMU - Carnegie Mellon University
Topic: A Language and Framework for Development of Secure Mobile Applications
Title: Domain Specific Security through Extensible Type Systems
Author(s): Nathan Fulton
Hard Problem: Scalability and Composability, Human Behavior
Abstract: Nathan Fulton. 2012. Security through extensible type systems. In Proceedings of the 3rd annual conference on Systems, programming, and applications: software for humanity (SPLASH '12). ACM, New York, NY, USA, 107-108. DOI=10.1145/2384716.2384761 http://doi.acm.org/10.1145/2384716.2384761
Researchers interested in security often wish to introduce new primitives into a language. Extensible languages hold promise in such scenarios, but only if the extension mechanism is sufficiently safe and expressive. This paper describes several modifications to an extensible language motivated by end-to-end security concerns. (ID#:14-2516)
URL: http://dl.acm.org/citation.cfm?id=2384761
Publication Location: Proceedings of the SPLASH 2012 Student Research Competition
CMU - Carnegie Mellon University
Topic: Race Vulnerability Study and Hybrid Race Detection (CMU/University of Nebraska, Lincoln Collaborative Proposal)
Title: SimRT: An Automated Framework to Support Regression Testing for Data Races
Author(s): Vingting Yu, Witawas Srisa-an, and Gregg Rothermel
Abstract: Tingting Yu, Witawas Srisa-an, and Gregg Rothermel. 2014. SimRT: an automated framework to support regression testing for data races. In Proceedings of the 36th International Conference on Software Engineering (ICSE 2014). ACM, New York, NY, USA, 48-59. DOI=10.1145/2568225.2568294 http://doi.acm.org/10.1145/2568225.2568294
Concurrent programs are prone to various classes of difficult-to-detect faults, of which data races are particularly prevalent. Prior work has attempted to increase the cost-effectiveness of approaches for testing for data races by employing race detection techniques, but to date, no work has considered cost-effective approaches for re-testing for races as programs evolve. In this paper we present SimRT, an automated regression testing framework for use in detecting races introduced by code modifications. SimRT employs a regression test selection technique, focused on sets of program elements related to race detection, to reduce the number of test cases that must be run on a changed program to detect races that occur due to code modifications, and it employs a test case prioritization technique to improve the rate at which such races are detected. Our empirical study of SimRT reveals that it is more efficient and effective for revealing races than other approaches, and that its constituent test selection and prioritization components each contribute to its performance. (ID#:14-2517)
URL: http://dl.acm.org/citation.cfm?id=2568294
Publication Location: Proceedings of the International Conference on Software Engineering (ICSE) 2014
CMU - Carnegie Mellon University
Topic: Architecture-based Self-securing Systems
Title: Measuring Attack Surface in Software Architecture
Author(s): Jeffrey Gennari and David Garlan
Abstract: From CMU.edu: In this report we show how to adapt the notion of "attack surgace" to formally evaluate security properties at the architectural level of design and to identity the vulnerabilities in architectural designs. Further we explore the application of this metric in the context of architecture-based transformations to improve security by reducing the attack surface. The transformations are described in detail and validated with a simple experiment. (ID#:14-2518)
URL: http://reports-archive.adm.cs.cmu.edu/anon/isr2011/CMU-ISR-11-121.pdf
Publication Location: Technical Report, CMU-ISR-11-121
CMU - Carnegie Mellon University
Topic: Architecture-based Self-securing Systems
Title: Evolution Styles: foundations and models for software architecture evolution
Author(s): David Garlan, Jeffrey M. Barnes and Bradley Schmerl
Abstract: Jeffrey M. Barnes, David Garlan, and Bradley Schmerl. 2014. Evolution styles: foundations and models for software architecture evolution. Softw. Syst. Model. 13, 2 (May 2014), 649-678. DOI=10.1007/s10270-012-0301-9 http://dx.doi.org/10.1007/s10270-012-0301-9
As new market opportunities, technologies, platforms, and frameworks become available, systems require large-scale and systematic architectural restructuring to accommodate them. Today's architects have few techniques to help them plan this architecture evolution. In particular, they have little assistance in planning alternative evolution paths, trading off various aspects of the different paths, or knowing best practices for particular domains. In this paper, we describe an approach for planning and reasoning about architecture evolution. Our approach focuses on providing architects with the means to model prospective evolution paths and supporting analysis to select among these candidate paths. To demonstrate the usefulness of our approach, we show how it can be applied to an actual architecture evolution. In addition, we present some theoretical results about our evolution path constraint specification language. (ID#:14-2519)
URL: http://dl.acm.org/citation.cfm?id=2617332
Publication Location: Software and Systems Modeling
CMU - Carnegie Mellon University
Topic: Architecture-based Self-securing Systems
Title: Architecture-based run-time diagnosis of multiple, correlated faults
Author(s): Paulo Casanova, Bradley Schmerl, David Garlan, and Rui Abreu
Abstract: Paulo Casanova, David Garlan, Bradley Schmerl, and Rui Abreu. 2013. Diagnosing architectural run-time failures. In Proceedings of the 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS '13). IEEE Press, Piscataway, NJ, USA, 103-112
Self-diagnosis is a fundamental capability of self-adaptive systems. In order to recover from faults, systems need to know which part is responsible for the incorrect behavior. In previous work we showed how to apply a design-time diagnosis technique at run time to identify faults at the architectural level of a system. Our contributions address three major shortcomings of our previous work: 1) we present an expressive, hierarchical language to describe system behavior that can be used to diagnose when a system is behaving different to expectation; the hierarchical language facilitates mapping low level system events to architecture level events; 2) we provide an automatic way to determine how much data to collect before an accurate diagnosis can be produced; and 3) we develop a technique that allows the detection of correlated faults between components. Our results are validated experimentally by injecting several failures in a system and accurately diagnosing them using our algorithm. (ID#:14-2520)
URL: http://dl.acm.org/citation.cfm?id=2487354
Publication Location: Software Architecture
CMU - Carnegie Mellon University
Topic: Architecture-based Self-securing Systems
Title: Software engineering for self-adaptive systems: A second research roadmap
Author(s): Rogerio de Lemos, Holger Giese, Hausi A. Muller, et al.
Hard Problem: Resilient Architectures
Abstract: Available from Springer via link listed below.. (ID#:14-2521)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-35813-5_1
Publication Location: Software Engineering for Self-Adaptive Systems II
CMU - Carnegie Mellon University
Topic: Architecture-based Self-securing Systems
Title: Diagnosing architectural run-time failures
Author(s): Paulo Casanova, David Garlan, Bradley Schmerl and Rui Abreu
Abstract: Paulo Casanova, David Garlan, Bradley Schmerl, and Rui Abreu. 2013. Diagnosing architectural run-time failures. In Proceedings of the 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS '13). IEEE Press, Piscataway, NJ, USA, 103-112.
Self-diagnosis is a fundamental capability of self-adaptive systems. In order to recover from faults, systems need to know which part is responsible for the incorrect behavior. In previous work we showed how to apply a design-time diagnosis technique at run time to identify faults at the architectural level of a system. Our contributions address three major shortcomings of our previous work: 1) we present an expressive, hierarchical language to describe system behavior that can be used to diagnose when a system is behaving different to expectation; the hierarchical language facilitates mapping low level system events to architecture level events; 2) we provide an automatic way to determine how much data to collect before an accurate diagnosis can be produced; and 3) we develop a technique that allows the detection of correlated faults between components. Our results are validated experimentally by injecting several failures in a system and accurately diagnosing them using our algorithm. (ID#:14-2522)
URL: http://dl.acm.org/citation.cfm?id=2487354
Publication Location: the 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems
CMU - Carnegie Mellon University
Topic: Using Crowdsourcing to Analyze and Summarize the Security of Mobile Applications
Title: Expectation and Purpose: Understanding Users' Mental Models of Mobile App Privacy through Crowdsourcing
Author(s): Jialiu Lin, Shahriyar Amini, Jason Hong, Norman Sadeh, Janne Lindqvist, Joy Zhang
Abstract: Jialiu Lin, Shahriyar Amini, Jason I. Hong, Norman Sadeh, Janne Lindqvist, and Joy Zhang. 2012. Expectation and purpose: understanding users' mental models of mobile app privacy through crowdsourcing. In Proceedings of the 2012 ACM Conference on Ubiquitous Computing(UbiComp '12). ACM, New York, NY, USA, 501-510. DOI=10.1145/2370216.2370290 http://doi.acm.org/10.1145/2370216.2370290
Smartphone security research has produced many useful tools to analyze the privacy-related behaviors of mobile apps. However, these automated tools cannot assess people's perceptions of whether a given action is legitimate, or how that action makes them feel with respect to privacy. For example, automated tools might detect that a blackjack game and a map app both use one's location information, but people would likely view the map's use of that data as more legitimate than the game. Our work introduces a new model for privacy, namely privacy as expectations. We report on the results of using crowdsourcing to capture users' expectations of what sensitive resources mobile apps use. We also report on a new privacy summary interface that prioritizes and highlights places where mobile apps break people's expectations. We conclude with a discussion of implications for employing crowdsourcing as a privacy evaluation technique. (ID#:14-2523)
URL: http://dl.acm.org/citation.cfm?id=2370290
Publication Location: UbiComp 2012
CMU - Carnegie Mellon University
Topic: Secure Composition of Systems and Policies
Title: A Type System for Reasoning about Trace Properties For Distributed Systems
Author(s): Limin Jia, Deepak Garg, Anupam Datta
Abstract: Not Found (ID#:14-2524)
URL: Not Found
Publication Location: Draft CMU Technical Paper
CMU - Carnegie Mellon University
Topic: Secure Composition of Systems and Policies
Title: Compositional Flaws - A Technical Account
Author(s): Anupam Datta, Limin Jia and Jeannette Wing
Abstract: not found (ID#:14-2525)
URL: not found
Publication Location: Draft CMU Technical Paper
CMU - Carnegie Mellon University
Topic: Secure Composition of Systems and Policies
Title: Compositional Security for Higher-Order Programs
Author(s): Limin Jia, Deepak Garg and Anupam Datta
Abstract: Located as a PPT on CPSVO-SoS (ID#:14-2526)
URL: http://cps-vo.org/node/9531
Publication Location: not available
CMU - Carnegie Mellon University
Topic: Secure Composition of Systems and Policies
Title: An Epistemic Formulation of Information Flow Analysis
Author(s): Arbob Ahmad and Robert Harper
Abstract: From cmu.edu: The non-interference (NI) property defines a program to be secure if changes to high-security inputs cannot alter the values of low-security outputs. NI indirectly states the epistemic property that no low-security principal acquires knowledge of high-security data. We consider a directly epistemic account of information flow (IF) security focusing on the knowledge flows engendered by the program's execution. Storage effects are of primary interest, since principals acquire knowledge from the execution only through these effects. The IF properties of the individual effectful actions are characterized using a substructural epistemic logic that accounts for the knowledge transferred through their execution. We prove that a low-security principal never acquires knowledge of a high-security input by execution a well-typed program.
The epistemic approach has several advantages over NI. First, it directly accounts for the knowledge flow engendered by a program. Second, in contrast to the bimodal NI property, the epistemic approach accounts for authorized declassification. We prove that a low-security principal acquires knowledge of a high security input only if it is authorized by a proof in authorization logic. Third, the explicit formulation of IF properties as an epistemic theory provides a crisp treatment of "side channels". Rather than prove that a principle does not know a secret, we instead prove that it is not provable that the principal knows that secret. The latter statement characterizes the "minimal model," for which a precise statement may be made, whereas the former applies to "any model," including those with "side channels" that violate the model's basic premises. Fourth, the NI property is re-positioned as providing an adequacy proof of epistemic theory of effects, ensuring that the logical theory corresponds to the actual program behavior. In this way we obtain a generalization of the classical approach to IF security that extends to authorized declassification. (ID#:14-2527)
URL: http://www.cs.cmu.edu/~adahmad/epi-if-draft.pdf
Publication Location: IEEE 26th Computer Security Foundations Symposium (CSF 2013)
CMU - Carnegie Mellon University
Topic: Trust from Explicit Evidence: Integrating Digital Signatures and Formal Proofs
Title: Inductive types in homotopy type theory
Author(s): Steven Awodey, Nicola Gambino, and Kristina Sojakova
Abstract: Steve Awodey, Nicola Gambino, and Kristina Sojakova. 2012. Inductive Types in Homotopy Type Theory. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS '12). IEEE Computer Society, Washington, DC, USA, 95-104. DOI=10.1109/LICS.2012.21 http://dx.doi.org/10.1109/LICS.2012.21
Homotopy type theory is an interpretation of Martin-LAPf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research. (ID#:14-2528)
URL: http://dl.acm.org/citation.cfm?id=2359495
Publication Location: Proceedings of the 27th Conference on Logic in Computer Science (LICS 2012)
CMU - Carnegie Mellon University
Topic: Trust from Explicit Evidence: Integrating Digital Signatures and Formal Proofs
Title: Higher-Order Processes, Functions, and Sessions: A monadic integration
Author(s): Bernardo Toninho, Luis Caires, and Frank Pfenning
Abstract: Bernardo Toninho, Luis Caires, and Frank Pfenning. 2013. Higher-Order processes, functions, and sessions: a monadic integration. In Proceedings of the 22nd European conference on Programming Languages and Systems (ESOP'13), Matthias Felleisen and Philippa Gardner (Eds.). Springer-Verlag, Berlin, Heidelberg, 350-369. DOI=10.1007/978-3-642-37036-6_20 http://dx.doi.org/10.1007/978-3-642-37036-6_20
In prior research we have developed a Curry-Howard interpretation of linear sequent calculus as session-typed processes. In this paper we uniformly integrate this computational interpretation in a functional language via a linear contextual monad that isolates session-based concurrency. Monadic values are open process expressions and are first class objects in the language, thus providing a logical foundation for higher-order session typed processes. We illustrate how the combined use of the monad and recursive types allows us to cleanly write a rich variety of concurrent programs, including higher-order programs that communicate processes. We show the standard metatheoretic result of type preservation, as well as a global progress theorem, which to the best of our knowledge, is new in the higher-order session typed setting. (ID#:14-2529)
URL: http://dl.acm.org/citation.cfm?id=2450295
Publication Location: Programming Languages and Systems
CMU - Carnegie Mellon University
Topic: Systematic Testing of Distributed and Multi-threaded Systems at Scale
Title: Estimating Runtime of Stateless Exploration
Author(s): Jiri Simsa, Randy Bryant, Garth Gibson, Jason Hickey, John Wilkes
Abstract: From CMU.edu: In the past 15 years, stateless exploration, a collection of techniques for automated and systematic testing of concurrent programs, has experienced wide-spread adoption. As stateless exploration moves into practice, becoming part of testing infrastructures of large-scale system developers, new practical challenges are being identified. In this paper we address the problem of efficient allocation of resources to stateless exploration runs. To this end, this paper presents techniques for estimating the total runtime of stateless exploration runs and policies for allocating resources among tests based on these runtime estimates.
Evaluating our techniques on a collection of traces from a real-world deployment at Google, we demonstrate the techniques' success at providing accurate runtime estimations, achieving estimation accuracy above 60% after as little as 1% of the state space has been explored. We further show that these estimates can be used to implement intelligent resource allocation policies that meet testing objectives more than twice as efficiently as the round-robin policy. (ID#:14-2530)
URL: http://www.pdl.cmu.edu/PDL-FTP/Storage/CMU-PDL-12-113.pdf
Publication Location: CMU-PDL-12-113, 2012
CMU - Carnegie Mellon University
Topic: Systematic Testing of Distributed and Multi-threaded Systems at Scale
Title: Borrow checking: A safe alias analysis for types with ownership and mutability
Author(s): Niko Matsakis, Brian Anderson, Ben Blum, Tim Chevalier, Graydon Hoare, Patrick Walton, David Herman
Abstract: not found (ID#:14-2531)
URL: not found
Publication Location: PLDI 2013.
CMU - Carnegie Mellon University
Topic: Validating Productivity Benefits of Type-Like Behavioral Specifications
Title: Searching the State Space: A Qualitative Study of API Protocol Usability
Author(s): Joshua Sunshine, James D Herbsleb, Jonathan Aldrich
Abstract: From CMU.edu: Application Programming Interfaces (APIs) often define protocols - restrictions on the order of client class to API methods. API protocols are common and difficult to use, which has generated tremendous research effort in alternative specifications, implementation, and verification techniques. However, little is understood about the barriers programmers face when using these APIs, and therefore the research effort may be misdirected.
To understand these barriers better, we perform a two-part qualitative study. First, we study developer forums to identify problems that developers have with protocols. Second, we perform a think-aloud observational study, in which we systematically observe professional programmers struggle with these same problems to get more detail on the nature of their struggles and how they use available resources. In our observations, programmer time was spent primarily on four types of searches of the protocol state space. These observations suggest protocol-targeted tools, languages, and verification techniques will be most effective if they enable programmers to efficiently perform state search. (ID#:14-2532)
URL: http://www.cs.cmu.edu/~jssunshi/pubs/searchingfse14draft.pdf
Publication Location: not available
CMU - Carnegie Mellon University
Topic: Improving the Usability of Security Requirements by Software Developers through Empirical Studies and Analysis
Title: Security Requirements Patterns: Understanding the Science Behind the Art of Pattern Writing
Author(s): Maria Riaz, Laurie Williams
Abstract: Riaz, M.; Williams, L., "Security requirements patterns: understanding the science behind the art of pattern writing," Requirements Patterns (RePa), 2012 IEEE Second International Workshop on , vol., no., pp.29,34, 24-24 Sept. 2012
doi: 10.1109/RePa.2012.6359977
Security requirements engineering ideally combines expertise in software security with proficiency in requirements engineering to provide a foundation for developing secure systems. However, security requirements are often inadequately understood and improperly specified, often due to lack of security expertise and a lack of emphasis on security during early stages of system development. Software systems often have common and recurrent security requirements in addition to system-specific security needs. Security requirements patterns can provide a means of capturing common security requirements while documenting the context in which a requirement manifests itself and the tradeoffs involved. The objective of this paper is to aid in understanding of the process for pattern development and provide considerations for writing effective security requirements patterns. We analyzed existing literature on software patterns, problem solving and cognition to outline the process for developing software patterns. We also reviewed strategies for specifying reusable security requirements and security requirements patterns. Our proposed considerations can aid pattern writers in capturing necessary contextual information when documenting security requirements patterns to facilitate application and integration of security requirements. (ID#:14-2533)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6359977&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F6338383%2F6359964%2F06359977.pdf%3Farnumber%3D6359977
Publication Location: 2nd IEEE Workshop on Requirements Engineering Patterns (RePa'12)
CMU - Carnegie Mellon University
Topic: Proofs and Signatures
Title: Behavioral Polymorphism and Parametricity in Session-Based Communication Author(s): Luis Caires, Jorge A. Perez, Frank Pfenning, and Bernardo Toninho
Abstract: Luis Caires, Jorge A. Perez, Frank Pfenning, and Bernardo Toninho. 2013. Behavioral polymorphism and parametricity in session-based communication. In Proceedings of the 22nd European conference on Programming Languages and Systems (ESOP'13), Matthias Felleisen and Philippa Gardner (Eds.). Springer-Verlag, Berlin, Heidelberg, 330-349. DOI=10.1007/978-3-642-37036-6_19 http://dx.doi.org/10.1007/978-3-642-37036-6_19
We investigate a notion of behavioral genericity in the context of session type disciplines. To this end, we develop a logically motivated theory of parametric polymorphism, reminiscent of the Girard-Reynolds polymorphic l-calculus, but casted in the setting of concurrent processes. In our theory, polymorphism accounts for the exchange of abstract communication protocols and dynamic instantiation of heterogeneous interfaces, as opposed to the exchange of data types and dynamic instantiation of individual message types. Our polymorphic session-typed process language satisfies strong forms of type preservation and global progress, is strongly normalizing, and enjoys a relational parametricity principle. Combined, our results confer strong correctness guarantees for communicating systems. In particular, parametricity is key to derive non-trivial results about internal protocol independence, a concurrent analogous of representation independence, and non-interference properties of modular, distributed systems. (ID#:14-2534)
URL: http://dl.acm.org/citation.cfm?id=2450294
Publication Location: ESOP'13 Proceedings of the 22nd European conference on Programming Languages and Systems
CMU - Carnegie Mellon University
Topic: Proofs and Signatures
Title: LiquidPi: Inferrable Dependent Session Types
Author(s): Dennis Griffith and Elsa Gunter
Abstract: Available from Springer via link listed below.. (ID#:14-2535)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-38088-4_13
Publication Location: 5th NASA Formal Methods Symposium (NFM), May 2013
CMU - Carnegie Mellon University
Topic: Proofs and Signatures
Title: Linear Logic Propositions as Session Types
Author(s): Luis Caires, Frank Pfenning, and Bernardo Toninho
Abstract: From CMU.edu: Throughout the years, several typing disciplines for the p-calculus have been proposed. Arguably, the most widespread of these typing disciplines consists of session types. Session types describe the input/output behavior of processes and traditionally provide strong guarantees about this behavior (i.e., deadlock freedom and fidelity). While these systems exploit a fundamental notion of linearity, the precise connection between linear logic and session types has not been well understood.
This paper proposes a type system for the p-calculus that corresponds to a standard sequent calculus presentation of intuitionistic linear logic, interpreting linear propositions as session types and thus providing a purely logical account of all key features and properties of session types. We show the deep correspondence between linear logic and session types by exhibiting a tight operational correspondence between cut elimination steps and process reductions. We also discuss an alternative presentation of linear session types based on classical linear logic, and compare our development with other more traditional session type systems. (ID#:14-2536)
URL: http://www.cs.cmu.edu/~btoninho/mscs12.pdf
Publication Location: Mathematical Structures in Computer Science (MSCS)
CMU - Carnegie Mellon University
Topic: Security Reasoning for Distributed Systems with Uncertainty
Title: A Generalization of SAT and #SAT for Robust Policy Evaluation
Author(s): E. Zawadzki, A. Platzer, G. Gordon
Abstract: Erik Zawadzki, Andre Platzer, and Geoffrey J. Gordon. 2013. A generalization of SAT and #SAT for robust policy evaluation. In Proceedings of the Twenty-Third international joint conference on Artificial Intelligence (IJCAI'13), Francesca Rossi (Ed.). AAAI Press 2583-2589.
Both SAT and #SAT can represent difficult problems in seemingly dissimilar areas such as planning, verification, and probabilistic inference. Here, we examine an expressive new language, #SAT, that generalizes both of these languages. #SAT problems require counting the number of satisfiable formulas in a concisely-describable set of existentially-quantified, propositional formulas. We characterize the expressiveness and worst-case difficulty of #SAT by proving it is complete for the complexity class #PNP[1], and relating this class to more familiar complexity classes. We also experiment with three new general-purpose #SAT solvers on a battery of problem distributions including a simple logistics domain. Our experiments show that, despite the formidable worst-case complexity of #PNP[1], many of the instances can be solved efficiently by noticing and exploiting a particular type of frequent structure. (ID#:14-2537)
URL: http://dl.acm.org/citation.cfm?id=2540500
Publication Location: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence
CMU - Carnegie Mellon University
Topic: Geo-Temporal Characterization of Security Threats
Title: A Large-Scale Exploratory Analysis of the Cyber-Threat Landscape over Time
Author(s): Ghita Mezzour, L. Richard Carley, Kathleen M. Carley
Hard Problem: Policy governed secure collaboration, resilient architectures.
Abstract: Available from Springer via link listed below.. (ID#:14-2538)
URL: http://link.springer.com/article/10.1007%2Fs11416-014-0217-8
Publication Location: Springer
CMU - Carnegie Mellon University
Topic: No Listed Topic
Title: Efficient Exploratory Testing of Concurrent Systems
Author(s): Jiri Simsa, Randy Bryant, Garth Gibson, Jason Hickey
Abstract: From CMU.edu: In our experience, exploratory testing has reached a level of maturity that makes it a practical and often the most cost-effective approach to testing. Notably, previous work has demonstrated that exploratory testing is capable of finding bugs even in well-tested systems [4, 17, 24, 23]. However, the number of bugs found gives little indication of the efficiency of a testing approach. To drive testing efficiency, this paper focuses on techniques for measuring and maximizing the coverage achieved by exploratory testing. In particular, this paper describes the design, implementation, and evaluation of Eta, a framework for exploratory testing of multi-threaded components of a large-scale cluster management system at Google. For simpler tests (with millions to billions of possible executions), Eta achieves complete coverage one to two order of magnitude faster than random testing. For complex test, Eta adopts a state space reduction technique to avoid the need to explore over 85% of executions and harnesses parallel processing to explore multiple test executions concurrently, achieving a throughput of up to 17.5x. (ID#:14-2539)
URL: http://www.pdl.cmu.edu/PDL-FTP/associated/CMU-PDL-11-113.pdf
Publication Location: Carnegie Mellon University Parallel Data Laboratory Techical Report CMU-PDL-11-113
CMU - Carnegie Mellon University
Topic: No Listed Topic
Title: Landslide: Systematic Exploration for Kernel-Space Race Detection
Author(s): Ben Blum
Abstract: From pitt.edu: Systematic exploration is an approach to finding race conditions by deterministically executing every possible interleaving of thread transitions and identifying which ones expose bugs. Current systematic exploration techniques are suitable for testing user-space programs, but are inadequate for testing kernels, where the testing framework's control over concurrency is more complicated.
We present Landslide, a systematic exploration tool for finding races in kernels. Landslide targets Pebbles, the kernel specification that students implement in the undergraduate Opening Systems course at Carnegie Mellon University (15-410). We discuss the techniques Landslide uses to address the general challenges of kernel-level concurrency, and we evaluate its effectiveness and usability as a debugging aid. We show that our techniques make systematic testing in kernel-space feasible and that Landslide is a useful tool for doing so in the context of 15-410. (ID#:14-2540)
URL: http://www.pdl.cmu.edu/PDL-FTP/associated/CMU-CS-12-118.pdf
Publication Location: Carnegie Mellon University Parallel Data Laboratory Techical Report CMU-PDL-12-118
CMU - Carnegie Mellon University
Topic: No Listed Topic
Title: Scalable Dynamic Partial Order Reduction
Author(s): Jiri Simsa, Randal Bryant, Garth Gibson and Jason Hickey
Abstract: From Springer: Systematic testing, first demonstrated in small, specialized cases 15 years ago, has matured sufficiently for large-scale systems developers to begin to put it into practice. With actual deployment come new, pragmatic challenges to the usefulness of the techniques. In this paper we are concerned with scaling dynamic partial order reduction, a key technique for mitigating the state space explosion problem, to very large clusters. In particular, we present a new approach for distributed dynamic partial order reduction. Unlike previous work, our approach is based on a novel exploration algorithm that 1) enables trading space complexity for parallelism, 2) achieves efficient load-balancing through time-slicing, 3) provides for fault tolerance, which we consider a mandatory aspect of scalability, 4) scales to more than a thousand parallel workers, and 5) is guaranteed to avoid redundant exploration of overlapping portions of the state space. (ID#:14-2541)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-35632-2_4
Publication Location: 3rd International Conference on Runtime Verification (RV2012) 2012
CMU - Carnegie Mellon University
Topic: No Listed Topic
Title: Architecture-Based Self-Protecting Software Systems
Author(s): Eric Yuan, Sam Malek, Bradley Schmerl, David Garlan and Jeffrey Gennari
Abstract: Eric Yuan, Sam Malek, Bradley Schmerl, David Garlan, and Jeff Gennari. 2013. Architecture-based self-protecting software systems. In Proceedings of the 9th international ACM Sigsoft conference on Quality of software architectures (QoSA '13). ACM, New York, NY, USA, 33-42. DOI=10.1145/2465478.2465479 http://doi.acm.org/10.1145/2465478.246547
Since conventional software security approaches are often manually developed and statically deployed, they are no longer sufficient against today's sophisticated and evolving cyber security threats. This has motivated the development of self-protecting software that is capable of detecting security threats and mitigating them through runtime adaptation techniques. In this paper, we argue for an architecture-based self- protection (ABSP) approach to address this challenge. In ABSP, detection and mitigation of security threats are informed by an architectural representation of the running system, maintained at runtime. With this approach, it is possible to reason about the impact of a potential security breach on the system, assess the overall security posture of the system, and achieve defense in depth. To illustrate the effectiveness of this approach, we present several architecture adaptation patterns that provide reusable detection and mitigation strategies against well-known web application security threats. Finally, we describe our ongoing work in realizing these patterns on top of Rainbow, an existing architecture-based adaptation framework. (ID#:14-2542)
URL: http://dl.acm.org/citation.cfm?id=2465479
Publication Location: QoSA '13 Proceedings of the 9th international ACM Sigsoft conference on Quality of software architectures
CMU - Carnegie Mellon University
Topic: No Listed Topic
Title: Finding Security Vulnerabilities that are Architectural Flaws using Constraints
Author(s): Radu Vanciu and Marwan Abi-Antoun
Abstract: Vanciu, R.; Abi-Antoun, M., "Finding architectural flaws using constraints," Automated Software Engineering (ASE), 2013 IEEE/ACM 28th International Conference on , vol., no., pp.334,344, 11-15 Nov. 2013 doi: 10.1109/ASE.2013.6693092
During Architectural Risk Analysis (ARA), security architects use a runtime architecture to look for security vulnerabilities that are architectural flaws rather than coding defects. The current ARA process, however, is mostly informal and manual. In this paper, we propose Scoria, a semi-automated approach for finding architectural flaws. Scoria uses a sound, hierarchical object graph with abstract objects and dataflow edges, where edges can refer to nodes in the graph. The architects can augment the object graph with security properties, which can express security information unavailable in code. Scoria allows architects to write queries on the graph in terms of the hierarchy, reachability, and provenance of a dataflow object. Based on the query results, the architects enhance their knowledge of the system security and write expressive constraints. The expressiveness is richer than previous approaches that check only for the presence or absence of communication or do not track a dataflow as an object. To evaluate Scoria, we apply these constraints to several extended examples adapted from the CERT standard for Java to confirm that Scoria can detect injected architectural flaws. Next, we write constraints to enforce an Android security policy and find one architectural flaw in one Android application. (ID#:14-2543)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6693092&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6693092
Publication Location: Location Not Available
Note:
Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to SoS.Project (at) SecureDataBank.net for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.
NCSU – North Carolina State University
These publications were done for the Lablet activities at this school, and were listed in the Quarterly Reports back to the government. Please direct any comments to research (at) securedatabank.net if there are any questions or concerns regarding these publications.
NCSU - North Carolina State University
Topic: Developing a User Profile to Predict Phishing Susceptibility and Security Technology Acceptance
Title: Keeping up with the Joneses: Assessing phishing susceptibility in an email task
Author(s): Hong, K. W., Kelley, C. M., Mayhorn, C. B., & Murphy-Hill, E
Hard Problem: Human Behavior
Abstract: From NCSU.edu: Most prior research on preventing phishing attacks focuses on technology to identify and prevent the delivery of phishing emails. The current study supports an ongoing effort to develop a user-profile that predicts when phishing attacks will be successful. We sought to identify the behavioral, cognitive and perceptual attributes that make some individuals more vulnerable to phishing attack than others. Fifty-three participants responded to a number of self-report measures (e.g., dispositional trust) and completed the 'Bob Jones' email task that was designed to empirically evaluate phishing susceptibility. Over 92% of participants were to some extent vulnerable to phishing attacks. Additionally, individual differences in gender, trust, and personality were associated with phishing vulnerability. Application and implications for future research are discussed.(ID#:14-2544)
URL: http://www4.ncsu.edu/~khong/papers/kwh_etal_hfes_13.pdf
Publication Location: Human Factors and Ergonomics Society 57th Annual Meeting 2013
NCSU - North Carolina State University
Topic: Developing a User Profile to Predict Phishing Susceptibility and Security Technology Acceptance
Title: Something smells phishy: Exploring definitions, consequences, and reactions to phishing
Author(s): Kelley, C. M., Hong, K. W., Mayhorn, C. B., & Murphy-Hill, E
Hard Problem: Human Behavior
Abstract: From NCSU.edu: One hundred fifty-five participants completed a survey on Amazon's Mechanical Turk that assessed characteristics of phishing attacks and requested participants to describe their previous experiences and the related consequences. Results indicated almost all participants had been targets of a phishing with 22% reporting these attempts were successful. Participants reported actively engaging in efforts to protect themselves online by noticing the "padlock icon" and seeking additional information to verify the legitimacy of e-retailers. Moreover, participants indicated that phishers most frequently pose as members of organizations and that phishing typically occurs via email yet they are aware that other media might also make them susceptible to phishing scams. The reported consequences of phishing attacks go beyond financial loss, with many participants describing social ramifications such as embarrassment and reduced trust. Implications for research in risk communication and design roles by human factors/ergonomics (HF/E) professionals are discussed. (ID#:14-2545)
URL: http://www4.ncsu.edu/~khong/papers/ck_etal_hfes_12.pdf
Publication Location: Human Factors and Ergonomics Society 56th Annual Meeting 2012
NCSU - North Carolina State University
Topic: Developing a User Profile to Predict Phishing Susceptibility and Security Technology Acceptance
Title: Have you smelled something phishy - full title "Have you smelled something phishy? A cross-cultural study on conceptions and experiences of phishing between China and the U.S."
Author(s): Lui, Y., & Mayhorn, C. B.
Hard Problem: Human Behavior
Abstract: Not Found; see "American and Indian conceptualizations of phishing"
below (ID#:14-2546)
URL: Not found; see "American and Indian..." below
Publication Location: Twelfth Annual North Carolina State University Undergraduate Summer Research Symposium 2013
NCSU - North Carolina State University
Topic: Developing a User Profile to Predict Phishing Susceptibility and Security Technology Acceptance
Title: American and Indian conceptualizations of phishing
Author(s): Tembe, R., Hong, K. W., Mayhorn, C. B., Murphy-Hill, E., & Kelley, C. M.
Hard Problem: Human Behavior
Abstract: titled "Phishing in international waters: exploring cross-national differences in phishing conceptualizations between Chinese, Indian and American samples";
Rucha Tembe, Olga Zielinska, Yuqi Liu, Kyung Wha Hong, Emerson Murphy-Hill, Chris Mayhorn, and Xi Ge. 2014. Phishing in international waters: exploring cross-national differences in phishing conceptualizations between Chinese, Indian and American samples. In Proceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 8 , 7 pages. DOI=10.1145/2600176.2600178 http://doi.acm.org/10.1145/2600176.2600178
One hundred-sixty four participants from the United States, India and China completed a survey designed to assess past phishing experiences and whether they engaged in certain online safety practices (e.g., reading a privacy policy). The study investigated participants' reported agreement regarding the characteristics of phishing attacks, types of media where phishing occurs and the consequences of phishing. A multivariate analysis of covariance indicated that there were significant differences in agreement regarding phishing characteristics, phishing consequences and types of media where phishing occurs for these three nationalities. Chronological age and education did not influence the agreement ratings; therefore, the samples were demographically equivalent with regards to these variables. A logistic regression analysis was conducted to analyze the categorical variables and nationality data. Results based on self-report data indicated that (1) Indians were more likely to be phished than Americans, (2) Americans took protective actions more frequently than Indians by destroying old documents, and (3) Americans were more likely to notice the "padlock" security icon than either Indian or Chinese respondents. The potential implications of these results are discussed in terms of designing culturally sensitive anti-phishing solutions. (ID#:14-2547)
URL: http://dl.acm.org/citation.cfm?id=2600178
Publication Location: International Workshop on the Socio-Technical Aspects of Security and Trust 2013
NCSU - North Carolina State University
Topic: Developing a User Profile to Predict Phishing Susceptibility and Security Technology Acceptance
Title: Phishing in international waters: Exploring cross-cultural differences in phishing conceptualizations between Chinese, Indian, and American samples
Author(s): Tembe, R., Zielinska, O., Liu, Y., Hong, K. W., Mayhorn, C. B., & Murphy-Hill
Hard Problem: Human Behavior
Abstract:
Rucha Tembe, Olga Zielinska, Yuqi Liu, Kyung Wha Hong, Emerson Murphy-Hill, Chris Mayhorn, and Xi Ge. 2014. Phishing in international waters: exploring cross-national differences in phishing conceptualizations between Chinese, Indian and American samples. In Proceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 8 , 7 pages. DOI=10.1145/2600176.2600178 http://doi.acm.org/10.1145/2600176.2600178
One hundred-sixty four participants from the United States, India and China completed a survey designed to assess past phishing experiences and whether they engaged in certain online safety practices (e.g., reading a privacy policy). The study investigated participants' reported agreement regarding the characteristics of phishing attacks, types of media where phishing occurs and the consequences of phishing. A multivariate analysis of covariance indicated that there were significant differences in agreement regarding phishing characteristics, phishing consequences and types of media where phishing occurs for these three nationalities. Chronological age and education did not influence the agreement ratings; therefore, the samples were demographically equivalent with regards to these variables. A logistic regression analysis was conducted to analyze the categorical variables and nationality data. Results based on self-report data indicated that (1) Indians were more likely to be phished than Americans, (2) Americans took protective actions more frequently than Indians by destroying old documents, and (3) Americans were more likely to notice the "padlock" security icon than either Indian or Chinese respondents. The potential implications of these results are discussed in terms of designing culturally sensitive anti-phishing solutions. (ID#:14-2548)
URL: http://dl.acm.org/citation.cfm?id=2600178
Publication Location: First HotSoS: Symposium and Bootcamp on the Science of Security 2014
NCSU - North Carolina State University
Topic: Developing a User Profile to Predict Phishing Susceptibility and Security Technology Acceptance
Title: One Phish, Two Phish, How to Avoid the Internet Phish: Analysis of Training Strategies to Detect Phishing Emails
Author(s): Zielinska, O., Tembe, R., Hong, K. W., Xe, G., Murphy-Hill, E. & Mayhorn, C. B.
Hard Problem: Human Behavior
Abstract: Not found (ID#:14-2549)
URL: Not found
Publication Location: Human Factors and Ergonomics Society.
NCSU - North Carolina State University
Topic: Software Security Metrics
Title: Using Templates to Elicit Implied Security Requirements from Functional Requirements - A Controlled Experiment
Author(s): M. Riaz, J. Slankas, J. King, L. Williams
Hard Problem: Metrics
Abstract: not found (ID#:14-2550)
URL: not found
Publication Location: International Symposium on Empirical Software Engineering and Measurement (ESEM) 2014
NCSU - North Carolina State University
Topic: Software Security Metrics
Title: Hidden in Plain Sight: Automatically Identifying Security Requirements from Natural Language Artifacts
Author(s): M. Riaz, J. Slankas, J. King, L. Williams.
Hard Problem: Metrics
Abstract: Seems to be the same as "Discovering Security Requirements from Natural Language", from NCSU.edu: Natural language artifacts, such as requirements specifications, often explicitly state the security requirements for software systems. However, these artifacts may also imply additional security requirements that developers may overlook but should consider to strengthen the overall security of the system. The goal of this research is to aid requirements engineers in producing a more comprehensive and classified set of security requirements by (1) automatically identifying security-relevantsentences in natural language requirements artifacts, and (2) providing context-specific security requirements templates to help translate the security-relevant sentences into functional security requirements. Using machine learning techniques, we have developed a tool-assisted process that takes as input a set of natural language artifacts. Our process automatically identifies security-relevant sentences in the artifacts and classifies them according to the security objectives, either explicitly stated or implied by the sentences. We classified 10,963 sentences in six different documents from healthcare domain and extracted corresponding security objectives. Our manual analysis showed that 46% of the sentences were security-relevant. Of these, 28% explicitly mention security while 72% of the sentences are functional requirements with security implications. Using our tool, we correctly predict and classify 82% of the security objectives for all the sentences (precision). We identify 79% of all security objectives implied by the sentences within the documents (recall). Based on our analysis, we develop context-specific templates that can be instantiated into a set of functional security requirements by filling in key information from security-relevant sentences. (ID#:14-2551)
URL: http://www4.ncsu.edu/~mriaz/docs/re14main-hidden-in-plain-sight-preprint.pdf
Publication Location: IEEE International Requirements Engineering Conference (RE) 2014
NCSU - North Carolina State University
Topic: Software Security Metrics
Title: Integration of Network and Application Access Control Configuration Verification
Author(s): Mohammed Alsaleh, and Ehab Al-Shaer
Hard Problem: Metrics
Abstract: Not found. See: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5990556 (ID#:14-2552)
URL: Not found
Publication Location: Journal of Advanced Research 2014
NCSU - North Carolina State University
Topic: Software Security Metrics
Title: A Formal Framework for Network Security Design Synthesis
Author(s): Rahman, M. A. and Al-Shaer, E.
Hard Problem: Metrics
Abstract: Mohammad Ashiqur Rahman and Ehab Al-Shaer. 2013. A Formal Framework for Network Security Design Synthesis. In Proceedings of the 2013 IEEE 33rd International Conference on Distributed Computing Systems (ICDCS '13). IEEE Computer Society, Washington, DC, USA, 560-570. DOI=10.1109/ICDCS.2013.70 http://dx.doi.org/10.1109/ICDCS.2013.70
Due to the extensive use of Internet services and emerging security threats, most enterprise networks deploy varieties of security devices for controlling resource access based on organizational security requirements. These requirements are becoming more fine-grained, where access control depends on heterogeneous isolation patterns like access deny, trusted communication, and payload inspection. However, organizations are looking to design usable and optimal security configurations that can harden the network security within enterprise budget constraints. This requires analyzing various alternative security architectures in order to find a security design that satisfies the organizational security requirements as well as the business constraints. In this paper, we present ConfigSynth, an automated framework for synthesizing network security configurations by exploring various security design alternatives to provide an optimal solution. The main design alternatives include different kinds of isolation patterns for traffic flows in different segments of the network. ConfigSynth takes security requirements and business constraints along with the network topology as inputs. Then it synthesizes optimal and cost-effective security configurations satisfying the constraints. ConfigSynth also provides optimal placements of different security devices in the network according to the given network topology. ConfigSynth uses Satisfiability Modulo Theories (SMT) for modeling this synthesis problem. We demonstrate the scalability of the tool using simulated experiments. (ID#:14-2553)
URL: http://dl.acm.org/citation.cfm?id=2549698
Publication Location: International Conference on Distributed Computing Systems (ICDCS), 2013
NCSU - North Carolina State University
Topic: Software Security Metrics
Title: A Formal Approach for Network Security Management Based on Qualitative Risk Analysis
Author(s): Rahman, M. A. and Al-Shaer, E.
Hard Problem: Metrics
Abstract: Rahman, M.A; Al-Shaer, E., "A formal approach for network security management based on qualitative risk analysis," Integrated Network Management (IM 2013), 2013 IFIP/IEEE International Symposium on , vol., no., pp.244,251, 27-31 May 2013
The risk analysis is an important process for enforcing and strengthening efficient and effective security. Due to the significant growth of the Internet, application services, and associated security attacks, information professionals face challenges in assessing risk of their networks. The assessment of risk may vary with the enterprise's requirements. Hence, a generic risk analysis technique is suitable. Moreover, configuring a network with correct security policy is a difficult problem. The assessment of risk aids in realizing necessary security policy. Risk is a function of security threat and impact. Security threats depend on the traffic reachability. Security devices like firewalls are used to selectively allow or deny traffic. However, the connection between the network risk and the security policy is not easy to establish. A small modification in the network topology or in the security policy, can change the risk significantly. It is hard to manually follow a systematic process for configuring the network towards security hardening. Hence, an automatic generation of proper security controls, e.g., firewall rules and host placements in the network topology, is crucial to keep the overall security risk low. In this paper, we first present a declarative model for the qualitative risk analysis. We consider transitive reachability, i.e., reachability considering one or more intermediate hosts, in order to compute exposure of vulnerabilities. Next, we formalize our risk analysis model and the security requirements as a constraint satisfaction problem using the satisfiability modulo theories (SMT). A solution to the problem synthesizes necessary firewall policies and host placements. We also evaluate the scalability of the proposed risk analysis technique as well as the synthesis model. (ID#:14-2554)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6572992&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6572992
Publication Location: IFIP/IEEE International Symposium on Integrated Network Management (IM), IEEE, 2013
NCSU - North Carolina State University
Topic: Software Security Metrics
Title: ConfigSynth: A Formal Framework for Optimal Network Security Design
Author(s): Rahman, M. A. and Al-Shaer, E.
Hard Problem: Metrics
Abstract: Rahman, M.A; Al-Shaer, E., "A Formal Framework for Network Security Design Synthesis," Distributed Computing Systems (ICDCS), 2013 IEEE 33rd International Conference on , vol., no., pp.560,570, 8-11 July 2013doi: 10.1109/ICDCS.2013.70
Due to the extensive use of Internet services and emerging security threats, most enterprisenetworks deploy varieties of security devices for controlling resource access based on organizationalsecurity requirements. These requirements are becoming more fine-grained, where access control depends on heterogeneous isolation patterns like access deny, trusted communication, and payload inspection. However, organizations are looking to design usable and optimal security configurations that can harden the network security within enterprise budget constraints. This requires analyzing various alternative security architectures in order to find a security design that satisfies the organizational security requirements as well as the business constraints. In this paper, we present ConfigSynth, an automated framework for synthesizing network security configurations by exploring various security design alternatives to provide an optimal solution. The main design alternatives include different kinds of isolation patterns for traffic flows in different segments of the network. ConfigSynth takes security requirements and business constraints along with the network topology as inputs. Then it synthesizes optimal and cost-effective security configurations satisfying the constraints. ConfigSynth also provides optimal placements of different security devices in thenetwork according to the given network topology. ConfigSynth uses Satisfiability Modulo Theories (SMT) for modeling this synthesis problem. We demonstrate the scalability of the tool using simulated experiments. (ID#:14-2556)
URL: http://ieeeexplore.com/xpl/articleDetails.jsp?tp=&arnumber=6681625&queryText%3Dnetwork+security
Publication Location: Network & Distributed System Security Symposium (NDSS), February 2013 (Short paper)
NCSU - North Carolina State University
Topic: Software Security Metrics
Title: Objective Metrics for Firewall Security: A Holistic View
Author(s): Mohammed Noraden Alsaleh, Saeed Al-Haj and Ehab Al-Shaer
Abstract: Alsaleh, M.N.; Al-Haj, S.; Al-Shaer, E., "Objective metrics for firewall security: A holistic view," Communications and Network Security (CNS), 2013 IEEE Conference on , vol., no., pp.470,477, 14-16 Oct. 2013 doi: 10.1109/CNS.2013.6682762
Firewalls are the primary security devices in cyber defense. Yet, the security of firewalls depends on the quality of protection provided by the firewall policy. The lack of metrics and attack incident data makes measuring the security of firewall policies a challenging task. In this paper, we present a new set of quantitative metrics that can be used to measure, as well as, compare the security level of firewall policies in an enterprise network. The proposed metrics measure the risk of attacks on the network that is imposed due to weaknesses in the firewall policy. We also measure the feasibility of mitigating or removing that risk. The presented metrics are proven to be (1) valid as compared with the ground truth, and (2) practically useful as each one implies actionable security hardening. (ID#:14-2557)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6682762&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6682762
Publication Location: Symposium on Security Analytics and Automation (SafeConfig), 2013
Note:
Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to SoS.Project (at) SecureDataBank.net for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.
UIUC – University of Illinois at Urbana-Champaign
These publications were done for the Lablet activities at this school, and were listed in the Quarterly Reports back to the government. Please direct any comments to research (at) securedatabank.net if there are any questions or concerns regarding these publications.
UIUC - University of Illinois at Urbana-Champaign
Topic: Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems
Title: Proving Abstractions of Dynamical Systems through Numerical Simulations
Author(s): Sayan Mitra
Hard Problem: Scalability and Composability, Metrics
Abstract: ACM Library
Sayan Mitra. 2014. Proving abstractions of dynamical systems through numerical simulations. InProceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 12 , 9 pages. DOI=10.1145/2600176.2600188 http://doi.acm.org/10.1145/2600176.2600188
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. (ID#:14-2558)
URL: http://dl.acm.org/citation.cfm?id=2600188
Publication Location: Hot Topics in Science of Security (HOTSOS) 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems
Title: Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells
Author(s): Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra and Marta Kwiatkowska
Hard Problem: Scalability and Composability, Metrics
Abstract: Available from Springer via link listed below.. (ID#:14-2559)
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_25#
Publication Location: Computer Aided Verification (CAV 2014)
UIUC - University of Illinois at Urbana-Champaign
Topic: Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems
Title: Decentralized Control of Switched Nested Systems with l2-induced Norm Performance
Author(s): Anshuman Mishra, Cedric Langbort, and Geir Dullerud
Hard Problem: Scalability and Composability, Metrics
Abstract: Abstract not available (ID#:14-2560)
URL: URL not available
Similar paper with same authors and same topic: "Optimal decentralized control of a stochastically switched system..." Link
Publication Location: Proceedings of the American Control Conference (ACC) 2014
Topic: Data Driven Security Models and Analysis
Title: An Experiment Using Factor Graph for Early Attack Detection
Author(s): P. Cao, K.-W. Chung, A. Slagell, Z. Kalbarczyk, R. Iyer
Hard Problem: Metrics, Resilient Architectures, Human Behavior
Abstract: Not Found (ID#:14-2561)
URL: Not found
Similar paper with same authors and same topic : "Preemptive Intrusion Detection" by P. Cao, K.-W. Chung, A. Slagell, Z. Kalbarczyk, R. Iyer Link
Publication Location: Workshop on Learning from Authoritative Security Experiment Results (LASER) 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: A Hypothesis Testing Framework for Network Security
Title: Towards Correct Network Virtualization
Author(s): Soudeh Ghorbani and Brighten Godfrey
Hard Problem: Scalability and Composability, Policy-Governed Secure Collaboration, Metrics, Resilient Architectures
Abstract: ACM Digital Library
In SDN, the underlying infrastructure is usually abstracted for applications that can treat the network as a logical or virtual entity. Commonly, the ``mappings" between virtual abstractions and their actual physical implementations are not one-to-one, e.g., a single "big switch" abstract object might be implemented using a distributed set of physical devices. A key question is, what abstractions could be mapped to multiple physical elements while faithfully preserving their native semantics? E.g., can an application developer always expect her abstract "big switch" to act exactly as a physical big switch, despite being implemented using multiple physical switches in reality?
We show that the answer to that question is "no" for existing virtual-to-physical mapping techniques: behavior can differ between the virtual "big switch" and the physical network, providing incorrect application-level behavior. We also show that that those incorrect behaviors occur despite the fact that the most pervasive and commonly-used correctness invariants, such as per-packet consistency, are preserved throughout. These examples demonstrate that for practical notions of correctness, new systems and a new analytical framework are needed. We take the first steps by defining end-to-end correctness, a correctness condition that focuses on applications only, and outline a research vision to obtain virtualization systems with correct virtual to physical mappings (ID#:14-2562)
URL: http://dl.acm.org/citation.cfm?id=2620754
Publication Location: ACM Workshop on Hot Topics in Software Defined Networks (HotSDN), August 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Agent-Based Modeling of User Circumvention of Security
Author(s): V. Kothari, J. Blythe, S.W. Smith, and R. Koppel
Hard Problem: Human Behavior
Collaborating: In collaboration with Dartmouth University
Abstract: ACM Digital Library
Vijay Kothari, Jim Blythe, Sean Smith, and Ross Koppel. 2014. Agent-based modeling of user circumvention of security. In Proceedings of the 1st International Workshop on Agents and CyberSecurity (ACySE '14). ACM, New York, NY, USA, , Article 5 , 4 pages. DOI=10.1145/2602945.2602948 http://doi.acm.org/10.1145/2602945.2602948
Security subsystems are often designed with flawed assumptions arising from system designers' faulty mental models. Designers tend to assume that users behave according to some textbook ideal, and to consider each potential exposure/interface in isolation. However, fieldwork continually shows that even well-intentioned users often depart from this ideal and circumvent controls in order to perform daily work tasks, and that "incorrect" user behaviors can create unexpected links between otherwise "independent" interfaces. When it comes to security features and parameters, designers try to find the choices that optimize security utility---except these flawed assumptions give rise to an incorrect curve, and lead to choices that actually make security worse, in practice.
We propose that improving this situation requires giving designers more accurate models of real user behavior and how it influences aggregate system security. Agent-based modeling can be a fruitful first step here. In this paper, we study a particular instance of this problem, propose user-centric techniques designed to strengthen the security of systems while simultaneously improving the usability of them, and propose further directions of inquiry. (ID#:14-2563)
URL: http://dl.acm.org/citation.cfm?id=2602948
Publication Location: 1st International Workshop on Agents and CyberSecurity. ACM. May 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Theoretical Foundations of Threat Assessment by Inverse Optimal Control
Title: Equilibrium configurations of a Kirchhoff elastic rod under quasi-static manipulation
Author(s): Timothy Bretl and Zoe McCarthy
Abstract: Available from Springer via link listed below.. (ID#:14-2564)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-36279-8_5
ACM Library link for "Quasi-static manipulation of a Kirchhoff elastic rod based on a geometric analysis of equilibrium configurations : http://dl.acm.org/citation.cfm?id=2568347
Publication Location: Workshop on Algorithmic Foundations of Robotics 12
UIUC - University of Illinois at Urbana-Champaign
Title: Mechanics and manipulation of planar elastic kinematic chains
Topic: Science of Human Circumvention of Security
Author(s): Zoe McCarthy and Timothy Bretl
Abstract: McCarthy, Z.; Bretl, T., "Mechanics and manipulation of planar elastic kinematic chains," Robotics and Automation (ICRA), 2012 IEEE International Conference on , vol., no., pp.2798,2805, 14-18 May 2012
doi: 10.1109/ICRA.2012.6224693
In this paper, we study quasi-static manipulation of a planar kinematic chain with a fixed base in which each joint is a linearly-elastic torsional spring. The shape of this chain when in static equilibrium can be represented as the solution to a discrete-time optimal control problem, with boundary conditions that vary with the position and orientation of the last link. We prove that the set of all solutions to this problem is a smooth manifold that can be parameterized by a single chart. For manipulation planning, we show several advantages of working in this chart instead of in the space of boundary conditions, particularly in the context of a sampling-based planning algorithm. Examples are provided in simulation. (ID#:14-2565)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6224693&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6224693
Publication Location: IEEE International Conference on Robotics and Automation, 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Experiments in quasi-static manipulation of a planar elastic rod
Author(s): D. Matthews and Timothy Bretl
Abstract: Matthews, D.; Bretl, T., "Experiments in quasi-static manipulation of a planar
elastic rod," Intelligent Robots and Systems (IROS), 2012 IEEE/RSJ International Conference on , vol., no., pp.5420,5427, 7-12 Oct. 2012
doi: 10.1109/IROS.2012.6385876
In this paper, we introduce and experimentally validate a sampling-based planning algorithm for quasi-static manipulation of a planar elastic rod. Our algorithm is an immediate consequence of deriving a global coordinate chart of finite dimension that suffices to describe all possible configurations of the rod that can be placed in static equilibrium by fixing the position and orientation of each end. Hardware experiments confirm this derivation in the case where the "rod" is a thin, flexible strip of metal that has a fixed base and that is held at the other end by an industrial robot. We show an example in which a path of the robot that was planned by our algorithm causes the metal strip to move between given start and goal configurations while remaining in quasi-static equilibrium. (ID#:14-2566)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6385876&url=http%3A%2F
%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6385876
Publication Location: IEEE/RSJ International Conference on Intelligent Robots and Systems, 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: A brain-machine interface to navigate mobile robots along human-like paths amidst obstacles
Author(s): A. Akce, J. Norton, and T. Bretl
Abstract: Akce, A; Norton, J.; Bretl, T., "A brain-machine interface to navigate mobile robots along human-like paths amidst obstacles," Intelligent Robots and Systems (IROS), 2012 IEEE/RSJ International Conference on , vol., no., pp.4084,4089, 7-12 Oct. 2012
doi: 10.1109/IROS.2012.6386024
This paper presents an interface that allows a human user to specify a desired path for a mobile robot in a planar workspace with noisy binary inputs that are obtained at low bit-rates through an electroencephalograph (EEG). We represent desired paths as geodesics with respect to a cost function that is defined so that each path-homotopy class contains exactly one (local) geodesic. We apply max-margin structured learning to recover a cost function that is consistent with observations of human walking paths. We derive an optimal feedback communication protocol to select a local geodesic-equivalently, a path-homotopy class-using a sequence of noisy bits. We validate our approach with experiments that quantify both how well our learned cost function characterizes human walking data and how well human subjects perform with the resulting interface in navigating a simulated robot with EEG. (ID#:14-2567)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6386024&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6386024
Publication Location: IEEE/RSJ International Conference on Intelligent Robots and Systems, 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Quasi-Static Manipulation of a Kirchhoff Elastic Rod based on a Geometric Analysis of Equilibrium Configurations
Author(s): T. Bretl and Z. McCarthy
Abstract: Timothy Bretl and Zoe Mccarthy. 2014. Quasi-static manipulation of a Kirchhoff elastic rod based on a geometric analysis of equilibrium configurations. Int. J. Rob. Res. 33, 1 (January 2014), 48-68. DOI=10.1177/0278364912473169 http://dx.doi.org/10.1177/0278364912473169
Consider a thin, flexible wire of fixed length that is held at each end by a robotic gripper. Any curve traced by this wire when in static equilibrium is a local solution to a geometric optimal control problem, with boundary conditions that vary with the position and orientation of each gripper. We prove that the set of all local solutions to this problem over all possible boundary conditions is a smooth manifold of finite dimension that can be parameterized by a single chart. We show that this chart makes it easy to implement a sampling-based algorithm for quasi-static manipulation planning. We characterize the performance of such an algorithm with experiments in simulation. (ID#:14-2568)
URL: http://dl.acm.org/citation.cfm?id=2568347
Publication Location: International Journal of Robotics Research, 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Mechanics and Quasi-Static Manipulation of Planar Elastic Kinematic Chains
Author(s): T. Bretl and Z. McCarthy
Abstract: Bretl, T.; McCarthy, Z., "Mechanics and Quasi-Static Manipulation of Planar Elastic Kinematic Chains," Robotics, IEEE Transactions on , vol.29, no.1, pp.1,14, Feb. 2013 DOI: 10.1109/TRO.2012.2218911
In this paper, we study quasi-static manipulation of a planar kinematic chain with a fixed base in which each joint is a linearly elastic torsional spring. The shape of this chain when in static equilibrium can be represented as the solution to a discrete-time optimal control problem, with boundary conditions that vary with the position and orientation of the last link. We prove that the set of all solutions to this problem is a smooth three-manifold that can be parameterized by a single chart. Empirical results in simulation show that straight-line paths in this chart are uniformly more likely to be feasible (as a function of distance) than straight-line paths in the space of boundary conditions. These results, which are consistent with an analysis of visibility properties, suggest that the chart we derive is a better choice of space in which to apply a sampling-based algorithm for manipulation planning. We describe such an algorithm and show that it is easy to implement. (ID#:14-2569)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6327684
Publication Location: IEEE Transactions on Robotics, 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Inverse optimal control for deterministic continuous-time nonlinear systems
Author(s): M. Johnson, N. Aghasadeghi, and T. Bretl
Abstract: Johnson, M.; Aghasadeghi, N.; Bretl, T., "Inverse optimal control for deterministic continuous-time nonlinear systems," Decision and Control (CDC), 2013 IEEE 52nd Annual Conference on , vol., no., pp.2906,2913, 10-13 Dec. 2013
doi: 10.1109/CDC.2013.6760325
Inverse optimal control is the problem of computing a cost function with respect to which observed state and input trajectories are optimal. We present a new method of inverse optimal control based on minimizing the extent to which observed trajectories violate first-order necessary conditions for optimality. We consider continuous-time deterministic optimal control systems with a cost function that is a linear combination of known basis functions. We compare our approach with three prior methods of inverse optimal control. We demonstrate the performance of these methods by performing simulation experiments using a collection of nominal system models. We compare the robustness of these methods by analysing how they perform under perturbations to the system. To this purpose, we consider two scenarios: one in which we exactly know the set of basis functions in the cost function, and another in which the true cost function contains an unknown perturbation. Results from simulation experiments show that our new method is more computationally efficient than prior methods, performs similarly to prior approaches under large perturbations to the system, and better learns the true cost function under small perturbations. (ID#:14-2570)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6760325&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6760325
Publication Location: IEEE International Conference on Robotics and Automation, 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: A Dynamic Game-Theoretic Approach to Resilient Control System Design for Cascading Failures
Author(s): Quanyan Zhu and Tamer Basar
Abstract: Quanyan Zhu and Tamer Basar. 2012. A dynamic game-theoretic approach to resilient control system design for cascading failures. In Proceedings of the 1st international conference on High Confidence Networked Systems (HiCoNS '12). ACM, New York, NY, USA, 41-46. DOI=10.1145/2185505.2185512 http://doi.acm.org/10.1145/2185505.2185512 The migration of many current critical infrastructures, such as power grids and transportations systems, into open public networks has posed many challenges in control systems. Modern control systems face uncertainties not only from the physical world but also from the cyber space. In this paper, we propose a hybrid game-theoretic approach to investigate the coupling between cyber security policy and robust control design. We study in detail the case of cascading failures in industrial control systems and provide a set of coupled optimality criteria in the linear-quadratic case. This approach can be further extended to more general cases of parallel cascading failures. (ID#:14-2571)
URL: http://dl.acm.org/citation.cfm?id=2185512&dl=ACM&coll=DL&CFID=551960065&CFTOKEN=77203732
Publication Location: Conference on High Confidence Networked Systems (HiCoNS) at CPSWeek 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Game-Theoretic Methods for Distributed Management of Energy Resources in the Smart Grid
Author(s): Quanyan Zhu and Tamer Basar
Abstract: Quanyan Zhu; Jiangmeng Zhang; Sauer, P.W.; Dominguez-Garcia, A; Basar, T., "A game-theoretic framework for control of distributed renewable-based energy resources in smart grids," American Control Conference (ACC), 2012 , vol., no., pp.3623,3628, 27-29 June 2012
doi: 10.1109/ACC.2012.6315275
Renewable energy plays an important role in distributed energy resources in smart grid systems. Deployment and integration of renewable energy resources require an intelligent management to optimize their usage in the current power grid. In this paper, we establish a game-theoretic framework for modeling the strategic behavior of buses that are connected to renewable energy resources and study the equilibrium distributed power generation at each bus. Our framework takes a cross-layer approach, taking into account the economic factors as well as system stability issues at each bus. We propose an iterative algorithm to compute Nash equilibrium solutions based on a sequence of linearized games. Simulations and numerical examples are used to illustrate the algorithm and corroborate the results. (ID#:14-2572)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6315275&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6315275
Publication Location: Annual CMU Electricity Conference 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Agent-based cyber control strategy design for resilient control systems: Concepts, architecture and methodologies
Author(s): C. Rieger, Quanyan Zhu and Tamer Basar
Abstract: Rieger, C.; Quanyan Zhu; Basar, T., "Agent-based cyber control strategy design for resilient control systems: Concepts, architecture and methodologies," Resilient Control Systems (ISRCS), 2012 5th International Symposium on , vol., no., pp.40,47, 14-16 Aug. 2012
doi: 10.1109/ISRCS.2012.6309291
The implementation of automated regulatory control has been around since the middle of the last century through analog means. It has allowed engineers to operate the plant more consistently by focusing on overall operations and settings instead of individual monitoring of local instruments (inside and outside of a control room). A similar approach is proposed for cyber security, where current border-protection designs have been inherited from information technology developments that lack consideration of the high-reliability, high consequence nature of industrial control systems. Instead of an independent development, however, an integrated approach is taken to develop a holistic understanding of performance. This performance takes shape inside a multi-agent design, which provides a notional context to model highly decentralized and complex industrial process control systems, the nervous system of critical infrastructure. The resulting strategy will provide a framework for researching solutions to security and unrecognized interdependency concerns with industrial control systems. (ID#:14-2573)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6309291&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Ftp%3D%26arnumber%3D6309291
Publication Location: Resilient Control Systems 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Dependable demand response management in smart grid: A Stackelberg game approach
Author(s): S. Maharjan, Quanyan Zhu, Y. Zhang, S. Gjessing, and Tamer Basar
Abstract: Maharjan, S.; Quanyan Zhu; Yan Zhang; Gjessing, S.; Basar, T., "Dependable Demand Response Management in the Smart Grid: A Stackelberg Game Approach," Smart Grid, IEEE Transactions on , vol.4, no.1, pp.120,132, March 2013
doi: 10.1109/TSG.2012.2223766
Demand Response Management (DRM) is a key component in the smart grid to effectively reduce power generation costs and user bills. However, it has been an open issue to address the DRM problem in a network of multiple utility companies and consumers where every entity is concerned about maximizing its own benefit. In this paper, we propose a Stackelberg game between utility companies and end-users to maximize the revenue of each utility company and the payoff of each user. We derive analytical results for the Stackelberg equilibrium of the game and prove that a unique solution exists. We develop a distributed algorithm which converges to the equilibrium with only local information available for both utility companies and end-users. Though DRM helps to facilitate the reliability of power supply, the smart grid can be succeptible to privacy and security issues because of communication links between the utility companies and the consumers. We study the impact of an attacker who can manipulate the price information from the utility companies. We also propose a scheme based on the concept of shared reserve power to improve the grid reliability and ensure its dependability. (ID#:14-2574)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6464552
Publication Location: IEEE Trans. on Smart Grid, Special Issue on Smart Grid Communication Systems: Reliability, Dependability & Performance, 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Resilience in consensus dynamics via competitive interconnections
Author(s): Bahman Gharesifard and Tamer Basar
Abstract: We show that competitive engagements within the agents of a network can result in resilience in consensus dynamics with respect to the presence of an adversary. We first show that interconnections with an adversary, with linear dynamics, can make the consensus dynamics diverge, or drive its evolution to a state different from the average. We then introduce a second network, interconnected with the original network via an engagement topology. This network has no information about the adversary and each agent in it has only access to partial information about the state of the other network. We introduce a dynamics on the coupled network which corresponds to a saddle-point dynamics of a certain zero-sum game and is distributed over each network, as well as the engagement topology. We show that, by appropriately choosing a design parameter corresponding to the competition between these two networks, the coupled dynamics can be made resilient with respect to the presence of the adversary. Our technical approach combines notions of graph theory and stable perturbations of nonsymmetric matrices. We demonstrate our results on an example of kinematic-based flocking in presence of an adversary. (ID#:14-2575)
URL: http://www.ifac-papersonline.net/Detailed/56775.html
Publication Location: IFAC Workshop on Distributed Estimation and Control in Networked Systems 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: SODEXO: A system framework for deployment and exploitation of deceptive honeybots in social networks
Author(s): Q. Zhu, A. Clark, R.Poovendran, T. Basar
Abstract: As social networking sites such as Facebook and Twitter are becoming increasingly popular, a growing number of malicious attacks, such as phishing and malware, are exploiting them. Among these attacks, social botnets have sophisticated infrastructure that leverages compromised users accounts, known as bots, to automate the creation of new social networking accounts for spamming and malware propagation. Traditional defense mechanisms are often passive and reactive to non-zero-day attacks. In this paper, we adopt a proactive approach for enhancing security in social networks by infiltrating botnets with honeybots. We propose an integrated system named SODEXO which can be interfaced with social networking sites for creating deceptive honeybots and leveraging them for gaining information from botnets. We establish a Stackelberg game framework to capture strategic interactions between honeybots and botnets, and use quantitative methods to understand the tradeoffs of honeybots for their deployment and exploitation in social networks. We design a protection and alert system that integrates both microscopic and macroscopic models of honeybots and optimally determines the security strategies for honeybots. We corroborate the proposed mechanism with extensive simulations and comparisons with passive defenses. (ID#:14-2576)
URL: http://arxiv.org/abs/1207.5844
Publication Location: IEEE International Conference on Computer Communications (INFOCOM) 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Deceptive routing in relay networks
Author(s): A. Clark, Q. Zhu, R. Poovendran, T. Basar
Abstract: Available from Springer via link listed below.. (ID#:14-2577)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-34266-0_10
Publication Location: Conference on Decision and Game Theory for Security (GameSec) 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Game--theoretic analysis of node capture and cloning attack with multiple attackers in wireless sensor networks
Author(s): Q. Zhu, L. Bushnell, T. Basar
Abstract: Quanyan Zhu; Bushnell, L.; Basar, T., "Game-theoretic analysis of node capture and cloning attack with multiple attackers in wireless sensor networks," Decision and Control (CDC), 2012 IEEE 51st Annual Conference on , vol., no., pp.3404,3411, 10-13 Dec. 2012
doi: 10.1109/CDC.2012.6426481
Wireless sensor networks are subject to attacks such as node capture and cloning, where an attacker physically captures sensor nodes, replicates the nodes, which are deployed into the network, and proceeds to take over the network. In this paper, we develop models for such an attack when there are multiple attackers in a network, and formulate multi-player games to model the noncooperative strategic behavior between the attackers and the network. We consider two cases: a static case where the attackers' node capture rates are time-invariant and the network's clone detection/revocation rate is a linear function of the state, and a dynamic case where the rates are general functions of time. We characterize Nash equilibrium solutions for both cases and derive equilibrium strategies for the players. In the static case, we study both the single-attacker and the multi-attacker games within an optimization framework, provide conditions for the existence of Nash equilibria and characterize them in closed forms. In the dynamic case, we study the underlying multi-person differential game under an open-loop information structure and provide a set of conditions to characterize the open-loop Nash equilibrium. We show the equivalence of the Nash equilibrium for the multi-person game to the saddle-point equilibrium between the network and the attackers as a team. We illustrate our results with numerical examples. (ID#:14-2578)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6426481
Publication Location: IEEE Conference on Decision and Control (CDC) 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Deceptive routing games
Author(s): Q. Zhu, A. Clark, R. Poovendran, T. Basar
Abstract: Quanyan Zhu; Clark, A; Poovendran, R.; Basar, T., "Deceptive routing games," Decision and Control (CDC), 2012 IEEE 51st Annual Conference on , vol., no., pp.2704,2711, 10-13 Dec. 2012
doi: 10.1109/CDC.2012.6426515
The use of a shared medium leaves wireless networks, including mobile ad hoc and sensor networks, vulnerable to jamming attacks. In this paper, we introduce a jamming defense mechanism for multiple-path routing networks based on maintaining deceptive flows, consisting of fake packets, between a source and a destination. An adversary observing a deceptive flow will expend energy on disrupting the fake packets, allowing the real data packets to arrive at the destination unharmed. We model this deceptive flow-based defense within a multi-stage stochastic game framework between the network nodes, which choose a routing path and flow rates for the real and fake data, and an adversary, which chooses which fraction of each flow to target at each hop. We develop an efficient, distributed procedure for computing the optimal routing at each hop and the optimal flow allocation at the destination. Furthermore, by studying the equilibria of the game, we quantify the benefit arising from deception, as reflected in an increase in the valid throughput. Our results are demonstrated via a simulation study. (ID#:14-2579)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6426515&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F6416474%2F6425800%2F06426515.pdf%3Farnumbe...
Publication Location: IEEE Conference on Decision and Control (CDC) 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: GUIDEX: A game-theoretic Incentive-Based mechanism for intrusion detection networks
Author(s): Q. Zhu, C. Fung, R. Boutaba, T. Basar
Abstract: Quanyan Zhu; Fung, C.; Boutaba, R.; Basar, T., "GUIDEX: A Game-Theoretic Incentive-Based Mechanism for Intrusion Detection Networks," Selected Areas in Communications, IEEE Journal on , vol.30, no.11, pp.2220,2230, December 2012
doi: 10.1109/JSAC.2012.121214
Traditional intrusion detection systems (IDSs) work in isolation and can be easily compromised by unknown threats. An intrusion detection network (IDN) is a collaborative IDS network intended to overcome this weakness by allowing IDS peers to share detection knowledge and experience, and hence improve the overall accuracy of intrusion assessment. In this work, we design an IDN system, called GUIDEX, using game-theoretic modeling and trust management for peers to collaborate truthfully and actively. We first describe the system architecture and its individual components, and then establish a game-theoretic framework for the resource management component of GUIDEX. We establish the existence and uniqueness of a Nash equilibrium under which peers can communicate in a reciprocal incentive compatible manner. Based on the duality of the problem, we develop an iterative algorithm that converges geometrically to the equilibrium. Our numerical experiments and discrete event simulation demonstrate the convergence to the Nash equilibrium and the security features of GUIDEX against free riders, dishonest insiders and DoS attacks. (ID#:14-2580)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6354280&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F49%2F6354264%2F06354280.pdf%3Farnumber%3D6...
Publication Location: IEEE Journal on Selected Areas in Communications (JSAC) Special Issue on Economics of Communication Networks & Systems
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: An Impact-Aware Defense against Stuxnet
Author(s): A. Clark, Q. Zhu, R. Poovendran and T. Basar
Abstract: Clark, A; Quanyan Zhu; Poovendran, R.; Basar, T., "An impact-aware defense against Stuxnet," American Control Conference (ACC), 2013 , vol., no., pp.4140,4147, 17-19 June 2013
doi: 10.1109/ACC.2013.6580475
The Stuxnet worm is a sophisticated malware designed to sabotage industrial control systems (ICSs). It exploits vulnerabilities in removable drives, local area communication networks, and programmable logic controllers (PLCs) to penetrate the process control network (PCN) and the control system network (CSN). Stuxnet was successful in penetrating the control system network and sabotaging industrial control processes since the targeted control systems lacked security mechanisms for verifying message integrity and source authentication. In this work, we propose a novel proactive defense system framework, in which commands from the system operator to the PLC are authenticated using a randomized set of cryptographic keys. The framework leverages cryptographic analysis and control-and game-theoretic methods to quantify the impact of malicious commands on the performance of the physical plant. We derive the worst-case optimal randomization strategy as a saddle-point equilibrium of a game between an adversary attempting to insert commands and the system operator, and show that the proposed scheme can achieve arbitrarily low adversary success probability for a sufficiently large number of keys. We evaluate our proposed scheme, using a linear-quadratic regulator (LQR) as a case study, through theoretical and numerical analysis. (ID#:14-2581)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6580475&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6580475
Publication Location: American Control Conference (ACC) 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Price-based distributed control for networked plug-in electric vehicles
Author(s): B. Gharesifard, T. Basar, and A.D. Dominguez-Garcia
Abstract: Gharesifard, B.; Basar, T.; Dominguez-Garcia, AD., "Price-based distributed control for networked plug-in electric vehicles," American Control Conference (ACC), 2013 , vol., no., pp.5086,5091, 17-19 June 2013 doi: 10.1109/ACC.2013.6580628
We introduce a framework for controlling the charging and discharging processes of plug-in electric vehicles (PEVs) via pricing strategies. Our framework consists of a hierarchical decision-making setting with two layers, which we refer to as aggregator layer and retail market layer. In the aggregator layer, there is a set of aggregators that are requested (and will be compensated for) to provide certain amount of energy over a period of time. In the retail market layer, the aggregator offers some price for the energy that PEVs may provide; the objective is to choose a pricing strategy to incentivize the PEVs so as they collectively provide the amount of energy that the aggregator has been asked for. The focus of this paper is on the decision-making process that takes places in the retail market layer, where we assume that each individual PEV is a price-anticipating decision-maker. We cast this decision-making process as a game, and provide conditions on the pricing strategy of the aggregator under which this game has a unique Nash equilibrium. We propose a distributed consensus-based iterative algorithm through which the PEVs can seek for this Nash equilibrium. Numerical simulations are included to illustrate our results. (ID#:14-2582)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6580628
Publication Location: American Control Conference (ACC) 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Toward a theory of multi-resolution games
Author(s): Q. Zhu and T. Basar
Abstract: University of Illinois at Urbana-Champaign
Modern critical infrastructures are highly integrated systems composed of many complex interactions between different system modules or agents including cyber and physical components as well as human factors. Their growing complexity demands novel techniques (ID#:14-2583)
URL: https://wiki.engr.illinois.edu/download/attachments/229421613/ZhuBasar_SIAM2013.pdf?version=1&modificationDate=1383488188000
Publication Location: 2013 SIAM Conference on Control and Its Applications (CT13)
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Resilient distributed control of multi-agent cyber-physical systems
Author(s): Q. Zhu, L. Bushnell, T. Basar
Abstract: Available from Springer via link listed below. (ID#:14-2584)
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-01159-2_16
Publication Location: CISS Workshop on Cyber-Physical Systems 2013
**Title: A price-based approach to control of networked distributed energy resources
** Price-Based Distributed Control for Networked Plug-in Electric Vehicles (alternate title)
Author(s): B. Gharesifard, T. Basar, and A. D. Dominguez-Garcia
Abstract: no abstract found (ID#:14-2585)
URL: http://energy.ece.illinois.edu/aledan/publications_files/ACC_2013.pdf
Publication Location: Special Issue on Cyber-Physical-Systems, IEEE Transactions on Automatic Control
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Resilient Control of Cyber-Physical Systems against Denial-of-Service Attacks
Author(s): Y. Yuan, Q. Zhu, F. Sun, Q. Wang, and T. Basar
Abstract: Yuan Yuan; Quanyan Zhu; Fuchun Sun; Qinyi Wang; Basar, T., "Resilient control of cyber-physical systems against Denial-of-Service attacks," Resilient Control Systems (ISRCS), 2013 6th International Symposium on , vol., no., pp.54,59, 13-15 Aug. 2013
doi: 10.1109/ISRCS.2013.6623750
The integration of control systems with modern information technologies has posed potential security threats for critical infrastructures. The communication channels of the control system are vulnerable to malicious jamming and Denial-of-Service (DoS) attacks, which lead to severe time-delays and degradation of control performances. In this paper, we design resilient controllers for cyber-physical control systems under DoS attacks. We establish a coupled design framework which incorporates the cyber configuration policy of Intrusion Detection Systems (IDSs) and the robust control of dynamical system. We propose design algorithms based on value iteration methods and linear matrix inequalities for computing the optimal cyber security policy and control laws. We illustrate the design principle with an example from power systems. The results are corroborated by numerical examples and simulations. (ID#:14-2586)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6623750&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel7%2F6601033%2F6623739%2F06623750.pdf%3Farnumber%3D6623750
Publication Location: International Symposium on Resilient Control Systems (ISRCS 2013)
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Hierarchical Architectures of Resilient Control Systems: Concepts, Metrics and Design Principles
Author(s): Q. Zhu, D. Wei, K. Ji, C. Rieger, and T. Basar
Abstract: Security of control systems is becoming a pivotal concern in critical national infrastructures such as the power grid and nuclear plants. In this paper, we adopt a hierarchical viewpoint to these security issues, addressing security concerns at each level and emphasizing a holistic cross-layer philosophy for developing security solutions. We propose a bottom-up framework that establishes a model from the physical and control levels to the supervisory level, incorporating concerns from network and communication levels. We show that the game-theoretical approach can yield cross-layer security strategy solutions to the cyber-physical systems. (ID#:14-2587)
URL: See: "A Hierarchical Security Architecture for Cyber-Physical Systems"
Publication Location: Special Issue of the IEEE Transactions on Cybernetics: "Resilient Control Architectures and Systems"
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Distributed optimization by myopic strategic interactions and the price of heterogeneity
Author(s): B. Gharesifard, B. Touri, T. Basar, and C. Langbort
Abstract: Gharesifard, B.; Touri, B.; Basar, T.; Langbort, C., "Distributed optimization by myopic strategic interactions and the price of heterogeneity," Decision and Control (CDC), 2013 IEEE 52nd Annual Conference on , vol., no., pp.1174,1179, 10-13 Dec. 2013
doi: 10.1109/CDC.2013.6760041
This paper is concerned with the tradeoffs between low-cost heterogenous designs and optimality. We study a class of constrained myopic strategic games on networks which approximate the solutions to a constrained quadratic optimization problem; the Nash equilibria of these games can be found using best-response dynamical systems, which only use local information. The notion of price of heterogeneity captures the quality of our approximations. This notion relies on the structure and the strength of the interconnections between agents. We study the stability properties of these dynamical systems and demonstrate their complex characteristics, including abundance of equilibria on graphs with high sparsity and heterogeneity. We also introduce the novel notions of social equivalence and social dominance, and show some of their interesting implications, including their correspondence to consensus. Finally, using a classical result of Hirsch [1], we fully characterize the stability of these dynamical systems for the case of star graphs with asymmetric interactions. Various examples illustrate our results. (ID#:14-2588)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6760041&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6760041
Publication Location: IEEE Conference on Decision and Control (CDC), December 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Game-theoretic methods for robustness, security and resilience of cyber-physical control systems: Games-in-games principle for optimal cross-layer resilient control systems
Author(s): Q. Zhu and T. Basar
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Not IEEE Modern critical infrastructures are highly integrated systems composed of many complex interactions between different system modules or agents including cyber and physical components as well as human factors. Their growing complexity demands novel design techniques for scalable and efficient control and computations for providing system security and resilience. This dissertation develops new game-theoretic frameworks for addressing security and resilience problems residing at multiple layers of the cyber-physical systems including robust and resilient control, secure network routing and management of information security and smart grid energy systems. Hybrid distributed reinforcement learning algorithms are developed as practical modeling tools for defense systems with different levels of rationality and intelligence at different times. The learning algorithms enable online computations of defense strategies, such as routing decisions and configuration policies, for nonzero-sum security games with incomplete information. In addition, games-in-games frameworks are proposed for system-wide modeling of complex hierarchical systems, where games played at different levels interact through their outcomes, action spaces, and costs. This concept is applied to robust and resilient control of power systems in which a zero-sum differential game for physical robust control design is nested in and coupled with a zero-sum stochastic game for security policy design. At the networking layer of the system, multi-hop secure routing games also exhibit the games-in-games structure, and their equilibrium solutions are characterized by backward induction solving a sequence of nested games. This approach leads to a distributed secure routing protocol that enables the resilience of network routing and self-recovery mechanisms in face of adversarial attacks. Finally, in order to address emerging energy management issues of the smart grid, we establish a fundamental game-theoretic framework for analyzing system equilibrium under distributed generations, renewable energy sources and active participation of utility users. Furthermore, we develop a novel game framework and its equilibrium solution, named mirror Stackelberg equilibrium, for modeling the demand response management in the smart grid. This approach enables quantitative study of the value of demand response brought by emerging smart grid technologies as compared to the current supply-side economic dispatch model. It facilitates fundamental understanding of pricing, energy policies and infrastructural investment decision in future highly interconnected and interdependent energy systems. Examples from power systems, cognitive radio communication networks, and the smart grid are used as driving examples for illustrating new solution concepts, distributed algorithms and analytical techniques presented in this dissertation. (ID#:14-2589)
URL: http://oatd.org/oatd/record?record=handle%5C:2142%5C%2F45479
Publication Location: IEEE Control Systems Magazine
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: A three-stage Colonel Blotto game with applications to cyberphysical security
Author(s): A. Gupta, G. Schwartz C. Langbort, S. Sastry, and T. Basar
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Gupta, A; Schwartz, G.; Langbort, C.; Sastry, S.S.; Basar, T., "A three-stage Colonel Blotto game with applications to cyberphysical security," American Control Conference (ACC), 2014 , vol., no., pp.3820,3825, 4-6 June 2014 doi: 10.1109/ACC.2014.6859164
We consider a three-step three-player complete information Colonel Blotto game in this paper, in which the first two players fight against a common adversary. Each player is endowed with a certain amount of resources at the beginning of the game, and the number of battlefields on which a player and the adversary fights is specified. The first two players are allowed to form a coalition if it improves their payoffs. In the first stage, the first two players may add battlefields and incur costs. In the second stage, the first two players may transfer resources among each other. The adversary observes this transfer, and decides on the allocation of its resources to the two battles with the players. At the third step, the adversary and the other two players fight on the updated number of battlefields and receive payoffs. We characterize the subgame-perfect Nash equilibrium (SPNE) of the game in various parameter regions. In particular, we show that there are certain parameter regions in which if the players act according to the SPNE strategies, then (i) one of the first two players add battlefields and transfer resources to the other player (a coalition is formed), (ii) there is no addition of battlefields and no transfer of resources (no coalition is formed). We discuss the implications of the results on resource allocation for securing cyberphysical systems. (ID#:14-2590)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6859164&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel7%2F6849600%2F6858556%2F06859164.pdf%3Farnumber%3D6859164
Publication Location: 2014 American Control Conference (ACC) 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Stability properties of infected networks with low curing rates
Author(s): A. Khanafer, T. Basar, and B. Gharesifard
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Khanafer, A; Basar, T.; Gharesifard, B., "Stability properties of infected networks with low curing rates," American Control Conference (ACC), 2014 , vol., no., pp.3579,3584, 4-6 June 2014 doi: 10.1109/ACC.2014.6859418
In this work, we analyze the stability properties of a recently proposed dynamical system that describes the evolution of the probability of infection in a network. We show that this model can be viewed as a concave game among the nodes. This characterization allows us to provide a simple condition, that can be checked in a distributed fashion, for stabilizing the origin. When the curing rates at the nodes are low, a residual infection stays within the network. Using properties of Hurwitz Mertzel matrices, we show that the residual epidemic state is locally exponentially stable. We also demonstrate that this state is globally asymptotically stable. Furthermore, we investigate the problem of stabilizing the network when the curing rates of a limited number of nodes can be controlled. In particular, we characterize the number of controllers required for a class of undirected graphs. Several simulations demonstrate our results. (ID#:14-2591)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6859418&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6859418
Publication Location: 2014 American Control Conference (ACC) 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Control over lossy networks: A dynamic game approach
Author(s): J. Moon and T. Basar
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Jun Moon; Basar, T., "Control over TCP-like lossy networks: A dynamic game approach," American Control Conference (ACC), 2013 , vol., no., pp.1578,1583, 17-19 June 2013 doi: 10.1109/ACC.2013.6580060
This paper considers H optimal control of LTI systems where the loop is closed over TCP-like lossy networks. Following a game theoretic formulation of the problem, we first obtain an explicit Hcontroller. We then analyze the infinite-horizon behavior of the H controller. In particular, we provide necessary and sufficient conditions in terms of the packet drop probability and the H disturbance attenuation parameter under which the optimal controller is unique and stabilizes the closed-loop system in the mean-square sense. It is also shown that these conditions are coupled; therefore, they cannot be determined independently. A numerical example is presented to illustrate the main results. (ID#:14-2592)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6580060&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6580060
Publication Location: 2014 American Control Conference (ACC) 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Actors Programming for the Mobile Cloud
Author(s): Gul Agha
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: From UCLA; different title, same content; no abstract available (ID#:14-2593)
URL: http://www.cs.ucla.edu/~palsberg/course/cs239/papers/karmani-agha.pdf
Publication Location: International Symposium on Parallel and Distributed Computing 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: The Science of Summarizing Systems: Generating Security Properties Using Data Mining and Formal Analysis
Title: Using Control-Flow Techniques in a Security Context: A Survey on Common Prototypes and Their Common Weakness
Author(s): Seeger, M.M
Abstract: Seeger, M.M., "Using Control-Flow Techniques in a Security Context: A Survey on Common Prototypes and Their Common Weakness," Network Computing and Information Security (NCIS), 2011 International Conference on , vol.2, no., pp.133,137, 14-15 May 2011
doi: 10.1109/NCIS.2011.126
Practical approaches using control-flow techniques in order to detect changes in the control-flow of a program have been subject of many scientific works. This work focuses on three common tools making use of control- and data-flow analysis in order to detect alternations and reveals their common weakness in terms of the ability to react directly to a dynamic change in control-flow. With a general focus on static analysis of binaries or source code, detection of dynamic changes in the executive flow cannot be detected. In order to emphasize this shortcoming of static analysis, we present an approach for dynamically changing a program's control-flow and validate it by depicting a proof of concept. (ID#:14-2594)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=5948809&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D5948809
Publication Location: Network Computing and Information Security (NCIS), 2011
UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Parameterized concurrent multi-party session types
Author(s): Minas Charalambides, Peter Dinges, and Gul Agha
Abstract: From arXiv: Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful in verifying some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with inherent asynchrony. For example, the sliding window protocol is inexpressible in previously proposed session type systems. This paper describes System-A, a new typing language which overcomes many of the expressiveness limitations of prior work. System-A explicitly supports asynchrony and parallelism, as well as multiple forms of parameterization. We define System-A and show how it can be used for the static verification of a large class of asynchronous communication protocols. (ID#:14-2595)
URL: http://arxiv.org/pdf/1208.4632.pdf
Publication Location: International Workshop on Foundations of Coordination Languages and Self Adaptation 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Why Do Scala Developers Mix the Actor Model with Other Concurrency Models
Author(s): Samira Tasharo , Peter Dinges, and Ralph Johnson
Abstract: Samira Tasharofi, Peter Dinges, and Ralph E. Johnson. 2013. Why do scala developers mix the actor model with other concurrency models?. In Proceedings of the 27th European conference on Object-Oriented Programming (ECOOP'13), Giuseppe Castagna (Ed.). Springer-Verlag, Berlin, Heidelberg, 302-326. DOI=10.1007/978-3-642-39038-8_13 http://dx.doi.org/10.1007/978-3-642-39038-8_13
Mixing the actor model with other concurrency models in a single program can break the actor abstraction. This increases the chance of creating deadlocks and data races--two mistakes that are hard to make with actors. Furthermore, it prevents the use of many advanced testing, modeling, and verification tools for actors, as these require pure actor programs. This study is the first to point out the phenomenon of mixing concurrency models by Scala developers and to systematically identify the factors leading to it. We studied 15 large, mature, and actively maintained actor programs written in Scala and found that 80% of them mix the actor model with another concurrency model. Consequently, a large part of real-world actor programs does not use actors to their fullest advantage. Inspection of the programs and discussion with the developers reveal two reasons for mixing that can be influenced by researchers and library-builders: weaknesses in the actor library implementations, and shortcomings of the actor model itself. (ID#:14-2596)
URL: http://dl.acm.org/citation.cfm?id=2525001
Publication Location: ECOOP 2013 - Object-Oriented Programming
UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Automated inference of atomic sets for safe concurrent execution
Author(s): Peter Dinges, Minas Charalambides, and Gul Agha
Abstract: Peter Dinges, Minas Charalambides, and Gul Agha. 2013. Automated inference of atomic sets for safe concurrent execution. In Proceedings of the 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE '13). ACM, New York, NY, USA, 1-8. DOI=10.1145/2462029.2462030 http://doi.acm.org/10.1145/2462029.2462030
Atomic sets are a synchronization mechanism in which the programmer specifies the groups of data that must be accessed as a unit. The compiler can check this specification for consistency, detect deadlocks, and automatically add the primitives to prevent interleaved access. Atomic sets relieve the programmer from the burden of recognizing and pruning execution paths which lead to interleaved access, thereby reducing the potential for data races. However, manually converting programs from lock-based synchronization to atomic sets requires reasoning about the program's concurrency structure, which can be a challenge even for small programs. Our analysis eliminates the challenge by automating the reasoning. Our implementation of the analysis allowed us to derive the atomic sets for large code bases such as the Java collections framework in a matter of minutes. The analysis is based on execution traces; assuming all traces reflect intended behavior, our analysis enables safe concurrency by preventing unobserved interleavings which may harbor latentHeisenbugs (ID#:14-2597)
URL: http://dl.acm.org/citation.cfm?id=2462030
Publication Location: Workshop on Program Analysis for Software Tools and Engineering 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Performance Evaluation of Sensor Networks by Statistical Modeling and Euclidean Model Checking
Author(s): YoungMin Kwon and Gul Agha
Abstract: Youngmin Kwon and Gul Agha. 2013. Performance evaluation of sensor networks by statistical modeling and euclidean model checking. ACM Trans. Sen. Netw. 9, 4, Article 39 (July 2013), 38 pages. DOI=10.1145/2489253.2489256 http://doi.acm.org/10.1145/2489253.2489256
Modeling and evaluating the performance of large-scale wireless sensor networks (WSNs) is a challenging problem. The traditional method for representing the global state of a system as a cross product of the states of individual nodes in the system results in a state space whose size is exponential in the number of nodes. We propose an alternative way of representing the global state of a system: namely, as a probability mass function (pmf) which represents the fraction of nodes in different states. A pmf corresponds to a point in a Euclidean space of possible pmf values, and the evolution of the state of a system is represented by trajectories in this Euclidean space. We propose a novel performance evaluation method that examines all pmf trajectories in a dense Euclidean space by exploring only finite relevant portions of the space. We call our method Euclidean model checking. Euclidean model checking is useful both in the design phase--where it can help determine system parameters based on a specification--and in the evaluation phase--where it can help verify performance properties of a system. We illustrate the utility of Euclidean model checking by using it to design a time difference of arrival (TDoA) distance measurement protocol and to evaluate the protocol's implementation on a 90-node WSN. To facilitate such performance evaluations, we provide a Markov model estimation method based on applying a standard statistical estimation technique to samples resulting from the execution of a system. (ID#:14-2599)
URL: http://dl.acm.org/citation.cfm?id=2489256
Publication Location: ACM Transactions on Sensor Networks
UIUC - University of Illinois at Urbana-Champaign
Topic: Beyond Reachability Properties
Title: A Formal Definition of Protocol Indistinguishability and its Verification on Maude-NPA
Author(s): S. Escobar, C. Meadows, J. Meseguer, and S. Santiago
Abstract: not available: Possible broken lnk. (ID#:14-2600)
URL: http://users.dsic.upv.es/~sescobar/papers-security.html
Publication Location: UIUC Technical Report
UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Differentially Private Iterative Synchronous Consensus
Author(s): Zhenqi Huang, Sayan Mitra, Geir Dullerud
Abstract: Zhenqi Huang, Sayan Mitra, and Geir Dullerud. 2012. Differentially private iterative synchronous consensus. In Proceedings of the 2012 ACM workshop on Privacy in the electronic society (WPES '12). ACM, New York, NY, USA, 81-90. DOI=10.1145/2381966.2381978 http://doi.acm.org/10.1145/2381966.2381978
The iterative consensus problem requires a set of processes or agents with different initial values, to interact and update their states to eventually converge to a common value. Protocols solving iterative consensus serve as building blocks in a variety of systems where distributed coordination is required for load balancing, data aggregation, sensor fusion, filtering, and synchronization. In this paper, we introduce the private iterative consensus problem where agents are required to converge while protecting the privacy of their initial values from honest but curious adversaries. Protecting the initial states, in many applications, suffice to protect all subsequent states of the individual participants.
We adapt the notion of differential privacy in this setting of iterative computation. Next, we present (i) a server-based and (ii) a completely distributed randomized mechanism for solving differentially private iterative consensus with adversaries who can observe the messages as well as the internal states of the server and a subset of the clients. Our analysis establishes the tradeoff between privacy and the accuracy: for given e, b >0, the e-differentially private mechanism for N agents, is guaranteed to convergence to a value withinO(/1/e bN) of the average of the initial values, with probability at least (1-b). (ID#:14-2601)
URL: http://dl.acm.org/citation.cfm?id=2381978
Publication Location: Workshop on Privacy in the Electronic Society (WPES), collocated with of 19th ACM Conference on Computer and Communications Security (CCS) 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Using Run-Time Checking to Provide Safety and Progress for Distributed Cyber-Physical Systems
Author(s): Stanley Bak, Fardin Abdi, Zhenqi Huang and Marco Caccamo
Abstract: Bak, S.; Abad, F.AT.; Zhenqi Huang; Caccamo, M., "Using run-time checking to provide safety and progress for distributed cyber-physical systems," Embedded and Real-Time Computing Systems and Applications (RTCSA), 2013 IEEE 19th International Conference on , vol., no., pp.287,296, 19-21 Aug. 2013
doi: 10.1109/RTCSA.2013.6732229
Cyber-physical systems (CPS) may interact and manipulate objects in the physical world, and therefore ideally would have formal guarantees about their behavior. Performing static-time proofs of safety invariants, however, may be intractable for systems with distributed physical-world interactions. This is further complicated when realistic communication models are considered, for which there may not be bounds on message delays, or even that messages will eventually reach their destination. In this work, we address the challenge of proving safety and progress in distributed CPS communicating over an unreliable communication layer. This is done in two parts. First, we show that system safety can be verified by partially relying upon run-time checks, and that dropping messages if the run-time checks fail will maintain safety. Second, we use a notion of compatible action chains to guarantee system progress, despite unbounded message delays. We demonstrate the effectiveness of our approach on a multi-agent vehicle flocking system, and show that the overhead of the proposed run-time checks is not overbearing. (ID#:14-2602)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6732229&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel7%2F6720220%2F6732192%2F06732229.pdf%3Farnumber%3D6732229
Publication Location: IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2013)
UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Classification of Cyber-physical System Adversaries
Author(s): R. Essick, J.-W. Lee, and G.E. Dullerud
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Essick, R.; Lee, J.; Dullerud, G.E., "Control of Linear Switched Systems With Receding Horizon Modal Information," Automatic Control, IEEE Transactions on , vol.59, no.9, pp.2340,2352, Sept. 2014
doi: 10.1109/TAC.2014.2321251
We provide an exact solution to two performance problems--one of disturbance attenuation and one of windowed variance minimization--subject to exponential stability. Considered are switched systems, whose parameters come from a finite set and switch according to a language such as that specified by an automaton. The controllers are path-dependent, having finite memory of past plant parameters and finite foreknowledge of future parameters. Exact, convex synthesis conditions for each performance problem are expressed in terms of nested linear matrix inequalities. The resulting semidefinite programming problem may be solved offline to arrive at a suitable controller. A notion of path-by-path performance is introduced for each performance problem, leading to improved system performance. Non-regular switching languages are considered and the results are extended to these languages. Two simple, physically motivated examples are given to demonstrate the application of these results.(ID#:14-2603)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6808501&url=http%3A%2F%2Fieeexplore.ieee.org%2Fstamp%2Fstamp.jsp%3Ftp%3D%26arnumber%3D6808501
Publication Location: IEEE Transactions on Automatic Control, 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Path-By-Path Output Regulation of Switched Systems With a Receding Horizon of Modal Knowledge
Author(s): R. Essick, J.-W. Lee, and G.E. Dullerud
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Essick, R.; Ji-Woong Lee; Dullerud, G., "Path-by-path output regulation of switched systems with a receding horizon of modal knowledge," American Control Conference (ACC), 2014 , vol., no., pp.2650,2655, 4-6 June 2014
doi: 10.1109/ACC.2014.6859318
We address a discrete-time LQG control problem over a fixed performance window and apply a receding-horizon type control strategy, resulting in an exact solution to the problem in terms of semidefinite programming. The systems considered take parameters from a finite set, and switch between them according to an automaton. The controller has a finite preview of future parameters, beyond which only the set of parameters is known. We provide necessary and sufficient convex conditions for the existence of a controller which guarantees both exponential stability and finite-horizon performance levels for the system; the performance levels may differ according to the particular parameter sequence within the performance window. A simple, physics-based example is provided to illustrate the main results. (ID#:14-2604)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6859318&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6859318
Publication Location: proceedings of the American Control Conference (ACC), 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Proofs from Simulations and Modular Annotations
Author(s): Zhenqi Huang and Sayan Mitra
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Zhenqi Huang and Sayan Mitra. 2014. Proofs from simulations and modular annotations. InProceedings of the 17th international conference on Hybrid systems: computation and control(HSCC '14). ACM, New York, NY, USA, 183-192. DOI=10.1145/2562059.2562126 http://doi.acm.org/10.1145/2562059.2562126
We present a modular technique for simulation-based bounded verification for nonlinear dynamical systems. We introduce the notion of input-to-state discrepancy of each subsystem Ai in a larger nonlinear dynamical system A which bounds the distance between two (possibly diverging) trajectories of Ai in terms of their initial states and inputs. Using the IS discrepancy functions, we construct a low dimensional deterministic dynamical system M(d). For any two trajectories of A starting d distance apart, we show that one of them bloated by a factor determined by the trajectory of M contains the other. Further, by choosing appropriately small d's the overapproximations computed by the above method can be made arbitrarily precise. Using the above results we develop a sound and relatively complete algorithm for bounded safety verification of nonlinear ODEs. Our preliminary experiments with a prototype implementation of the algorithm show that the approach can be effective for verification of nonlinear models. (ID#:14-2605)
URL: http://dl.acm.org/citation.cfm?id=2562126
Publication Location: International Conference on Hybrid Systems: Computation and Control (HSCC 2014)
UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: On Price of Privacy in Distributed Control Systems
Author(s): Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir Dullerud
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir E. Dullerud. 2014. On the cost of differential privacy in distributed control systems. In Proceedings of the 3rd international conference on High confidence networked systems (HiCoNS '14). ACM, New York, NY, USA, 105-114. DOI=10.1145/2566468.2566474 http://doi.acm.org/10.1145/2566468.2566474
Individuals sharing information can improve the cost or performance of a distributed control system. But, sharing may also violate privacy. We develop a general framework for studying the cost of differential privacy in systems where a collection of agents, with coupled dynamics, communicate for sensing their shared environment while pursuing individual preferences. First, we propose a communication strategy that relies on adding carefully chosen random noise to agent states and show that it preserves differential privacy. Of course, the higher the standard deviation of the noise, the higher the cost of privacy. For linear distributed control systems with quadratic cost functions, the standard deviation becomes independent of the number agents and it decays with the maximum eigenvalue of the dynamics matrix. Furthermore, for stable dynamics, the noise to be added is independent of the number of agents as well as the time horizon up to which privacy is desired. Finally, we show that the cost of e-differential privacy up to time T, for a linear stable system with N agents, is upper bounded by O(T3/ Ne2). (ID#:14-2606)
URL: http://dl.acm.org/citation.cfm?id=2566468.2566474
Publication Location: ACM International Conference on High Confidence Networked Systems (HiCoNS) 2014
UIUC - University of Illinois at Urbana-Champaign
Topic: End-to-end Analysis of Side Channels
Title: Website Detection Using Remote Traffic Analysis
Author(s): Xun Gong, Nikita Borisov, Negar Kiyavash, Nabil Schear
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development, and Deployment
Abstract: Xun Gong, Nikita Borisov, Negar Kiyavash, and Nabil Schear. 2012. Website detection using remote traffic analysis. In Proceedings of the 12th international conference on Privacy Enhancing Technologies (PETS'12), Simone Fischer-Hubner and Matthew Wright (Eds.). Springer-Verlag, Berlin, Heidelberg, 58-78. DOI=10.1007/978-3-642-31680-7_4 http://dx.doi.org/10.1007/978-3-642-31680-7_4
Recent work in traffic analysis has shown that traffic patterns leaked through side channels can be used to recover important semantic information. For instance, attackers can find out which website, or which page on a website, a user is accessing simply by monitoring the packet size distribution. We show that traffic analysis is even a greater threat to privacy than previously thought by introducing a new attack that can be carried out remotely. In particular, we show that, to perform traffic analysis, adversaries do not need to directly observe the traffic patterns. Instead, they can gain sufficient information by sending probes from a far-off vantage point that exploits a queuing side channel in routers.
To demonstrate the threat of such remote traffic analysis, we study a remote website detection attack that wo rks against home broadband users. Because the remotely observed traffic patterns are more noisy than those obtained using previous schemes based on direct local traffic monitoring, we take a dynamic time warping (DTW) based approach to detecting fingerprints from the same website. As a new twist on website fingerprinting, we consider a website detection attack, where the attacker aims to find out whether a user browses a particular web site, and its privacy implications. We show experimentally that, although the success of the attack is highly variable, depending on the target site, for some sites very low error rates. We also show how such website detection can be used to deanonymize message board users. (ID#:14-2607)
URL: http://dl.acm.org/citation.cfm?id=2359021
Publication Location: 12th Privacy Enhancing Technologies Symposium (PETS) 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Attack-Tolerant Systems
Title: An Algorithmic Approach to Error Localization and Partial Recomputation for Low-Overhead Fault Tolerance on Parallel Systems
Author(s): Joseph Sloan, Greg Bronevetsky, and Rakesh Kumar
Abstract: Sloan, J.; Kumar, R.; Bronevetsky, G., "An algorithmic approach to error localization and partial recomputation for low-overhead fault tolerance," Dependable Systems and Networks (DSN), 2013 43rd Annual IEEE/IFIP International Conference on , vol., no., pp.1,12, 24-27 June 2013 doi: 10.1109/DSN.2013.6575309
The increasing size and complexity of massively parallel systems (e.g. HPC systems) is making it increasingly likely that individual circuits will produce erroneous results. For this reason, novel fault tolerance approaches are increasingly needed. Prior fault tolerance approaches often rely on checkpoint-rollback based schemes. Unfortunately, such schemes are primarily limited to rare error event scenarios as the overheads of such schemes become prohibitive if faults are common. In this paper, we propose a novel approach for algorithmic correction of faulty application outputs. The key insight for this approach is that even under high error scenarios, even if the result of an algorithm is erroneous, most of it is correct. Instead of simply rolling back to the most recent checkpoint and repeating the entire segment of computation, our novel resilience approach uses algorithmic error localization and partial recomputation to efficiently correct the corrupted results. We evaluate our approach in the specific algorithmic scenario of linear algebra operations, focusing on matrix-vector multiplication (MVM) and iterative linear solvers. We develop a novel technique for localizing errors in MVM and show how to achieve partial recomputation within this algorithm, and demonstrate that this approach both improves the performance of the Conjugate Gradient solver in high error scenarios by 3x-4x and increases the probability that it completes successfully by up to 60% with parallel experiments up to 100 nodes. (ID#:14-2608)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6575309
Publication Location: IEEE/IFIP International Conference on Dependable Systems and Networks, DSN, 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: From Measurements to Security Science - Data-Driven Approach
Title: Adapting Bro into SCADA: building a specification-based intrusion detection system for the DNP3 protocol
Author(s): H. Lin, A. Slagell, C. Di Martino, Z. Kalbarczyk, and R. Iyer
Abstract: When SCADA systems are exposed to public networks, attackers can more easily penetrate the control systems that operate electrical power grids, water plants, and other critical infrastructures. To detect such attacks, SCADA systems require an intrusion detection technique that can understand the information carried by their usually proprietary network protocols.
To achieve that goal, we propose to attach to SCADA systems a specification-based intrusion detection framework based on Bro [7][8], a runtime network traffic analyzer. We have built a parser in Bro to support DNP3, a network protocol widely used in SCADA systems that operate electrical power grids. This built-in parser provides a clear view of all network events related to SCADA systems. Consequently, security policies to analyze SCADA-specific semantics related to the network events can be accurately defined. As a proof of concept, we specify a protocol validation policy to verify that the semantics of the data extracted from network packets conform to protocol definitions. We performed an experimental evaluation to study the processing capabilities of the proposed intrusion detection framework .(ID#:14-2609)
URL: http://dl.acm.org/citation.cfm?id=2459982
Publication Location: Annual Cyber Security and Information Intelligence Research Workshop (CSIIRW 2012)
UIUC - University of Illinois at Urbana-Champaign
Topic: From Measurements to Security Science - Data-Driven Approach
Title: Semantic Security Analysis of SCADA Networks to Detect Malicious Control Commands in Power Grids
Author(s): H. Lin, A. Slagell, Z. Kalbarczyk, P. Sauer, R. Iyer
Abstract: Hui Lin, Adam Slagell, Zbigniew Kalbarczyk, Peter W. Sauer, and Ravishankar K. Iyer. 2013. Semantic security analysis of SCADA networks to detect malicious control commands in power grids. In Proceedings of the first ACM workshop on Smart energy grid security (SEGS '13). ACM, New York, NY, USA, 29-34. DOI=10.1145/2516930.2516947 http://doi.acm.org/10.1145/2516930.2516947
In the current generation of SCADA (Supervisory Control And Data Acquisition) systems used in power grids, a sophisticated attacker can exploit system vulnerabilities and use a legitimate maliciously crafted command to cause a wide range of system changes that traditional contingency analysis does not consider and remedial action schemes cannot handle. To detect such malicious commands, we propose a semantic analysis framework based on a distributed network of intrusion detection systems (IDSes). The framework combines system knowledge of both cyber and physical infrastructure in power grid to help IDS to estimate execution consequences of control commands, thus to reveal attacker's malicious intentions. We evaluated the approach on the IEEE 30-bus system. Our experiments demonstrate that: (i) by opening 3 transmission lines, an attacker can avoid detection by the traditional contingency analysis and instantly put the tested 30-bus system into an insecure state and (ii) the semantic analysis provides reliable detection of malicious commands with a small amount of analysis time. (ID#:14-2610)
URL: http://dl.acm.org/citation.cfm?id=2516947
Publication Location: IEEE Int'l Conference on Smart Grid Communications, SmartGridComm 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Protocol Verification: Beyond Reachability Properties
Title: Asymmetric unification: A new unification paradigm for cryptographic protocol analysis
Author(s): Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos'e Meseguer, Paliath Narendran, Sonia Santiago and Ralf Sasse
Abstract: Available from Springer via link listed below.. (ID#:14-2611)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-38574-2_16
Publication Location: Intl. Conf. On Automated Deduction (CADE 2013)
UIUC - University of Illinois at Urbana-Champaign
Topic: Protocol Verification: Mathematical Foundations & Analysis Techniques for Protocol Indistinguishability
Title: Sequential Protocol Compositon in Maude-NPA
Author(s): Santiago Escobar, Catherine Meadows, Jose Meseguer and Sonia Santiago
Hard Problem: Scalability and Composability
Abstract: Santiago Escobar, Catherine Meadows, Jos\&\#233; Meseguer, and Sonia Santiago. 2010. Sequential protocol composition in maude-NPA. In Proceedings of the 15th European conference on Research in computer security (ESORICS'10), Dimitris Gritzalis, Bart Preneel, and Marianthi Theoharidou (Eds.). Springer-Verlag, Berlin, Heidelberg, 303-318.
Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified separately and composed when desired. This allows one to reason about many different compositions with minimal changes to the specification. Moreover, we show that, by a simple protocol transformation, we are able to analyze and verify this dynamic composition in the current Maude-NPA tool. We prove soundness and completeness of the protocol transformation with respect to the extended operational semantics, and illustrate our results on some examples. (ID#:14-2612)
URL: http://dl.acm.org/citation.cfm?id=1888906
Publication Location: Computer Security - ESORICS 2010
UIUC - University of Illinois at Urbana-Champaign
Topic: Protocol Verification: Mathematical Foundations & Analysis Techniques for Protocol Indistinguishability
Title: A Rewriting- based forward semantics for Maude-NPA
Author(s): Santiago Escobar, Catherine Meadows, Jose Meseguer and Sonia Santiago
Hard Problem: Scalability and Composability
Abstract: The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It tries to find secrecy or authentication attacks by searching backwards from an insecure attack state pattern that may contain logical variables, in such a way that logical variables become properly instantiated in order to find an initial state. The execution mechanism for this logical reachability is narrowing modulo an equational theory. Although Maude-NPA also possesses a forwards semantics naturally derivable from the backwards semantics, it is not suitable for state space exploration or protocol simulation.
In this paper we define an executable forwards semantics for Maude-NPA, instead of its usual backwards one, and restrict it to the case of concrete states, that is, to terms without logical variables. This case corresponds to standard rewriting modulo an equational theory. We prove soundness and completeness of the backwards narrowing-based semantics with respect to the rewriting-based forwards semantics. We show its effectiveness as an analysis method that complements the backwards analysis with new prototyping, simulation, and explicit-state model checking features by providing some experimental results. (ID#:14-2613)
URL: http://dl.acm.org/citation.cfm?id=2600186&dl=ACM&coll=DL&CFID=552978724&CFTOKEN=96539078
Publication Location: In Proceedings HotSoS '14
UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security (SHuCS)
Title: Circumvention of Security: Good Users Do Bad Things
Author(s): J. Blythe, R. Koppel, and S.W. Smith
Hard Problem: Human Behavior
Abstract: Blythe, J.; Koppel, R.; Smith, S.W., "Circumvention of Security: Good Users Do Bad Things," Security & Privacy, IEEE , vol.11, no.5, pp.80,83, Sept.-Oct. 2013 doi: 10.1109/MSP.2013.110
Conventional wisdom is that the textbook view describes reality, and only bad people (not good people trying to get their jobs done) break the rules. And yet it doesn't, and good people circumvent. (ID#:14-2614)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6630017
Publication Location: IEEE Security and Privacy 2013
UIUC - University of Illinois at Urbana-Champaign
Topic: Quantitative Security Metrics for Cyber-Human Systems
Title: Simulation debugging and visualization in the Mobius modeling framework
Author(s): Buchanan, Craig
Hard Problem: Metrics
Abstract: Available from Springer via link listed below.. (ID#:14-2615)
URL: http://link.springer.com/chapter/10.1007/978-3-319-10696-0_18
Publication Location: M.S. Thesis, ECE Dept., Univ. of Illinois
UIUC - University of Illinois at Urbana-Champaign
Topic: No Topic Listed
Title: VeriFlow: Verifying Network-Wide Invariants in Real Time
Author(s): Ahmed Khurshid, Kelvin Zou, Wenxuan Zhou, Matthew Caesar, P. Brighten Godfrey
Abstract: Networks are complex and prone to bugs. Existing tools that check configuration files and data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise.
Is it possible to check network-wide invariants in real time, as the network state evolves? The key challenge here is to achieve extremely low latency during the checks so that network performance is not affected. In this paper, we present a preliminary design, VeriFlow, which suggests that this goal is achievable. VeriFlow is a layer between a software-defined networking controller and network devices that checks for network-wide invariant violations dynamically as each forwarding rule is inserted. Based on an implementation using a Mininet OpenFlow network and Route Views trace data, we find that VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion. (ID#:14-2616)
URL: http://dl.acm.org/citation.cfm?id=2342452
Publication Location: ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (HotSDN), August 2012
UIUC - University of Illinois at Urbana-Champaign
Topic: Data Driven Security Models and Analysis
Title: An Experiment Using Factor Graph for Early Attack Detection
Author(s): P. Cao, K-W. Chung, A. Slagell, Z. Kalbarcyk, R. Iyer
Hard Problem: Metrics, Resilient Architectures, Human Behavior
Abstract: Not Found (ID#:14-2617)
URL: Not found
See: : "Preemptive Intrusion Detection" by P. Cao, K-W. Chung, A. Slagell, Z. Kalbarczyk, R. Iyer at http://dl.acm.org/citation.cfm?id=2600177
Note:
Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to SoS.Project (at) SecureDataBank.net for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.
UMD - University of Maryland
These publications were done for the Lablet activities at this school, and were listed in the Quarterly Reports back to the government. Please direct any comments to research (at) securedatabank.net if there are any questions or concerns regarding these publications.
UMD - University of Maryland, College Park
Topic: Trust, Recommendation Systems, and Collaboration
Title: A Fresh Look at Network Science: Interdependent Multigraphs Models Inspired From Statistical Physics
Author(s): J.S. Baras
Hard Problem: Scalability and Composability, Policy-Governed Secure Collaboration, Human Behavior
Abstract: Baras, J.S., "A fresh look at network science: Interdependent multigraphs models inspired from statistical physics," Communications, Control and Signal Processing (ISCCSP), 2014 6th International Symposium on , vol., no., pp.497,500, 21-23 May 2014
doi: 10.1109/ISCCSP.2014.6877921
We consider several challenging problems in complex networks (communication, control, social, economic, biological, hybrid) as problems in cooperative multi-agent systems. We describe a general model for cooperative multi-agent systems that involves several interacting dynamic multigraphs and identify three fundamental research challenges underlying these systems from a network science perspective. We show that the framework of constrained coalitional network games captures in a fundamental way the basic tradeoff of benefits vs. cost of collaboration, in multi-agent systems, and demonstrate that it can explain network formation and the emergence or not of collaboration. Multi-metric problems in such networks are analyzed via a novel multiple partially ordered semirings approach. We investigate the interrelationship between the collaboration and communication multigraphs in cooperative swarms and the role of the communication topology, among the collaborating agents, in improving the performance of distributed task execution. Expander graphs emerge as efficient communication topologies for collaborative control. We relate these models and approaches to statistical physics. (ID#:14-2618)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6877921&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel7%2F6862736%2F6877795%2F06877921.pdf%3Farnumber%3D6877921
Publication Location: Proceedings 6th International Symposium on Communications, Control and Signal Processing (ISCCSP 2014)
UMD - University of Maryland, College Park
Topic: Trust, Recommendation Systems, and Collaboration
Title: Using Trust in Distributed Consensus With Adversaries in Sensor and Other Networks
Author(s): X. Liu and J.S. Baras
Hard Problem: Scalability and Composability, Policy-Governed Secure Collaboration, Human Behavior
Abstract: From UMD.edu: Extensive research efforts have been devoted to distributed consensus with adversaries. Many diverse applications drive this increased interest in this area including distributed collaborative sensor networks, sensor fusion and distributed collaborative control. We consider the problem of detecting Byzantine adversaries in a network of agents with the goal of reaching consensus. We propose a novel trust model that establishes both local trust based on local evidences and global trust based on local exchange of local trust values. We describe a trust-aware consensus algorithm that integrates the trust evaluation mechanism into the traditional consensus algorithm and propose various local decision rules based on local evidence. To further enhance the robustness of trust evaluation itself, we also provide a trust propagation scheme in order to take into account evidences of other nodes in the network. Then we show by simulation that the trust aware consensus algorithm can effectively detect Byzantine adversaries and excluding them from consensus iterations even in sparse networks with connectivity less than 2f + 1, where f is the number of adversaries. These results can be applied for fusion of trust evidences as well as for sensor fusion when malicious sensors are present like for example in power grid sensing and monitoring (ID#:14-2619)
URL: https://www.isr.umd.edu/~baras/publications/papers/2014/X_%20Liu_J_S_%20Baras_Using_Trust_in_Distributed_Consensus.html
Publication Location: Proceedings of 17th International Confernce on Information Fusion (FUSION 2014)
UMD - University of Maryland, College Park
Topic: Trust, Recommendation Systems, and Collaboration
Title: Soft Contract Verification
Author(s): Nguyen, Tobin-Hochstadt, Van Horn
Abstract: Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. 2014. Soft contract verification. InProceedings of the 19th ACM SIGPLAN international conference on Functional programming (ICFP '14). ACM, New York, NY, USA, 139-152. DOI=10.1145/2628136.2628156 http://doi.acm.org/10.1145/2628136.2628156
Behavioral software contracts are a widely used mechanism for governing the flow of values between components. However, run-time monitoring and enforcement of contracts imposes significant overhead and delays discovery of faulty components to run-time.
To overcome these issues, we present soft contract verification, which aims to statically prove either complete or partial contract correctness of components, written in an untyped, higher-order language with first-class contracts. Our approach uses higher-order symbolic execution, leveraging contracts as a source of symbolic values including unknown behavioral values, and employs an updatable heap of contract invariants to reason about flow-sensitive facts. We prove the symbolic execution soundly approximates the dynamic semantics and that verified programs can't be blamed.
The approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of an off-the-shelf solver to decide problems without heavy encodings. The approach is competitive with a wide range of existing tools - including type systems, flow analyzers, and model checkers - on their own benchmarks. (ID#:14-2620)
URL: http://dl.acm.org/citation.cfm?id=2628156
Publication Location: proceedings of The 19th ACM SIGPLAN International Conference on Functional Programming 2014
UMD - University of Maryland, College Park
Topic: Verifcation of Hyperproperties
Title: Temporal Logics for Hyperproperties
Author(s): Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and Cesar Sanchez
Abstract: Available from Springer the via link listed below. (ID#:14-2621)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-54792-8_15
Publication Location: Conference on Principles of Security and Trust 2014
Note:
Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to SoS.Project (at) SecureDataBank.net for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.