SoS Lablet Annual Report - CMU

Lablet Annual Report
Purpose: To highlight progress made within the first base year (March 2014 to Present). Information is generally at a higher level which is accessible to the interested public. This will be published in an overall SoS Annual Report to be shared with stakeholders to highlight the accomplishments the Lablets have made over the past year.

A). Lablet Introduction

The Carnegie Mellon University (CMU) Science of Security (SoS) Lablet fosters scientific research in support of the cybersecurity mission of the National Security Agency. The CMU SoS Lablet has the mission to advance the state of cybersecurity research by focusing on the hardest technical problems, with emphasis on scale through composability of modeling and reasoning and on human behavior and usability for developers, evaluators, operators, and end users. The CMU Lablet also addresses SoS hard problems related to resilient architectures, predictive metrics, and policy-governed collaboration. Each of these five areas features a high level of technical challenge, a real opportunity for operational significance, and a high likelihood of benefit from the synergetic Lablet approach.

The CMU SoS Lablet includes a set of interlinked technical projects that involve fifteen faculty from more than four CMU academic departments, and seven other partner universities, including Cornell University, University of California at Irvine and Berkeley, University of Pittsburgh, Wayne State University, University of Nebraska, and University of Texas, San Antonio. Ten PhD students are supported, as well as several postdoctoral researchers, for the purpose of supporting the growth of researchers in SoS.

The major accomplishments over the past year are summarized in the following descriptions of our eleven projects.

B). Fundamental Research
High level report of results for each project that helped move security science forward -- in most cases it should point to a "hard problem". - 1 paragraph per project

PROJECT - Race Vulnerability Study and Hybrid Race Detection

PIs - Jonathan Aldrich (CMU) and Witawas Srisa-an (University of Nebraska, Lincoln)

Race conditions, since they are non-deterministic in nature, are notoriously hard to detect, yet they are a common cause of security vulnerabilities. In this project, we aim to improve the tradeoff between scalability and precision in race detectors. Existing race detectors suffer from either many false positives or unacceptably high overhead, which impedes their use in real world systems. Our hybrid race detection technique aims to be efficient and precise enough for practical large-scale applications.

In addition, we aim to better understand the human factors that cause race conditions. To do so, we are assembling a dataset of reproducible race vulnerabilities in real world programs and cataloging them to identify recurring problems. We are also running programming experiments to compare concurrency paradigms (e.g. the Cilk vs. OpenMP) to understand how these paradigms impact the security of the resulting code. If the study uncovers interesting relationships between races and security attacks, it can further contribute to security metrics research by providing another dimension of security assessment criteria. We also hope these studies will open up opportunities to mitigate race-related vulnerabilities.

PROJECT - A Language and Framework for Development of Secure Mobile Applications

PI - Jonathan Aldrich (CMU)

The goal of this project is to produce a language and framework that enables the construction of secure mobile applications with known security properties. The framework-based approach requires composition between the framework and its plugins, with modular type system and analysis techniques that avoid reanalyzing each individual component.

For example, providing programmers with mechanisms for constructing commands that are as convenient as strings while being as secure as prepared SQL statements is a promising mechanism for eliminating injection vulnerabilities. Mechanisms for embedding domain-specific languages (DSLs) for constructing commands within a programming language exist, but none have achieved widespread use, in part because prior techniques were unmodular, so that separately-defined embedded DSLs could not be used together. In this project we address these limitations using a novel mechanism called type-specific languages that supports modular DSL embeddings by associating a unique DSL with appropriate types.

Key issues include scalability (e.g. between client, server, and other distributed resources), tool usability, and security attributes such as confidentiality, integrity, and mitigation of common vulnerabilities seen in present technologies.Human behavior is also secondarily relevant, both because human limitations are the cause of many of the security vulnerabilities that we hope to eliminate, but also because an understanding of the way humans develop software is key to ensuring that our approach is usable and enhances (rather than detracts from) developer productivity.

PROJECT - Usable Formal Methods for the Design and Comp of Security and Privacy Policies

PI – Travis Breaux

When software developers reuse existing libraries, frameworks, platforms or services, they often cannot assess the security requirements satisfied by those third-party programs. We developed techniques for expressing data flow requirements and checking whether these flows preserve the use and collection limitation principles from international privacy standards. The approach is based on Description Logic and supports verification across requirements compositions, which occur when mobile apps are run on mobile devices or other platforms, or when software employs remote services for storage, authentication, etc. The results will appear in the proceedings of the 23rd IEEE International Requirements Engineering Conference, and the source code and a demonstration have been made available online.

