A Language and Framework for Development of Secure Mobile Applications - April 2017

Public Audience
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

PI(s): Jonathan Aldrich (CMU), Josh Sunshine (CMU)

1) HARD PROBLEM(S) ADDRESSED (with short descriptions)
This refers to Hard Problems, released November 2012.

a. Scalability and composability is a primary concern of the project. The goal is to produce a language and framework that enables the construction of secure mobile applications with known security properties. The framework-based approach requires composition between the framework and its plugins, with modular type system and analysis techniques that avoid reanalyzing each individual component. Key issues include scalability (e.g. between client, server, and other distributed resources), tool usability, and security attributes such as confidentiality, integrity, and mitigation of common vulnerabilities seen in present technologies.

b. Human behavior is also secondarily relevant, both because human limitations are the cause of many of the security vulnerabilities that we hope to eliminate, but also because an understanding of the way humans develop software is key to ensuring that our approach is usable and enhances (rather than detracts from) developer productivity.

2) PUBLICATIONS - for Current Quarter
Report papers written as a results of this research. If accepted by or submitted to a journal, which journal. If presented at a conference, which conference.

• Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, Matthew A. Hammer. Toward Semantic Foundations for Program Editors. To appear in Proc. Summit on Advances in Programming Languages (SNAPL), May 2017.
• Ian Voysey, Cyrus Omar, Matthew Hammer. Running Incomplete Programs. In the POPL Off the Beaten Track Workshop (OBT), January 2017.
• Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew Hammer. Hazelnut: A Bidirectionally Typed Structure Editor Calculus. In the Symposium on Principles of Programming Languages (POPL), January 2017.

3) KEY HIGHLIGHTS
Providing programmers with mechanisms for constructing commands that are as convenient as strings while being as secure as prepared SQL statements is a promising mechanism for eliminating injection vulnerabilities. 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 paper describing this work, entitled "Safely Composable Type-Specific Languages," was awarded an ECOOP '14 distinguished paper award.