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.