T. D. Breaux, D. Smullen, H. Hibshi. "Detecting Repurposing and Over-collection in Multi-Party Privacy Requirements Specifications." To Appear: IEEE 23rd International Requirements Engineering Conference, Ottawa, Canada, Sep. 2015.

Security is based on defense-in-depth, which requires the satisfaction of multiple security requirements to mitigate security threats. However, the prevailing mechanism for information assurance is based on checklists, which assume a single threat context (often the union of all possible threats and mitigations).  We developed a technique to measure the impact of composing security requirements on perceived security risk in the presence of changing threats. The technique is based on multi-level modeling, a statistical technique that can measure the correlation of multiple factors on a dependent variable, such as risk perception. As we scale this approach to an increasing number of threats, the results can be used to propose a minimal set of security requirements likely believed to mitigate the most relevant threats. The results will appear in the proceedings of the 23rd IEEE International Requirements Engineering

H. Hibshi, T. D. Breaux, S. B. Broomell, "Assessment of Risk Perception in Security Requirements Composition." To Appear: IEEE 23rd International Requirements Engineering Conference, 2015.

Codifying privacy regulations to be consistent with the their high-level intuition can be difficult for security architects or application domain experts of information systems. We provide a formal framework to use UML sequence diagrams as a practical means to graphically express privacy regulations and policies to enable domain experts to verify and confirm the codification is valid. Once intuitively confirmed, our framework introduces an algorithmic approach to formalizing the semantics of sequence diagrams in terms of linear temporal logic (LTL) templates. In all the templates, different semantic aspects are expressed as separate, yet simple LTL formulas that can be composed to define the complex semantics of sequence diagrams. We leverage the analytical powers of automated decision procedures for LTL formulas to determine if a collection of sequence diagrams is consistent, and independent and also to verify if a system design conforms to the privacy policies. This work will appear in IEEE Transactions on Dependable and Secure Computing in 2015.  

Hui Shen, Ram Krishnan, Rocky Slavin, and Jianwei Niu. "Sequence Diagrams Aided Privacy Policy Specification". To appear: IEEE Transactions on Dependable and Secure Computing (TDSC), 14 pages, 2015.

PROJECT - Geo-Temporal Characterization of Security Threats

PI – Kathleen Carley

This project aims to develop a global characterization of cyber-security threats.  Using data from Symantec, and other indicators at the nation-state level a threatened and threatening profile per country is produced.  Questions addressed include, but are not limited to, which countries are most vulnerable to which types of threats?  Are cyber threats following traditional lines of hostilities at the global level, or are new threats emerging?  Social network and statistical techniques are used to assess the overall threat profile.

PROJECT - USE: User Security Behavior

PI – Lorrie Cranor

The Security Behavior Observatory addresses the hard problem of "Understanding and Accounting for Human Behavior" by collecting data directly from people's own home computers, thereby capturing people's computing behavior "in the wild". This data is the closest to the ground truth of the users' everyday security and privacy challenges that the research community has ever collected. We expect the insights discovered by analyzing this data will profoundly impact multiple research domains, including but not limited to behavioral sciences, computer security & privacy, economics, and human-computer interaction. The Security Behavior Observatory will also address the "Predictive Security Metrics" hard problem in two ways; first, by evaluating established metrics for measuring their user-reported security behaviors by comparing them to users' actual computing behavior, and second, by proposing new predictive metrics on user behavior with the respect to computer security and privacy founded on highly ecologically-valid data analyses.

PROJECT – Secure Composition of Systems and Policies

PI(s) – Anupam Datta, Limin Jia

Interface-confinement is a common mechanism that secures untrusted code by executing it inside a sandbox. The sandbox limits (confines) the code’s interaction with key system resources to a restricted set of interfaces. This practice is seen in web browsers, hypervisors, and other security-critical systems. Motivated by these systems, we develop a program logic, called System M, for modeling and proving safety properties of systems that execute adversary-supplied code via interface-confinement.

In addition to using computation types to specify effects of computations, System M includes a novel invariant type to specify the properties of interface-confined code. System M supports compositional proof--security proofs of sequentially composed programs are built from proofs of their sub-programs. System M also admits concurrent composition--properties proved of a program hold when that program executes concurrently with other, even adversarial, programs. System M can be used to model and verify protocols as well as system designs.

We demonstrate the reasoning principles of System M by verifying the state integrity property of the design of Memoir, a previously proposed trusted computing system.

PROJECT - Science of Secure Frameworks

PI – David Garlan, Bradley Schmerl

