2016 SoS Lablet Annual Report - CMU

Lablet Annual Report
Purpose: To highlight progress made within the reporting year. 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 SoS Lablet includes eleven projects, seven university subcontracts, and about fifty faculty, postdoc, and PhD student researchers working at eight campuses. At Carnegie Mellon, researchers are drawn from six different academic departments in three different colleges. The team also works with industry, including Bosch, Google, and Microsoft.

The CMU Lablet focuses primarily in two of the five Hard Problem areas, which are (1) scalability and composability and (5) human behavior. There is significant effort in two other areas, which are (2) policy-governed secure collaboration and (4) resiliency.

This report presents highlights from the active Lablet projects.  

PROJECT: Security Reasoning for Distributed Systems with Certainty
PI: Andre Platzer
HARD PROBLEMS: (1) Scalability and composability, (4) Resilience.

Our research project investigates using artificial intelligence and optimization techniques for security problems related to systems with physical behavior. Many real-world devices--such as industrial plants and autonomous vehicles--use complicated control policies to guide the underlying dynamics of the system to desirable states. These control policies are, in general, difficult to analyze and prove to be free of security defects. Our research project is focused on improving capabilities of automatic synthesis and verification of the control of such systems--especially in the face of both benign uncertainty (e.g., sensor noise) and adversarial action. In particular, we are solving an open problem in this field: designing controllers using approximate techniques while retaining guarantees about the resulting behavior quality. As an alternative to exact approaches, approximate techniques can be faster, but need guarantees on their errors. In 2015/2016, we have made substantial progress on approximately solving a class of optimization problem related to both anomaly detection and security policy synthesis. Anomaly detection and security policy synthesis are essential capabilities for security in complicated systems where uncertainty is present and must be handled in a principled fashion. We have developed a robust implementation of an approximate solver for such problems. This includes solving a wealth of issues associated with numerical stability and basis generation. Current work includes developing a novel variant of Monte Carlo Tree Search (MCTS). This MCTS variant allows us to use our approximate solver to tackle continuous real-world policy synthesis problems that are difficult to solve using other methods because of the exponential runtime scaling of conventional methods.

PROJECT: Highly Configurable Systems
PI(s): Christian Kästner, Jürgen Pfeffer
HARD PROBLEMS:  (1) Scalability and composability

We address scalability of assurances for highly configurable systems with exponentially growing configuration spaces. A compositional analysis of options will allow to scale the analysis; for this it's important to investigate how options are implemented and how they interact. In addition, modular and timely recertification of changes and variations is essential to make security judgments scale in practice. The team evaluated variational call graphs to predict vulnerabilities. Because vulnerable and non-vulnerable function measures can come from multiple, different statistical populations, the team adopted a bootstrap from the entire population of total functions to yield an empirical distribution of t-statistics upon which comparisons could be made.

PROJECT: A Language and Framework for Development of Secure Mobile Applications
PI: Jonathan Aldrich
HARD PROBLEMS: (1) Scalability and composability

Composability is a primary concern of the project. The goal is to produce a language and framework that enables the construction of secure mobile applications with known security properties. Restricting the authority of untrusted code is difficult in today's systems because by default, code has the same authority as the user running it. Object capabilities are a promising way to implement the principle of least authority, but take away many conveniences provided by today's module systems. This year we developed a module system design that is capability-safe, yet preserves most of the convenience of conventional module systems. We demonstrated how to ensure key security and privacy properties of a program as a mode of use of our module system.

PROJECT: Race Vulnerability Study and Hybrid Race Detection
PI: Jonathan Aldrich
HARD PROBLEMS: (1) Scalability and composability. (4) Resiliency

Today’s software ecosystems present many challenges to program analysis including the need to identify problems that occur due to (1) interactions among applications, (2) mismatching interfaces between applications and underlying frameworks that change due to frequent updates, and (3) increased use of dynamic features to load code at runtime. As researchers, engineers, and analysts struggle to cope with these emerging challenges they are forced to create complex workflows based on existing tools to meet their needs. Often, however, such approaches result in inefficient, ineffective workflows that are not practical for real-world use. As a result, defective and vulnerable applications are released. Even when defects and vulnerabilities are identified, long delays are often encountered before they can be corrected. To address these problems we developed JITANA, a new hybrid analysis framework for Android applications. JITANA has been designed to overcome the aforementioned challenges while maintaining the best parts of existing program analyses. With JITANA, existing analysis techniques continue to be effective but are significantly more efficient. To highlight the benefits of JITANA, we provide three use cases in which we show that JITANA can (1) detect shared Inter-Application Communication (IAC) channels among real-world applications, (2) support the creation of a real-time visualization engine to provide real-time feedback on code coverage, and (3) analyze large sets of applications on a device simultaneously to detect IAC channels.

