SoS Quarterly Summary Report - CMU - January 2016
Lablet Summary Report
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. Complex combinations of configurations and intra-feature dependencies can lead to design flaws and errors that can be exploited by attackers. A system called UberSpark has been developed (Datta, Jia) that supports at-scale secure object abstractions in C99 code using the CompCert compiler.
- Epistemic models for security. A type checker has been implemented (Harper) that enables experimentation with larger scale examples. Importantly, it will also enable experimentation with error messaging and guidance to developers to facilitate development of assured secure policies.
New Approaches to Security Problems - these highlights focus on new methods to address existing security problems
- Safely-composable domain specific languages. Injection vulnerabilities (such as SQL injection) are well understood, but they still exist in practice. This is largely due to the "bureaucratic difficulty" of developing code that consistently avoids this vulnerability. An alternative approach (Aldrich/Sunshine) called type-specific languages addresses this while providing the same convenience as the simple string handling (that originally senabled the vulnerabilities). A paper describing this work received a Distinguished Paper Award in the ECOOP 2014 conference.
- Design and composition of security and privacy policies. Regulatory agencies require adherence to privacy policies for many software applications, including mobile apps. A technical approach was developed (Breaux) to assess mappings from API to policy outcomes, and this detected numerous policy violations in a set of 501 Android apps. (Paper to appear in ICSE 2016.)
- Science of secure frameworks. A novel analyzer has been developed (Aldrich) for Android apps that can better support incremental re-analysis of app code, reducing the need for complete re-analysis for large complex component-based systems.
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. The Security Behavior Observatory is now in version 5.0 with improved data collection sensors. After a lengthy process to develop the observational infrastructure and obtain human-subjects clearances, results are now emerging (Christin, Acquisti, Telang, Cranor) for this project. These first results will relate self-reported actions to secure user systems against actual security states and outcomes.
B). Community Interaction
Jonathan Aldrich was General Chair for the SPLASH 2015 conference, hosted in Pittsburgh. This is a top-tier conference attended by nearly 200 people.
The CMU team is gearing up for the HotSoS 2016 conference, also hosted in Pittsburgh. The Call for Papers is disseminated, and a Program Committee has been established, chaired jointly by Prof David Brumley (CMU CyLab director) and Prof William Scherlis (ISR director).
Prof Lorrie Cranor is taking a one-year leave of absence from CMU to become Chief Technologist at the Federal Trade Commission. She is expert on privacy engineering, and has testified before the U.S. Congress on this topic. (Nicholas Christin, her co-lead on the Lablet project, will lead that project until her return.)
Prof William Scherlis testified in December before the United States Nuclear Regulatory Commission regarding software assurance and cybersecurity for embedded software in nuclear power plants.
C.Educational
Transitions
Prof Lorrie Cranor -- see above.
Dr. Juergen Pfeffer is taking a leave of absence. His joint project with Kastner will continue under Kastner's lead, with Pfeffer continuing as a collaborator and Pfeffer's PhD students continuing their involvement. His joint project with Garlan and Schmerl will continue under the leadership of Garlan.
Dr. Alain Forget, who has been a postdoc with Cranor's project, has completed his fellowship and joined the technical staff at Google.
- Approved by NSA
- Scalability and Composability
- Policy-Governed Secure Collaboration
- Metrics
- Resilient Architectures
- Human Behavior
- CMU
- A Language and Framework for Development of Secure Mobile Applications
- Epistemic Models for Security
- Geo-Temporal Characterization of Security Threats
- Highly Configurable Systems
- Multi-Model Run-Time Security Analysis
- Race Vulnerability Study and Hybrid Race Detection
- Science of Secure Frameworks
- Secure Composition of Systems and Policies
- Security Reasoning for Distributed Systems with Uncertainty
- Usable Formal Methods for the Design and Composition of Security and Privacy Policies
- USE: User Security Behavior
- FY14-18
- Jan'16