In this project, we are building scientific basis for the security of framework-based applications. Software frameworks, such as Android, are used ubiquitously in modern applications because they offer a unique means for achieving composition and reuse at scale.  Achieving security in framework-based applications can be challenging because of the close coupling between a framework and its plugins:  Plugin developers must understand and obey the constraints in the framework's security model, which can be quite complex, in order to achieve security of the resulting application. We are investigating a combination of static and dynamic checking of framework security rules that can be used to provide secure frameworks that still maintain the flexibility to allow extensive plugins.

Our work in this project is focused on Android, along the following thrusts: 1) use of static analysis and model checking techniques to identify potential vulnerabilities that a set of apps installed on a device (we call this an app ecosystem) may exhibit; 2) architectural modeling and analysis of the app ecosystem to augment vulnerability checking; 3) use of architectural models at run time to guide run time analysis and mitigation of these vulnerabilities. Furthermore, we are 4) applying sandboxing techniques at the framework level to provide better protection on mobile platforms.

This project is being done in conjuction with our subcontractors: Prof. Sam Malek at George Mason University and Prof. Marwan Abi Antoun at Wayne State University.

PROJECT - Epistemic Models for Security

PI – Robert Harper

We are using a combination of methods to achieve modular analysis of the security properties of concurrent imperative programs.  We use a type system based on the lax modality to express and enforce information flow constraints.  We use a novel linear epistemic logic to analyze the execution traces of programs to derive which principals learn which secrets in a given run.  We prove that for a well-typed program, a low-security principal can learn a high-security secret only if it is explicitly authorized to do so by an integrated authorization logic. 

All of these methods, being grounded in logic and type theory, are inherently compositional in nature.

PROJECT - Multi-model run-time security analysis

PI – Juergen Pfeffer

Our research focuses on creating the scientific foundations to support model-based, run-time diagnosis and the repair of security attacks. Specifically, our research develops models that (a) scale gracefully with the size of system and have appropriate real-time characteristics for run-time use, and (b) support composition through multi-model analysis. In this research, we develop a rigorous basis for composing architectural models with organizational network models to provide much richer capabilities than is available from either in isolation. The following hard problems are addressed in this project. Composability through multiple semantic models (here, architectural, organizational, and behavioral), which provide separation of concerns, while supporting synergistic benefits through integrated analyses. Scalability to large complex distributed systems using architectural models. Resilient architectures through the use of adaptive models that can be used at run-time to predict, detect and repair security attacks. Predictive security metrics by adapting social network-based metrics to the problem of architecture-level anomaly detection.

We have developed an approach to detect insider threats by clustering the paths on the architecture graph so generated. We represent the entire activity log over an underlying software system as a graph. For every user, a sequence of observed activities becomes a path on the architecture graph. We developed a clustering approach to cluster these paths. Anomalous paths are further investigated by incorporating organizational context (e.g., role of user). The clustering method is built on a generative model to generate sequences. A core challenge of investigating insider threat is the availability of datasets. In this project, a simulator for web systems has been developed for generating data that include malicious behavior. Furthermore, real-world datasets including one from Los Alamos, one from CERT, and one from the "Vegas" lab have been evaluated for their suitability for insider attack research.

PROJECT - Highly Configurable Systems

PI – Juergen Pfeffer

This project complements the Science of Security endeavor with a focus on the often overlooked problems of configuration options in systems. Whereas current approaches work on specific snapshots and require expensive recertification, our approaches extend underlying mathematical models (data-dependence graphs) with configuration knowledge and will thus scale analyses and reduce the need for repeating analyses. Furthermore, we explore whether configuration complexity and configuration-specific program-dependence is a suitable empirical predictor for the likelihood and severity of vulnerabilities in complex systems. Finally, technical and empirical results of our work will also bring new approaches to the field of social network analysis that can be very powerful and applicable for Science of Security far beyond the scope of the current Lablet. The SoS hard problems are addressed as follows. Scalability and composability: Isolating configuration options or controlling their interactions will lead us toward composable analysis with regard to configuration options. Predictive security metrics: To what degree can configuration-related indicate implementations that are more prone to vulnerabilities or in which vulnerabilities have more severe consequences?

In this project we finished implementing and testing a tool to extract precise call graphs with function pointers for product lines/compile-time variability. This overcomes a key limitation of previous approaches which are inaccurate due to their lack of pointer analysis and allow for more precise composability analysis. The tools will be available as part of the next version of TypeChef. Using this infrastructure we extracted a variety of network models based on files, functions, and features from Linux and other systems (e.g. Busybox) and started with assessment of reasonability of selected network metrics for analyzing software systems. We also compiled lists of known Linux vulnerabilities (CVEs) and started to correlate them with results from graph analysis and other metrics. The goal is to identify whether certain characteristics, e.g., position in the call graph, increase the chance for a function to be a security risk.

