SoS Quarterly Summary Report - CMU - July 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). It is difficult to compositionally verify security properties of extensible commodity systems software (e.g., BIOS, OS, hypervisor) written in low-level languages. We are developing a system called UberSpark that enforces verifiably secure-object abstractions in systems software written in C99 and assembly. UberSpark enforces abstractions found in higher-level languages (e.g., interfaces, function-call semantics for implementations of interfaces, access control on interfaces, forms of concurrency) using a combination of hardware mechanisms and light-weight static analysis. UberSpark also provides 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. Uberspark: Collectively, these abstractions enable compositional verification of security invariants without sacrificing performance. The team 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.The team has received extremely positive and encouraging reviews from our first paper submission to the IEEE Symposium on Security and Privacy (see Fiscal Year to Date: Uberspark) in applying UberSpark to a commodity micro-hypervisor. Accordingly, they submitted a revised version to the USENIX Security Symposium 2016

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

• A Language and Framework for Development of Secure Mobile Applications. (Aldrich). A promising mechanism for eliminating injection vulnerabilities is to provide programmers with mechanisms for constructing commands that are as convenient as strings while being as secure as prepared SQL statements. 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. We describe a novel mechanism called type-specific languages that supports modular DSL embeddings by associating a unique DSL with appropriate types. Our earlier paper describing this work, entitled "Safely Composable Type-Specific Languages," was awarded an ECOOP '14 distinguished paper award.
• Usable formal methods for the 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.)
• Science of Secure Frameworks. (Garlan, Schmerl). We developed a tool called Separ, that combines static analysis with lightweight formal methods to automatically infer security-relevant properties from a bundle of apps. It then uses a constraint solver to synthesize possible security exploits, from which fine-grained security policies are derived and automatically enforced to protect a given device. In our experiments with over 4,000 Android apps, Separ has proven to be highly effective at detecting previously unknown vulnerabilities as well as preventing their exploitation. A paper describing results from the integration of approaches at CMU and Lablet subcontractor UCI was accepted at the European Conference on Software Architecture. We developed an architecture style for Android that captures the modifiable architectures of Android systems, and that supports security analysis as a system evolves. We illustrate the use of the style with two security analyses: a predicate-based approach defined over architectural structure that can detect some common security vulnerabilities, and inter-app permission leakage determined by model checking. These results are reported in a paper accepted at the European Conference on Software Architecture.
• Multi-Model Run-time Security Analysis. (Garlan, Schmerl, Pfeffer). We concluded a project, co-sponsored by General Dynamics,to integrate social network simulation with software architecture simulation. The aim of this project is to demonstrate how having this integrated approach gives better insight into the flow of misinformation through socio-technical networks than looking at the analysis of either network alone. One of the insights gained is identifying the challenge of integrating the different semantics for simulation in the two domains: social network simulations are probabilistic and accumulative - the interesting results involve how much penetration a piece of misinformation makes into the network; on the other hand, software simulation (while probabilistic) is more behavioral and transactional, and interesting results relate not to changes in the network, but variations in the behavior. We plan to address the challenge of understanding how to combine the different insights gained. We briefed on our work and brainstormed future directions with a group of NSA researchers in Laurel, MD. We identified a set of research topics, and focused in on how we are addressing uncertainty and human-in-the-loop adaptations for security. We identified a collaboration point in developing a realistic example system to demonstrate (a) the particular needs of this NSA group and (b) how our research might address this work. We are continuing work on developing this example.

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.). Since the last report, we successfully deployed version 5.0 and are currently deploying version 6.0 of our client data collection software. Within each of these releases, we added additional sensors to collect more information from our participants that we can apply to future research. Most notably, we added a file hash sensor to calculate hash values for downloaded files and executables and a user interface sensor to record user interactions with visual elements of the applications on their computer, such as system tray notifications. A separate paper submitted to the Twelfth Symposium on Usable Privacy and Security (SOUPS 2016) examined the relationships between users' self-reported engagement in securing their computers and the actual security states and outcomes on their machines.

B). Community Interaction

SAF|ART|INT. The Lablet sponsors agreed to provide modest funding to support the Carnegie Mellon Exploratory Workshop on Safety and Control for Artificial Intelligence, held on 27 June 2016. Results from this workshop informed the discussions at the workshop held the next day, 28 June 2016, that was co-sponsored by the White House Office of Science and Technology Policy (OSTP) and Carnegie Mellon.

Approximately 130 people from academia, industry, and government attended the Exploratory Workshop. Speakers included Ed Felten (OSTP), Bill Scherlis (CMU, chair), Eric Horvitz (Microsoft), Andrew Moore (CMU), Richar Mallah (Future of Life Inst), Tom Mitchell (CMU), Dario Amodei (Google), Claire Le Goues (CMU), and Robert Rahmer (IARPA). Speakers at the 28 June workshop included Ed Felten (White House OSTP), Bill Scherlis (CMU), Manuela Veloso (CMU), John Launchbury (DARPA), Jason Matheny (IARPA), Andy Grotto (White House NSC), Claire Tomlin (UC Berkeley), Tom Dietterich (Oregon State), Emma Brunskill (CMU), Michael Littman (Brown), Jeannette Wing (Microsoft), Kathleen Fisher (Tufts), Anupam Datta (CMU), Sarah Loos (Google), Mike Wagner (CMU), Drew Bagnell (Uber), Reid Simmons (NSF), Brian Murray (ZF), and Doug Schmidt (Vanderbilt).

Most talks from the workshop will be made avilable by video at the combined workshop website (www.cmu.edu/safartint/).

CMU ISR REU Program. CMU Lablet faculty leads (Josh Sunshine, Christian Kastner) are leading a summer program, Research Experience for Undergraduates (REU), sponsored by NSF. This is a highly competitive program -- more than one hundred students from diverse universities applied for 18 summer positions. These students are resident on campus and working with faculty in the Instiitute for Software Research, with many assigned to Lablet projects.

Kaestner keynote. Presented invited keynote at VACE workshop (Workshop on Variability and Complexity in Software Design) on quality assurance for highly configurable software systems (including security issues) in Austin, TX (May 2016).

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.

Transitions

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