SoS Quarterly Summary Report - CMU - July 2017

Lablet Summary Report -- Highlights from the CMU Projects

A. Fundamental Research

New Approaches to Security Problems

A Language and Framework for Development of Secure Mobile Applications. (Aldrich, Sunshine).

Injection vulnerabilities are a challenge for web application developers, since constant vigilance is required to ensure that checks are made to assure the strings provided as inputs are free of taint. The goal of this project is to providing programmers with mechanisms for constructing commands that are as convenient as strings but that are also as secure as structured and prepared SQL statements. A particular technical challenge is modularity, enabling separately-defined embedded domain-specific languages (DSLs) to be used together. The project focuses on type-specific languages that support modular DSL embeddings by associating a unique DSL with appropriate types. The typy statically typed programming language features a fragmentary semantics that includes type-checking and translation of meanings into Python.

The team also developed the Hazelnut structure editor, which has the significant innovation of supporting structure editing without imposing the overbearing "outside in" process characteristic of previous structure editors. Hazelnut is based on a small bidirectionally typed lambda calculus extended with holes and a cursor, analogous to Huet's zipper. (Details are in a POPL 2017 paper.)

Usable formal methods for the design and composition of security and privacy policies. (Breaux, Niu (UTSA)).

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, the team has proposed a semi-automated framework that consists of a mapping that links policy phrases to API functions that process sensitive information, along with an information flow analysis to detect misalignments. A case study was undertaken of 501 top Android apps that discovered 63 potential privacy policy violations. (A paper presenting these results was presented at the ACM/IEEE 38th International Software Engineering Conference (ICSE), 2016. In addition, CMU and UTSA published a website for mobile app developers and regulators to help detect and repair potential privacy violations in mobile app source code: http://polidroid.org/)

Science of Secure Frameworks. (Garlan, Schmerl, Sunshine, Aldrich, Abi Antoun (Wayne State), Makek (UCI)).

The team has constructed a framework for generating exploits for Android apps that are vulnerable to inter-component communication (ICC) vulnerabilities based on Intents, which are messages that Android apps exchange. The framework leverages an analysis that is path-sensitive, enabling the generation of exploits capable of executing particular program paths of an Android app. The framework is pluggable, allowing the automatic generation of exploits that can execute a particular program statement identified as vulnerable to an ICC-based attack. The researchers are finalizing the experiments and collecting results for future publication.

Race Vulnerability Study and Hybrid Race Detection (Aldrich, Srisa-an (Univ Nebraska Lincoln).

Malware authors can inject malicious and obfuscated payloads into legitimate applications by repackaging software. Repackaging can force analysts to expend effort separating benign obfuscation (e.g., to protect vendor intellectual property) from obfuscation to hide malicious payloads. The SEMEO filtering approach can assess aspects of semantic equivalence of obfuscated and original versions of a method. The approach handles seven common types of obfuscation separately and in combination. SEMEO provided over 76% recall and 100% precision in identifying semantically equivalent methods for a small set of representative Android apps. In tests, SEMEO prevailed over all existing techniques tested. It also detected repackaging of Pokemon Go (a non-trivial real-world app) into a malicious version. (A paper is submitted to the IEEE Symposium on Security and Privacy, Oakland, 2017.) On platforms such as Android, software engineers need to be able to analyze interacting apps to detect such problems. Current approaches fail to scale up. The JITANA program analysis framework is designed to analyze multiple Android apps simultaneously. It is built around the class-loader, enabling it to analyze large numbers of interacting apps, perform on-demand analysis of large libraries, and effectively analyze dynamically generated code. JITANA is able to effectively and efficiently analyze complex apps including Facebook, PokemonGo, and Pandora. (A paper describing this topic appears in the International Conference on Software Engineering (ICSE), 2017.)

Highly configurable systems (Kastner).

Built a prototype static analysis tool for JavaScript/Node.js to assure the absence of certain kinds of malicious package updates in npm packages. This addresses the risk that a attackers with access to an npm account can easily compromise systems that automatically update dependencies by injecting unnoticed malicious code in minor updates. The work defends against such attacks for the commonly used and often very simple packages on npm. In two recent workshop papers, identified and addressed key challenges in scaling analyses for highly configurable systems: Internal representations to efficiently share analysis information across configurations and analysis of build systems that often contain significant sources of variability and are necessary to understand for performing a sound analysis. Also coded and analyzed interview data from interviews with developers, reviewers, and policy makers regarding software security and safety certification practices using Common Criteria and DO178.

B. Community Interaction

UberSpark.

As noted last quarter, the team has open-sourced and released the first academic prototype of UberSpark. The development and evolution of the framework continues at http://uberspark.org. Google is applying UberSpark to additional application domains. The intent is to foster the growth of the next generation of systems developers who can design and develop low-level verifiable and trustworthy systems with a focus on verifiability, development compatibility and performance.

Polidroid.

CMU and UTSA published a website for mobile app developers and regulators to help detect and repair potential privacy violations in mobile app source code: http://polidroid.org/

C. Other Activity

N/A this quarter