PROJECT - Security Reasoning for Distributed Systems with Uncertainty

PI – Andre Platzer

This project has made two contributions that will help reasoning about security goals in uncertain systems. First, we described a new problem class called #E-SAT (Zawadzki, Platzer, & Gordon, A Generalization of SAT and #SAT for Robust Policy Evaluation, 2013), which is a quantified generalization of SAT, one of the most important problems in computer science. Our extension includes both counting (#) and search (E) quantifiers. We demonstrated that a number of questions about the robustness and reliability of policies can be set up as #E-SAT instances. We also gave a rigorous theoretical characterization of the problem’s worst-case complexity. Furthermore, we designed an algorithm that, despite the problem class’s formidable worst-case complexity, performed extremely well empirically. The empirical success was due to exploiting a type of structure that seems common in practice.

Our second contribution is ongoing work on a set of approximate optimization techniques. These techniques involve solving an optimization problem within a restricted basis of functions. This technique, called Galerkin approximation, allows problems to be solved rapidly but with some loss in solution quality. We are currently focused on applying these methods to anomaly detection problems, but hope to extend our work to policy synthesis questions shortly since the solver technique is general. Many anomaly detection and policy synthesis questions can be cast as instances of a general problem called the linear complementarity problem (LCP) (Zawadzki, Gordon, & Platzer, A Projection Algorithm for Strictly Monotone Linear Complementarity Problems, 2013). The LCP subsumes a broad class of optimization problems that include quadratic programming. We have already theoretically investigated this method, implemented five different solvers based on these techniques, and are currently evaluating the method empirically. We are experimenting using anomaly detection LCP instances that represent one-class kernel support vector machines (SVMs). One-class SVMs are used in practice to perform anomaly detection, such as in phishing detection. Additionally, we have a new result that characterizes the class of functional approximation methods that are compatible with fast, iterative methods for the LCP. What makes the LCP approach particularly interesting is that it provides general approximation techniques and theoretical results about error bounds that hold for general classes of LCPs (not just SVMs) and so can apply to a broad range of security problems stemming from policy optimization, classification, and anomaly detection.

C). Publications
Please list all publications published in the base year starting in March 2014 to present.