PROJECT: Usable Formal Methods for the Design and Comp of Security and Privacy Policies.
PI: Travis Breaux
HARD PROBLEMS: (1) Scalability and composability. (2) Policy-governed secure collaboration. (5) Human behavior

Our research evaluates security pattern selection and application by designers in response to attack patterns. There are two threads of effort. The first area of research is based on theory in psychology concerning how designers comprehend and interpret their environment and how they plan and project solutions into the future, with the aim of better understanding how these activities exist in designing more secure systems. These are not typical models of attackers and defenders, but models of developer behavior, including our ability to influence that behavior with interventions. The evaluation is based on formal models of attack scenarios that are used to measure security risk and promote risk reduction strategies based on assurance cases constructed by the analyst. The aim is to improve the usability of formal methods for studying security design and composition. The second area focuses on tracing vulnerabilities from requirements to code, building on knowledge about information type categories. Crowdsourcing was used to collect and classify information type categories while using inter-rater reliability statistics to iteratively measure agreement during ontology construction. The results were used to find privacy policy violations in mobile applications.

PROJECT: Geo-Temporal Characterization of Security Threats
PI: Kathleen Carley
HARD PROBLEMS: (2) Policy-governed secure collaboration. (5) Human behavior

This goal of the project is to provide an empirical basis for understanding global security issues based on network models of interactions among actors of various kinds. Results could assist in understanding what nation-states are most threatening and may need special policies. We developed a data-informed global map of which country was purportedly attacking which, using what form of cyber-attack. Results showed wide variations in infrastructure that complicate the development of new procedures to enhance security at the global level. Results also showed that countries with high corruption and unsophisticated IT support are likely to be used by others as the apparent source of attacks. Results also showed that most global-scale attacks were between the US and China, or between former members of the USSR and Russia. However, in the past year, attacks between US and China have decreased. These results suggest the possibility of empirically-driven policy creation and evaluation.

In addition, the global cyber-attack map and the associated information and analysis from this project enable us to identify capability and IT gaps at the nation-state level. This is important in improving the selection of intervention policies and in prioritizing intervention strategies. This analysis is also critical for developing a global predictive attack model, which is the next research step, as well as providing an empirical basis for assessing human and organizational variability in capability to thwart and to engage in attacks at the nation-state level. Results provide insight into how to determine whether attacks that appear to be coming from a country are being directed out for malicious intent or whether that country is being inadvertently used by other countries and is so appearing malicious.

The results suggest that it should be possible to discriminate cyber-attacks that are primarily motivated by economic factors from those that are part of a large political attack. In particular, this analysis shows that attacks are more likely to occur from one country to another if the receiving country has greater GDP than the sender, if the receiving country and the sender are allies, and if the sending country has a higher level of corruption. In contrast, there are instances of attacks where the timing appears consistent with other hostile activities. The next step would be to assess whether in fact such political attacks may be part of an overall strategy of attack between adversaries.

PROJECT: USE: User Security Behavior
PI: Lorrie Cranor
HARD PROBLEMS: (5) Human behavior

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. Preliminary results suggest that the extent to which people care about security is not strongly correlated with the actual level of security (or insecurity) that we observed on participants’ machines. A question that then arises is whether users are more likely to engage in “risky” behavior when they believe they are operating securely.

PROJECT: Secure Composition of Systems and Policies
PI(s): Anupam Datta, Limin Jia
HARD PROBLEMS: (1) Scalability and composability. (4) Resiliency

At a high-level our work addresses the scalability and composability problem. The reasoning principles we are developing will allow both sequential and parallel composition of an arbitrary number of verified and unverified system program modules in varying configurations. Our program logic takes into consideration that components execute in a potentially adversarial environment (e.g., untrusted system modules), and therefore, the compositionality of components in the presence of such adversaries is built into our semantic model.

PROJECT: Multi-Model Run-time Security Analysis
PI(s): David Garlan, Bradley Schmerl, Jürgen Pfeffer
HARD PROBLEMS: (1) Scalability and composability. (4) Resiliency

