SoS Quarterly Summary Report - CMU - April 2016

Lablet Summary Report -- Highlights from the CMU Projects

A). Fundamental Research

Theoretical Foundations - these highlights extend existing methods for modeling that could not previously address the hard security problems.

• Secure composition of systems and policies (Datta, Jia). Complex combinations of configurations and intra-feature dependencies can lead to design flaws and errors that can be exploited by attackers. The UberSpark system supports at-scale secure object abstractions, including a restricted language called CASM to make assembly verifiable via tools aimed at C99, while retaining its performance and low-level access to hardware. The CASM code is then compiled using the certifying CompCert compiler into executable binaries. After verification, The C code is compiled using a certifying compiler while the CASM code is translated into its corresponding assembly instructions. Collectively, these abstractions enable compositional verification of security invariants without sacrificing performance. We have validated UberSpark by building and verifying security invariants of a performant hypervisor and several of its extensions, and demonstrating only minor performance overhead, and low verification costs. Applications are being explored related to password authentication and associated crypto.
• Reasoning with uncertainty (Platzer, Kozen, et al.). 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 team are currently working on LCP instances based on Markov decision processes (MDPs), which are a popular framework for making sequential decisions in uncertain environments. Synthesizing good security polices is an example of this kind of task. For example, we may want to automatically generate a good policy for when access control restrictions should be escalated in response to anomalous system behavior, while still allowing legitimate users to work productively. Our MDP approximation techniques will improve policy synthesis capability for many of these large security problems.

New Approaches to Security Problems - these highlights focus on new methods to address existing security problems

• Highly configurable systems. (Kaestner). The team compared ten systematic sampling strategies for making assurances in large configuration spaces of systems and infrastructure software including the Linux kernel. Identified assumptions underlying many of the sampling strategies and how they are limiting or unrealistic in practice. Provided a ranking of sampling strategies under different assumptions. Results are to be presented at the ICSE 2016 conference in May 2016.
• Design and composition of security and privacy policies (Breaux). Mobile applications frequently access sensitive personal information to meet user or business requirements. Because this information is sensitive, regulators increasingly require mobile app developers to publish privacy policies that describe what information is collected, for what purpose is the information used and with whom it is shared. Furthermore, regulators have fined companies when these policies are inconsistent with the actual data practices of mobile apps. To help app developers check their privacy policies against their apps for consistency, we propose a semi-automated framework that consists of a policy terminology-API map that links policy phrases to API functions that process sensitive information, and information flow analysis to detect misalignments. We present our results from a collection of API to policy phrase mappings followed by a case study of 501 top Android apps that discovered 63 potential privacy policy violations..(Paper to appear in ICSE 2016, May 2016.)

Scientific Instrumentation - these highlights demonstrate new research to build the tools needed to conduct security experiments that could not previously have been performed.

• Tools to study long-term, security-related user behavior (Cranor, Christin, Acquisti, et al.). The Security Behavior Observatory is now deploying version 6.0 with additional data collection sensors. The team has initial results that examine the relationships between user self-reports in securing their computers and the actual security states and outcomes on their machines. These results are in a paper submitted to the Twelfth Symposium on Usable Privacy and Security (SOUPS 2016) conference.

B). Community Interaction

The CMU team is now fully prepared for the HotSoS 2016 conference hosted at CMU in Pittsburgh. The conference program features four keynote presentations, nine refereed papers, fifteen refereed posters, and two selected tutorial sessions. About one hundred people are registered for the conference. The Proceedings (138pp) is completed and will be disseminated at the conference on a storage key, along with the 2015 SoS Annual Report. The papers and poster summaries will also appear in the ACM Digital Library. There are twenty-four members of the Program Committee and nine additional reviewers. Conference chair is Prof William Scherlis, who is also chair of the Program Committee, with co-chair Prof David Brumley (CMU CyLab director).

The National Science Foundation has made an award to CMU to provide $5,000 in travel funds for students to attend the conference.

Christian Kaestner, project lead for the Highly Configurable Systems project, is presenting an invited keynote address at the Workshop on Variability and Complexity in Software Design (VACE) on quality assurance for highly configurable software systems, including security issues.

C. Education

Prof Lorrie Cranor -- continues her work as Chief Technologist at the Federal Trade Commission. Cranor has arranged her schedule to be at CMU several days each week, allowing her to maintain continuity in her project. Nicolas Christin is acting Project Lead.

Michael Maass, PhD student working with Jonathan Aldrich and William Scherlis, has completed his PhD work and will take a position at Bosch Research in Pittsburgh with a focus on IoT security. He will lead the design of security components for the Bosch smart home framework.

Transitions

Prof Robert Harper, who has been the project lead for epistemic models, is discontinuing his work with the Lablet due to health issues.