• J. Shahen, J. Niu, M. Tripunitara. "Mohawk+T: Efficient Analysis of Administrative Temporal Role-Based Access Control (ATRBAC) Policies", 20th ACM Symposium on Access Control Models and Technologies (SACMAT), pp. 15-26.  Vienna, Austria, June 1 – 3, 2015.  Presented by Jonathan Shahen.
• H. Hibshi, T. Breaux, M. Riaz, L. Williams. “Discovering Decision-Making Patterns for Security Novices and Experts”.  TR CMU-ISR-15-101, March 2015.
• Hui Shen, Ram Krishnan, Rocky Slavin, and Jianwei Niu. "Sequence Diagram Aided Privacy Policy Specification", IEEE Transactions on Dependable and Secure Computing, Issue 99, December 19, 2014
• H. Hibshi, T. Breaux, M. Riaz, L. Williams. “A Framework to Measure Experts’ Decision Making in Security Requirements Analysis”, IEEE 1st International Workshop on Evolving Security and Privacy Requirements Engineering, pp. 13-18, Karlskrona, Sweden, August 25 - 29, 2014.  Presented by Hanan Hibshi
• R. Slavin, J.-M. Lehker, J. Niu, T. Breaux. “Managing Security Requirement Patterns Using Feature Diagram Hierarchies”, IEEE 22nd International Requirements Engineering Conference, pp. 193-202, Karlskrona, Sweden, August 25 – 29, 2014.  Presented by Rocky Slavin.
• Rao, H. Hibshi, T. Breaux, J-M. Lehker, J. Niu, “Less is More? Investigating the Role of Examples in Security Studies using Analogical Transfer”, 2014 Symposium and Bootcamp on the Science of Security (HotSoS), Article 7.  Raleigh, NC, April 8 -9, 2014.  Presented by Hanan Hibshi
• Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson. "Detection of Design Flaws in the Android Permission Protocol through Bounded Verification", Proceedings of the 20th International Symposium on Formal Methods (FM 2015), pgs 73-89. Oslo, Norway, June 24 – 26, 2015.  Presented by Eunsuk Kang.
• Javier Camara, Gabriel A. Moreno and David Garlan.  “Reasoning about Human Participation in Self-Adaptive Systems”, Proceedings of the 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2015), Florence, Italy, May 18 – 19, 2015.  Presented by Javier Camara.
• Alireza Sadeghi, Hamid Bagheri, and Sam Malek.   “Analysis of Android Inter-App Security Vulnerabilities Using COVERT”.  37th International Conference on Software Engineering (ICSE), Tool Demo Track, Florence, Italy, May 16 – 24, 2015.  Presented by Alireza Sadeghi.
• Bradley Schmerl, Jeff Gennari, David Garlan.  “An Architecture Style for Android Security Analysis” (Poster),  Symposium and Bootcamp on the Science of Security (HotSoS), Urbana IL, April 21-22, 2015.  No presenter.
• Khalaj, E., Wang, Y., Giang, A., Abi-Antoun, M., and Rajlich, V. "Impact Analysis based on a Global Hierarchical Object Graph", 22nd IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER), pgs 221-23.  Montreal, Canada, March 2 – 6, 2015.  Presented by Marwan Abi-Antoun.
• Hamid Bagheri, Alireza Sadeghi, Joshua Garcia, and Sam Malek. "COVERT: Compositional Analysis of Android Inter-App Security Vulnerabilities".Technical Report GMU-CS-TR-2015-1.  Accepted to appear in the IEEE Transactions on Software Engineering
• Vanciu, R., Khalaj, E. and Abi-Antoun, M.  "Comparative Evaluation of Architectural and Code-Level Approaches for Finding Security Vulnerabilities", Workshop on Security Information Workers, co-located with ACM Conference on Computer and Communications Security (CCS), pgs 27-34, Scottsdale, AZ, November 3 – 7, 2014.  Presented by E. Khalaj.
• Riyadh Mahmood, Nariman Mirzaei, and Sam Malek. "EvoDroid: Segmented Evolutionary Testing of Android Apps", Proceedings of the 22th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2014), pgs 599-609. Hong Kong, November 16 – 22, 2014.  Presented by Riyadh Mahmood.
• Marwan Abi-Antoun, Sumukhi Chandrashekar, Radu Vanciu, and Andrew Giang. "Are Object Graphs Extracted Using Abstract Interpretation Significantly Different from the Code?", IEEE International Working Conference on Source Code Analysis and Manipulation, pgs 245-54.  Victoria, British Columbia, Canada, September, 28 – 29, 2014.  Presented by Marwan Abi-Antoun.
• Marwan Abi-Antoun, Sumukhi Chandrashekar, Radu Vanciu, and Andrew Giang.  "Are Object Graphs Extracted Using Abstract Interpretation Significantly Different from the Code?" (Extended Version). Technical report, Wayne State University, September 2014.
• Javier Camara, Antonia Lopes, David Garlan and Bradley Schmerl. "Impact Models for Architecture-Based Self-Adaptive Systems", Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS2014), pgs 89-107.  Bertinoro, Italy, September 10 – 12, 2014.  Presented by Javier Camara.  
• Jonathan Aldrich, Cyrus Omar, Alex Potanin, and Du Li.  "Language-Based Architectural Control", 6th International Workshop on Aliasing, Capabilities, and Ownership (IWACO), Uppsala, Sweden, July 28 – August 1, 2014.  Presented by Jonathan Aldrich.
• Khalaj, E., Vanciu, R., and Abi-Antoun, M. "Is There Value in Reasoning about Security at the Architectural Level: a Comparative Evaluation?" Poster at Symposium and Bootcamp on the Science of Security (HotSoS), Article 30, Raleigh, NC, April 8 – 9, 2014.  Presented by E. Khalaj.
• Khalil Ghorbal, Jean-Baptiste Jeannin, Erik W. Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell.  "Hybrid theorem proving of aerospace systems: Applications and challenges". Journal of Aerospace Information Systems. Vol 11:10, Pg 702 – 13, October 2014.
• Forget, Alain, Komanduri, Saranga, Acquisti, Alessandro, Christin, Nicolas, Cranor, Lorrie, Telang, Rahul.  2014.  "Building the Security Behavior Observatory: An Infrastructure for Long-term Monitoring of Client Machines", IEEE Symposium and Bootcamp on the Science of Security (HotSoS) 2014. Raleigh, NC, August 8 – 9, 2014.  Presented by Alain Forget.
• Forget, S. Komanduri, A. Acquisti, N. Christin, L.F. Cranor, R. Telang. “Security Behavior Observatory: Infrastructure for Long-term Monitoring of Client Machines”. Carnegie Mellon University CyLab Technical Report CMU-CyLab-14-009.  July 14, 2014.  Presented by Alain Forget.
• S. Zhou, J. Al-Kofahi, T. Nguyen, C. Kastner, and S. Nadi. “Extracting Configuration Knowledge from Build Files with Symbolic Analysis”, Proceedings of the 3rd International Workshop on Release Engineering (Releng), New York, NY: ACM Press. Florence, Italy, May 19, 2015.  Presented by Shurui Zhou.
• Ferreira , Gabriel & Kastner, Christian & Pfeffer, Jurgen & Apel, Sven. “Characterizing Configuration Complexity in Highly-Configurable Systems with Variational Call Graphs”, HotSoS 2015 Symposium and Bootcamp on the Science of Security, Article 17, Urbana-Champaign, IL, April 21-22, 2015.  Presented by Gabriel Ferreira.
• C. Hunsen, J. Siegmund, O. Lessenich, S. Apel, B. Zhang, C. Kastner, and M. Becker.  “Preprocessor-Based Variability in Open-Source and Industrial Software Systems: An Empirical Study”.  Empirical Software Engineering (ESE), Special Issue on Empirical Evidence on Software Product Line Engineering, Springer Science+Business Media, New York, April 14, 2015.  Presented by Claus Hunsen.
• S. Nadi, T. Berger, C. Kastner, and K. Czarnecki. “Where do Configuration Constraints Stem From? An Extraction Approach and an Empirical Study", IEEE Transactions on Software Engineering (TSE), Issue 99.  March 23, 2015.  Presented by Sarah Nadi.  
• Max Lillack, Christian Kästner, Eric Bodden. “Tracking Load-time Configuration Options”, In Proceedings of  the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), Vasteras, Sweden, September 15 – 19, 2014.  Presented by Max Lillack.
• Kästner, Christian & Pfeffer, Jürgen. “Limiting Recertification in Highly Configurable Systems. Analyzing Interactions and Isolation among Configuration Options”,  HotSoS 2014: 2014 Symposium and Bootcamp on the Science of Security, Article 23, Raleigh, NC, April 8-9, 2014.  Presented by Juergen Pfeffer.
• Hemank Lamba, Thomas J. Glazier, Bradley Schmerl, Jurgen Pfeffer, David Garlan. "Detecting Insider Threats in Software Systems using Graph Models of Behavioral Paths" (short paper). HotSoS 2015 Symposium and Bootcamp on the Science of Security, Article 20, Urbana-Champaign, IL, April 21-22, 2015.  Presented by Hemank Lamba.
• Limin Jia, Shayak Sen, Deepak Garg, and Anupam Datta.  “System M: A Program Logic for Code Sandboxing and Identification”,  Carnegie Mellon University, Technical Report CMU-CyLab-13-001, 2013 (updated July 2014).
• Ghita Mezzour.  "Assessing the Global Cyber and Biological Threat", Ph.D. Thesis, Carnegie Institute of Technology, Electrical and Computer Engineering & School of Computer Science, Institute for Software Research, Carnegie Mellon University, Pittsburgh, PA, April 2015.  Presented by Ghita Mezzour.
• Ghita Mezzour, Kathleen M. Carley, and L. Richard Carley.  “An Empirical Study of Global Malware Encounters”, Proceedings of ACM Symposium and Bootcamp on the Science of Security (HotSoS), Article 8, Urbana, IL, April 21 – 22, 2015.  Presented by Ghita Mezzour.
• Ghita Mezzour,Kathleen Carley.  “Spam Diffusion in a Social Network Initiated by Hacked Email Accounts”, International Journal of Security and Networks, 9(3), pg 144-53.  November 2014.
• Mezzour, Ghita & Carley, Richard L & Carley, Kathleen M.  “Global Mapping of Cyber Attacks”. Carnegie Mellon University, School of Computer Science, Institute for Software Research, Technical Report CMU-ISR-14-111. October 2014.
• Mezzour, Ghita & Carley, Richard L & Carley, Kathleen M. “Longitudinal analysis of a large corpus of cyber threat descriptions”. Journal of Computer Virology and Hacking Techniques, Published online by Springer June 9, 2014, Springer Paris.
• Tingting Yu. "SimExplorer: A Testing Framework to Detect Elusive Software Faults". University of Nebraska at Lincoln Doctoral Dissertation, August 2014.  Presented by Tingting Yu.
• Tingting Yu, Witawas Srisa-an, and Gregg Rothermel. "SimRT: An Automated Framework to Support Regression Testing for Data Races". In Proceedings of the International Conference on Software Engineering (ICSE), pgs 48-59, Hyderabad, India, May 31 – June 7, 2014.  Presented by Tingting Yu.
• Joshua Sunshine, James D. Herbsleb, and Jonathan Aldrich.  “Searching the State Space: A Qualitative Study of API Protocol Usability”,  International Conference on Program Comprehension (ICPC), co-located with ICSE, Florence, Italy, May 18 – 19, 2015.  Presented by Joshua Sunshine.
• Cyrus Omar, Chenglong Wang, and Jonathan Aldrich. “Composable and Hygienic Typed Syntax Macros”,  30th Symposium on Applied Computing (SAC), Salamanca, Spain, April 13 – 7, 2015.  Presented by Cyrus Omar.
• Nathan Fulton, Cyrus Omar, and Jonathan Aldrich. “Statically Typed String Sanitation Inside a Python”, Workshop on Privacy and Security in Programming (PSP), pgs 3-10, Portland, OR, Oct 20 – 24, 2014.  Presented by Nathan Fulton.
• Darya Kurilova, Alex Potanin, and Jonathan Aldrich. “Wyvern: Impacting Software Security via Programming Language Design”, Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU), Portland, OR, October 20 – 24, 2014.  Presented by Darya Kurilova.
• Michael Coblenz, Jonathan Aldrich, Brad Myers, and Joshua Sunshine. “Considering Productivity Effects of Explicit Type Declarations”, Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU), pgs 59-61, Portland, OR, October 20 – 24, 2014.  Presented by Michael Coblenz.
• Cyrus Omar, Darya Kurilova, Ligia Nistor, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. “Safely Composable Type-Specific Languages”, European Conference on Object-Oriented Programming (ECOOP), pgs 105 - 30, Uppsala, Sweden, July 28 – August 1, 2014.  Presented by Cyrus Omar.
• Michael Maass, Bill Scherlis, and Jonathan Aldrich. “In-Nimbo Sandboxing”, Symposium and Bootcamp on the Science of Security (HotSOS), 2014.  Raleigh, NC, August 8 – 9, 2014.  Presented by Michael Maass.
• Joshua Sunshine, James D. Herbsleb, and Jonathan Aldrich.  “Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming”,  Proceedings of the European Conference on Object-Oriented Programming (ECOOP), pgs 157-81, Uppsala, Sweden, July 28 – August 1, 2014.  Presented by Joshua Sunshine.