This last year, we addressed composability through composing multiple semantic models (here, architectural, organizational, and behavioral), for the detection of anomalies in software systems. We made progress on these fronts: We developed software that generates large scale architectures (in the order of a thousand software elements) from descriptions of architecture styles. We have applied this to a description of cloud-based Amazon web service systems. This is used as the basis of simulations for insider threat scenarios to test analysis of large scale systems. We extract user traces from these simulations. We developed an algorithm to find anomalous users leveraging these traces. We use a model based approach to cluster user sequences and find outliers. Such a technique can be useful in finding potentially anomalous users, insiders, or compromised accounts. The algorithm can also extract out the different roles that generated the traces automatically, from the clusters.

In a Masters student project, we built a prototype that integrates software simulations like the one described above with social network simulations to model misinformation flow through a cyber-social network. The project uncovered a number of challenges in doing this - namely that software simulations are predominantly deterministic, not accumulative, and do not change much over time, whereas social network simulation are non-deterministic, accumulate state at different time steps, and change over time as agents or interactions are created or destroyed. This set of challenges helps define the agenda for how to analyze misinformation flow in cyber-social systems.

Designing secure cyber-physical systems (CPS) is a particularly difficult task since security vulnerabilities stem not only from traditional cybersecurity concerns, but also physical ones as well. Many of the standard methods for CPS design make strong and unverified assumptions about the trustworthiness of physical devices, such as sensors. When these assumptions are violated, subtle inter-domain vulnerabilities are introduced into the system model. In this paper we propose to use formal specification of analysis contracts to expose security assumptions and guarantees of analyses from reliability, control, and sensor security domains. We showed that this specification allows us to determine where these assumptions are violated or ignore important failure modes that open the door to malicious attacks. We demonstrated how this approach can help discover and prevent vulnerabilities in a self-driving car example.

PROJECT: Science of Secure Frameworks
PI(s): David Garlan, Bradley Schmerl, Jonathan Aldrich
HARD PROBLEMS: (1) Scalability and composability. (4) Resiliency

This project has multiple threads of activity.

This past year we investigated approaches for using software architecture coupled with static and dynamic analysis to build scalable and composable frameworks. Malek, our UCI subcontractor, developed lightweight formal verification techniques to detect several inter-component communication (ICC) vulnerabilities on Android devices, and integrated into COVERT. The approach is composable and scalable in that reevaluation of the analysis when a new app is installed is only re-run on affected areas. We also made progress on formalizing the Android permission protocol, with an aim to exhaustively analyze and uncover flaws in the protocols. We are in the process of updating this specification to conform to the most recent version of Android (Marshmallow).

In collaboration with Malek at UCI, we have integrated the tool for static analysis of Android ICC to generate an Acme architecture instance that can be further analyzed with architectural tools. We began development of Raindroid, a probing infrastructure using the open source Xposed framework for Android. Raindroid probes intent communication between apps in Android, and communicates with Rainbow, our self-adaptive framework, that can effect changes. We began integrating this with COVERT to identify potentially vulnerable communications, and then effect certain context-sensitive changes to the communication (such as denying, querying the user, or letting it pass). We explored this in the context of applications that dynamically load code. This work addresses the resiliency hard problem by combining information from static analysis (COVERT) with run time mitigations of vulnerabilities (Raindroid/Rainbow).

In collaboration with Abi-Antoun at Wayne State, we continued development and evaluation of Scoria, a tool that provides a semi-automated algorithm for iteratively refining global hierarchical graphs of programs for understanding their architectural structures and data flows. Developed a dynamic web interface to begin evaluation of the tool with professionals.

Additionally, the CMU team made progress on our research assuring architectural control through a capability-based module system. In particular, we completed specifying a type system that enforces capabilities and drafted a basic soundness proof for the language. We also specified a refined concrete syntax for the module system and made progress on a prototype implementation, completed the first prototype implementation, demonstrated the idea of architectural control through a small concrete example, and make progress on extending our basic soundness proof with a proof of capability safety.

The CMU team, in collaboration with Bosch, began investigation how to design frameworks to support checking of security policies, targeted at an Internet of Things framework being developed by Bosch, build on Android. We developed a tool that enforces policies on inter-app communication and tested it with three proprietary apps from Bosch, and showed that it is possible to define and enforce custom security policies within a framework.

The final thread of activity focuses on the Java sandbox, which was developed to securely encapsulate such components, but is primarily used to secure applications launched from the web while treating all of their components uniformly. We developed and evaluated MAJIC, a tool that assists developers in recovering and refining a security policy from Java bytecode and that uses the policy to sandbox targeted application components. MAJIC automates complex sandboxing tasks developers previously had to perform manually. The overhead introduced by MAJIC on large, real world applications is low, with 6.6% overhead at borders between sandboxed and unsandboxed code and an additional 6.9% overhead across the application due to the use of the sandbox.