SoS Quarterly Summary Report - CMU - January 2017

Lablet Summary Report -- Highlights from the CMU Projects

A. Fundamental Research

Theoretical Foundations - these highlights extend existing methods for modeling to better 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. The team is developing a system called UberSpark designed to enforce 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. Collectively, these abstractions enable compositional verification of security invariants without sacrificing performance. The UberSpark approach has been validated 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. Complementary to UberSpark, the program logic, System M, allows proofs of safety for programs that execute adversary-supplied code without forcing the adversarial code to be available for deep typing analysis. The key insight is to model adversary-supplied code based on interface-confinement which reduces the task of reasoning about dynamically obtained adversary code into analysis of invariants over the interfaces the adversarial code is confined to.

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, 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 forthcoming 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 will appear 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. 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

Prof Lorrie Cranor -- returns in January 2017 from a year as Chief Technologist at the Federal Trade Commission.