D). Community Engagements
Briefly describe your Lablets community outreach efforts to extend scientific rigor in the community/culture. For example, list workshops, seminars, competitions, etc. that your Lablet has accomplished since March 2014 to present.

• Panelist: Jonathan Aldrich, "Language Composition", DSLDI 2015 workshop in association with the ECOOP 2015 conference.
• Invited Talk: Jonathan Aldrich, “Safely Composable Type-Specific Languages” and “Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming,” IFIP Working Group on Language Design, April 2015
• Invited Talk: Jonathan Aldrich, “Searching the State Space: A Qualitative Study of API Protocol Usability,” IFIP Working Group on Language Design, June 2014
• Workshop Organizater: Joshua Sunshine co-organized the 2014 Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU) co-located with OOPSLA SPLASH. The workshop focuses on applying the research techniques from two lablet funded papers (“Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming" and "Searching the State Space: A Qualitative Study of API Protocol Usability.") to further programming languages and language features. The workshop was attended by 34 researchers from around the world. 
• Invited Talk: Travis D. Breaux, "Hermeneutics of Information Privacy" at the IFIP Working Group 2.9 on Requirements Engineering, Cozumel, Mexico, February 18, 2015
• Keynote Talk: Travis D. Breaux, "Going Native - Relying on Pidgins and Creoles to Construct High Confidence Software," High Confidence Software and Systems Conference, Annapolis, MD, May 6, 2014
• Keynote Talk: Travis D. Breaux, "Verifying Data Protection Rules in Complex Data Ecosystems," NSA/CSS Mission Compliance Conference, Baltimore, May 7, 2014
• Panelist: Travis D. Breaux, “Overview of Privacy Engineering Approaches,” NIST Privacy Engineering Workshop, Gaithersburg, MD, April 9, 2014
• Invited Talk: Arbob Ahmad, 2015 SoS Lablet Summer Workshop, Carnegie Mellon University, Pittsburgh, PA, July 14-15, 2015.
• Distinguished Talk: Lorrie Cranor.  Security, Privacy, and Human Behavior. Women in Cybersecurity, Atlanta, GA, March 27, 2015.
• Keynote Talk: Alessandro Acquisti. SPION (Security and Privacy in Online Social Networks) Closing Workshop: "You Are Not Alone," Leuven, December 2014.
• Invited Talk: Sam Malek, "A Tool for Automated Detection of Inter-Application Security Vulnerabilities in Android", National Security Agency, College Park, Maryland, March 2015.
• Invited Talk: Sam Malek, "Automated Detection and Mitigation of Inter-Application Security Vulnerabilities in Android." 2nd International Workshop on Software Development Lifecycle for Mobile. Hong Kong, China, November 2014.
• Keynote Talk: Bradley Schmerl, "Challenges in Engineering Dependable Self-Adaptive System. International Workshop on Recent Advances in the DependabIlity AssessmeNt of Complex systEms (RADIANCE)," Rio de Janeiro, Brazil, June 22, 2015.
• Invited Talk: Bradley Schmerl, "Reasoning about Human Involvement in Self-Adaptive Systems." University of Campinas, Campinas, Brazil, June 26, 2015.
• Invited Talk: David Garlan, "Identifying and resolving consistency issues between model representations," NASA Jet Propulsion Lab, July 2015
• Invited Talk: David Garlan, "Self-Adaptive Systems," 2nd Latin-American School on Software Engineering (ELA-ES 2015), Porto Alegre, Brazil, June 2015
• Keynote Talk: David Garlan, "Modeling Challenges for Cyber-Physical Systems," The International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS), Florence, Italy, May 17, 2015
• Invited Talk: David Garlan, "Software Architecture: A Travelogue," The Future of Software Engineering, Hyderabad, India, May 2014.
• Inited Talk: Limin Jia, “Design, implementation, and verification of XMHF”, WiCys (Women in Cyber security), Nashville, TN, March 2014
• Invited Talk: Limin Jia, “Proving Trace Properties of Programs that Execute Adversary-supplied Code”, INRIA Prosecco seminar, INRIA, Paris, France, June 2014
• Invited Talk: Limin Jia, “Proving Systems Secure Against Adversaries”, Leigh University, Leigh, PA, Oct. 2014
• Keynote Talk: Kathleen M. Carley, “Twitter, Terror and Terms:  Network analytics for assessing large scale media data,” PolNet, Portland, OR, June 2015
• Keynote Talk: Kathleen M. Carley, “Social Media Analytics Using Dynamic Network Methodologies,” DHS CCICADA, Pittsburgh, PA, March 2015
• Invited Talk: Kathleen M. Carley, “Dynamic Network Analysis & Global Mapping,” National Research Council and NGA, Washington DC, April 2015
• Invited Talk: Kathleen M. Carley, “Cyber Security & Dynamic Network Methodologies,” CERT, Pittsburgh, PA, April 2015
• Invited Talk: Kathleen M. Carley, “Characterizing Insider Threats Using Network Analytics,” Science of Security Lablet Meeting, Carnegie Mellon University, Pittsburgh, PA, July 14-15, 2015.
• Invited Talk: Kathleen M. Carley, “DNA, Networks and Simulation,” CASOS Summer Institute, Carnegie Mellon University – training to apx 25 attendees from around the world, July 5-12, 2015
• Invited Talk: Kathleen M. Carley, “Dynamic-network analysis and *ORA”, INSNA Sunbelt XXXV, Brighton, UK - training to apx 15 attendees from around the world, June 23-28, 2015
• Invited Talk: Kathleen M. Carley, “Social Network Analysis for Science of Security,” HotSOS, UIUC, Urbana-Champaigne, IL = dydactic seminar to apx 35 people at HotSoS, April 21-22, 2015

E). Educational
Briefly describe any changes to curriculum at your school or elsewhere that indicates an increased training or rigor in security research that your Lablet has accomplished since March 2014 to present.

Courses –

• Jonathan Aldrich. "Secure Coding", Course Number 14-735, Spring 2015
• Juergen Pfeffer.  "Introduction to Network Science", Course Number(s) 08-622/08-302, Fall 2014
• Lorrie Cranor. “Usable Privacy and Security,” Course Number(s): 05-436 / 05-836 / 08-534 / 08-734, Spring 2015
• Co-taught by David Garlan and Bradley Schmerl. “Self-Adaptive Systems” Course Number 17-707, Spring 2015
• Anupam Datta. “Secure Software Systems,  Building verifiable systems” Course Number 18-732, Spring 2015
• Kathleen M. Carley.  “New module was developed for Dynamic Network Analysis” Course Number(s) 08-801/08-640,  Spring 2015
• Co-Taught Kathleen M. Carley, Travis Breaux, and Lorrie Cranor. “Special Practicum project based on insider espionage developed based on SoS research” Course Number 08-999, Fall 2014